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/nzexpr.rs | 116 -------------------------------------- 1 file changed, 116 deletions(-) delete mode 100644 dhall/src/semantics/nze/nzexpr.rs (limited to 'dhall/src/semantics/nze/nzexpr.rs') 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