From faccb680fbede2191e23161e7060be843bcc229e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 22 Dec 2019 19:16:34 +0000
Subject: Update dhall-lang submodule

---
 dhall/src/semantics/phase/normalize.rs | 119 ++++++++++++---------------------
 1 file changed, 42 insertions(+), 77 deletions(-)

(limited to 'dhall/src/semantics/phase/normalize.rs')

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) => {
-- 
cgit v1.2.3