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 ++++++++++++++++++++++++++++ dhall/src/semantics/nze/mod.rs | 4 +- dhall/src/semantics/nze/nzexpr.rs | 116 -------------------------------------- 3 files changed, 89 insertions(+), 118 deletions(-) create mode 100644 dhall/src/semantics/nze/env.rs delete mode 100644 dhall/src/semantics/nze/nzexpr.rs (limited to 'dhall/src/semantics/nze') 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 {} diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index 213404c..1cd2363 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -1,2 +1,2 @@ -pub mod nzexpr; -pub(crate) use nzexpr::*; +pub mod env; +pub(crate) use env::*; diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs deleted file mode 100644 index c065a5b..0000000 --- a/dhall/src/semantics/nze/nzexpr.rs +++ /dev/null @@ -1,116 +0,0 @@ -use crate::semantics::core::var::AlphaVar; -use crate::syntax::{Label, V}; - -pub(crate) type Binder = Label; - -#[derive(Debug, Clone)] -pub(crate) struct NameEnv { - names: Vec, -} - -#[derive(Debug, Clone, Copy)] -pub(crate) struct VarEnv { - size: usize, -} - -#[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), -} - -impl NameEnv { - pub fn new() -> Self { - NameEnv { names: Vec::new() } - } - pub fn from_binders(names: impl Iterator) -> Self { - NameEnv { - names: names.collect(), - } - } - pub fn as_varenv(&self) -> VarEnv { - VarEnv { - size: self.names.len(), - } - } - - pub fn insert(&self, x: &Binder) -> Self { - let mut env = self.clone(); - env.insert_mut(x); - env - } - pub fn insert_mut(&mut self, x: &Binder) { - self.names.push(x.clone()) - } - pub fn remove_mut(&mut self) { - self.names.pop(); - } - - pub fn unlabel_var(&self, var: &V) -> Option { - let V(name, idx) = var; - let (idx, _) = self - .names - .iter() - .rev() - .enumerate() - .filter(|(_, n)| *n == name) - .nth(*idx)?; - Some(AlphaVar::new(V((), idx))) - } - pub fn label_var(&self, var: &AlphaVar) -> V { - let name = &self.names[self.names.len() - 1 - var.idx()]; - let idx = self - .names - .iter() - .rev() - .take(var.idx()) - .filter(|n| *n == name) - .count(); - V(name.clone(), idx) - } -} - -impl VarEnv { - pub fn new() -> Self { - VarEnv { size: 0 } - } - pub fn size(&self) -> usize { - self.size - } - pub fn insert(&self) -> Self { - VarEnv { - size: self.size + 1, - } - } - pub fn lookup(&self, var: &NzVar) -> AlphaVar { - self.lookup_fallible(var).unwrap() - } - pub fn lookup_fallible(&self, var: &NzVar) -> Option { - let idx = self.size.checked_sub(var.idx() + 1)?; - Some(AlphaVar::new(V((), idx))) - } -} - -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) - } - // 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" - ), - } - } -} -- cgit v1.2.3