Typecheck more cases

2 files changed, 19 insertions, 5 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)
 }
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index f2d1bf2..0f3754e 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -189,7 +189,7 @@ macro_rules! make_type {
     };
 }
 
-fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
+pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
     use syntax::Builtin::*;
     rc(match b {
         Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -321,7 +321,14 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
 
             let v = type_with(ctx, v)?;
             let binder = ctx.new_binder(x);
-            type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())
+            let e =
+                type_with(&ctx.insert_value(&binder, v.clone())?, e.clone())?;
+            // let e_ty = e.get_type()?;
+            // Ok(Value::from_kind_and_type(
+            //     ValueKind::PartialExpr(ExprKind::Let(x.clone(), None, v, e)),
+            //     e_ty,
+            // ))
+            Ok(e)
         }
         Embed(p) => Ok(p.clone().into_typed().into_value()),
         Var(var) => match ctx.lookup(&var) {