diff options
author | Nadrieril | 2020-01-25 10:15:17 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-25 10:15:17 +0000 |
commit | 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f (patch) | |
tree | 91c8bcfe35b3e99a5332458531a45b58ecfb8be7 /dhall/src/semantics/phase/normalize.rs | |
parent | b72f0968ac19058b9cc513ab0ed1785133232a3d (diff) |
Typecheck more cases
Diffstat (limited to 'dhall/src/semantics/phase/normalize.rs')
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index e848601..066a004 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -625,12 +625,14 @@ pub(crate) fn normalize_one_layer( // `RetWhole`), so they won't appear here. ExprKind::Lam(_, _, _) | ExprKind::Pi(_, _, _) - | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Var(_) - | ExprKind::Annot(_, _) => { + | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Let(_, _, val, body) => { + Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) + } + ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), ExprKind::Assert(_) => Ret::Expr(expr), @@ -895,11 +897,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { closure: Closure::new(env, body.clone()), } } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.normalize_whnf(env); + return body.normalize_whnf(&env.insert_value(val)); + } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); normalize_one_layer(e, &ty) } }; + // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } |