diff options
Diffstat (limited to 'dhall/src/semantics/core')
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 145 | ||||
| -rw-r--r-- | dhall/src/semantics/core/mod.rs | 4 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 338 | ||||
| -rw-r--r-- | dhall/src/semantics/core/valuef.rs | 323 | ||||
| -rw-r--r-- | dhall/src/semantics/core/var.rs | 295 |
5 files changed, 1105 insertions, 0 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs new file mode 100644 index 0000000..00e1493 --- /dev/null +++ b/dhall/src/semantics/core/context.rs @@ -0,0 +1,145 @@ +use std::collections::HashMap; +use std::rc::Rc; + +use crate::syntax::{Label, V}; + +use crate::core::value::Value; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::TypeError; + +#[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_valuef_and_type(ValueF::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 new file mode 100644 index 0000000..08213f7 --- /dev/null +++ b/dhall/src/semantics/core/mod.rs @@ -0,0 +1,4 @@ +pub mod context; +pub mod value; +pub mod valuef; +pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs new file mode 100644 index 0000000..bd7a9b9 --- /dev/null +++ b/dhall/src/semantics/core/value.rs @@ -0,0 +1,338 @@ +use std::cell::{Ref, RefCell, RefMut}; +use std::rc::Rc; + +use crate::syntax::{Builtin, Const, Span}; + +use crate::core::context::TypecheckContext; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; +use crate::phase::normalize::{apply_any, normalize_whnf}; +use crate::phase::typecheck::{builtin_to_value, const_to_value}; +use crate::phase::{NormalizedExpr, Typed}; + +#[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 ValueF is the first + /// constructor of the final Normal Form (NF). + WHNF, + /// Normal Form, i.e. completely normalized. + /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the + /// ValueF 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, +} +use Form::{Unevaled, NF, WHNF}; + +/// Partially normalized value. +/// 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, + value: ValueF, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) + ty: Option<Value>, + span: Span, +} + +/// 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. +#[derive(Clone)] +pub(crate) struct Value(Rc<RefCell<ValueInternal>>); + +#[derive(Copy, Clone)] +/// Controls conversion from `Value` to `Expr` +pub(crate) struct ToExprOptions { + /// Whether to convert all variables to `_` + pub(crate) alpha: bool, + /// Whether to normalize before converting + pub(crate) normalize: bool, +} + +impl ValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_valuef(&self) -> &ValueF { + &self.value + } + + fn normalize_whnf(&mut self) { + take_mut::take_or_recover( + self, + // Dummy value in case the other closure panics + || ValueInternal { + form: Unevaled, + value: ValueF::Const(Const::Type), + ty: None, + span: Span::Artificial, + }, + |vint| match (&vint.form, &vint.ty) { + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + value: normalize_whnf(vint.value, &ty), + ty: vint.ty, + span: vint.span, + }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: NF, + value: ValueF::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.value.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 Value { + fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value { + ValueInternal { + form, + value, + ty: Some(ty), + span, + } + .into_value() + } + pub(crate) fn const_sort() -> Value { + ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + span: Span::Artificial, + } + .into_value() + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { + Value::new(v, Unevaled, t, Span::Artificial) + } + pub(crate) fn from_valuef_and_type_and_span( + v: ValueF, + t: Value, + span: Span, + ) -> Value { + Value::new(v, Unevaled, t, span) + } + pub(crate) fn from_valuef_and_type_whnf(v: ValueF, 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() { + ValueF::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 ValueF may be entirely unnormalized, in aprticular it may just be an + /// unevaled PartialExpr. You probably want to use `as_whnf`. + fn as_valuef(&self) -> Ref<ValueF> { + Ref::map(self.as_internal(), ValueInternal::as_valuef) + } + /// 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<ValueF> { + self.normalize_whnf(); + self.as_valuef() + } + + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + if opts.normalize { + self.normalize_whnf(); + } + self.as_valuef().to_expr(opts) + } + pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { + 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) -> ValueF { + 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 app(&self, v: Value) -> Value { + let body_t = match &*self.get_type_not_sort().as_whnf() { + ValueF::Pi(x, t, e) => { + v.check_type(t); + e.subst_shift(&x.into(), &v) + } + _ => unreachable!("Internal type error"), + }; + Value::from_valuef_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 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, + value: self.value.shift(delta, var)?, + ty: self.ty.shift(delta, var)?, + span: self.span.clone(), + }) + } +} + +impl Subst<Value> for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match &*self.as_valuef() { + // 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. + ValueF::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, + value: self.value.subst_shift(var, val), + ty: self.ty.subst_shift(var, val), + span: self.span.clone(), + } + } +} + +// 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 ValueF::Const(c) = &vint.value { + write!(fmt, "{:?}", c) + } else { + let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); + x.field("value", &vint.value); + 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/valuef.rs b/dhall/src/semantics/core/valuef.rs new file mode 100644 index 0000000..e9ac391 --- /dev/null +++ b/dhall/src/semantics/core/valuef.rs @@ -0,0 +1,323 @@ +use std::collections::HashMap; + +use crate::syntax::{ + Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, +}; + +use crate::core::value::{ToExprOptions, Value}; +use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::phase::typecheck::rc; +use crate::phase::{Normalized, NormalizedExpr}; + +/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are +/// normalized on-demand. +/// If you compare for equality two `ValueF`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(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ValueF { + /// 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(ExprF<Value, Normalized>), +} + +impl ValueF { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_valuef_and_type(self, t) + } + + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + match self { + ValueF::Lam(x, t, e) => rc(ExprF::Lam( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueF::AppliedBuiltin(b, args) => args + .iter() + .map(|v| v.to_expr(opts)) + .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), + ValueF::Pi(x, t, e) => rc(ExprF::Pi( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), + ValueF::Const(c) => rc(ExprF::Const(*c)), + ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueF::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.to_expr(opts), + )), + ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), + ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + n.to_expr(opts), + )))), + ValueF::NEListLit(elts) => rc(ExprF::NEListLit( + elts.iter().map(|n| n.to_expr(opts)).collect(), + )), + ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueF::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueF::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) + }) + .collect(), + )), + ValueF::UnionConstructor(l, kts) => rc(ExprF::Field( + ValueF::UnionType(kts.clone()).to_expr(opts), + l.clone(), + )), + ValueF::UnionLit(l, v, kts) => rc(ExprF::App( + ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), + v.to_expr(opts), + )), + ValueF::TextLit(elts) => rc(ExprF::TextLit( + elts.iter() + .map(|contents| contents.map_ref(|e| e.to_expr(opts))) + .collect(), + )), + ValueF::Equivalence(x, y) => rc(ExprF::BinOp( + crate::syntax::BinOp::Equivalence, + x.to_expr(opts), + y.to_expr(opts), + )), + ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + } + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueF::Var(_) + | ValueF::Const(_) + | ValueF::BoolLit(_) + | ValueF::NaturalLit(_) + | ValueF::IntegerLit(_) + | ValueF::DoubleLit(_) => {} + + ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueF::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueF::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueF::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueF::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueF::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueF::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueF::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueF::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueF::TextLit(elts) => { + for x in elts.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } + ValueF::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueF::PartialExpr(e) => { + e.map_mut(Value::normalize_mut); + } + } + } + + pub(crate) fn from_builtin(b: Builtin) -> ValueF { + ValueF::AppliedBuiltin(b, vec![]) + } +} + +impl Shift for ValueF { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(match self { + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.shift(delta, var)?) + } + ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.shift(delta, var)?) + } + ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + } + ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), + }) + } +} + +impl Subst<Value> for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) + } + ValueF::PartialExpr(e) => { + ValueF::PartialExpr(e.subst_shift(var, val)) + } + ValueF::TextLit(elts) => { + ValueF::TextLit(elts.subst_shift(var, val)) + } + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueF::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.subst_shift(var, val)) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.subst_shift(var, val)) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.subst_shift(var, val)) + } + ValueF::RecordLit(kvs) => { + ValueF::RecordLit(kvs.subst_shift(var, val)) + } + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.subst_shift(var, val)) + } + ValueF::UnionType(kts) => { + ValueF::UnionType(kts.subst_shift(var, val)) + } + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueF::Equivalence(x, y) => ValueF::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs new file mode 100644 index 0000000..f9d3478 --- /dev/null +++ b/dhall/src/semantics/core/var.rs @@ -0,0 +1,295 @@ +use std::collections::HashMap; + +use crate::syntax::{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 ValueF 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 crate::syntax::ExprF<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 crate::syntax::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 crate::syntax::ExprF<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 crate::syntax::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() + } +} |