From 70af1a47bce9e6c8282d6e53cf82aeda9aab10de Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 22:08:57 +0000
Subject: Tweak ConstantClosure

---
 dhall/src/semantics/nze/value.rs     | 20 +++++++-------------
 dhall/src/semantics/tck/typecheck.rs | 26 ++++++++++++++------------
 2 files changed, 21 insertions(+), 25 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 724e3e8..67ab90a 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -58,7 +58,7 @@ pub(crate) enum Closure {
         body: TyExpr,
     },
     /// Closure that ignores the argument passed
-    ConstantClosure { env: NzEnv, body: TyExpr },
+    ConstantClosure { body: Value },
 }
 
 /// A text literal with interpolations.
@@ -521,11 +521,8 @@ impl Closure {
         }
     }
     /// New closure that ignores its argument
-    pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self {
-        Closure::ConstantClosure {
-            env: env.clone(),
-            body,
-        }
+    pub fn new_constant(body: Value) -> Self {
+        Closure::ConstantClosure { body }
     }
 
     pub fn apply(&self, val: Value) -> Value {
@@ -533,7 +530,7 @@ impl Closure {
             Closure::Closure { env, body, .. } => {
                 body.eval(&env.insert_value(val))
             }
-            Closure::ConstantClosure { env, body, .. } => body.eval(env),
+            Closure::ConstantClosure { body, .. } => body.clone(),
         }
     }
     fn apply_var(&self, var: NzVar) -> Value {
@@ -545,7 +542,7 @@ impl Closure {
                 );
                 self.apply(val)
             }
-            Closure::ConstantClosure { env, body, .. } => body.eval(env),
+            Closure::ConstantClosure { body, .. } => body.clone(),
         }
     }
 
@@ -559,17 +556,14 @@ impl Closure {
     /// If the closure variable is free in the closure, return Err. Otherwise, return the value
     /// with that free variable remove.
     pub fn remove_binder(&self) -> Result<Value, ()> {
-        let v = NzVar::fresh();
         match self {
             Closure::Closure { .. } => {
+                let v = NzVar::fresh();
                 // TODO: handle case where variable is used in closure
                 // TODO: return information about where the variable is used
                 Ok(self.apply_var(v))
             }
-            Closure::ConstantClosure { .. } => {
-                // Ok: the variable is indeed ignored
-                Ok(self.apply_var(v))
-            }
+            Closure::ConstantClosure { body, .. } => Ok(body.clone()),
         }
     }
 }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e3f57c2..20076cd 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -200,20 +200,22 @@ fn type_one_layer(
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
-                            Some(Some(ty)) => Value::from_kind_and_type(
-                                ValueKind::PiClosure {
-                                    binder: Binder::new(x.clone()),
-                                    annot: ty.clone(),
-                                    closure: Closure::new_constant(
-                                        env.as_nzenv(),
-                                        scrut.clone(),
-                                    ),
-                                },
-                                type_of_function(
+                            Some(Some(ty)) => {
+                                let pi_ty = type_of_function(
                                     ty.get_type()?,
                                     scrut.get_type()?,
-                                )?,
-                            ),
+                                )?;
+                                Value::from_kind_and_type(
+                                    ValueKind::PiClosure {
+                                        binder: Binder::new(x.clone()),
+                                        annot: ty.clone(),
+                                        closure: Closure::new_constant(
+                                            scrut_nf,
+                                        ),
+                                    },
+                                    pi_ty,
+                                )
+                            }
                             Some(None) => scrut_nf,
                             None => return mkerr("MissingUnionField"),
                         },
-- 
cgit v1.2.3