diff options
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 20 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 26 |
2 files changed, 21 insertions, 25 deletions
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 724e3e8..67ab90a 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -58,7 +58,7 @@ pub(crate) enum Closure { body: TyExpr, }, /// Closure that ignores the argument passed - ConstantClosure { env: NzEnv, body: TyExpr }, + ConstantClosure { body: Value }, } /// A text literal with interpolations. @@ -521,11 +521,8 @@ impl Closure { } } /// New closure that ignores its argument - pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { - Closure::ConstantClosure { - env: env.clone(), - body, - } + pub fn new_constant(body: Value) -> Self { + Closure::ConstantClosure { body } } pub fn apply(&self, val: Value) -> Value { @@ -533,7 +530,7 @@ impl Closure { Closure::Closure { env, body, .. } => { body.eval(&env.insert_value(val)) } - Closure::ConstantClosure { env, body, .. } => body.eval(env), + Closure::ConstantClosure { body, .. } => body.clone(), } } fn apply_var(&self, var: NzVar) -> Value { @@ -545,7 +542,7 @@ impl Closure { ); self.apply(val) } - Closure::ConstantClosure { env, body, .. } => body.eval(env), + Closure::ConstantClosure { body, .. } => body.clone(), } } @@ -559,17 +556,14 @@ impl Closure { /// If the closure variable is free in the closure, return Err. Otherwise, return the value /// with that free variable remove. pub fn remove_binder(&self) -> Result<Value, ()> { - let v = NzVar::fresh(); match self { Closure::Closure { .. } => { + let v = NzVar::fresh(); // TODO: handle case where variable is used in closure // TODO: return information about where the variable is used Ok(self.apply_var(v)) } - Closure::ConstantClosure { .. } => { - // Ok: the variable is indeed ignored - Ok(self.apply_var(v)) - } + Closure::ConstantClosure { body, .. } => Ok(body.clone()), } } } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index e3f57c2..20076cd 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -200,20 +200,22 @@ fn type_one_layer( match scrut_nf.kind() { ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > - Some(Some(ty)) => Value::from_kind_and_type( - ValueKind::PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant( - env.as_nzenv(), - scrut.clone(), - ), - }, - type_of_function( + Some(Some(ty)) => { + let pi_ty = type_of_function( ty.get_type()?, scrut.get_type()?, - )?, - ), + )?; + Value::from_kind_and_type( + ValueKind::PiClosure { + binder: Binder::new(x.clone()), + annot: ty.clone(), + closure: Closure::new_constant( + scrut_nf, + ), + }, + pi_ty, + ) + } Some(None) => scrut_nf, None => return mkerr("MissingUnionField"), }, |