summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/core/mod.rs3
-rw-r--r--dhall/src/semantics/core/value.rs28
-rw-r--r--dhall/src/semantics/core/visitor.rs134
-rw-r--r--dhall/src/semantics/mod.rs1
-rw-r--r--dhall/src/syntax/ast/expr.rs2
-rw-r--r--dhall/src/syntax/ast/visitor.rs3
6 files changed, 169 insertions, 2 deletions
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<Value> {
}
}
+impl<V> ValueKind<V> {
+ #[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<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),
+ )
+ }
+}
+
+// #[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<Self> {
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<V2, Self::Error>;
+ fn visit_val_under_binder(
+ mut self,
+ _label: &'a AlphaLabel,
+ val: &'a V1,
+ ) -> Result<V2, Self::Error> {
+ self.visit_val(val)
+ }
+ fn visit_vec(&mut self, x: &'a [V1]) -> Result<Vec<V2>, Self::Error> {
+ x.iter().map(|e| self.visit_val(e)).collect()
+ }
+ fn visit_opt(
+ &mut self,
+ x: &'a Option<V1>,
+ ) -> Result<Option<V2>, Self::Error> {
+ Ok(match x {
+ Some(x) => Some(self.visit_val(x)?),
+ None => None,
+ })
+ }
+ fn visit_map<T>(
+ &mut self,
+ x: impl IntoIterator<Item = (&'a Label, &'a V1)>,
+ ) -> Result<T, Self::Error>
+ where
+ V1: 'a,
+ T: FromIterator<(Label, V2)>,
+ {
+ x.into_iter()
+ .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?)))
+ .collect()
+ }
+ fn visit_optmap<T>(
+ &mut self,
+ x: impl IntoIterator<Item = (&'a Label, &'a Option<V1>)>,
+ ) -> Result<T, Self::Error>
+ where
+ V1: 'a,
+ T: FromIterator<(Label, Option<V2>)>,
+ {
+ x.into_iter()
+ .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?)))
+ .collect()
+ }
+
+ fn visit(
+ self,
+ input: &'a ValueKind<V1>,
+ ) -> Result<ValueKind<V2>, Self::Error> {
+ visit_ref(self, input)
+ }
+}
+
+fn visit_ref<'a, Visitor, V1, V2>(
+ mut v: Visitor,
+ input: &'a ValueKind<V1>,
+) -> Result<ValueKind<V2>, 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::<Result<_, _>>()?,
+ ),
+ 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<F1, F2> {
+ pub visit_val: F1,
+ pub visit_under_binder: F2,
+}
+
+impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2>
+ for TraverseRefWithBindersVisitor<F1, F2>
+where
+ V1: 'a,
+ F1: FnMut(&'a V1) -> Result<V2, Err>,
+ F2: FnOnce(&'a AlphaLabel, &'a V1) -> Result<V2, Err>,
+{
+ type Error = Err;
+
+ fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error> {
+ (self.visit_val)(val)
+ }
+ fn visit_val_under_binder(
+ self,
+ label: &'a AlphaLabel,
+ val: &'a V1,
+ ) -> Result<V2, Self::Error> {
+ (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<SE, E> ExprKind<SE, E> {
.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<SE2, Err>,
) -> Result<ExprKind<SE2, E>, 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 09:35:18 +0000