summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-01-30 11:24:48 +0000
committerNadrieril2020-01-30 11:24:48 +0000
commit7dd2d64073b662acccb39601591c754279385308 (patch)
tree9d07c65c601875fbce4faea171f0edface776186
parentb55e291825e4e7c6899d9bf7051b816660fa43a3 (diff)
No need for the current env to tck Foo/build closures
-rw-r--r--dhall/src/semantics/builtins.rs6
-rw-r--r--dhall/src/semantics/nze/env.rs11
-rw-r--r--dhall/src/semantics/tck/env.rs13
3 files changed, 3 insertions, 27 deletions
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()
}