Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@brendanzab
brendanzab committed Apr 29, 2018
1 parent 59271dc commit 23cd73c
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 34 deletions.
86 changes: 54 additions & 32 deletions src/semantics/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,68 +56,59 @@ pub fn check_module(raw_module: &RawModule) -> Result<Module, TypeError> {
///
/// Since this may 'unstick' some neutral terms, the returned term will need to
/// be re-evaluated afterwards to ensure that it remains in its normal form.
pub fn subst(value: &Value, subst_name: &Name, subst_term: &Rc<Term>) -> Rc<Term> {
pub fn subst(value: &Value, substs: &[(Name, Rc<Term>)]) -> Rc<Term> {
match *value {
Value::Universe(level) => Rc::new(Term::Universe(Ignore::default(), level)),
Value::Constant(ref c) => Rc::new(Term::Constant(Ignore::default(), c.clone())),
Value::Pi(ref scope) => {
let ((name, Embed(ann)), body) = nameless::unbind(scope.clone());
Rc::new(Term::Pi(
Ignore::default(),
nameless::bind(
(name, Embed(subst(&ann, subst_name, subst_term))),
subst(&body, subst_name, subst_term),
),
nameless::bind((name, Embed(subst(&ann, substs))), subst(&body, substs)),
))
},
Value::Lam(ref scope) => {
let ((name, Embed(ann)), body) = nameless::unbind(scope.clone());
Rc::new(Term::Lam(
Ignore::default(),
nameless::bind(
(name, Embed(subst(&ann, subst_name, subst_term))),
subst(&body, subst_name, subst_term),
),
nameless::bind((name, Embed(subst(&ann, substs))), subst(&body, substs)),
))
},
Value::RecordType(ref scope) => {
let ((label, Embed(ann)), body) = nameless::unbind(scope.clone());
Rc::new(Term::RecordType(
Ignore::default(),
nameless::bind(
(label, Embed(subst(&ann, subst_name, subst_term))),
subst(&body, subst_name, subst_term),
),
nameless::bind((label, Embed(subst(&ann, substs))), subst(&body, substs)),
))
},
Value::Record(ref scope) => {
let ((label, Embed(expr)), body) = nameless::unbind(scope.clone());
Rc::new(Term::Record(
Ignore::default(),
nameless::bind(
(label, Embed(subst(&expr, subst_name, subst_term))),
subst(&body, subst_name, subst_term),
),
nameless::bind((label, Embed(subst(&expr, substs))), subst(&body, substs)),
))
},
Value::EmptyRecordType => Rc::new(Term::EmptyRecordType(Ignore::default())),
Value::EmptyRecord => Rc::new(Term::EmptyRecord(Ignore::default())),
Value::Neutral(ref n) => match **n {
Neutral::Var(Var::Free(ref n)) if n == subst_name => subst_term.clone(),
Value::Neutral(ref neutral) => match **neutral {
Neutral::Var(Var::Free(ref name)) => match substs.iter().find(|s| *name == s.0) {
Some(&(_, ref term)) => term.clone(),
None => Rc::new(Term::Var(Ignore::default(), Var::Free(name.clone()))),
},
Neutral::Var(ref var) => Rc::new(Term::Var(Ignore::default(), var.clone())),
Neutral::App(ref expr, ref arg) => Rc::new(Term::App(
subst(&Value::Neutral(expr.clone()), subst_name, subst_term),
subst(arg, subst_name, subst_term),
subst(&Value::Neutral(expr.clone()), substs),
subst(arg, substs),
)),
Neutral::If(ref cond, ref if_true, ref if_false) => Rc::new(Term::If(
Ignore::default(),
subst(&Value::Neutral(cond.clone()), subst_name, subst_term),
subst(if_true, subst_name, subst_term),
subst(if_false, subst_name, subst_term),
subst(&Value::Neutral(cond.clone()), substs),
subst(if_true, substs),
subst(if_false, substs),
)),
Neutral::Proj(ref expr, ref label) => Rc::new(Term::Proj(
Ignore::default(),
subst(&Value::Neutral(expr.clone()), subst_name, subst_term),
subst(&Value::Neutral(expr.clone()), substs),
Ignore::default(),
label.clone(),
)),
Expand Down Expand Up @@ -185,7 +176,7 @@ pub fn normalize(context: &Context, term: &Rc<Term>) -> Result<Rc<Value>, Intern
Value::Lam(ref scope) => {
// FIXME: do a local unbind here
let ((name, Embed(_)), body) = nameless::unbind(scope.clone());
normalize(context, &subst(&*body, &name, arg))
normalize(context, &subst(&*body, &vec![(name, arg.clone())]))
},
Value::Neutral(ref expr) => Ok(Rc::new(Value::from(Neutral::App(
expr.clone(),
Expand Down Expand Up @@ -335,7 +326,10 @@ pub fn check(

if Label::pattern_eq(&label, &ty_label) {
let expr = check(context, &raw_expr, &ann)?;
let ty_body = normalize(context, &subst(&ty_body, &label.0, &expr))?;
let ty_body = normalize(
context,
&subst(&ty_body, &vec![(label.0.clone(), expr.clone())]),
)?;
let body = check(context, &raw_body, &ty_body)?;

return Ok(Rc::new(Term::Record(
Expand Down Expand Up @@ -509,7 +503,7 @@ pub fn infer(context: &Context, raw_term: &Rc<RawTerm>) -> Result<(Rc<Term>, Rc<
let ((name, Embed(ann)), body) = nameless::unbind(scope.clone());

let arg = check(context, raw_arg, &ann)?;
let body = normalize(context, &subst(&*body, &name, &arg))?;
let body = normalize(context, &subst(&*body, &vec![(name, arg.clone())]))?;

Ok((Rc::new(Term::App(expr, arg)), body))
},
Expand Down Expand Up @@ -562,10 +556,13 @@ pub fn infer(context: &Context, raw_term: &Rc<RawTerm>) -> Result<(Rc<Term>, Rc<
let (expr, ty) = infer(context, expr)?;

match ty.lookup_record_ty(label) {
Some(ty) => Ok((
Rc::new(Term::Proj(span, expr, label_span, label.clone())),
ty.clone(),
)),
Some(ty) => {
let substs = field_substs(&expr, &label, &ty);
Ok((
Rc::new(Term::Proj(span, expr, label_span, label.clone())),
normalize(context, &subst(&ty, &substs))?,
))
},
None => Err(TypeError::NoFieldInType {
label_span: label_span.0,
expected_label: label.clone(),
Expand All @@ -575,3 +572,28 @@ pub fn infer(context: &Context, raw_term: &Rc<RawTerm>) -> Result<(Rc<Term>, Rc<
},
}
}

fn field_substs(expr: &Rc<Term>, label: &Label, ty: &Rc<Type>) -> Vec<(Name, Rc<Term>)> {
let mut substs = vec![];
let mut current_scope = ty.record_ty();

while let Some(scope) = current_scope {
let ((curr_label, Embed(_)), body) = nameless::unbind(scope);

if Label::pattern_eq(&curr_label, &label) {
break;
}

let proj = Rc::new(Term::Proj(
Ignore::default(),
expr.clone(),
Ignore::default(),
curr_label.clone(),
));

substs.push((curr_label.0, proj));
current_scope = body.record_ty();
}

substs
}
4 changes: 2 additions & 2 deletions src/syntax/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ pub enum Value {
}

impl Value {
fn record_ty(&self) -> Option<Bind<(Label, Embed<Rc<Value>>), Rc<Value>>> {
pub fn record_ty(&self) -> Option<Bind<(Label, Embed<Rc<Value>>), Rc<Value>>> {
match *self {
Value::RecordType(ref scope) => Some(scope.clone()),
_ => None,
Expand All @@ -471,7 +471,7 @@ impl Value {
None
}

fn record(&self) -> Option<Bind<(Label, Embed<Rc<Value>>), Rc<Value>>> {
pub fn record(&self) -> Option<Bind<(Label, Embed<Rc<Value>>), Rc<Value>>> {
match *self {
Value::Record(ref scope) => Some(scope.clone()),
_ => None,
Expand Down

0 comments on commit 23cd73c

Please sign in to comment.