From 7dd2d64073b662acccb39601591c754279385308 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:24:48 +0000
Subject: No need for the current env to tck Foo/build closures

---
 dhall/src/semantics/builtins.rs |  6 +-----
 dhall/src/semantics/nze/env.rs  | 11 ++---------
 dhall/src/semantics/tck/env.rs  | 13 -------------
 3 files changed, 3 insertions(+), 27 deletions(-)

(limited to 'dhall/src/semantics')

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 2efa266..0b105c7 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -224,11 +224,7 @@ pub(crate) fn apply_builtin(
         Value(Value),
         DoneAsIs,
     }
-    let make_closure = |e| {
-        type_with(&env.to_alpha_tyenv(), &e)
-            .unwrap()
-            .normalize_whnf(&env)
-    };
+    let make_closure = |e| typecheck(&e).unwrap().normalize_whnf(&env);
 
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 3c42ee7..dee597a 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, TyEnv, Value, ValueKind};
+use crate::semantics::{AlphaVar, Value, ValueKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) enum NzVar {
@@ -9,7 +9,7 @@ pub(crate) enum NzVar {
 }
 
 #[derive(Debug, Clone)]
-pub(crate) enum NzEnvItem {
+enum NzEnvItem {
     // Variable is bound with given type
     Kept(Value),
     // Variable has been replaced by corresponding value
@@ -48,9 +48,6 @@ impl NzEnv {
     pub fn new() -> Self {
         NzEnv { items: Vec::new() }
     }
-    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();
@@ -72,10 +69,6 @@ impl NzEnv {
             NzEnvItem::Replaced(x) => x.clone(),
         }
     }
-
-    pub fn size(&self) -> usize {
-        self.items.len()
-    }
 }
 
 /// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`.
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1276a48..d4cc37d 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -45,11 +45,6 @@ impl NameEnv {
     pub fn new() -> Self {
         NameEnv { names: Vec::new() }
     }
-    pub fn from_binders(names: impl Iterator<Item = Label>) -> Self {
-        NameEnv {
-            names: names.collect(),
-        }
-    }
     pub fn as_varenv(&self) -> VarEnv {
         VarEnv {
             size: self.names.len(),
@@ -99,14 +94,6 @@ 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_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-- 
cgit v1.2.3