diff options
| m--------- | dhall-lang | 0 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 119 |
2 files changed, 42 insertions, 77 deletions
diff --git a/dhall-lang b/dhall-lang -Subproject 31e90e1996f6c4cb50e03ccb1f3c45beb4bd278 +Subproject 0ee92af46a01a889c6d8d7c72926c959d034b19 diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 65384c2..6258ae8 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -259,37 +259,23 @@ pub(crate) fn apply_builtin( _ => Ret::DoneAsIs, } } - (ListBuild, [t, f]) => match &*f.as_whnf() { - // fold/build fusion - ValueKind::AppliedBuiltin(ListFold, args) => { - if args.len() >= 2 { - Ret::Value(args[1].clone()) - } else { - // Do we really need to handle this case ? - unimplemented!() - } - } - _ => { - let list_t = Value::from_builtin(List).app(t.clone()); - Ret::Value( - f.app(list_t.clone()) - .app({ - // Move `t` under new variables - let t1 = t.under_binder(Label::from("x")); - let t2 = t1.under_binder(Label::from("xs")); - make_closure!( - λ(x : #t) -> - λ(xs : List #t1) -> - [ var(x, 1, #t2) ] # var(xs, 0, List #t2) - ) - }) - .app( - EmptyListLit(t.clone()) - .into_value_with_type(list_t), - ), - ) - } - }, + (ListBuild, [t, f]) => { + let list_t = Value::from_builtin(List).app(t.clone()); + Ret::Value( + f.app(list_t.clone()) + .app({ + // Move `t` under new variables + let t1 = t.under_binder(Label::from("x")); + let t2 = t1.under_binder(Label::from("xs")); + make_closure!( + λ(x : #t) -> + λ(xs : List #t1) -> + [ var(x, 1, #t2) ] # var(xs, 0, List #t2) + ) + }) + .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), + ) + } (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() { EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()), NEListLit(xs) => { @@ -301,31 +287,20 @@ pub(crate) fn apply_builtin( } _ => Ret::DoneAsIs, }, - (OptionalBuild, [t, f]) => match &*f.as_whnf() { - // fold/build fusion - ValueKind::AppliedBuiltin(OptionalFold, args) => { - if args.len() >= 2 { - Ret::Value(args[1].clone()) - } else { - // Do we really need to handle this case ? - unimplemented!() - } - } - _ => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ret::Value( - f.app(optional_t.clone()) - .app({ - let t1 = t.under_binder(Label::from("x")); - make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) - }) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), - ) - } - }, + (OptionalBuild, [t, f]) => { + let optional_t = Value::from_builtin(Optional).app(t.clone()); + Ret::Value( + f.app(optional_t.clone()) + .app({ + let t1 = t.under_binder(Label::from("x")); + make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) + }) + .app( + EmptyOptionalLit(t.clone()) + .into_value_with_type(optional_t), + ), + ) + } (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf() { EmptyOptionalLit(_) => { @@ -336,27 +311,17 @@ pub(crate) fn apply_builtin( } _ => Ret::DoneAsIs, }, - (NaturalBuild, [f]) => match &*f.as_whnf() { - // fold/build fusion - ValueKind::AppliedBuiltin(NaturalFold, args) => { - if !args.is_empty() { - Ret::Value(args[0].clone()) - } else { - // Do we really need to handle this case ? - unimplemented!() - } - } - _ => Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure!( - λ(x : Natural) -> 1 + var(x, 0, Natural) - )) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), - ), - }, + (NaturalBuild, [f]) => Ret::Value( + f.app(Value::from_builtin(Natural)) + .app(make_closure!( + λ(x : Natural) -> 1 + var(x, 0, Natural) + )) + .app( + NaturalLit(0) + .into_value_with_type(Value::from_builtin(Natural)), + ), + ), + (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() { NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()), NaturalLit(n) => { |