From 8e2da26650e202f9ccb1531fc8a88cfd89e54b6d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 15:15:08 +0000 Subject: Implement traverse_ref for ValueKind --- dhall/src/semantics/core/mod.rs | 3 + dhall/src/semantics/core/value.rs | 28 ++++++++ dhall/src/semantics/core/visitor.rs | 134 ++++++++++++++++++++++++++++++++++++ dhall/src/semantics/mod.rs | 1 + dhall/src/syntax/ast/expr.rs | 2 +- dhall/src/syntax/ast/visitor.rs | 3 +- 6 files changed, 169 insertions(+), 2 deletions(-) create mode 100644 dhall/src/semantics/core/visitor.rs (limited to 'dhall') diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs index 90d74ea..6f577f0 100644 --- a/dhall/src/semantics/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs @@ -1,3 +1,6 @@ pub mod context; pub mod value; pub mod var; +pub mod visitor; +pub(crate) use value::*; +pub(crate) use var::*; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 5f244b7..f7c2fbf 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -388,6 +388,34 @@ impl ValueKind { } } +impl ValueKind { + #[allow(dead_code)] + 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 AlphaLabel, &'a V) -> V2, + ) -> ValueKind { + 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), + ) + } +} + +// #[allow(dead_code)] +// fn equiv(x: &Value, y:&Value) -> bool { +// let map = |kind| { + +// }; +// map(x) == map(y) +// } + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs new file mode 100644 index 0000000..c7cf79e --- /dev/null +++ b/dhall/src/semantics/core/visitor.rs @@ -0,0 +1,134 @@ +use std::iter::FromIterator; + +use crate::semantics::{AlphaLabel, ValueKind}; +use crate::syntax::Label; + +/// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets +/// us have as much mutability as we can. See the equivalent file in `crate::syntax` for more +/// details. +pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized { + type Error; + + fn visit_val(&mut self, val: &'a V1) -> Result; + fn visit_val_under_binder( + mut self, + _label: &'a AlphaLabel, + val: &'a V1, + ) -> Result { + self.visit_val(val) + } + fn visit_vec(&mut self, x: &'a [V1]) -> Result, Self::Error> { + x.iter().map(|e| self.visit_val(e)).collect() + } + fn visit_opt( + &mut self, + x: &'a Option, + ) -> Result, Self::Error> { + Ok(match x { + Some(x) => Some(self.visit_val(x)?), + None => None, + }) + } + fn visit_map( + &mut self, + x: impl IntoIterator, + ) -> Result + where + V1: 'a, + T: FromIterator<(Label, V2)>, + { + x.into_iter() + .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?))) + .collect() + } + fn visit_optmap( + &mut self, + x: impl IntoIterator)>, + ) -> Result + where + V1: 'a, + T: FromIterator<(Label, Option)>, + { + x.into_iter() + .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?))) + .collect() + } + + fn visit( + self, + input: &'a ValueKind, + ) -> Result, Self::Error> { + visit_ref(self, input) + } +} + +fn visit_ref<'a, Visitor, V1, V2>( + mut v: Visitor, + input: &'a ValueKind, +) -> Result, Visitor::Error> +where + Visitor: ValueKindVisitor<'a, V1, V2>, +{ + use ValueKind::*; + Ok(match input { + Lam(l, t, e) => { + Lam(l.clone(), v.visit_val(t)?, v.visit_val_under_binder(l, e)?) + } + Pi(l, t, e) => { + Pi(l.clone(), v.visit_val(t)?, v.visit_val_under_binder(l, e)?) + } + AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?), + Var(v) => Var(v.clone()), + Const(k) => Const(*k), + BoolLit(b) => BoolLit(*b), + NaturalLit(n) => NaturalLit(*n), + IntegerLit(n) => IntegerLit(*n), + DoubleLit(n) => DoubleLit(*n), + EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_val(t)?), + NEOptionalLit(x) => NEOptionalLit(v.visit_val(x)?), + EmptyListLit(t) => EmptyListLit(v.visit_val(t)?), + NEListLit(xs) => NEListLit(v.visit_vec(xs)?), + RecordType(kts) => RecordType(v.visit_map(kts)?), + RecordLit(kvs) => RecordLit(v.visit_map(kvs)?), + UnionType(kts) => UnionType(v.visit_optmap(kts)?), + UnionConstructor(l, kts) => { + UnionConstructor(l.clone(), v.visit_optmap(kts)?) + } + UnionLit(l, t, kts) => { + UnionLit(l.clone(), v.visit_val(t)?, v.visit_optmap(kts)?) + } + TextLit(ts) => TextLit( + ts.iter() + .map(|t| t.traverse_ref(|e| v.visit_val(e))) + .collect::>()?, + ), + Equivalence(x, y) => Equivalence(v.visit_val(x)?, v.visit_val(y)?), + PartialExpr(e) => PartialExpr(e.traverse_ref(|e| v.visit_val(e))?), + }) +} + +pub struct TraverseRefWithBindersVisitor { + pub visit_val: F1, + pub visit_under_binder: F2, +} + +impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> + for TraverseRefWithBindersVisitor +where + V1: 'a, + F1: FnMut(&'a V1) -> Result, + F2: FnOnce(&'a AlphaLabel, &'a V1) -> Result, +{ + type Error = Err; + + fn visit_val(&mut self, val: &'a V1) -> Result { + (self.visit_val)(val) + } + fn visit_val_under_binder( + self, + label: &'a AlphaLabel, + val: &'a V1, + ) -> Result { + (self.visit_under_binder)(label, val) + } +} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 1eeef86..3ef1aba 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,3 +1,4 @@ pub mod core; pub mod phase; pub mod to_expr; +pub(crate) use self::core::*; diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 68cb524..376480f 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -189,7 +189,7 @@ impl ExprKind { .visit(self) } - fn traverse_ref<'a, SE2, Err>( + pub(crate) fn traverse_ref<'a, SE2, Err>( &'a self, visit_subexpr: impl FnMut(&'a SE) -> Result, ) -> Result, Err> diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs index 424048b..f9fd379 100644 --- a/dhall/src/syntax/ast/visitor.rs +++ b/dhall/src/syntax/ast/visitor.rs @@ -1,6 +1,7 @@ -use crate::syntax::*; use std::iter::FromIterator; +use crate::syntax::*; + /// A visitor trait that can be used to traverse `ExprKind`s. We need this pattern so that Rust lets /// us have as much mutability as we can. /// For example, `traverse_ref_with_special_handling_of_binders` cannot be made using only -- cgit v1.2.3