summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/core/value.rs34
-rw-r--r--dhall/src/semantics/tck/typecheck.rs10
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"),
}