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') 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