Remove extra types stored in Value

3 files changed, 20 insertions, 47 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 423364d..715e045 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -19,10 +19,6 @@ pub(crate) struct BuiltinClosure<Value> {
     pub b: Builtin,
     /// Arguments applied to the closure so far.
     pub args: Vec<Value>,
-    /// Keeps the types of the partial applications around to be able to convert back to TyExpr.
-    /// If the args so far are `x_1`, ..., `x_n`, this contains the types of `b`, `b x1`, ...,
-    /// `b x_1 x_2 ... x_(n-1)`.
-    pub types: Vec<Value>,
 }
 
 impl BuiltinClosure<Value> {
@@ -31,15 +27,13 @@ impl BuiltinClosure<Value> {
             env,
             b,
             args: Vec::new(),
-            types: Vec::new(),
         }
     }
 
-    pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind {
+    pub fn apply(&self, a: Value) -> ValueKind {
         use std::iter::once;
         let args = self.args.iter().cloned().chain(once(a.clone())).collect();
-        let types = self.types.iter().cloned().chain(once(f_ty)).collect();
-        apply_builtin(self.b, args, types, self.env.clone())
+        apply_builtin(self.b, args, self.env.clone())
     }
     /// This doesn't break the invariant because we already checked that the appropriate arguments
     /// did not normalize to something that allows evaluation to proceed.
@@ -49,9 +43,9 @@ impl BuiltinClosure<Value> {
         }
     }
     pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
-        HirKind::Expr(self.args.iter().zip(self.types.iter()).fold(
+        HirKind::Expr(self.args.iter().fold(
             ExprKind::Builtin(self.b),
-            |acc, (v, ty)| {
+            |acc, v| {
                 ExprKind::App(
                     Hir::new(HirKind::Expr(acc), Span::Artificial),
                     v.to_hir(venv),
@@ -260,12 +254,7 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-fn apply_builtin(
-    b: Builtin,
-    args: Vec<Value>,
-    types: Vec<Value>,
-    env: NzEnv,
-) -> ValueKind {
+fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
     use Builtin::*;
     use ValueKind::*;
 
@@ -493,12 +482,7 @@ fn apply_builtin(
     match ret {
         Ret::ValueKind(v) => v,
         Ret::Value(v) => v.kind().clone(),
-        Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure {
-            b,
-            args,
-            types,
-            env,
-        }),
+        Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }),
     }
 }
 
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index acb2e51..981d894 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -13,16 +13,10 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
         ValueKind::LamClosure { closure, .. } => {
             closure.apply(a).kind().clone()
         }
-        ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type_not_sort())
+        ValueKind::AppliedBuiltin(closure) => closure.apply(a),
+        ValueKind::UnionConstructor(l, kts) => {
+            ValueKind::UnionLit(l.clone(), a, kts.clone())
         }
-        ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
-            l.clone(),
-            a,
-            kts.clone(),
-            uniont.clone(),
-            f.get_type_not_sort(),
-        ),
         _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
     }
 }
@@ -326,11 +320,9 @@ pub(crate) fn normalize_one_layer(
                 Some(r) => Ret::Value(r.clone()),
                 None => Ret::Expr(expr),
             },
-            UnionType(kts) => Ret::ValueKind(UnionConstructor(
-                l.clone(),
-                kts.clone(),
-                v.get_type_not_sort(),
-            )),
+            UnionType(kts) => {
+                Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
+            }
             PartialExpr(ExprKind::BinOp(
                 BinOp::RightBiasedRecordMerge,
                 x,
@@ -402,11 +394,11 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Merge(ref handlers, ref variant, _) => {
             match handlers.kind() {
                 RecordLit(kvs) => match variant.kind() {
-                    UnionConstructor(l, _, _) => match kvs.get(l) {
+                    UnionConstructor(l, _) => match kvs.get(l) {
                         Some(h) => Ret::Value(h.clone()),
                         None => Ret::Expr(expr),
                     },
-                    UnionLit(l, v, _, _, _) => match kvs.get(l) {
+                    UnionLit(l, v, _) => match kvs.get(l) {
                         Some(h) => Ret::Value(h.app(v.clone())),
                         None => Ret::Expr(expr),
                     },
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index d05c545..a771b91 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -93,10 +93,8 @@ pub(crate) enum ValueKind {
     RecordType(HashMap<Label, Value>),
     RecordLit(HashMap<Label, Value>),
     UnionType(HashMap<Label, Option<Value>>),
-    // Also keep the type of the uniontype around
-    UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
-    // Also keep the type of the uniontype and the constructor around
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
+    UnionConstructor(Label, HashMap<Label, Option<Value>>),
+    UnionLit(Label, Value, HashMap<Label, Option<Value>>),
     TextLit(TextLit),
     Equivalence(Value, Value),
     /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
@@ -298,14 +296,14 @@ impl Value {
                         .collect(),
                 ),
                 ValueKind::UnionType(kts) => map_uniontype(kts),
-                ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
+                ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
                     Hir::new(
                         HirKind::Expr(map_uniontype(kts)),
                         Span::Artificial,
                     ),
                     l.clone(),
                 ),
-                ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
+                ValueKind::UnionLit(l, v, kts) => ExprKind::App(
                     Hir::new(
                         HirKind::Expr(ExprKind::Field(
                             Hir::new(
@@ -418,13 +416,12 @@ impl ValueKind {
                     x.normalize();
                 }
             }
-            ValueKind::UnionType(kts)
-            | ValueKind::UnionConstructor(_, kts, _) => {
+            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
                 for x in kts.values().flat_map(|opt| opt) {
                     x.normalize();
                 }
             }
-            ValueKind::UnionLit(_, v, kts, _, _) => {
+            ValueKind::UnionLit(_, v, kts) => {
                 v.normalize();
                 for x in kts.values().flat_map(|opt| opt) {
                     x.normalize();