diff options
Diffstat (limited to 'dhall/src/semantics/core')
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 144 | ||||
| -rw-r--r-- | dhall/src/semantics/core/mod.rs | 3 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 591 | ||||
| -rw-r--r-- | dhall/src/semantics/core/var.rs | 295 |
4 files changed, 0 insertions, 1033 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs deleted file mode 100644 index f755f72..0000000 --- a/dhall/src/semantics/core/context.rs +++ /dev/null @@ -1,144 +0,0 @@ -use std::collections::HashMap; -use std::rc::Rc; - -use crate::error::TypeError; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::syntax::{Label, V}; - -#[derive(Debug, Clone)] -enum CtxItem { - Kept(AlphaVar, Value), - Replaced(Value), -} - -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>); - -impl TypecheckContext { - pub fn new() -> Self { - TypecheckContext(Rc::new(Vec::new())) - } - pub fn insert_type(&self, x: &Label, t: Value) -> Self { - let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); - TypecheckContext(Rc::new(vec)) - } - pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> { - let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Replaced(e))); - Ok(TypecheckContext(Rc::new(vec))) - } - pub fn lookup(&self, var: &V<Label>) -> Option<Value> { - let mut var = var.clone(); - let mut shift_map: HashMap<Label, _> = HashMap::new(); - for (l, i) in self.0.iter().rev() { - match var.over_binder(l) { - None => { - let i = i.under_multiple_binders(&shift_map); - return Some(match i { - CtxItem::Kept(newvar, t) => { - Value::from_kind_and_type(ValueKind::Var(newvar), t) - } - CtxItem::Replaced(v) => v, - }); - } - Some(newvar) => var = newvar, - }; - if let CtxItem::Kept(_, _) = i { - *shift_map.entry(l.clone()).or_insert(0) += 1; - } - } - // Unbound variable - None - } - /// Given a var that makes sense in the current context, map the given function in such a way - /// that the passed variable always makes sense in the context of the passed item. - /// Once we pass the variable definition, the variable doesn't make sense anymore so we just - /// copy the remaining items. - fn do_with_var<E>( - &self, - var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>, - ) -> Result<Self, E> { - let mut vec = Vec::new(); - vec.reserve(self.0.len()); - let mut var = var.clone(); - let mut iter = self.0.iter().rev(); - for (l, i) in iter.by_ref() { - vec.push((l.clone(), f(&var, i)?)); - if let CtxItem::Kept(_, _) = i { - match var.over_binder(l) { - None => break, - Some(newvar) => var = newvar, - }; - } - } - for (l, i) in iter { - vec.push((l.clone(), (*i).clone())); - } - vec.reverse(); - Ok(TypecheckContext(Rc::new(vec))) - } - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - if delta < 0 { - Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) - } else { - Some(TypecheckContext(Rc::new( - self.0 - .iter() - .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) - .collect::<Result<_, _>>()?, - ))) - } - } - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) - .unwrap() - } -} - -impl Shift for CtxItem { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - CtxItem::Kept(v, t) => { - CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) - } - CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), - }) - } -} - -impl Shift for TypecheckContext { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - self.shift(delta, var) - } -} - -impl Subst<Value> for CtxItem { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), - CtxItem::Kept(v, t) => match v.shift(-1, var) { - None => CtxItem::Replaced(val.clone()), - Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), - }, - } - } -} - -impl Subst<Value> for TypecheckContext { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.subst_shift(var, val) - } -} - -/// Don't count contexts when comparing stuff. -/// This is dirty but needed. -impl PartialEq for TypecheckContext { - fn eq(&self, _: &Self) -> bool { - true - } -} -impl Eq for TypecheckContext {} diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs deleted file mode 100644 index 90d74ea..0000000 --- a/dhall/src/semantics/core/mod.rs +++ /dev/null @@ -1,3 +0,0 @@ -pub mod context; -pub mod value; -pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs deleted file mode 100644 index 6fa00ac..0000000 --- a/dhall/src/semantics/core/value.rs +++ /dev/null @@ -1,591 +0,0 @@ -use std::cell::{Ref, RefCell, RefMut}; -use std::collections::HashMap; -use std::rc::Rc; - -use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; -use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; -use crate::semantics::to_expr; -use crate::syntax::{ - Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, Span, -}; - -use self::Form::{Unevaled, NF, WHNF}; - -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation -/// automatically. Uses a RefCell to share computation. -/// Can optionally store a type from typechecking to preserve type information. -/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence -/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively -/// normalize as needed. -#[derive(Clone)] -pub(crate) struct Value(Rc<RefCell<ValueInternal>>); - -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form -/// Invariant: if `form` is `NF`, `value` must be fully normalized -#[derive(Debug)] -struct ValueInternal { - form: Form, - kind: ValueKind, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) - ty: Option<Value>, - span: Span, -} - -#[derive(Debug, Clone, Copy)] -pub(crate) enum Form { - /// No constraints; expression may not be normalized at all. - Unevaled, - /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may - /// not be normalized. This means that the first constructor of the contained ValueKind is the first - /// constructor of the final Normal Form (NF). - WHNF, - /// Normal Form, i.e. completely normalized. - /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the - /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so - /// if we have the first constructor of the NF at all levels, we actually have the NF. - NF, -} - -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { - /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), - // Invariant: in whnf, the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec<Value>), - - Var(AlphaVar), - Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), - EmptyOptionalLit(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec<Value>), - RecordType(HashMap<Label, Value>), - RecordLit(HashMap<Label, Value>), - UnionType(HashMap<Label, Option<Value>>), - UnionConstructor(Label, HashMap<Label, Option<Value>>), - UnionLit(Label, Value, HashMap<Label, Option<Value>>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec<InterpolatedTextContents<Value>>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprKind<Value, Normalized>), -} - -impl Value { - fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { - ValueInternal { - form, - kind, - ty: Some(ty), - span, - } - .into_value() - } - pub(crate) fn const_sort() -> Value { - ValueInternal { - form: NF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: Span::Artificial, - } - .into_value() - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { - Value::new(v, Unevaled, t, Span::Artificial) - } - pub(crate) fn from_kind_and_type_and_span( - v: ValueKind, - t: Value, - span: Span, - ) -> Value { - Value::new(v, Unevaled, t, span) - } - pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { - Value::new(v, WHNF, t, Span::Artificial) - } - pub(crate) fn from_const(c: Const) -> Self { - const_to_value(c) - } - pub(crate) fn from_builtin(b: Builtin) -> Self { - builtin_to_value(b) - } - pub(crate) fn with_span(self, span: Span) -> Self { - self.as_internal_mut().span = span; - self - } - - pub(crate) fn as_const(&self) -> Option<Const> { - match &*self.as_whnf() { - ValueKind::Const(c) => Some(*c), - _ => None, - } - } - pub(crate) fn span(&self) -> Span { - self.as_internal().span.clone() - } - - fn as_internal(&self) -> Ref<ValueInternal> { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut<ValueInternal> { - self.0.borrow_mut() - } - /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an - /// unevaled PartialExpr. You probably want to use `as_whnf`. - pub(crate) fn as_kind(&self) -> Ref<ValueKind> { - Ref::map(self.as_internal(), ValueInternal::as_kind) - } - /// This is what you want if you want to pattern-match on the value. - /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut - /// panics. - pub(crate) fn as_whnf(&self) -> Ref<ValueKind> { - self.normalize_whnf(); - self.as_kind() - } - - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::value_to_expr(self, opts) - } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { - self.as_whnf().clone() - } - /// Before discarding type information, check that it matches the expected return type. - pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { - self.check_type(ty); - self.to_whnf_ignore_type() - } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_value(self) - } - - /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. - fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { - match Rc::get_mut(&mut self.0) { - // Mutate directly if sole owner - Some(refcell) => f(RefCell::get_mut(refcell)), - // Otherwise mutate through the refcell - None => f(&mut self.as_internal_mut()), - } - } - /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this. - pub(crate) fn normalize_mut(&mut self) { - self.mutate_internal(|vint| vint.normalize_nf()) - } - - pub(crate) fn normalize_whnf(&self) { - let borrow = self.as_internal(); - match borrow.form { - Unevaled => { - drop(borrow); - self.as_internal_mut().normalize_whnf(); - } - // Already at least in WHNF - WHNF | NF => {} - } - } - pub(crate) fn normalize_nf(&self) { - self.as_internal_mut().normalize_nf(); - } - - pub(crate) fn app(&self, v: Value) -> Value { - let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueKind::Pi(x, t, e) => { - v.check_type(t); - e.subst_shift(&x.into(), &v) - } - _ => unreachable!("Internal type error"), - }; - Value::from_kind_and_type_whnf( - apply_any(self.clone(), v, &body_t), - body_t, - ) - } - - /// In debug mode, panic if the provided type doesn't match the value's type. - /// Otherwise does nothing. - pub(crate) fn check_type(&self, ty: &Value) { - debug_assert_eq!( - Some(ty), - self.get_type().ok().as_ref(), - "Internal type error" - ); - } - pub(crate) fn get_type(&self) -> Result<Value, TypeError> { - Ok(self.as_internal().get_type()?.clone()) - } - /// When we know the value isn't `Sort`, this gets the type directly - pub(crate) fn get_type_not_sort(&self) -> Value { - self.get_type() - .expect("Internal type error: value is `Sort` but shouldn't be") - } -} - -impl ValueInternal { - fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) - } - fn as_kind(&self) -> &ValueKind { - &self.kind - } - - fn normalize_whnf(&mut self) { - take_mut::take_or_recover( - self, - // Dummy value in case the other closure panics - || ValueInternal { - form: Unevaled, - kind: ValueKind::Const(Const::Type), - ty: None, - span: Span::Artificial, - }, - |vint| match (&vint.form, &vint.ty) { - (Unevaled, Some(ty)) => ValueInternal { - form: WHNF, - kind: normalize_whnf(vint.kind, &ty), - ty: vint.ty, - span: vint.span, - }, - // `value` is `Sort` - (Unevaled, None) => ValueInternal { - form: NF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: vint.span, - }, - // Already in WHNF - (WHNF, _) | (NF, _) => vint, - }, - ) - } - fn normalize_nf(&mut self) { - match self.form { - Unevaled => { - self.normalize_whnf(); - self.normalize_nf(); - } - WHNF => { - self.kind.normalize_mut(); - self.form = NF; - } - // Already in NF - NF => {} - } - } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } - } - } -} - -impl ValueKind { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_kind_and_type(self, t) - } - - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::kind_to_expr(self, opts) - } - - pub(crate) fn normalize_mut(&mut self) { - match self { - ValueKind::Var(_) - | ValueKind::Const(_) - | ValueKind::BoolLit(_) - | ValueKind::NaturalLit(_) - | ValueKind::IntegerLit(_) - | ValueKind::DoubleLit(_) => {} - - ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize_mut(); - } - - ValueKind::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueKind::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } - ValueKind::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueKind::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![]) - } -} - -impl Shift for Value { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Value(self.0.shift(delta, var)?)) - } -} - -impl Shift for ValueInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(ValueInternal { - form: self.form, - kind: self.kind.shift(delta, var)?, - ty: self.ty.shift(delta, var)?, - span: self.span.clone(), - }) - } -} - -impl Shift for ValueKind { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.shift(delta, var)?) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.shift(delta, var)?) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.shift(delta, var)?) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.shift(delta, var)?) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.shift(delta, var)?) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.shift(delta, var)?) - } - ValueKind::UnionConstructor(x, kts) => { - ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.shift(delta, var)?) - } - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.shift(delta, var)?, - y.shift(delta, var)?, - ), - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.shift(delta, var)?) - } - }) - } -} - -impl Subst<Value> for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match &*self.as_kind() { - // If the var matches, we can just reuse the provided value instead of copying it. - // We also check that the types match, if in debug mode. - ValueKind::Var(v) if v == var => { - if let Ok(self_ty) = self.get_type() { - val.check_type(&self_ty.subst_shift(var, val)); - } - val.clone() - } - _ => Value(self.0.subst_shift(var, val)), - } - } -} - -impl Subst<Value> for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - ValueInternal { - // The resulting value may not stay in wnhf after substitution - form: Unevaled, - kind: self.kind.subst_shift(var, val), - ty: self.ty.subst_shift(var, val), - span: self.span.clone(), - } - } -} - -impl Subst<Value> for ValueKind { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) - } - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.subst_shift(var, val)) - } - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.subst_shift(var, val)) - } - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.subst_shift(var, val)) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.subst_shift(var, val)) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.subst_shift(var, val)) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.subst_shift(var, val)) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.subst_shift(var, val)) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.subst_shift(var, val)) - } - ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( - x.clone(), - kts.subst_shift(var, val), - ), - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), - } - } -} - -// TODO: use Rc comparison to shortcut on identical pointers -impl std::cmp::PartialEq for Value { - fn eq(&self, other: &Self) -> bool { - *self.as_whnf() == *other.as_whnf() - } -} -impl std::cmp::Eq for Value {} - -impl std::fmt::Debug for Value { - fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let vint: &ValueInternal = &self.as_internal(); - if let ValueKind::Const(c) = &vint.kind { - write!(fmt, "{:?}", c) - } else { - let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); - x.field("value", &vint.kind); - if let Some(ty) = vint.ty.as_ref() { - x.field("type", &ty); - } else { - x.field("type", &None::<()>); - } - x.finish() - } - } -} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs deleted file mode 100644 index 1548713..0000000 --- a/dhall/src/semantics/core/var.rs +++ /dev/null @@ -1,295 +0,0 @@ -use std::collections::HashMap; - -use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; - -/// Stores a pair of variables: a normal one and one -/// that corresponds to the alpha-normalized version of the first one. -/// Equality is up to alpha-equivalence (compares on the second one only). -#[derive(Clone, Eq)] -pub struct AlphaVar { - normal: V<Label>, - alpha: V<()>, -} - -// Exactly like a Label, but equality returns always true. -// This is so that ValueKind equality is exactly alpha-equivalence. -#[derive(Clone, Eq)] -pub struct AlphaLabel(Label); - -pub(crate) trait Shift: Sized { - // Shift an expression to move it around binders without changing the meaning of its free - // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an - // expression from under a binder, if the expression does not refer to that bound variable. - // Returns None if delta was negative and the variable was free in the expression. - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>; - - fn over_binder<T>(&self, x: T) -> Option<Self> - where - T: Into<AlphaVar>, - { - self.shift(-1, &x.into()) - } - - fn under_binder<T>(&self, x: T) -> Self - where - T: Into<AlphaVar>, - { - // Can't fail since delta is positive - self.shift(1, &x.into()).unwrap() - } - - fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self - where - Self: Clone, - { - let mut v = self.clone(); - for (x, n) in shift_map { - v = v.shift(*n as isize, &x.into()).unwrap(); - } - v - } -} - -pub(crate) trait Subst<S> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self; -} - -impl AlphaVar { - pub(crate) fn to_var(&self, alpha: bool) -> V<Label> { - if alpha { - V("_".into(), self.alpha.1) - } else { - self.normal.clone() - } - } - pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self { - AlphaVar { - normal, - alpha: V((), alpha), - } - } -} - -impl AlphaLabel { - pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { - if alpha { - "_".into() - } else { - self.to_label() - } - } - pub(crate) fn to_label(&self) -> Label { - self.clone().into() - } -} - -impl Shift for AlphaVar { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(AlphaVar { - normal: self.normal.shift(delta, &var.normal)?, - alpha: self.alpha.shift(delta, &var.alpha)?, - }) - } -} - -/// Equality up to alpha-equivalence -impl std::cmp::PartialEq for AlphaVar { - fn eq(&self, other: &Self) -> bool { - self.alpha == other.alpha - } -} -impl std::cmp::PartialEq for AlphaLabel { - fn eq(&self, _other: &Self) -> bool { - true - } -} - -impl std::fmt::Debug for AlphaVar { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1) - } -} - -impl std::fmt::Debug for AlphaLabel { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "AlphaLabel({})", &self.0) - } -} - -impl From<Label> for AlphaVar { - fn from(x: Label) -> AlphaVar { - AlphaVar { - normal: V(x, 0), - alpha: V((), 0), - } - } -} -impl<'a> From<&'a Label> for AlphaVar { - fn from(x: &'a Label) -> AlphaVar { - x.clone().into() - } -} -impl From<AlphaLabel> for AlphaVar { - fn from(x: AlphaLabel) -> AlphaVar { - let l: Label = x.into(); - l.into() - } -} -impl<'a> From<&'a AlphaLabel> for AlphaVar { - fn from(x: &'a AlphaLabel) -> AlphaVar { - x.clone().into() - } -} - -impl From<Label> for AlphaLabel { - fn from(x: Label) -> AlphaLabel { - AlphaLabel(x) - } -} -impl From<AlphaLabel> for Label { - fn from(x: AlphaLabel) -> Label { - x.0 - } -} -impl Shift for () { - fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> { - Some(()) - } -} - -impl<A: Shift, B: Shift> Shift for (A, B) { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some((self.0.shift(delta, var)?, self.1.shift(delta, var)?)) - } -} - -impl<T: Shift> Shift for Option<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - None => None, - Some(x) => Some(x.shift(delta, var)?), - }) - } -} - -impl<T: Shift> Shift for Box<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Box::new(self.as_ref().shift(delta, var)?)) - } -} - -impl<T: Shift> Shift for std::rc::Rc<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?)) - } -} - -impl<T: Shift> Shift for std::cell::RefCell<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?)) - } -} - -impl<T: Shift, E: Clone> Shift for ExprKind<T, E> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(self.traverse_ref_with_special_handling_of_binders( - |v| Ok(v.shift(delta, var)?), - |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - )?) - } -} - -impl<T: Shift> Shift for Vec<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some( - self.iter() - .map(|v| Ok(v.shift(delta, var)?)) - .collect::<Result<_, _>>()?, - ) - } -} - -impl<K, T: Shift> Shift for HashMap<K, T> -where - K: Clone + std::hash::Hash + Eq, -{ - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some( - self.iter() - .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) - .collect::<Result<_, _>>()?, - ) - } -} - -impl<T: Shift> Shift for InterpolatedTextContents<T> { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(self.traverse_ref(|x| Ok(x.shift(delta, var)?))?) - } -} - -impl<S> Subst<S> for () { - fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {} -} - -impl<S, A: Subst<S>, B: Subst<S>> Subst<S> for (A, B) { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - (self.0.subst_shift(var, val), self.1.subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for Option<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.as_ref().map(|x| x.subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for Box<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - Box::new(self.as_ref().subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - std::rc::Rc::new(self.as_ref().subst_shift(var, val)) - } -} - -impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - std::cell::RefCell::new(self.borrow().subst_shift(var, val)) - } -} - -impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.map_ref_with_special_handling_of_binders( - |v| v.subst_shift(var, val), - |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ) - } -} - -impl<S, T: Subst<S>> Subst<S> for Vec<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.iter().map(|v| v.subst_shift(var, val)).collect() - } -} - -impl<S, T: Subst<S>> Subst<S> for InterpolatedTextContents<T> { - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.map_ref(|x| x.subst_shift(var, val)) - } -} - -impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T> -where - K: Clone + std::hash::Hash + Eq, -{ - fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { - self.iter() - .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) - .collect() - } -} |