diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 53 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 67 | ||||
| -rw-r--r-- | dhall/src/semantics/core/var.rs | 32 | ||||
| -rw-r--r-- | dhall/src/semantics/to_expr.rs | 23 | ||||
| -rw-r--r-- | dhall/src/syntax/ast/expr.rs | 9 |
5 files changed, 28 insertions, 156 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 826ba15..3a7930e 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,6 +1,4 @@ -use std::cell::RefCell; use std::collections::HashMap; -use std::rc::Rc; use crate::error::TypeError; use crate::semantics::core::value::Value; @@ -17,28 +15,14 @@ enum CtxItem { #[derive(Debug, Clone)] pub(crate) struct TyCtx { ctx: Vec<(Binder, CtxItem)>, - /// Keeps track of the next free binder id to assign. Shared among all the contexts to ensure - /// unicity across the expression. - next_uid: Rc<RefCell<u64>>, -} - -#[derive(Debug, Clone)] -pub(crate) struct VarCtx<'b> { - ctx: Vec<&'b Binder>, } impl TyCtx { pub fn new() -> Self { - TyCtx { - ctx: Vec::new(), - next_uid: Rc::new(RefCell::new(0)), - } + TyCtx { ctx: Vec::new() } } fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self { - TyCtx { - ctx: vec, - next_uid: self.next_uid.clone(), - } + TyCtx { ctx: vec } } pub fn insert_type(&self, x: &Binder, t: Value) -> Self { let mut vec = self.ctx.clone(); @@ -79,10 +63,7 @@ impl TyCtx { None } pub fn new_binder(&self, l: &Label) -> Binder { - let mut next_uid = self.next_uid.borrow_mut(); - let uid = *next_uid; - *next_uid += 1; - Binder::new(l.clone(), uid) + Binder::new(l.clone()) } /// Given a var that makes sense in the current context, map the given function in such a way @@ -133,34 +114,6 @@ impl TyCtx { } } -impl<'b> VarCtx<'b> { - pub fn new() -> Self { - VarCtx { ctx: Vec::new() } - } - pub fn insert(&self, binder: &'b Binder) -> Self { - VarCtx { - ctx: self.ctx.iter().copied().chain(Some(binder)).collect(), - } - } - pub fn lookup(&self, binder: &Binder) -> Option<usize> { - self.ctx - .iter() - .rev() - .enumerate() - .find(|(_, other)| binder.same_binder(other)) - .map(|(i, _)| i) - } - pub fn lookup_by_name(&self, binder: &Binder) -> Option<usize> { - self.ctx - .iter() - .rev() - .filter(|other| binder.name() == other.name()) - .enumerate() - .find(|(_, other)| binder.same_binder(other)) - .map(|(i, _)| i) - } -} - impl Shift for CtxItem { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(match self { diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 26b8672..b4e4e61 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,10 +1,9 @@ -use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::{TyCtx, VarCtx}; +use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; @@ -164,7 +163,7 @@ impl Value { &self, opts: to_expr::ToExprOptions, ) -> NormalizedExpr { - to_expr::value_to_expr(&VarCtx::new(), self, opts) + to_expr::value_to_expr(self, opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> { self.as_whnf().clone() @@ -410,65 +409,6 @@ impl<V> ValueKind<V> { } } -/// Compare two values for equality modulo alpha/beta-equivalence. -// TODO: use Rc comparison to shortcut on identical pointers -fn equiv(val1: &Value, val2: &Value) -> bool { - struct ValueWithCtx<'v, 'c> { - val: &'v Value, - ctx: Cow<'c, VarCtx<'v>>, - } - impl<'v, 'c> PartialEq for ValueWithCtx<'v, 'c> { - fn eq(&self, other: &ValueWithCtx<'v, 'c>) -> bool { - equiv_with_ctx(&*self.ctx, self.val, &*other.ctx, other.val) - } - } - // Push the given context into every subnode of the ValueKind. That way, normal equality of the - // resulting value will take into account the context. - fn push_context_through<'v, 'c>( - ctx: &'c VarCtx<'v>, - kind: &'v ValueKind<Value>, - ) -> ValueKind<ValueWithCtx<'v, 'c>> { - kind.map_ref_with_special_handling_of_binders( - |val| ValueWithCtx { - val, - ctx: Cow::Borrowed(ctx), - }, - |binder, val| ValueWithCtx { - val, - ctx: Cow::Owned(ctx.insert(binder)), - }, - ) - } - - fn equiv_with_ctx<'v, 'c>( - ctx1: &'c VarCtx<'v>, - val1: &'v Value, - ctx2: &'c VarCtx<'v>, - val2: &'v Value, - ) -> bool { - use ValueKind::Var; - let kind1 = val1.as_whnf(); - let kind2 = val2.as_whnf(); - - if let (Var(v1), Var(v2)) = (&*kind1, &*kind2) { - let b1 = v1.binder(); - let b2 = v2.binder(); - if b1.same_binder(&b2) { - return true; - } - match (ctx1.lookup(&b1), ctx2.lookup(&b2)) { - (Some(i), Some(j)) => i == j, - _ => false, - } - } else { - push_context_through(ctx1, &*kind1) - == push_context_through(ctx2, &*kind2) - } - } - - equiv_with_ctx(&VarCtx::new(), val1, &VarCtx::new(), val2) -} - impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(Value(self.0.shift(delta, var)?)) @@ -646,9 +586,10 @@ impl Subst<Value> for ValueKind<Value> { } } +// TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { - equiv(self, other) + *self.as_whnf() == *other.as_whnf() } } impl std::cmp::Eq for Value {} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index d21fa80..99d3125 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -9,21 +9,13 @@ use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; pub struct AlphaVar { normal: V<Label>, alpha: V<()>, - /// Id of the corresponding binder. - binder_uid: BinderUID, } -type BinderUID = u64; - // Exactly like a Label, but equality returns always true. // This is so that ValueKind equality is exactly alpha-equivalence. #[derive(Clone, Eq)] pub struct Binder { name: Label, - /// Id of the binder, unique across the current expression. Used to distinguish bindersinstead - /// of their name. The id won't actually be unique when there are imports around, but - /// typechecking ensures this can't cause a conflict. - uid: BinderUID, } pub(crate) trait Shift: Sized { @@ -65,20 +57,18 @@ pub(crate) trait Subst<S> { } impl AlphaVar { - pub(crate) fn binder(&self) -> Binder { - Binder::new(self.normal.0.clone(), self.binder_uid) + pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> { + if alpha { + V("_".into(), self.alpha.idx()) + } else { + self.normal.clone() + } } } impl Binder { - pub(crate) fn new(name: Label, uid: BinderUID) -> Self { - Binder { name, uid } - } - pub(crate) fn name(&self) -> &Label { - &self.name - } - pub(crate) fn same_binder(&self, other: &Binder) -> bool { - self.uid == other.uid + pub(crate) fn new(name: Label) -> Self { + Binder { name } } pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { if alpha { @@ -97,7 +87,6 @@ impl Shift for AlphaVar { Some(AlphaVar { normal: self.normal.shift(delta, &var.normal)?, alpha: self.alpha.shift(delta, &var.alpha)?, - binder_uid: self.binder_uid, }) } } @@ -108,6 +97,7 @@ impl std::cmp::PartialEq for AlphaVar { self.alpha == other.alpha } } +/// Equality up to alpha-equivalence impl std::cmp::PartialEq for Binder { fn eq(&self, _other: &Self) -> bool { true @@ -131,18 +121,14 @@ impl<'a> From<&'a Label> for AlphaVar { AlphaVar { normal: V(x.clone(), 0), alpha: V((), 0), - // TODO: evil evil but only used in shift - binder_uid: 0, } } } impl From<Binder> for AlphaVar { fn from(x: Binder) -> AlphaVar { - let binder_uid = x.uid; AlphaVar { normal: V(x.into(), 0), alpha: V((), 0), - binder_uid, } } } diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 1ece1cc..1adfd49 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,9 +1,8 @@ -use crate::semantics::core::context::VarCtx; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; use crate::semantics::{Value, ValueKind}; use crate::syntax; -use crate::syntax::{Builtin, ExprKind, V}; +use crate::syntax::{Builtin, ExprKind}; /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -16,7 +15,6 @@ pub(crate) struct ToExprOptions { /// Converts a value back to the corresponding AST expression. pub(crate) fn value_to_expr( - ctx: &VarCtx, val: &Value, opts: ToExprOptions, ) -> NormalizedExpr { @@ -25,25 +23,10 @@ pub(crate) fn value_to_expr( } let kind = val.as_kind(); - let kind = kind.map_ref_with_special_handling_of_binders( - |v| value_to_expr(ctx, v, opts), - |binder, v| value_to_expr(&ctx.insert(binder), v, opts), - ); + let kind = kind.map_ref(|v| value_to_expr(v, opts)); match kind { ValueKind::Var(v) => { - let b = v.binder(); - let (idx, name) = if opts.alpha { - (ctx.lookup(&b), "_".into()) - } else { - (ctx.lookup_by_name(&b), b.name().clone()) - }; - match idx { - Some(idx) => rc(ExprKind::Var(V(name, idx))), - None => panic!( - "internal error: binder {:?} not found in environment", - b - ), - } + rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha))) } ValueKind::Lam(x, t, e) => { rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 376480f..0ac31a5 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -173,6 +173,15 @@ pub enum ExprKind<SubExpr, Embed> { Embed(Embed), } +impl<Label> V<Label> { + pub(crate) fn name(&self) -> &Label { + &self.0 + } + pub(crate) fn idx(&self) -> usize { + self.1 + } +} + impl<SE, E> ExprKind<SE, E> { pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>( &'a self, |