From 489174a426e6057a68b6edd2e9b4387d09912a25 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:56:52 +0000 Subject: Move envs to their own files --- dhall/src/semantics/nze/env.rs | 87 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 dhall/src/semantics/nze/env.rs (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs new file mode 100644 index 0000000..203d99a --- /dev/null +++ b/dhall/src/semantics/nze/env.rs @@ -0,0 +1,87 @@ +use crate::semantics::{AlphaVar, TyEnv, Value, ValueKind}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub(crate) enum NzVar { + /// Reverse-debruijn index: counts number of binders from the bottom of the stack. + Bound(usize), + /// Fake fresh variable generated for expression equality checking. + Fresh(usize), +} + +#[derive(Debug, Clone)] +pub(crate) enum NzEnvItem { + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value + Replaced(Value), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzEnv { + items: Vec, +} + +impl NzVar { + pub fn new(idx: usize) -> Self { + NzVar::Bound(idx) + } + pub fn fresh() -> Self { + use std::sync::atomic::{AtomicUsize, Ordering}; + // Global counter to ensure uniqueness of the generated id. + static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0); + let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst); + NzVar::Fresh(id) + } + /// Get index of bound variable. + /// Panics on a fresh variable. + pub fn idx(&self) -> usize { + match self { + NzVar::Bound(i) => *i, + NzVar::Fresh(_) => panic!( + "Trying to use a fresh variable outside of equality checking" + ), + } + } +} + +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(); + env.items.push(NzEnvItem::Kept(t)); + env + } + pub fn insert_value(&self, e: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Replaced(e)); + env + } + pub fn lookup_val(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( + ValueKind::Var(var.clone(), NzVar::new(idx)), + ty.clone(), + ), + NzEnvItem::Replaced(x) => x.clone(), + } + } + + pub fn size(&self) -> usize { + self.items.len() + } +} + +/// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`. +impl std::cmp::PartialEq for NzEnv { + fn eq(&self, _other: &Self) -> bool { + true + } +} +impl std::cmp::Eq for NzEnv {} -- cgit v1.2.3 From a928c3c4f51d87fd942e8a81727962c00abf6808 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 22:06:01 +0000 Subject: Cleanup variable handling --- dhall/src/semantics/nze/env.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 203d99a..3c42ee7 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -66,7 +66,7 @@ impl NzEnv { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), + ValueKind::Var(NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), -- cgit v1.2.3 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/nze/env.rs | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/nze/env.rs') 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`. -- cgit v1.2.3 From 17732b041dbd44f39ce3d04a289146db9882e865 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:53:37 +0000 Subject: Encapsulate partially applied builtin in a separate struct --- dhall/src/semantics/nze/env.rs | 8 -------- 1 file changed, 8 deletions(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index dee597a..a083076 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -70,11 +70,3 @@ impl NzEnv { } } } - -/// Ignore NzEnv when comparing; useful because we store them in `AppliedBuiltin`. -impl std::cmp::PartialEq for NzEnv { - fn eq(&self, _other: &Self) -> bool { - true - } -} -impl std::cmp::Eq for NzEnv {} -- cgit v1.2.3 From 673a580e11d31356bec25d73213b283685fd6ea3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:49:03 +0000 Subject: Clarify normalization to ensure we only nze once --- dhall/src/semantics/nze/env.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index a083076..073886e 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -62,7 +62,7 @@ impl NzEnv { pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( + NzEnvItem::Kept(ty) => Value::from_kind_and_type( ValueKind::Var(NzVar::new(idx)), ty.clone(), ), -- cgit v1.2.3 From d8de45763037937b5c2dedbe5f7bb95a4e7bc7cd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 19:56:31 +0000 Subject: Avoid unnecessary allocations of `Value`s --- dhall/src/semantics/nze/env.rs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'dhall/src/semantics/nze/env.rs') diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index 073886e..0b22a8b 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -59,14 +59,18 @@ impl NzEnv { env.items.push(NzEnvItem::Replaced(e)); env } - pub fn lookup_val(&self, var: &AlphaVar) -> Value { + pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind { let idx = self.items.len() - 1 - var.idx(); match &self.items[idx] { - NzEnvItem::Kept(ty) => Value::from_kind_and_type( - ValueKind::Var(NzVar::new(idx)), - ty.clone(), - ), - NzEnvItem::Replaced(x) => x.clone(), + NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)), + NzEnvItem::Replaced(x) => x.kind().clone(), + } + } + pub fn lookup_ty(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => ty.clone(), + NzEnvItem::Replaced(x) => x.get_type().unwrap(), } } } -- cgit v1.2.3