From 837298f26e07bb264a6b6f0286cbb811553b0477 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 14:49:17 +0000
Subject: Increase encapsulation for Closures

---
 dhall/src/semantics/core/value.rs    | 34 +++++++++++++++++++++++++++-------
 dhall/src/semantics/tck/typecheck.rs | 10 +++++-----
 2 files changed, 32 insertions(+), 12 deletions(-)

(limited to 'dhall/src/semantics')

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index af01177..bf75710 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -270,9 +270,7 @@ impl Value {
             } => TyExprKind::Expr(ExprKind::Lam(
                 binder.to_label(),
                 annot.to_tyexpr(venv),
-                closure
-                    .apply_var(NzVar::new(venv.size()))
-                    .to_tyexpr(venv.insert()),
+                closure.to_tyexpr(venv),
             )),
             ValueKind::PiClosure {
                 binder,
@@ -281,9 +279,7 @@ impl Value {
             } => TyExprKind::Expr(ExprKind::Pi(
                 binder.to_label(),
                 annot.to_tyexpr(venv),
-                closure
-                    .apply_var(NzVar::new(venv.size()))
-                    .to_tyexpr(venv.insert()),
+                closure.to_tyexpr(venv),
             )),
             ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
             ValueKind::UnionConstructor(l, kts, t) => {
@@ -576,12 +572,14 @@ impl Closure {
             body,
         }
     }
+    /// New closure that ignores its argument
     pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self {
         Closure::ConstantClosure {
             env: env.clone(),
             body,
         }
     }
+
     pub fn apply(&self, val: Value) -> Value {
         match self {
             Closure::Closure { env, body, .. } => {
@@ -592,7 +590,7 @@ impl Closure {
             }
         }
     }
-    pub fn apply_var(&self, var: NzVar) -> Value {
+    fn apply_var(&self, var: NzVar) -> Value {
         match self {
             Closure::Closure { arg_ty, .. } => {
                 let val = Value::from_kind_and_type(
@@ -606,6 +604,28 @@ impl Closure {
             }
         }
     }
+
+    /// Convert this closure to a TyExpr
+    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+        self.apply_var(NzVar::new(venv.size()))
+            .to_tyexpr(venv.insert())
+    }
+    /// 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 { .. } => {
+                // 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))
+            }
+        }
+    }
 }
 
 /// Compare two values for equality modulo alpha/beta-equivalence.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 0c5e779..bc1c87f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -6,7 +6,7 @@ use crate::error::{TypeError, TypeMessage};
 use crate::semantics::phase::normalize::merge_maps;
 use crate::semantics::phase::Normalized;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, NzVar, TyEnv, TyExpr,
+    type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
     TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax::{
@@ -48,7 +48,7 @@ fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
     Ok(Value::from_const(function_check(ks, kt)))
 }
 
-fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
+fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
     Err(TypeError::new(TypeMessage::Custom(x.to_string())))
 }
 
@@ -452,9 +452,9 @@ fn type_one_layer(
                                     return mkerr("MergeHandlerTypeMismatch");
                                 }
 
-                                let v = NzVar::fresh();
-                                // TODO: handle case where variable is used in closure
-                                closure.apply_var(v)
+                                closure.remove_binder().or_else(|()| {
+                                    mkerr("MergeReturnTypeIsDependent")
+                                })?
                             }
                             _ => return mkerr("NotAFunction"),
                         }
-- 
cgit v1.2.3