diff options
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/mod.rs | 1 | ||||
-rw-r--r-- | dhall/src/semantics/nze/env.rs | 87 | ||||
-rw-r--r-- | dhall/src/semantics/nze/mod.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/nze/nzexpr.rs | 116 | ||||
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 62 | ||||
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 137 | ||||
-rw-r--r-- | dhall/src/semantics/tck/mod.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 58 |
11 files changed, 239 insertions, 241 deletions
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<NzEnvItem>, +} + +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<Binder>, -} - -#[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<Item = Binder>) -> 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<Binder>) -> Option<AlphaVar> { - 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<Binder> { - 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<AlphaVar> { - 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<NzEnvItem>, -} - -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<Label>, +} + +/// Environment for typing expressions. +#[derive(Debug, Clone)] +pub(crate) struct TyEnv { + names: NameEnv, + items: NzEnv, +} + +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<AlphaVar> { + let idx = self.size.checked_sub(var.idx() + 1)?; + Some(AlphaVar::new(V((), idx))) + } +} + +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(), + } + } + + pub fn insert(&self, x: &Label) -> Self { + let mut env = self.clone(); + env.insert_mut(x); + env + } + pub fn insert_mut(&mut self, x: &Label) { + self.names.push(x.clone()) + } + pub fn remove_mut(&mut self) { + self.names.pop(); + } + + pub fn unlabel_var(&self, var: &V<Label>) -> Option<AlphaVar> { + 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<Label> { + 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 TyEnv { + pub fn new() -> Self { + TyEnv { + names: NameEnv::new(), + 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() + } + pub fn as_nzenv(&self) -> &NzEnv { + &self.items + } + pub fn as_nameenv(&self) -> &NameEnv { + &self.names + } + + pub fn insert_type(&self, x: &Label, t: Type) -> Self { + TyEnv { + names: self.names.insert(x), + items: self.items.insert_type(t), + } + } + pub fn insert_value(&self, x: &Label, e: Value) -> Self { + TyEnv { + names: self.names.insert(x), + items: self.items.insert_value(e), + } + } + pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> { + let var = self.names.unlabel_var(var)?; + let ty = self.items.lookup_val(&var).get_type().unwrap(); + Some((TyExprKind::Var(var), ty)) + } +} diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs index ba95847..28974af 100644 --- a/dhall/src/semantics/tck/mod.rs +++ b/dhall/src/semantics/tck/mod.rs @@ -1,4 +1,6 @@ pub mod context; +pub mod env; pub mod tyexpr; pub mod typecheck; +pub(crate) use env::*; pub(crate) use tyexpr::*; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index b64c519..262cda6 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,12 +1,10 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::AlphaVar; -use crate::semantics::nze::nzexpr::NameEnv; -use crate::semantics::phase::normalize::{normalize_tyexpr_whnf, NzEnv}; +use crate::semantics::phase::normalize::normalize_tyexpr_whnf; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; -use crate::semantics::tck::typecheck::TyEnv; -use crate::semantics::Value; +use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7a225f7..789105f 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -3,71 +3,19 @@ use std::cmp::max; use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::nze::{NameEnv, NzVar, VarEnv}; -use crate::semantics::phase::normalize::{merge_maps, NzEnv}; +use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::typecheck::{ builtin_to_value, const_to_value, type_of_builtin, }; use crate::semantics::phase::Normalized; use crate::semantics::{ - Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind, + Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind, }; use crate::syntax; use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, - Span, V, + BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span, }; -#[derive(Debug, Clone)] -pub(crate) struct TyEnv { - names: NameEnv, - items: NzEnv, -} - -impl TyEnv { - pub fn new() -> Self { - TyEnv { - names: NameEnv::new(), - 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() - } - pub fn as_nzenv(&self) -> &NzEnv { - &self.items - } - pub fn as_nameenv(&self) -> &NameEnv { - &self.names - } - - pub fn insert_type(&self, x: &Label, t: Type) -> Self { - TyEnv { - names: self.names.insert(x), - items: self.items.insert_type(t), - } - } - pub fn insert_value(&self, x: &Label, e: Value) -> Self { - TyEnv { - names: self.names.insert(x), - items: self.items.insert_value(e), - } - } - pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> { - let var = self.names.unlabel_var(var)?; - let ty = self.items.lookup_val(&var).get_type().unwrap(); - Some((TyExprKind::Var(var), ty)) - } -} - fn type_of_recordtype<'a>( tys: impl Iterator<Item = Cow<'a, TyExpr>>, ) -> Result<Type, TypeError> { |