From b0013503e06da01bec78b2957aeffc5115c5f53d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 19 Apr 2019 00:31:42 +0200 Subject: Start separating normalized values from syntactic expressions --- dhall/src/lib.rs | 1 + dhall/src/normalize.rs | 299 +++++++++++++++++++++++++++++-------------------- 2 files changed, 179 insertions(+), 121 deletions(-) (limited to 'dhall') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 544df6e..c85b962 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -3,6 +3,7 @@ #![feature(slice_patterns)] #![feature(label_break_value)] #![feature(non_exhaustive)] +#![feature(bind_by_move_pattern_guards)] #![cfg_attr(test, feature(custom_inner_attributes))] #![allow( clippy::type_complexity, diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 7a9ca2f..90c6841 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -216,6 +216,39 @@ where Continue(ExprF::App(ret, rest)) } +#[derive(Debug, Clone, PartialEq, Eq)] +enum Value { + Expr(SubExpr), + Lam( + Label, + SubExpr>, + SubExpr>, + ), + // App( + // SubExpr>, + // Vec>>, + // ), +} + +impl Value { + fn into_expr(self, ctx: &NormalizationContext) -> SubExpr { + match self { + Value::Expr(e) => e, + Value::Lam(x, t, e) => rc(ExprF::Lam( + x.clone(), + normalize_value(ctx, t).into_expr(ctx), + normalize_value(&ctx.skip(&x), e).into_expr(&ctx.skip(&x)), + )), + // Value::App(f, args) => rc(ExprF::App( + // normalize_value(ctx, f).into_expr(ctx), + // args.into_iter() + // .map(|e| normalize_value(ctx, e).into_expr(ctx)) + // .collect(), + // )), + } + } +} + #[derive(Debug, Clone)] enum EnvItem { Expr(SubExpr), @@ -268,138 +301,161 @@ enum WhatNext<'a, N, E> { DoneAsIs, } +fn reval(expr: SubExpr) -> Value { + match expr.as_ref() { + ExprF::Lam(x, t, e) => { + Value::Lam(x.clone(), t.embed_absurd(), e.embed_absurd()) + } + _ => Value::Expr(expr), + } +} + fn normalize_value( ctx: &NormalizationContext, expr: SubExpr>, -) -> SubExpr { +) -> Value { use dhall_core::BinOp::*; use dhall_core::ExprF::*; - match expr.as_ref() { + let e = match expr.as_ref() { Let(x, _, r, b) => { - let r = normalize_value(ctx, r.clone()); - normalize_value(&ctx.insert(x, r.clone()), b.clone()) - } - e => { - // Recursively normalize all subexpressions - let expr: ExprF, Label, X, Normalized<'static>> = e - .map_ref_with_special_handling_of_binders( - |e| normalize_value(ctx, e.clone()).unroll(), - |x, e| normalize_value(&ctx.skip(x), e.clone()).unroll(), - X::clone, - Normalized::clone, - Label::clone, - ); + let r = normalize_value(ctx, r.clone()).into_expr(ctx); + return normalize_value(&ctx.insert(x, r.clone()), b.clone()); + } + Lam(x, t, e) => return Value::Lam(x.clone(), t.clone(), e.clone()), + e => e, + }; - use WhatNext::*; - let what_next = match &expr { - Let(_, _, _, _) => unreachable!(), - Embed(e) => DoneRefSub(&e.0), - Var(v) => DoneSub(ctx.lookup(v)), - 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())) - } - Merge(RecordLit(handlers), UnionLit(l, v, _), _) => { - match handlers.get(&l) { - Some(h) => Continue(App(h.clone(), vec![v.clone()])), - None => DoneAsIs, - } - } - Merge(RecordLit(handlers), UnionConstructor(l, _), _) => { - match handlers.get(&l) { - Some(h) => DoneRefSub(h), - None => DoneAsIs, - } - } - Field(RecordLit(kvs), l) => match kvs.get(&l) { - Some(r) => DoneRefSub(r), - None => DoneAsIs, - }, - Field(UnionType(kts), l) => { - Done(UnionConstructor(l.clone(), kts.clone())) - } - Projection(_, ls) if ls.is_empty() => { - Done(RecordLit(std::collections::BTreeMap::new())) - } - Projection(RecordLit(kvs), ls) => Done(RecordLit( - ls.iter() - .filter_map(|l| { - kvs.get(l).map(|x| (l.clone(), x.clone())) - }) - .collect(), - )), - _ => DoneAsIs, - }; + // Recursively normalize all subexpressions + let expr: ExprF> = e + .map_ref_with_special_handling_of_binders( + |e| normalize_value(ctx, e.clone()), + |x, e| normalize_value(&ctx.skip(x), e.clone()), + X::clone, + Normalized::clone, + Label::clone, + ); - match what_next { - Continue(e) => normalize_value(ctx, e.embed_absurd().roll()), - Done(e) => e.roll(), - DoneRef(e) => e.roll(), - DoneSub(e) => e, - DoneRefSub(e) => e.clone(), - DoneAsIs => rc(expr.map_ref_simple(ExprF::roll).map_ref( - SubExpr::clone, - X::clone, - |_| unreachable!(), - Label::clone, - )), + let expr = match expr { + App(v, args) if args.is_empty() => return v, + App(Value::Lam(x, _, b), args) => { + let mut iter = args.into_iter(); + // We know args is nonempty + let a = iter.next().unwrap(); + // Beta reduce + let ctx2 = ctx.insert(&x, a.into_expr(ctx)); + let b2 = normalize_value(&ctx2, b).into_expr(&ctx2); + return normalize_value( + ctx, + App(b2, iter.map(|val| val.into_expr(ctx)).collect()) + .embed_absurd() + .roll(), + ); + } + expr => expr, + }; + + let expr: ExprF, Label, X, Normalized<'static>> = expr + .map_ref_with_special_handling_of_binders( + |e| e.clone().into_expr(ctx).unroll(), + |x, e| e.clone().into_expr(&ctx.skip(x)).unroll(), + X::clone, + Normalized::clone, + Label::clone, + ); + + use WhatNext::*; + let what_next = match &expr { + Embed(e) => DoneRefSub(&e.0), + Var(v) => DoneSub(ctx.lookup(v)), + Annot(x, _) => DoneRef(x), + Note(_, e) => DoneRef(e), + App(_, args) if args.is_empty() => unreachable!(), + Let(_, _, _, _) => unreachable!(), + Lam(_, _, _) => unreachable!(), + 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(_, _, _), _) => unreachable!(), + 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())) + } + Merge(RecordLit(handlers), UnionLit(l, v, _), _) => { + match handlers.get(&l) { + Some(h) => Continue(App(h.clone(), vec![v.clone()])), + None => DoneAsIs, + } + } + Merge(RecordLit(handlers), UnionConstructor(l, _), _) => { + match handlers.get(&l) { + Some(h) => DoneRefSub(h), + None => DoneAsIs, } } + Field(RecordLit(kvs), l) => match kvs.get(&l) { + Some(r) => DoneRefSub(r), + None => DoneAsIs, + }, + Field(UnionType(kts), l) => { + Done(UnionConstructor(l.clone(), kts.clone())) + } + Projection(_, ls) if ls.is_empty() => { + Done(RecordLit(std::collections::BTreeMap::new())) + } + Projection(RecordLit(kvs), ls) => Done(RecordLit( + ls.iter() + .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) + .collect(), + )), + _ => DoneAsIs, + }; + + match what_next { + Continue(e) => normalize_value(ctx, e.embed_absurd().roll()), + Done(e) => reval(e.roll()), + DoneRef(e) => reval(e.roll()), + DoneSub(e) => reval(e), + DoneRefSub(e) => reval(e.clone()), + DoneAsIs => reval(rc(expr.map_ref_simple(ExprF::roll).map_ref( + SubExpr::clone, + X::clone, + |_| unreachable!(), + Label::clone, + ))), } } @@ -414,6 +470,7 @@ fn normalize_value( /// fn normalize(e: SubExpr>) -> SubExpr { normalize_value(&NormalizationContext::new(), e) + .into_expr(&NormalizationContext::new()) } #[cfg(test)] -- cgit v1.2.3