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/core/value.rs | 4 +- dhall/src/semantics/mod.rs | 1 + dhall/src/semantics/nze/env.rs | 87 +++++++++++++++++++++ dhall/src/semantics/nze/mod.rs | 4 +- dhall/src/semantics/nze/nzexpr.rs | 116 ---------------------------- dhall/src/semantics/phase/normalize.rs | 62 +-------------- dhall/src/semantics/phase/typecheck.rs | 3 +- dhall/src/semantics/tck/env.rs | 137 +++++++++++++++++++++++++++++++++ dhall/src/semantics/tck/mod.rs | 2 + dhall/src/semantics/tck/tyexpr.rs | 6 +- dhall/src/semantics/tck/typecheck.rs | 58 +------------- 11 files changed, 239 insertions(+), 241 deletions(-) create mode 100644 dhall/src/semantics/nze/env.rs delete mode 100644 dhall/src/semantics/nze/nzexpr.rs create mode 100644 dhall/src/semantics/tck/env.rs (limited to 'dhall/src') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 90b30b4..7334552 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,12 +4,12 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; -use crate::semantics::nze::{NzVar, VarEnv}; -use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; +use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{ builtin_to_value, builtin_to_value_env, const_to_value, }; use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; +use crate::semantics::{NzEnv, NzVar, VarEnv}; use crate::semantics::{TyExpr, TyExprKind}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 1304502..ce08334 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -3,4 +3,5 @@ pub mod nze; pub mod phase; pub mod tck; pub(crate) use self::core::*; +pub(crate) use self::nze::*; pub(crate) use self::tck::*; 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" - ), - } - } -} diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index fa80b6e..ce37993 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,16 +1,13 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{ builtin_to_value_env, const_to_value, rc, }; use crate::semantics::phase::Normalized; use crate::semantics::tck::typecheck::type_with; -use crate::semantics::tck::typecheck::TyEnv; -use crate::semantics::{ - AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, -}; +use crate::semantics::NzEnv; +use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -838,53 +835,6 @@ pub(crate) fn normalize_whnf( } } -#[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 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() - } -} - /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let ty = match tye.get_type() { @@ -924,11 +874,3 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } - -/// Ignore NzEnv when comparing -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/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 4392365..2e22ad2 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,5 +1,4 @@ -use crate::semantics::phase::normalize::NzEnv; -use crate::semantics::{Value, ValueKind}; +use crate::semantics::{NzEnv, Value, ValueKind}; use crate::syntax; use crate::syntax::{ Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr, diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs new file mode 100644 index 0000000..32c2f21 --- /dev/null +++ b/dhall/src/semantics/tck/env.rs @@ -0,0 +1,137 @@ +use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value}; +use crate::syntax::{Label, V}; + +/// Environment for indexing variables. +#[derive(Debug, Clone, Copy)] +pub(crate) struct VarEnv { + size: usize, +} + +/// Environment for resolving names. +#[derive(Debug, Clone)] +pub(crate) struct NameEnv { + names: Vec