diff options
author | Nadrieril | 2019-04-30 18:52:39 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-30 18:52:39 +0200 |
commit | cc96566758f062bb2e1e7767009c3e709c0678b6 (patch) | |
tree | 2e61207c04c4a074facebf51452875950f21da5c | |
parent | ba0c760e9dc30a4babf9b76860153aa05d16e9eb (diff) |
Avoid some rewrapping of thunks
Diffstat (limited to '')
-rw-r--r-- | dhall/src/normalize.rs | 83 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 4 |
2 files changed, 51 insertions, 36 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index c89e147..f2bae80 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -163,7 +163,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value { [_, NEListLit(xs), _, cons, nil] => { let mut v = nil; for x in xs.into_iter().rev() { - v = cons.clone().app(x.normalize_whnf().clone()).app(v); + v = cons.clone().app_thunk(x).app(v); } v } @@ -197,7 +197,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value { nothing }, [_, NEOptionalLit(x), _, just, _] => { - just.app(x.normalize_whnf().clone()) + just.app_thunk(x) } ), NaturalBuild => improved_slice_patterns::match_vec!(args; @@ -678,43 +678,59 @@ impl Value { /// Apply to a value pub(crate) fn app(self, val: Value) -> Value { - match (self, val) { - (Value::Lam(x, _, e), val) => { - let val = Typed( - Thunk::from_whnf(val), - None, - std::marker::PhantomData, - ); + self.app_thunk(val.into_thunk()) + } + + /// Apply to a thunk + pub(crate) fn app_thunk(self, th: Thunk) -> Value { + // If nothing else matches, convert to Expr + let fallback = |f: Value, a: Thunk| { + Value::Expr(rc(ExprF::App( + f.normalize_to_expr(), + a.normalize_whnf().normalize_to_expr(), + ))) + }; + + match self { + Value::Lam(x, _, e) => { + let val = Typed(th, None, std::marker::PhantomData); e.subst_shift(&V(x, 0), &val).normalize_whnf().clone() } - (Value::AppliedBuiltin(b, mut args), val) => { - args.push(val); + Value::AppliedBuiltin(b, mut args) => { + args.push(th.normalize_whnf().clone()); apply_builtin(b, args) } - (Value::OptionalSomeClosure(_), val) => { - Value::NEOptionalLit(Thunk::from_whnf(val)) - } - (Value::ListConsClosure(t, None), val) => { - Value::ListConsClosure(t, Some(Thunk::from_whnf(val))) + Value::OptionalSomeClosure(_) => Value::NEOptionalLit(th), + Value::ListConsClosure(t, None) => { + Value::ListConsClosure(t, Some(th)) } - (Value::ListConsClosure(_, Some(x)), Value::EmptyListLit(_)) => { - Value::NEListLit(vec![x]) - } - (Value::ListConsClosure(_, Some(x)), Value::NEListLit(mut xs)) => { - xs.insert(0, x); - Value::NEListLit(xs) - } - (Value::NaturalSuccClosure, Value::NaturalLit(n)) => { - Value::NaturalLit(n + 1) + Value::ListConsClosure(t, Some(x)) => { + let v = th.normalize_whnf(); + match &*v { + Value::EmptyListLit(_) => Value::NEListLit(vec![x]), + Value::NEListLit(xs) => { + let mut xs = xs.clone(); + xs.insert(0, x); + Value::NEListLit(xs) + } + _ => { + drop(v); + fallback(Value::ListConsClosure(t, Some(x)), th) + } + } } - (Value::UnionConstructor(l, kts), val) => { - Value::UnionLit(l, Thunk::from_whnf(val), kts) + Value::NaturalSuccClosure => { + let v = th.normalize_whnf(); + match &*v { + Value::NaturalLit(n) => Value::NaturalLit(n + 1), + _ => { + drop(v); + fallback(Value::NaturalSuccClosure, th) + } + } } - // Can't do anything useful, convert to expr - (f, a) => Value::Expr(rc(ExprF::App( - f.normalize_to_expr(), - a.normalize_to_expr(), - ))), + Value::UnionConstructor(l, kts) => Value::UnionLit(l, th, kts), + f => fallback(f, th), } } @@ -1323,8 +1339,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value { UnionLit(l, v, kts) => match handlers.remove(&l) { Some(h) => { let h = h.normalize_whnf().clone(); - let v = v.normalize_whnf().clone(); - return h.app(v); + return h.app_thunk(v); } None => UnionLit(l, v, kts), }, diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 461f1cc..fb698d0 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -693,7 +693,7 @@ impl TypeIntermediate { ); Typed( Value::from_builtin(Builtin::List) - .app(t.clone().normalize_whnf()?) + .app(t.normalize_whnf()?) .into_thunk(), Some(const_to_type(Const::Type)), PhantomData, @@ -709,7 +709,7 @@ impl TypeIntermediate { ); Typed( Value::from_builtin(Builtin::Optional) - .app(t.clone().normalize_whnf()?) + .app(t.normalize_whnf()?) .into_thunk(), Some(const_to_type(Const::Type)), PhantomData, |