summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
authorNadrieril2020-01-25 10:20:53 +0000
committerNadrieril2020-01-25 10:21:02 +0000
commitf2e8c414993d5c9fcc63f5c035f755712c01dad0 (patch)
tree27391b13dce903650f930529454a5b3b7a6c9682 /dhall/src/semantics/phase
parent70e6e3a06c05cfe7d8ca3d6f072e7182639c147f (diff)
Enable comparing Closures for equality
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/phase/normalize.rs11
1 files changed, 7 insertions, 4 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 066a004..7f547d7 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -884,17 +884,20 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
let kind = match tye.kind() {
TyExprKind::Var(var) => return env.lookup_val(var),
TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+ let annot = annot.normalize_whnf(env);
ValueKind::LamClosure {
binder: Binder::new(binder.clone()),
- annot: annot.normalize_whnf(env),
- closure: Closure::new(env, body.clone()),
+ annot: annot.clone(),
+ closure: Closure::new(annot, env, body.clone()),
}
}
TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ let annot = annot.normalize_whnf(env);
+ let closure = Closure::new(annot.clone(), env, body.clone());
ValueKind::PiClosure {
binder: Binder::new(binder.clone()),
- annot: annot.normalize_whnf(env),
- closure: Closure::new(env, body.clone()),
+ annot,
+ closure,
}
}
TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {