Thread env through nztion to fix Foo/build closures

7 files changed, 95 insertions, 51 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index ed8d98b..c95a26d 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -276,13 +276,6 @@ fn generate_tests() -> std::io::Result<()> {
                     // TODO: record completion
                     || path == "simple/completion"
                     || path == "unit/Completion"
-                    // TODO: fix variables in Foo/build
-                    || path == "unit/ListBuildFoldFusion"
-                    || path == "unit/ListBuildImplementation"
-                    || path == "unit/NaturalBuildFoldFusion"
-                    || path == "unit/NaturalBuildImplementation"
-                    || path == "unit/OptionalBuildFoldFusion"
-                    || path == "unit/OptionalBuildImplementation"
             }),
             input_type: FileType::Text,
             output_type: Some(FileType::Text),
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),
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 6559082..92ba8fd 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -141,6 +141,11 @@ impl NameEnv {
     pub fn new() -> Self {
         NameEnv { names: Vec::new() }
     }
+    pub fn from_binders(names: impl Iterator<Item = Binder>) -> Self {
+        NameEnv {
+            names: names.collect(),
+        }
+    }
     pub fn as_quoteenv(&self) -> QuoteEnv {
         QuoteEnv {
             size: self.names.len(),
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 5fc72fc..a11cb75 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -4,9 +4,11 @@ use std::convert::TryInto;
 
 use crate::semantics::nze::{NzVar, QuoteEnv};
 use crate::semantics::phase::typecheck::{
-    builtin_to_value, const_to_value, rc, typecheck,
+    builtin_to_value_env, const_to_value, rc,
 };
 use crate::semantics::phase::Normalized;
+use crate::semantics::tck::typecheck::type_with;
+use crate::semantics::tck::typecheck::TyEnv;
 use crate::semantics::{
     AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind,
 };
@@ -73,6 +75,7 @@ pub(crate) fn apply_builtin(
     args: Vec<Value>,
     ty: &Value,
     types: Vec<Value>,
+    env: NzEnv,
 ) -> ValueKind<Value> {
     use syntax::Builtin::*;
     use ValueKind::*;
@@ -86,6 +89,11 @@ pub(crate) fn apply_builtin(
         ValueWithRemainingArgs(&'a [Value], Value),
         DoneAsIs,
     }
+    let make_closure = |e| {
+        type_with(&env.to_alpha_tyenv(), &e)
+            .unwrap()
+            .normalize_whnf(&env)
+    };
 
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
@@ -272,13 +280,12 @@ pub(crate) fn apply_builtin(
             Ret::Value(
                 f.app(list_t.clone())
                     .app(
-                        typecheck(make_closure!(
+                        make_closure(make_closure!(
                             λ(T : Type) ->
                             λ(a : var(T)) ->
                             λ(as : List var(T)) ->
                             [ var(a) ] # var(as)
                         ))
-                        .unwrap()
                         .app(t.clone()),
                     )
                     .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
@@ -300,12 +307,11 @@ pub(crate) fn apply_builtin(
             Ret::Value(
                 f.app(optional_t.clone())
                     .app(
-                        typecheck(make_closure!(
+                        make_closure(make_closure!(
                             λ(T : Type) ->
                             λ(a : var(T)) ->
                             Some(var(a))
                         ))
-                        .unwrap()
                         .app(t.clone()),
                     )
                     .app(
@@ -326,13 +332,10 @@ pub(crate) fn apply_builtin(
         },
         (NaturalBuild, [f]) => Ret::Value(
             f.app(Value::from_builtin(Natural))
-                .app(
-                    typecheck(make_closure!(
-                        λ(x : Natural) ->
-                        1 + var(x)
-                    ))
-                    .unwrap(),
-                )
+                .app(make_closure(make_closure!(
+                    λ(x : Natural) ->
+                    1 + var(x)
+                )))
                 .app(
                     NaturalLit(0)
                         .into_value_with_type(Value::from_builtin(Natural)),
@@ -366,7 +369,7 @@ pub(crate) fn apply_builtin(
             }
             v.to_whnf_check_type(ty)
         }
-        Ret::DoneAsIs => AppliedBuiltin(b, args, types),
+        Ret::DoneAsIs => AppliedBuiltin(b, args, types, env),
     }
 }
 
@@ -379,7 +382,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
         ValueKind::LamClosure { closure, .. } => {
             closure.apply(a).to_whnf_check_type(ty)
         }
-        ValueKind::AppliedBuiltin(b, args, types) => {
+        ValueKind::AppliedBuiltin(b, args, types, env) => {
             use std::iter::once;
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             let types = types
@@ -387,7 +390,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
                 .cloned()
                 .chain(once(f.get_type().unwrap()))
                 .collect();
-            apply_builtin(*b, args, ty, types)
+            apply_builtin(*b, args, ty, types, env.clone())
         }
         ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
             l.clone(),
@@ -625,6 +628,7 @@ fn apply_binop<'a>(
 pub(crate) fn normalize_one_layer(
     expr: ExprKind<Value, Normalized>,
     ty: &Value,
+    env: &NzEnv,
 ) -> ValueKind<Value> {
     use ValueKind::{
         BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
@@ -649,7 +653,7 @@ pub(crate) fn normalize_one_layer(
         }
         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::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)),
         ExprKind::Assert(_) => Ret::Expr(expr),
         ExprKind::App(v, a) => Ret::Value(v.app(a)),
         ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
@@ -659,11 +663,12 @@ pub(crate) fn normalize_one_layer(
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _)
-                    if args.len() == 1 =>
-                {
-                    args[0].clone()
-                }
+                ValueKind::AppliedBuiltin(
+                    syntax::Builtin::List,
+                    args,
+                    _,
+                    _,
+                ) if args.len() == 1 => args[0].clone(),
                 _ => panic!("internal type error"),
             };
             Ret::ValueKind(ValueKind::EmptyListLit(arg))
@@ -827,10 +832,10 @@ pub(crate) fn normalize_whnf(
     ty: &Value,
 ) -> ValueKind<Value> {
     match v {
-        ValueKind::AppliedBuiltin(b, args, types) => {
-            apply_builtin(b, args, ty, types)
+        ValueKind::AppliedBuiltin(b, args, types, env) => {
+            apply_builtin(b, args, ty, types, env)
         }
-        ValueKind::PartialExpr(e) => normalize_one_layer(e, ty),
+        ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()),
         ValueKind::TextLit(elts) => {
             ValueKind::TextLit(squash_textlit(elts.into_iter()))
         }
@@ -862,6 +867,9 @@ impl NzEnv {
     pub fn as_quoteenv(&self) -> QuoteEnv {
         QuoteEnv::construct(self.items.len())
     }
+    pub fn to_alpha_tyenv(&self) -> TyEnv {
+        TyEnv::from_nzenv_alpha(self)
+    }
 
     pub fn insert_type(&self, t: Value) -> Self {
         let mut env = self.clone();
@@ -890,6 +898,10 @@ impl NzEnv {
             NzEnvItem::Replaced(x) => x.clone(),
         }
     }
+
+    pub fn size(&self) -> usize {
+        self.items.len()
+    }
 }
 
 /// Normalize a TyExpr into WHNF
@@ -924,10 +936,18 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
         }
         TyExprKind::Expr(e) => {
             let e = e.map_ref(|tye| tye.normalize_whnf(env));
-            normalize_one_layer(e, &ty)
+            normalize_one_layer(e, &ty, env)
         }
     };
 
     // dbg!(tye.kind(), env, &kind);
     Value::from_kind_and_type_whnf(kind, ty)
 }
+
+/// Ignore NzEnv when comparing
+impl std::cmp::PartialEq for NzEnv {
+    fn eq(&self, _other: &Self) -> bool {
+        true
+    }
+}
+impl std::cmp::Eq for NzEnv {}
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 18e70e4..f559323 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -5,6 +5,7 @@ use std::collections::HashMap;
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::context::TyCtx;
 use crate::semantics::phase::normalize::merge_maps;
+use crate::semantics::phase::normalize::NzEnv;
 use crate::semantics::phase::Normalized;
 use crate::semantics::{AlphaVar, Binder, Value, ValueKind};
 use crate::syntax;
@@ -278,8 +279,11 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 }
 
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
+    builtin_to_value_env(b, &NzEnv::new())
+}
+pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value {
     Value::from_kind_and_type(
-        ValueKind::from_builtin(b),
+        ValueKind::from_builtin_env(b, env.clone()),
         crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
             .unwrap()
             .normalize_whnf_noenv(),
@@ -433,11 +437,12 @@ fn type_last_layer(
         }
         ExprKind::EmptyListLit(t) => {
             let arg = match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _)
-                    if args.len() == 1 =>
-                {
-                    args[0].clone()
-                }
+                ValueKind::AppliedBuiltin(
+                    syntax::Builtin::List,
+                    args,
+                    _,
+                    _,
+                ) if args.len() == 1 => args[0].clone(),
                 _ => return mkerr("InvalidListType"),
             };
             RetWhole(Value::from_kind_and_type(
@@ -596,7 +601,7 @@ fn type_last_layer(
         }
         ExprKind::BinOp(ListAppend, l, r) => {
             match &*l.get_type()?.as_whnf() {
-                ValueKind::AppliedBuiltin(List, _, _) => {}
+                ValueKind::AppliedBuiltin(List, _, _, _) => {}
                 _ => return mkerr("BinOpTypeMismatch"),
             }
 
@@ -666,6 +671,7 @@ fn type_last_layer(
                     syntax::Builtin::Optional,
                     args,
                     _,
+                    _,
                 ) if args.len() == 1 => {
                     let ty = &args[0];
                     let mut kts = HashMap::new();
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 4ca5d4d..e2619b5 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,6 +35,14 @@ impl TyEnv {
             items: NzEnv::new(),
         }
     }
+    pub fn from_nzenv_alpha(items: &NzEnv) -> Self {
+        TyEnv {
+            names: NameEnv::from_binders(
+                std::iter::repeat("_".into()).take(items.size()),
+            ),
+            items: items.clone(),
+        }
+    }
     pub fn as_quoteenv(&self) -> QuoteEnv {
         self.names.as_quoteenv()
     }
@@ -147,7 +155,7 @@ fn type_one_layer(
         ExprKind::EmptyListLit(t) => {
             let t = t.normalize_whnf(env.as_nzenv());
             match &*t.as_whnf() {
-                ValueKind::AppliedBuiltin(Builtin::List, args, _)
+                ValueKind::AppliedBuiltin(Builtin::List, args, _, _)
                     if args.len() == 1 => {}
                 _ => return mkerr("InvalidListType"),
             };
@@ -404,7 +412,7 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             let l_ty = l.get_type()?;
             match &*l_ty.as_whnf() {
-                ValueKind::AppliedBuiltin(Builtin::List, _, _) => {}
+                ValueKind::AppliedBuiltin(Builtin::List, _, _, _) => {}
                 _ => return mkerr("BinOpTypeMismatch"),
             }
 
@@ -572,7 +580,7 @@ fn type_one_layer(
 
 /// Type-check an expression and return the expression alongside its type if type-checking
 /// succeeded, or an error if type-checking failed.
-fn type_with(
+pub(crate) fn type_with(
     env: &TyEnv,
     expr: &Expr<Normalized>,
 ) -> Result<TyExpr, TypeError> {