Thread env through nztion to fix Foo/build closures

2 files changed, 21 insertions, 9 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 42da653..71c5c65 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -6,7 +6,9 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::{AlphaVar, Binder};
 use crate::semantics::nze::{NzVar, QuoteEnv};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv};
-use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
+use crate::semantics::phase::typecheck::{
+    builtin_to_value, builtin_to_value_env, const_to_value,
+};
 use crate::semantics::phase::{
     Normalized, NormalizedExpr, ToExprOptions, Typed,
 };
@@ -77,7 +79,8 @@ pub(crate) enum ValueKind<Value> {
     },
     // Invariant: in whnf, the evaluation must not be able to progress further.
     // Keep types around to be able to recover the types of partial applications.
-    AppliedBuiltin(Builtin, Vec<Value>, Vec<Value>),
+    // Keep env around to construct Foo/build closures; hopefully temporary.
+    AppliedBuiltin(Builtin, Vec<Value>, Vec<Value>, NzEnv),
 
     Var(AlphaVar, NzVar),
     Const(Const),
@@ -144,7 +147,10 @@ impl Value {
         const_to_value(c)
     }
     pub(crate) fn from_builtin(b: Builtin) -> Self {
-        builtin_to_value(b)
+        Self::from_builtin_env(b, &NzEnv::new())
+    }
+    pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+        builtin_to_value_env(b, env)
     }
     pub(crate) fn with_span(self, span: Span) -> Self {
         self.as_internal_mut().span = span;
@@ -318,7 +324,7 @@ impl Value {
                     .apply_var(NzVar::new(qenv.size()))
                     .to_tyexpr(qenv.insert()),
             )),
-            ValueKind::AppliedBuiltin(b, args, types) => {
+            ValueKind::AppliedBuiltin(b, args, types, _) => {
                 TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold(
                     ExprKind::Builtin(*b),
                     |acc, (v, ty)| {
@@ -561,7 +567,7 @@ impl ValueKind<Value> {
             | ValueKind::PiClosure { annot, .. } => {
                 annot.normalize_mut();
             }
-            ValueKind::AppliedBuiltin(_, args, _) => {
+            ValueKind::AppliedBuiltin(_, args, _, _) => {
                 for x in args.iter_mut() {
                     x.normalize_mut();
                 }
@@ -609,7 +615,10 @@ impl ValueKind<Value> {
     }
 
     pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
-        ValueKind::AppliedBuiltin(b, vec![], vec![])
+        ValueKind::from_builtin_env(b, NzEnv::new())
+    }
+    pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind<Value> {
+        ValueKind::AppliedBuiltin(b, vec![], vec![], env)
     }
 
     fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index 64250b0..61a7d0b 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -98,9 +98,12 @@ where
             annot: v.visit_val(annot)?,
             closure: closure.clone(),
         },
-        AppliedBuiltin(b, xs, types) => {
-            AppliedBuiltin(*b, v.visit_vec(xs)?, v.visit_vec(types)?)
-        }
+        AppliedBuiltin(b, xs, types, env) => AppliedBuiltin(
+            *b,
+            v.visit_vec(xs)?,
+            v.visit_vec(types)?,
+            env.clone(),
+        ),
         Var(v, w) => Var(v.clone(), *w),
         Const(k) => Const(*k),
         BoolLit(b) => BoolLit(*b),