Automate conversion between envs

3 files changed, 26 insertions, 22 deletions

diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 3b02074..ba7fb73 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -120,3 +120,9 @@ impl TyEnv {
         self.items.lookup_ty(&var)
     }
 }
+
+impl<'a> From<&'a TyEnv> for &'a NzEnv {
+    fn from(x: &'a TyEnv) -> Self {
+        x.as_nzenv()
+    }
+}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 05fa4b5..edba477 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -56,8 +56,8 @@ impl TyExpr {
     }
 
     /// 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.to_hir())
+    pub fn eval<'e>(&self, env: impl Into<&'e NzEnv>) -> Value {
+        Value::new_thunk(env.into(), self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index ac113cd..7f02832 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -73,11 +73,10 @@ fn type_one_layer(
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type()?;
             let body_ty = body_ty.to_tyexpr_tyenv(
-                &env.insert_type(&binder.clone(), annot.eval(env.as_nzenv())),
+                &env.insert_type(&binder.clone(), annot.eval(env)),
             );
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
-            type_one_layer(env, pi_ekind, Span::Artificial)?
-                .eval(env.as_nzenv())
+            type_one_layer(env, pi_ekind, Span::Artificial)?.eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.get_type()?.as_const() {
@@ -117,7 +116,7 @@ fn type_one_layer(
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval(env.as_nzenv())
+            t_tyexpr.eval(env)
         }
         ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
         ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
@@ -136,7 +135,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval(env.as_nzenv());
+            let t = t.eval(env);
             match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -242,7 +241,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
-                    let scrut_nf = scrut.eval(env.as_nzenv());
+                    let scrut_nf = scrut.eval(env);
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -262,7 +261,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Annot(x, t) => {
-            let t = t.eval(env.as_nzenv());
+            let t = t.eval(env);
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return span_err(&format!(
@@ -274,7 +273,7 @@ fn type_one_layer(
             x_ty
         }
         ExprKind::Assert(t) => {
-            let t = t.eval(env.as_nzenv());
+            let t = t.eval(env);
             match &*t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
@@ -315,7 +314,7 @@ fn type_one_layer(
                         );
                     }
 
-                    let arg_nf = arg.eval(env.as_nzenv());
+                    let arg_nf = arg.eval(env);
                     closure.apply(arg_nf)
                 }
                 _ => return mkerr(
@@ -380,11 +379,11 @@ fn type_one_layer(
                 x.get_type()?.to_tyexpr_tyenv(env),
                 y.get_type()?.to_tyexpr_tyenv(env),
             );
-            type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
+            type_one_layer(env, ekind, Span::Artificial)?.eval(env)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            let x_val = x.eval(env.as_nzenv());
-            let y_val = y.eval(env.as_nzenv());
+            let x_val = x.eval(env);
+            let y_val = y.eval(env);
             let kts_x = match x_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("RecordTypeMergeRequiresRecordType"),
@@ -589,8 +588,7 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot =
-                type_annot.as_ref().map(|t| t.eval(env.as_nzenv()));
+            let type_annot = type_annot.as_ref().map(|t| t.eval(env));
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -621,7 +619,7 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval(env.as_nzenv());
+                let annot_val = annot.eval(env);
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
@@ -670,7 +668,7 @@ fn type_one_layer(
                 let output_type = Value::from_builtin(Builtin::List)
                     .app(Value::from_kind(ValueKind::RecordType(kts)));
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval(env.as_nzenv());
+                    let annot_val = annot.eval(env);
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -710,7 +708,7 @@ fn type_one_layer(
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval(env.as_nzenv());
+            let selection_val = selection.eval(env);
             let sel_kts = match selection_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
@@ -782,14 +780,14 @@ pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
                     let annot = type_with(env, annot)?;
-                    let annot_nf = annot.eval(env.as_nzenv());
+                    let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Lam(binder.clone(), annot, body)
                 }
                 ExprKind::Pi(binder, annot, body) => {
                     let annot = type_with(env, annot)?;
-                    let annot_nf = annot.eval(env.as_nzenv());
+                    let annot_nf = annot.eval(env);
                     let body_env = env.insert_type(binder, annot_nf);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Pi(binder.clone(), annot, body)
@@ -808,7 +806,7 @@ pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
                     };
                     let val = type_with(env, &val)?;
                     let val_ty = val.get_type()?;
-                    let val_nf = val.eval(&env.as_nzenv());
+                    let val_nf = val.eval(env);
                     let body_env = env.insert_value(&binder, val_nf, val_ty);
                     let body = type_with(&body_env, body)?;
                     ExprKind::Let(binder.clone(), None, val, body)