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