diff options
| -rw-r--r-- | dhall/src/normalize.rs | 180 |
1 files changed, 69 insertions, 111 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index d02dd80..e88cc7b 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -1,6 +1,5 @@ #![allow(non_snake_case)] use std::collections::BTreeMap; -use std::fmt; use dhall_core::context::Context; use dhall_core::*; @@ -26,59 +25,40 @@ impl<'a> Typed<'a> { } } -fn apply_builtin<N, E>(b: Builtin, args: &[Expr<N, E>]) -> WhatNext<N, E> -where - N: fmt::Debug + Clone, - E: fmt::Debug + Clone, -{ +fn apply_builtin(b: Builtin, args: &[WHNF]) -> WhatNext<X, X> { + let args: Vec<_> = args + .iter() + .map(|val| val.clone().normalize_to_expr().unroll()) + .collect(); use dhall_core::Builtin::*; use dhall_core::ExprF::*; use WhatNext::*; - let (ret, rest) = match (b, args) { - (OptionalNone, [t, rest..]) => (rc(EmptyOptionalLit(t.roll())), rest), - (NaturalIsZero, [NaturalLit(n), rest..]) => { - (rc(BoolLit(*n == 0)), rest) + let ret = match (b, args.as_slice()) { + (OptionalNone, [t]) => rc(EmptyOptionalLit(t.roll())), + (NaturalIsZero, [NaturalLit(n)]) => rc(BoolLit(*n == 0)), + (NaturalEven, [NaturalLit(n)]) => rc(BoolLit(*n % 2 == 0)), + (NaturalOdd, [NaturalLit(n)]) => rc(BoolLit(*n % 2 != 0)), + (NaturalToInteger, [NaturalLit(n)]) => rc(IntegerLit(*n as isize)), + (NaturalShow, [NaturalLit(n)]) => rc(TextLit(n.to_string().into())), + (ListLength, [_, EmptyListLit(_)]) => rc(NaturalLit(0)), + (ListLength, [_, NEListLit(ys)]) => rc(NaturalLit(ys.len())), + (ListHead, [_, EmptyListLit(t)]) => rc(EmptyOptionalLit(t.clone())), + (ListHead, [_, NEListLit(ys)]) => { + rc(NEOptionalLit(ys.first().unwrap().clone())) } - (NaturalEven, [NaturalLit(n), rest..]) => { - (rc(BoolLit(*n % 2 == 0)), rest) + (ListLast, [_, EmptyListLit(t)]) => rc(EmptyOptionalLit(t.clone())), + (ListLast, [_, NEListLit(ys)]) => { + rc(NEOptionalLit(ys.last().unwrap().clone())) } - (NaturalOdd, [NaturalLit(n), rest..]) => { - (rc(BoolLit(*n % 2 != 0)), rest) - } - (NaturalToInteger, [NaturalLit(n), rest..]) => { - (rc(IntegerLit(*n as isize)), rest) - } - (NaturalShow, [NaturalLit(n), rest..]) => { - (rc(TextLit(n.to_string().into())), rest) - } - (ListLength, [_, EmptyListLit(_), rest..]) => (rc(NaturalLit(0)), rest), - (ListLength, [_, NEListLit(ys), rest..]) => { - (rc(NaturalLit(ys.len())), rest) - } - (ListHead, [_, EmptyListLit(t), rest..]) => { - (rc(EmptyOptionalLit(t.clone())), rest) - } - (ListHead, [_, NEListLit(ys), rest..]) => { - (rc(NEOptionalLit(ys.first().unwrap().clone())), rest) - } - (ListLast, [_, EmptyListLit(t), rest..]) => { - (rc(EmptyOptionalLit(t.clone())), rest) - } - (ListLast, [_, NEListLit(ys), rest..]) => { - (rc(NEOptionalLit(ys.last().unwrap().clone())), rest) - } - (ListReverse, [_, EmptyListLit(t), rest..]) => { - (rc(EmptyListLit(t.clone())), rest) - } - (ListReverse, [_, NEListLit(ys), rest..]) => { + (ListReverse, [_, EmptyListLit(t)]) => rc(EmptyListLit(t.clone())), + (ListReverse, [_, NEListLit(ys)]) => { let ys = ys.iter().rev().cloned().collect(); - (rc(NEListLit(ys)), rest) + rc(NEListLit(ys)) } - (ListIndexed, [_, EmptyListLit(t), rest..]) => ( - dhall::subexpr!([] : List ({ index : Natural, value : t })), - rest, - ), - (ListIndexed, [_, NEListLit(xs), rest..]) => { + (ListIndexed, [_, EmptyListLit(t)]) => { + dhall::subexpr!([] : List ({ index : Natural, value : t })) + } + (ListIndexed, [_, NEListLit(xs)]) => { let xs = xs .iter() .cloned() @@ -88,9 +68,9 @@ where dhall::subexpr!({ index = i, value = e }) }) .collect(); - (rc(NEListLit(xs)), rest) + rc(NEListLit(xs)) } - (ListBuild, [a0, g, rest..]) => { + (ListBuild, [a0, g]) => { 'ret: { // if let App(f2, args2) = g { // if let (Builtin(ListFold), [_, x, rest_inner..]) = @@ -106,18 +86,15 @@ where let a0 = a0.roll(); let a1 = shift0(1, &"x".into(), &a0); let g = g.roll(); - break 'ret ( - dhall::subexpr!( - g - (List a0) - (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs) - ([] : List a0) - ), - rest, + break 'ret dhall::subexpr!( + g + (List a0) + (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs) + ([] : List a0) ); } } - (OptionalBuild, [a0, g, rest..]) => { + (OptionalBuild, [a0, g]) => { 'ret: { // if let App(f2, args2) = g { // if let (Builtin(OptionalFold), [_, x, rest_inner..]) = @@ -132,75 +109,64 @@ where // }; let a0 = a0.roll(); let g = g.roll(); - break 'ret ( - dhall::subexpr!( - g - (Optional a0) - (λ(x: a0) -> Some x) - (None a0) - ), - rest, + break 'ret dhall::subexpr!( + g + (Optional a0) + (λ(x: a0) -> Some x) + (None a0) ); } } - (ListFold, [_, EmptyListLit(_), _, _, nil, rest..]) => { - (nil.roll(), rest) - } - (ListFold, [_, NEListLit(xs), _, cons, nil, rest..]) => ( + (ListFold, [_, EmptyListLit(_), _, _, nil]) => nil.roll(), + (ListFold, [_, NEListLit(xs), _, cons, nil]) => { xs.iter().rev().fold(nil.roll(), |acc, x| { let x = x.clone(); let acc = acc.clone(); let cons = cons.roll(); dhall::subexpr!(cons x acc) - }), - rest, - ), + }) + } // // fold/build fusion // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) // } - (OptionalFold, [_, NEOptionalLit(x), _, just, _, rest..]) => { + (OptionalFold, [_, NEOptionalLit(x), _, just, _]) => { let x = x.clone(); let just = just.roll(); - (dhall::subexpr!(just x), rest) + dhall::subexpr!(just x) } - (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing, rest..]) => { - (nothing.roll(), rest) + (OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing]) => { + nothing.roll() } // // fold/build fusion // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) // } - (NaturalBuild, [g, rest..]) => { - 'ret: { - // if let App(f2, args2) = g { - // if let (Builtin(NaturalFold), [x, rest_inner..]) = - // (f2.as_ref(), args2.as_slice()) - // { - // // fold/build fusion - // break 'ret ( - // rc(App(x.clone(), rest_inner.to_vec())), - // rest, - // ); - // } - // }; - let g = g.roll(); - break 'ret ( - dhall::subexpr!(g Natural (λ(x : Natural) -> x + 1) 0), - rest, - ); - } - } - (NaturalFold, [NaturalLit(0), _, _, zero, rest..]) => { - (zero.roll(), rest) + (NaturalBuild, [g]) => { + // 'ret: { + // if let App(f2, args2) = g { + // if let (Builtin(NaturalFold), [x, rest_inner..]) = + // (f2.as_ref(), args2.as_slice()) + // { + // // fold/build fusion + // break 'ret ( + // rc(App(x.clone(), rest_inner.to_vec())), + // rest, + // ); + // } + // }; + // } + let g = g.roll(); + dhall::subexpr!(g Natural (λ(x : Natural) -> x + 1) 0) } - (NaturalFold, [NaturalLit(n), t, succ, zero, rest..]) => { + (NaturalFold, [NaturalLit(0), _, _, zero]) => zero.roll(), + (NaturalFold, [NaturalLit(n), t, succ, zero]) => { let fold = rc(Builtin(NaturalFold)); let n = rc(NaturalLit(n - 1)); let t = t.roll(); let succ = succ.roll(); let zero = zero.roll(); - (dhall::subexpr!(succ (fold n t succ zero)), rest) + dhall::subexpr!(succ (fold n t succ zero)) } // (NaturalFold, Some(App(f2, args2)), _) => { // match (f2.as_ref(), args2.as_slice()) { @@ -213,11 +179,7 @@ where // } _ => return DoneAsIs, }; - // Put the remaining arguments back and eval again. In most cases - // ret will not be of a form that can be applied, so this won't go very deep. - // In lots of cases, there are no remaining args so this cann will just return ret. - let rest = rest.iter().map(ExprF::roll); - Continue(rest.fold(ret, |acc, e| rc(ExprF::App(acc, e))).unroll()) + Continue(ret.unroll()) } // #[derive(Debug, Clone)] @@ -403,11 +365,7 @@ impl Closure { } Closure::AppliedBuiltin(ctx, b, mut args) => { args.push(val); - let args_unrolled: Vec<_> = args - .iter() - .map(|val| val.clone().normalize_to_expr().unroll()) - .collect(); - match apply_builtin(b, &args_unrolled).into_value(&ctx) { + match apply_builtin(b, &args).into_value(&ctx) { Some(v) => v, None => { WHNF::Closure(Closure::AppliedBuiltin(ctx, b, args)) |