summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/var.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/core/var.rs')
-rw-r--r--dhall/src/semantics/core/var.rs295
1 files changed, 295 insertions, 0 deletions
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()
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 10:15:44 +0000