From f4a50a5da10eb2de1d7cf00ad6f6765605da366d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 18 Apr 2019 17:29:17 +0200 Subject: Make normalize manipulate SubExprs more directly --- dhall/src/normalize.rs | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'dhall/src/normalize.rs') diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 1561f01..80c2e9a 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -150,7 +150,7 @@ where ), // // fold/build fusion // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { - // normalize_ref(&App(bx(x.clone()), rest.to_vec())) + // normalize_value(&App(bx(x.clone()), rest.to_vec())) // } (OptionalFold, [_, NEOptionalLit(x), _, just, _, rest..]) => { let x = x.clone(); @@ -162,7 +162,7 @@ where } // // fold/build fusion // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { - // normalize_ref(&App(bx(x.clone()), rest.to_vec())) + // normalize_value(&App(bx(x.clone()), rest.to_vec())) // } (NaturalBuild, [g, rest..]) => { 'ret: { @@ -226,12 +226,12 @@ enum WhatNext<'a, N, E> { DoneAsIs, } -fn normalize_ref(expr: &Expr>) -> Expr { +fn normalize_value(expr: SubExpr>) -> SubExpr { use dhall_core::BinOp::*; use dhall_core::ExprF::*; // Recursively normalize all subexpressions let expr: ExprF, Label, X, Normalized<'static>> = - expr.map_ref_simple(|e| normalize_ref(e.as_ref())); + expr.as_ref().map_ref_simple(|e| normalize_value(e.clone()).unroll()); use WhatNext::*; // TODO: match by move @@ -325,17 +325,17 @@ fn normalize_ref(expr: &Expr>) -> Expr { }; match what_next { - Continue(e) => normalize_ref(&e.embed_absurd()), - ContinueSub(e) => normalize_ref(e.embed_absurd().as_ref()), - Done(e) => e, - DoneRef(e) => e.clone(), - DoneRefSub(e) => e.unroll(), - DoneAsIs => expr.map_ref_simple(ExprF::roll).map_ref( + Continue(e) => normalize_value(e.embed_absurd().roll()), + ContinueSub(e) => normalize_value(e.embed_absurd()), + Done(e) => e.roll(), + DoneRef(e) => e.roll(), + DoneRefSub(e) => e.clone(), + DoneAsIs => rc(expr.map_ref_simple(ExprF::roll).map_ref( SubExpr::clone, X::clone, |_| unreachable!(), Label::clone, - ), + )), } } @@ -349,7 +349,7 @@ fn normalize_ref(expr: &Expr>) -> Expr { /// leave ill-typed sub-expressions unevaluated. /// fn normalize(e: SubExpr>) -> SubExpr { - normalize_ref(e.as_ref()).roll() + normalize_value(e) } #[cfg(test)] -- cgit v1.2.3 From 486a26eb7cea0c99818fde2c3fd933f7aca40b52 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 18 Apr 2019 22:08:25 +0200 Subject: Use a context for substitution in normalization --- dhall/src/normalize.rs | 286 ++++++++++++++++++++++++++++++------------------- 1 file changed, 177 insertions(+), 109 deletions(-) (limited to 'dhall/src/normalize.rs') diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 80c2e9a..4dc5156 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -1,8 +1,11 @@ #![allow(non_snake_case)] -use crate::expr::*; +use std::fmt; + +use dhall_core::context::Context; use dhall_core::*; use dhall_generator as dhall; -use std::fmt; + +use crate::expr::*; impl<'a> Typed<'a> { pub fn normalize(self) -> Normalized<'a> { @@ -97,7 +100,7 @@ where } }; let a0 = a0.roll(); - let a1 = shift(1, &V("x".into(), 0), &a0); + let a1 = shift0(1, &"x".into(), &a0); let g = g.roll(); break 'ret ( dhall::subexpr!( @@ -217,125 +220,190 @@ where enum WhatNext<'a, N, E> { // Recurse on this expression Continue(Expr), - ContinueSub(SubExpr), // The following expression is the normal form Done(Expr), DoneRef(&'a Expr), + DoneSub(SubExpr), DoneRefSub(&'a SubExpr), // The current expression is already in normal form DoneAsIs, } -fn normalize_value(expr: SubExpr>) -> SubExpr { - use dhall_core::BinOp::*; - use dhall_core::ExprF::*; - // Recursively normalize all subexpressions - let expr: ExprF, Label, X, Normalized<'static>> = - expr.as_ref().map_ref_simple(|e| normalize_value(e.clone()).unroll()); +#[derive(Debug, Clone)] +enum EnvItem { + Expr(SubExpr), + Skip(Label, usize), +} - use WhatNext::*; - // TODO: match by move - let what_next = match &expr { - Let(f, _, r, b) => { - let vf0 = &V(f.clone(), 0); - // TODO: use a context - ContinueSub(subst_shift(vf0, &r.roll(), &b.roll())) +impl EnvItem { + fn shift0(&self, delta: isize, label: &Label) -> Self { + use EnvItem::*; + match self { + Expr(e) => Expr(shift0(delta, label, e)), + Skip(l, n) if l == label => Skip(l.clone(), *n + 1), + Skip(l, n) => Skip(l.clone(), *n), } - Annot(x, _) => DoneRef(x), - Note(_, e) => DoneRef(e), - App(f, args) if args.is_empty() => DoneRef(f), - App(App(f, args1), args2) => Continue(App( - f.clone(), - args1 - .iter() - .cloned() - .chain(args2.iter().map(ExprF::roll)) - .collect(), - )), - App(Builtin(b), args) => apply_builtin(*b, args), - App(Lam(x, _, b), args) => { - let mut iter = args.iter(); - // We know args is nonempty - let a = iter.next().unwrap(); - // Beta reduce - let vx0 = &V(x.clone(), 0); - let b2 = subst_shift(vx0, &a.roll(), &b); - Continue(App(b2, iter.map(ExprF::roll).collect())) - } - App(UnionConstructor(l, kts), args) => { - let mut iter = args.iter(); - // We know args is nonempty - let a = iter.next().unwrap(); - let e = rc(UnionLit(l.clone(), rc(a.clone()), kts.clone())); - Continue(App(e, iter.map(ExprF::roll).collect())) - } - BoolIf(BoolLit(true), t, _) => DoneRef(t), - BoolIf(BoolLit(false), _, f) => DoneRef(f), - // TODO: interpolation - // TextLit(t) => - OldOptionalLit(None, t) => Done(EmptyOptionalLit(t.roll())), - OldOptionalLit(Some(x), _) => Done(NEOptionalLit(x.roll())), - BinOp(BoolAnd, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x && *y)), - BinOp(BoolOr, BoolLit(x), BoolLit(y)) => Done(BoolLit(*x || *y)), - BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => Done(BoolLit(x == y)), - BinOp(BoolNE, BoolLit(x), BoolLit(y)) => Done(BoolLit(x != y)), - BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Done(NaturalLit(x + y)) - } - BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Done(NaturalLit(x * y)) - } - BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)), - BinOp(ListAppend, EmptyListLit(_), y) => DoneRef(y), - BinOp(ListAppend, x, EmptyListLit(_)) => DoneRef(x), - BinOp(ListAppend, NEListLit(xs), NEListLit(ys)) => { - let xs = xs.iter().cloned(); - let ys = ys.iter().cloned(); - Done(NEListLit(xs.chain(ys).collect())) + } +} + +struct NormalizationContext(Context); + +impl NormalizationContext { + fn new() -> NormalizationContext { + NormalizationContext(Context::new()) + } + fn insert(&self, x: &Label, e: SubExpr) -> NormalizationContext { + NormalizationContext(self.0.insert(x.clone(), EnvItem::Expr(e))) + } + fn skip(&self, x: &Label) -> NormalizationContext { + NormalizationContext( + self.0 + .map(|e| e.shift0(1, x)) + .insert(x.clone(), EnvItem::Skip(x.clone(), 0)), + ) + } + fn lookup(&self, var: &V