From 759705047eea74f538883c15b6abd3292bbebb13 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 19 Apr 2019 12:37:47 +0200 Subject: A partially applied builtin is a value --- dhall/src/normalize.rs | 69 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 42 insertions(+), 27 deletions(-) (limited to 'dhall') diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 90c6841..c053ca2 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -224,10 +224,7 @@ enum Value { SubExpr>, SubExpr>, ), - // App( - // SubExpr>, - // Vec>>, - // ), + AppliedBuiltin(Builtin, Vec), } impl Value { @@ -239,12 +236,14 @@ impl Value { 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(), - // )), + Value::AppliedBuiltin(b, args) if args.is_empty() => { + rc(ExprF::Builtin(b)) + } + Value::AppliedBuiltin(b, args) => { + let args_rolled: Vec<_> = + args.iter().map(|val| val.clone().into_expr(ctx)).collect(); + rc(ExprF::App(rc(ExprF::Builtin(b)), args_rolled)) + } } } } @@ -301,11 +300,26 @@ enum WhatNext<'a, N, E> { DoneAsIs, } +impl<'a> WhatNext<'a, X, X> { + fn into_value(self, ctx: &NormalizationContext) -> Option { + use WhatNext::*; + match self { + Continue(e) => Some(normalize_value(ctx, e.embed_absurd().roll())), + Done(e) => Some(reval(e.roll())), + DoneRef(e) => Some(reval(e.roll())), + DoneSub(e) => Some(reval(e)), + DoneRefSub(e) => Some(reval(e.clone())), + DoneAsIs => None, + } + } +} + fn reval(expr: SubExpr) -> Value { match expr.as_ref() { ExprF::Lam(x, t, e) => { Value::Lam(x.clone(), t.embed_absurd(), e.embed_absurd()) } + ExprF::Builtin(b) => Value::AppliedBuiltin(*b, vec![]), _ => Value::Expr(expr), } } @@ -323,6 +337,7 @@ fn normalize_value( return normalize_value(&ctx.insert(x, r.clone()), b.clone()); } Lam(x, t, e) => return Value::Lam(x.clone(), t.clone(), e.clone()), + ExprF::Builtin(b) => return Value::AppliedBuiltin(*b, vec![]), e => e, }; @@ -352,6 +367,18 @@ fn normalize_value( .roll(), ); } + App(Value::AppliedBuiltin(b, args1), args2) => { + let combined_args: Vec<_> = + args1.into_iter().chain(args2.into_iter()).collect(); + let args_unrolled: Vec<_> = combined_args + .iter() + .map(|val| val.clone().into_expr(ctx).unroll()) + .collect(); + match apply_builtin(b, &args_unrolled).into_value(ctx) { + Some(v) => return v, + None => return Value::AppliedBuiltin(b, combined_args), + } + } expr => expr, }; @@ -370,18 +397,10 @@ fn normalize_value( 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(_, args) if args.is_empty() => unreachable!(), + App(Builtin(_), _) => unreachable!(), App(Lam(_, _, _), _) => unreachable!(), App(UnionConstructor(l, kts), args) => { let mut iter = args.iter(); @@ -444,13 +463,9 @@ fn normalize_value( _ => 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( + match what_next.into_value(ctx) { + Some(e) => e, + None => reval(rc(expr.map_ref_simple(ExprF::roll).map_ref( SubExpr::clone, X::clone, |_| unreachable!(), -- cgit v1.2.3