diff options
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 34 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 10 |
2 files changed, 32 insertions, 12 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index af01177..bf75710 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -270,9 +270,7 @@ impl Value { } => TyExprKind::Expr(ExprKind::Lam( binder.to_label(), annot.to_tyexpr(venv), - closure - .apply_var(NzVar::new(venv.size())) - .to_tyexpr(venv.insert()), + closure.to_tyexpr(venv), )), ValueKind::PiClosure { binder, @@ -281,9 +279,7 @@ impl Value { } => TyExprKind::Expr(ExprKind::Pi( binder.to_label(), annot.to_tyexpr(venv), - closure - .apply_var(NzVar::new(venv.size())) - .to_tyexpr(venv.insert()), + closure.to_tyexpr(venv), )), ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv), ValueKind::UnionConstructor(l, kts, t) => { @@ -576,12 +572,14 @@ impl Closure { body, } } + /// New closure that ignores its argument pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { Closure::ConstantClosure { env: env.clone(), body, } } + pub fn apply(&self, val: Value) -> Value { match self { Closure::Closure { env, body, .. } => { @@ -592,7 +590,7 @@ impl Closure { } } } - pub fn apply_var(&self, var: NzVar) -> Value { + fn apply_var(&self, var: NzVar) -> Value { match self { Closure::Closure { arg_ty, .. } => { let val = Value::from_kind_and_type( @@ -606,6 +604,28 @@ impl Closure { } } } + + /// Convert this closure to a TyExpr + pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + self.apply_var(NzVar::new(venv.size())) + .to_tyexpr(venv.insert()) + } + /// 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 { .. } => { + // 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)) + } + } + } } /// Compare two values for equality modulo alpha/beta-equivalence. diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 0c5e779..bc1c87f 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, NzVar, TyEnv, TyExpr, + type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind, }; use crate::syntax::{ @@ -48,7 +48,7 @@ fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> { Ok(Value::from_const(function_check(ks, kt))) } -fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> { +fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> { Err(TypeError::new(TypeMessage::Custom(x.to_string()))) } @@ -452,9 +452,9 @@ fn type_one_layer( return mkerr("MergeHandlerTypeMismatch"); } - let v = NzVar::fresh(); - // TODO: handle case where variable is used in closure - closure.apply_var(v) + closure.remove_binder().or_else(|()| { + mkerr("MergeReturnTypeIsDependent") + })? } _ => return mkerr("NotAFunction"), } |