diff options
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 165 | ||||
| -rw-r--r-- | dhall/src/semantics/core/var.rs | 144 | ||||
| -rw-r--r-- | dhall/src/syntax/ast/expr.rs | 3 |
3 files changed, 39 insertions, 273 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index b4e4e61..28f8e37 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -381,21 +381,30 @@ impl ValueKind<Value> { } impl<V> ValueKind<V> { + pub(crate) fn traverse_ref_with_special_handling_of_binders<'a, V2, E>( + &'a self, + visit_val: impl FnMut(&'a V) -> Result<V2, E>, + visit_under_binder: impl FnMut(&'a Binder, &'a V) -> Result<V2, E>, + ) -> Result<ValueKind<V2>, E> { + use crate::semantics::visitor; + use visitor::ValueKindVisitor; + visitor::TraverseRefWithBindersVisitor { + visit_val, + visit_under_binder, + } + .visit(self) + } + pub(crate) fn map_ref_with_special_handling_of_binders<'a, V2>( &'a self, mut map_val: impl FnMut(&'a V) -> V2, mut map_under_binder: impl FnMut(&'a Binder, &'a V) -> V2, ) -> ValueKind<V2> { - use crate::semantics::visitor; use crate::syntax::trivial_result; - use visitor::ValueKindVisitor; - trivial_result( - visitor::TraverseRefWithBindersVisitor { - visit_val: |x| Ok(map_val(x)), - visit_under_binder: |l, x| Ok(map_under_binder(l, x)), - } - .visit(self), - ) + trivial_result(self.traverse_ref_with_special_handling_of_binders( + |x| Ok(map_val(x)), + |l, x| Ok(map_under_binder(l, x)), + )) } #[allow(dead_code)] @@ -411,7 +420,9 @@ impl<V> ValueKind<V> { impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Value(self.0.shift(delta, var)?)) + Some(Value(Rc::new(RefCell::new( + self.0.borrow().shift(delta, var)?, + )))) } } @@ -420,7 +431,10 @@ impl Shift for ValueInternal { Some(ValueInternal { form: self.form, kind: self.kind.shift(delta, var)?, - ty: self.ty.shift(delta, var)?, + ty: match &self.ty { + None => None, + Some(ty) => Some(ty.shift(delta, var)?), + }, span: self.span.clone(), }) } @@ -429,64 +443,11 @@ impl Shift for ValueInternal { impl Shift for ValueKind<Value> { 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)?) - } + _ => self.traverse_ref_with_special_handling_of_binders( + |x| Ok(x.shift(delta, var)?), + |b, x| Ok(x.shift(delta, &var.under_binder(b))?), + )?, }) } } @@ -502,7 +463,9 @@ impl Subst<Value> for Value { } val.clone() } - _ => Value(self.0.subst_shift(var, val)), + _ => Value(Rc::new(RefCell::new( + self.0.borrow().subst_shift(var, val), + ))), } } } @@ -513,7 +476,7 @@ impl Subst<Value> for 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), + ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)), span: self.span.clone(), } } @@ -522,65 +485,13 @@ impl Subst<Value> for ValueInternal { impl Subst<Value> for ValueKind<Value> { 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), + _ => self.map_ref_with_special_handling_of_binders( + |x| x.subst_shift(var, val), + |b, x| { + x.subst_shift(&var.under_binder(b), &val.under_binder(b)) + }, ), } } diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 99d3125..c21e53e 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,6 +1,6 @@ use std::collections::HashMap; -use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; +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. @@ -143,145 +143,3 @@ impl From<Binder> for Label { x.name } } -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() - } -} diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 0ac31a5..04b5adc 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -174,9 +174,6 @@ pub enum ExprKind<SubExpr, Embed> { } impl<Label> V<Label> { - pub(crate) fn name(&self) -> &Label { - &self.0 - } pub(crate) fn idx(&self) -> usize { self.1 } |