Introduce Thunks and normalize lazily

2 files changed, 28 insertions, 25 deletions

diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 5492b8b..0a27f32 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -49,6 +49,9 @@ impl TyExpr {
     pub fn kind(&self) -> &TyExprKind {
         &*self.kind
     }
+    pub fn span(&self) -> &Span {
+        &self.span
+    }
     pub fn get_type(&self) -> Result<Type, TypeError> {
         match &self.ty {
             Some(t) => Ok(t.clone()),
@@ -69,17 +72,18 @@ impl TyExpr {
         tyexpr_to_expr(self, opts, &mut env)
     }
 
-    pub fn normalize_whnf(&self, env: &NzEnv) -> Value {
-        normalize_tyexpr_whnf(self, env)
-    }
-    pub fn normalize_whnf_noenv(&self) -> Value {
-        self.normalize_whnf(&NzEnv::new())
+    /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
+    pub fn eval(&self, env: &NzEnv) -> Value {
+        Value::new_thunk(env, self.clone())
     }
-    pub fn normalize_nf(&self, env: &NzEnv) -> Value {
-        self.normalize_whnf(env)
+    /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
+    /// needed on demand.
+    pub fn eval_closed_expr(&self) -> Value {
+        self.eval(&NzEnv::new())
     }
-    pub fn normalize_nf_noenv(&self) -> Value {
-        self.normalize_nf(&NzEnv::new())
+    /// Eval a closed TyExpr fully and recursively;
+    pub fn rec_eval_closed_expr(&self) -> Value {
+        normalize_tyexpr_whnf(self, &NzEnv::new())
     }
 }
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index bc1c87f..d741b40 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -74,7 +74,7 @@ fn type_one_layer(
         ExprKind::Builtin(b) => {
             let t_expr = type_of_builtin(*b);
             let t_tyexpr = type_with(env, &t_expr)?;
-            t_tyexpr.normalize_whnf(env.as_nzenv())
+            t_tyexpr.eval(env.as_nzenv())
         }
         ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
         ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
@@ -93,7 +93,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.normalize_nf(env.as_nzenv());
+            let t = t.eval(env.as_nzenv());
             match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -196,7 +196,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
-                    let scrut_nf = scrut.normalize_nf(env.as_nzenv());
+                    let scrut_nf = scrut.eval(env.as_nzenv());
                     let scrut_nf_borrow = scrut_nf.kind();
                     match &*scrut_nf_borrow {
                         ValueKind::UnionType(kts) => match kts.get(x) {
@@ -224,7 +224,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Annot(x, t) => {
-            let t = t.normalize_whnf(env.as_nzenv());
+            let t = t.eval(env.as_nzenv());
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return mkerr(format!(
@@ -243,7 +243,7 @@ fn type_one_layer(
             x_ty
         }
         ExprKind::Assert(t) => {
-            let t = t.normalize_whnf(env.as_nzenv());
+            let t = t.eval(env.as_nzenv());
             match &*t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
@@ -268,7 +268,7 @@ fn type_one_layer(
                         ));
                     }
 
-                    let arg_nf = arg.normalize_nf(env.as_nzenv());
+                    let arg_nf = arg.eval(env.as_nzenv());
                     closure.apply(arg_nf)
                 }
                 _ => return mkerr(format!("apply to not Pi")),
@@ -329,11 +329,11 @@ fn type_one_layer(
             );
             let ty = type_one_layer(env, &ekind)?;
             TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
-                .normalize_nf(env.as_nzenv())
+                .eval(env.as_nzenv())
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            let x_val = x.normalize_whnf(env.as_nzenv());
-            let y_val = y.normalize_whnf(env.as_nzenv());
+            let x_val = x.eval(env.as_nzenv());
+            let y_val = y.eval(env.as_nzenv());
             let x_val_borrow = x_val.kind();
             let y_val_borrow = y_val.kind();
             let kts_x = match &*x_val_borrow {
@@ -478,9 +478,8 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot = type_annot
-                .as_ref()
-                .map(|t| t.normalize_whnf(env.as_nzenv()));
+            let type_annot =
+                type_annot.as_ref().map(|t| t.eval(env.as_nzenv()));
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -542,7 +541,7 @@ pub(crate) fn type_with(
         },
         ExprKind::Lam(binder, annot, body) => {
             let annot = type_with(env, annot)?;
-            let annot_nf = annot.normalize_nf(env.as_nzenv());
+            let annot_nf = annot.eval(env.as_nzenv());
             let body_env = env.insert_type(&binder, annot_nf.clone());
             let body = type_with(&body_env, body)?;
             let body_ty = body.get_type()?;
@@ -555,7 +554,7 @@ pub(crate) fn type_with(
                 Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
                 Span::Artificial,
             );
-            let ty = ty.normalize_whnf(env.as_nzenv());
+            let ty = ty.eval(env.as_nzenv());
             (
                 TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
                 Some(ty),
@@ -563,7 +562,7 @@ pub(crate) fn type_with(
         }
         ExprKind::Pi(binder, annot, body) => {
             let annot = type_with(env, annot)?;
-            let annot_nf = annot.normalize_whnf(env.as_nzenv());
+            let annot_nf = annot.eval(env.as_nzenv());
             let body =
                 type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
             let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
@@ -580,7 +579,7 @@ pub(crate) fn type_with(
             };
 
             let val = type_with(env, &val)?;
-            let val_nf = val.normalize_nf(&env.as_nzenv());
+            let val_nf = val.eval(&env.as_nzenv());
             let body = type_with(&env.insert_value(&binder, val_nf), body)?;
             let body_ty = body.get_type().ok();
             (