summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-20 19:30:01 +0200
committerNadrieril2019-04-20 19:30:47 +0200
commit375b27634ece7410d17fd46e0232caca696f8f74 (patch)
tree2275931019c98d4b4e211bf45cbebf77e873ba3f
parentcad6a315a224f4a5d63d0f49e11285304f18569c (diff)
Avoid a lot of slow Expr costruction
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs125
1 files changed, 52 insertions, 73 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 192a669..cd32e66 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -98,66 +98,49 @@ fn apply_builtin(
{
args.get(1).unwrap().clone()
}
- (ListBuild, [a0, g]) => {
- // TODO: avoid passing through Exprs
- let a0 = whnf_to_expr(a0);
- let a1 = shift0(1, &"x".into(), &a0);
- let g = whnf_to_expr(g);
- normalize_whnf(
- ctx,
- dhall::subexpr!(
- g
- (List a0)
- (λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
- ([] : List a0)
- ),
- )
- }
+ // TODO: avoid passing through Exprs
+ (ListBuild, [a0, g]) => g
+ .clone()
+ .app(AppliedBuiltin(ctx.clone(), List, vec![]).app(a0.clone()))
+ .app(normalize_whnf(ctx, {
+ let a0 = whnf_to_expr(a0);
+ let a1 = shift0(1, &"x".into(), &a0);
+ dhall::subexpr!(λ(x : a0) -> λ(xs : List a1) -> [ x ] # xs)
+ }))
+ .app(EmptyListLit(Now::from_whnf(a0.clone()))),
(ListFold, [_, EmptyListLit(_), _, _, nil]) => nil.clone(),
(ListFold, [_, NEListLit(xs), _, cons, nil]) => {
- // TODO: avoid passing through Exprs
- let nil = whnf_to_expr(nil);
- let cons = whnf_to_expr(cons);
- normalize_whnf(
- ctx,
- xs.iter().rev().fold(nil, |acc, x| {
- let x = now_to_expr(x);
- let acc = acc.clone();
- dhall::subexpr!(cons x acc)
- }),
- )
+ let mut v = nil.clone();
+ for x in xs.iter().rev() {
+ v = cons.clone().app(x.clone().normalize()).app(v);
+ }
+ v
}
// fold/build fusion
- (
- OptionalBuild,
- [_, WHNF::AppliedBuiltin(_, OptionalFold, args)],
- ) if args.len() == 2 => args.get(1).unwrap().clone(),
- (
- OptionalFold,
- [_, WHNF::AppliedBuiltin(_, OptionalBuild, args)],
- ) if args.len() == 2 => args.get(1).unwrap().clone(),
- (OptionalBuild, [a0, g]) => {
- // TODO: avoid passing through Exprs
- let a0 = whnf_to_expr(a0);
- let g = whnf_to_expr(g);
- normalize_whnf(
- ctx,
- dhall::subexpr!(
- g
- (Optional a0)
- (λ(x: a0) -> Some x)
- (None a0)
- ),
- )
+ (OptionalBuild, [_, WHNF::AppliedBuiltin(_, OptionalFold, args)])
+ if args.len() == 2 =>
+ {
+ args.get(1).unwrap().clone()
}
+ (OptionalFold, [_, WHNF::AppliedBuiltin(_, OptionalBuild, args)])
+ if args.len() == 2 =>
+ {
+ args.get(1).unwrap().clone()
+ }
+ // TODO: avoid passing through Exprs
+ (OptionalBuild, [a0, g]) => g
+ .clone()
+ .app(AppliedBuiltin(ctx.clone(), Optional, vec![]).app(a0.clone()))
+ .app(normalize_whnf(ctx, {
+ let a0 = whnf_to_expr(a0);
+ dhall::subexpr!(λ(x: a0) -> Some x)
+ }))
+ .app(EmptyOptionalLit(Now::from_whnf(a0.clone()))),
(OptionalFold, [_, EmptyOptionalLit(_), _, _, nothing]) => {
nothing.clone()
}
(OptionalFold, [_, NEOptionalLit(x), _, just, _]) => {
- // TODO: avoid passing through Exprs
- let just = whnf_to_expr(just);
- let x = now_to_expr(x);
- normalize_whnf(ctx, dhall::subexpr!(just x))
+ just.clone().app(x.clone().normalize())
}
// fold/build fusion
(NaturalBuild, [WHNF::AppliedBuiltin(_, NaturalFold, args)])
@@ -170,23 +153,23 @@ fn apply_builtin(
{
args.get(0).unwrap().clone()
}
- (NaturalBuild, [g]) => {
- // TODO: avoid passing through Exprs
- let g = whnf_to_expr(g);
- normalize_whnf(
+ // TODO: avoid passing through Exprs
+ (NaturalBuild, [g]) => g
+ .clone()
+ .app(AppliedBuiltin(ctx.clone(), Natural, vec![]))
+ .app(normalize_whnf(
ctx,
- dhall::subexpr!(g Natural (λ(x : Natural) -> x + 1) 0),
- )
- }
+ dhall::subexpr!((λ(x : Natural) -> x + 1)),
+ ))
+ .app(NaturalLit(0)),
(NaturalFold, [NaturalLit(0), _, _, zero]) => zero.clone(),
(NaturalFold, [NaturalLit(n), t, succ, zero]) => {
- // TODO: avoid passing through Exprs
- let t = whnf_to_expr(t);
- let succ = whnf_to_expr(succ);
- let zero = whnf_to_expr(zero);
- let fold = rc(ExprF::Builtin(NaturalFold));
- let n = rc(ExprF::NaturalLit(n - 1));
- normalize_whnf(ctx, dhall::subexpr!(succ (fold n t succ zero)))
+ let fold = AppliedBuiltin(ctx, NaturalFold, vec![])
+ .app(NaturalLit(n - 1))
+ .app(t.clone())
+ .app(succ.clone())
+ .app(zero.clone());
+ succ.clone().app(fold)
}
_ => return None,
};
@@ -290,15 +273,11 @@ impl WHNF {
))
}
WHNF::AppliedBuiltin(_ctx, b, args) => {
- if args.is_empty() {
- rc(ExprF::Builtin(b))
- } else {
- args.into_iter()
- .map(|e| e.normalize_to_expr())
- .fold(rc(ExprF::Builtin(b)), |acc, e| {
- rc(ExprF::App(acc, e))
- })
+ let mut e = WHNF::Expr(rc(ExprF::Builtin(b)));
+ for v in args {
+ e = e.app(v);
}
+ e.normalize_to_expr()
}
WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),