From 51dbaa0b66089bca63aa9cf69a1e0ec59df053b9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 21:10:59 +0200 Subject: Considerably simplify Embed handling --- dhall/src/core/thunk.rs | 2 - dhall/src/core/value.rs | 8 ++- dhall/src/phase/normalize.rs | 1 - dhall/src/phase/typecheck.rs | 3 +- dhall_syntax/src/core/expr.rs | 110 +++++++++------------------------------ dhall_syntax/src/core/visitor.rs | 60 ++++++--------------- dhall_syntax/src/printer.rs | 2 +- 7 files changed, 48 insertions(+), 138 deletions(-) diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 4d193f9..7c5c537 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -309,7 +309,6 @@ impl Shift for ThunkInternal { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(Normalized::clone(x)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +355,6 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - Normalized::clone, ), ), ThunkInternal::Value(_, v) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 88d7a20..20a6021 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -243,7 +243,7 @@ impl Value { y.normalize_to_expr_maybe_alpha(alpha), )), Value::PartialExpr(e) => { - rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha))) + rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } } @@ -333,8 +333,8 @@ impl Value { y.normalize_mut(); } Value::PartialExpr(e) => { - // TODO: need map_mut_simple - e.map_ref_simple(|v| { + // TODO: need map_mut + e.map_ref(|v| { v.normalize_nf(); }); } @@ -475,7 +475,6 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +499,6 @@ impl Subst for Value { &val.under_binder(x), ) }, - Normalized::clone, )) } // Retry normalizing since substituting may allow progress diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index f1045a5..2970f5f 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -381,7 +381,6 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { expr.as_ref().map_ref_with_special_handling_of_binders( |e| Thunk::new(ctx.clone(), e.clone()), |x, e| Thunk::new(ctx.skip(x), e.clone()), - |_| unreachable!(), ); normalize_one_layer(expr) diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 96ff246..e8b2544 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -376,12 +376,11 @@ fn type_with( e.as_ref().traverse_ref_with_special_handling_of_binders( |e| type_with(ctx, e.clone()), |_, _| unreachable!(), - |_| unreachable!(), )?; let ret = type_last_layer(ctx, &expr)?; match ret { RetTypeOnly(typ) => { - let expr = expr.map_ref_simple(|typed| typed.to_thunk()); + let expr = expr.map_ref(|typed| typed.to_thunk()); Typed::from_thunk_and_type( Thunk::from_partial_expr(expr), typ, diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs index e08d816..74eb993 100644 --- a/dhall_syntax/src/core/expr.rs +++ b/dhall_syntax/src/core/expr.rs @@ -245,92 +245,62 @@ impl ExprF { v.visit(self) } - pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, E2, Err>( + pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>( &'a self, visit_subexpr: impl FnMut(&'a SE) -> Result, visit_under_binder: impl FnOnce(&'a Label, &'a SE) -> Result, - visit_embed: impl FnOnce(&'a E) -> Result, - ) -> Result, Err> { + ) -> Result, Err> + where + E: Clone, + { self.visit(visitor::TraverseRefWithBindersVisitor { visit_subexpr, visit_under_binder, - visit_embed, }) } - fn traverse_ref<'a, SE2, E2, Err>( + fn traverse_ref<'a, SE2, Err>( &'a self, visit_subexpr: impl FnMut(&'a SE) -> Result, - visit_embed: impl FnOnce(&'a E) -> Result, - ) -> Result, Err> { - self.visit(visitor::TraverseRefVisitor { - visit_subexpr, - visit_embed, - }) + ) -> Result, Err> + where + E: Clone, + { + self.visit(visitor::TraverseRefVisitor { visit_subexpr }) } - pub fn map_ref_with_special_handling_of_binders<'a, SE2, E2>( + pub fn map_ref_with_special_handling_of_binders<'a, SE2>( &'a self, mut map_subexpr: impl FnMut(&'a SE) -> SE2, mut map_under_binder: impl FnMut(&'a Label, &'a SE) -> SE2, - map_embed: impl FnOnce(&'a E) -> E2, - ) -> ExprF { + ) -> ExprF + where + E: Clone, + { trivial_result(self.traverse_ref_with_special_handling_of_binders( |x| Ok(map_subexpr(x)), |l, x| Ok(map_under_binder(l, x)), - |x| Ok(map_embed(x)), )) } - pub fn map_ref<'a, SE2, E2>( + pub fn map_ref<'a, SE2>( &'a self, mut map_subexpr: impl FnMut(&'a SE) -> SE2, - map_embed: impl FnOnce(&'a E) -> E2, - ) -> ExprF { - trivial_result( - self.traverse_ref(|x| Ok(map_subexpr(x)), |x| Ok(map_embed(x))), - ) - } - - pub fn traverse_ref_simple<'a, SE2, Err>( - &'a self, - visit_subexpr: impl FnMut(&'a SE) -> Result, - ) -> Result, Err> - where - E: Clone, - { - self.traverse_ref(visit_subexpr, |x| Ok(E::clone(x))) - } - - pub fn map_ref_simple<'a, SE2>( - &'a self, - map_subexpr: impl Fn(&'a SE) -> SE2, ) -> ExprF where E: Clone, { - self.map_ref(map_subexpr, E::clone) + trivial_result(self.traverse_ref(|x| Ok(map_subexpr(x)))) } } -impl Expr { - fn traverse_embed( - &self, - visit_embed: impl FnMut(&E) -> Result, - ) -> Result, Err> { - self.visit(&mut visitor::TraverseEmbedVisitor(visit_embed)) - } - - fn map_embed(&self, mut map_embed: impl FnMut(&E) -> E2) -> Expr { - trivial_result(self.traverse_embed(|x| Ok(map_embed(x)))) - } - +impl Expr { pub fn traverse_resolve( &self, - visit_embed: impl FnMut(&E) -> Result, + visit_import: impl FnMut(&Import) -> Result, ) -> Result, Err> { self.traverse_resolve_with_visitor(&mut visitor::ResolveVisitor( - visit_embed, + visit_import, )) } @@ -339,7 +309,7 @@ impl Expr { visitor: &mut visitor::ResolveVisitor, ) -> Result, Err> where - F1: FnMut(&E) -> Result, + F1: FnMut(&Import) -> Result, { match self { ExprF::BinOp(BinOp::ImportAlt, l, r) => l @@ -371,42 +341,14 @@ impl SubExpr { pub fn rewrap(&self, x: Expr) -> SubExpr { SubExpr(Rc::new((x, (self.0).1.clone()))) } +} - pub fn traverse_embed( - &self, - visit_embed: impl FnMut(&E) -> Result, - ) -> Result, Err> { - Ok(self.rewrap(self.as_ref().traverse_embed(visit_embed)?)) - } - - pub fn map_embed( - &self, - map_embed: impl FnMut(&E) -> E2, - ) -> SubExpr { - self.rewrap(self.as_ref().map_embed(map_embed)) - } - - pub fn map_subexprs_with_special_handling_of_binders<'a>( - &'a self, - map_expr: impl FnMut(&'a Self) -> Self, - map_under_binder: impl FnMut(&'a Label, &'a Self) -> Self, - ) -> Self { - match self.as_ref() { - ExprF::Embed(_) => SubExpr::clone(self), - // This calls ExprF::map_ref - e => self.rewrap(e.map_ref_with_special_handling_of_binders( - map_expr, - map_under_binder, - |_| unreachable!(), - )), - } - } - +impl SubExpr { pub fn traverse_resolve( &self, - visit_embed: impl FnMut(&E) -> Result, + visit_import: impl FnMut(&Import) -> Result, ) -> Result, Err> { - Ok(self.rewrap(self.as_ref().traverse_resolve(visit_embed)?)) + Ok(self.rewrap(self.as_ref().traverse_resolve(visit_import)?)) } } diff --git a/dhall_syntax/src/core/visitor.rs b/dhall_syntax/src/core/visitor.rs index e39e95b..647f76f 100644 --- a/dhall_syntax/src/core/visitor.rs +++ b/dhall_syntax/src/core/visitor.rs @@ -278,21 +278,18 @@ where } } -pub struct TraverseRefWithBindersVisitor { +pub struct TraverseRefWithBindersVisitor { pub visit_subexpr: F1, pub visit_under_binder: F2, - pub visit_embed: F4, } -impl<'a, SE, E, SE2, E2, Err, F1, F2, F4> - ExprFFallibleVisitor<'a, SE, SE2, E, E2> - for TraverseRefWithBindersVisitor +impl<'a, SE, E, SE2, Err, F1, F2> ExprFFallibleVisitor<'a, SE, SE2, E, E> + for TraverseRefWithBindersVisitor where SE: 'a, - E: 'a, + E: 'a + Clone, F1: FnMut(&'a SE) -> Result, F2: FnOnce(&'a Label, &'a SE) -> Result, - F4: FnOnce(&'a E) -> Result, { type Error = Err; @@ -306,68 +303,45 @@ where ) -> Result { (self.visit_under_binder)(label, subexpr) } - fn visit_embed(self, embed: &'a E) -> Result { - (self.visit_embed)(embed) + fn visit_embed(self, embed: &'a E) -> Result { + Ok(embed.clone()) } } -pub struct TraverseRefVisitor { +pub struct TraverseRefVisitor { pub visit_subexpr: F1, - pub visit_embed: F3, } -impl<'a, SE, E, SE2, E2, Err, F1, F3> ExprFFallibleVisitor<'a, SE, SE2, E, E2> - for TraverseRefVisitor +impl<'a, SE, E, SE2, Err, F1> ExprFFallibleVisitor<'a, SE, SE2, E, E> + for TraverseRefVisitor where SE: 'a, - E: 'a, + E: 'a + Clone, F1: FnMut(&'a SE) -> Result, - F3: FnOnce(&'a E) -> Result, { type Error = Err; fn visit_subexpr(&mut self, subexpr: &'a SE) -> Result { (self.visit_subexpr)(subexpr) } - fn visit_embed(self, embed: &'a E) -> Result { - (self.visit_embed)(embed) - } -} - -pub struct TraverseEmbedVisitor(pub F1); - -impl<'a, 'b, E, E2, Err, F1> - ExprFFallibleVisitor<'a, SubExpr, SubExpr, E, E2> - for &'b mut TraverseEmbedVisitor -where - F1: FnMut(&E) -> Result, -{ - type Error = Err; - - fn visit_subexpr( - &mut self, - subexpr: &'a SubExpr, - ) -> Result, Self::Error> { - Ok(subexpr.rewrap(subexpr.as_ref().visit(&mut **self)?)) - } - fn visit_embed(self, embed: &'a E) -> Result { - (self.0)(embed) + fn visit_embed(self, embed: &'a E) -> Result { + Ok(embed.clone()) } } pub struct ResolveVisitor(pub F1); -impl<'a, 'b, E, E2, Err, F1> - ExprFFallibleVisitor<'a, SubExpr, SubExpr, E, E2> +impl<'a, 'b, E2, Err, F1> + ExprFFallibleVisitor<'a, SubExpr, SubExpr, Import, E2> for &'b mut ResolveVisitor where - F1: FnMut(&E) -> Result, + F1: FnMut(&Import) -> Result, { type Error = Err; fn visit_subexpr( &mut self, - subexpr: &'a SubExpr, + subexpr: &'a SubExpr, ) -> Result, Self::Error> { Ok(subexpr.rewrap( subexpr @@ -375,7 +349,7 @@ where .traverse_resolve_with_visitor(&mut **self)?, )) } - fn visit_embed(self, embed: &'a E) -> Result { + fn visit_embed(self, embed: &'a Import) -> Result { (self.0)(embed) } } diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs index 25d4ca8..48e56be 100644 --- a/dhall_syntax/src/printer.rs +++ b/dhall_syntax/src/printer.rs @@ -156,7 +156,7 @@ impl Expr { }; // Annotate subexpressions with the appropriate phase, defaulting to Base - let phased_self = match self.map_ref_simple(|e| PhasedExpr(e, Base)) { + let phased_self = match self.map_ref(|e| PhasedExpr(e, Base)) { Pi(a, b, c) => { if &String::from(&a) == "_" { Pi(a, b.phase(Operator), c) -- cgit v1.2.3