From df245c316029f5b3037c14514bd3535613f26222 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 6 Mar 2019 00:43:25 +0100
Subject: Implement normalization for some more builtins

---
 dhall/src/core.rs | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

(limited to 'dhall/src/core.rs')

diff --git a/dhall/src/core.rs b/dhall/src/core.rs
index e4d09ae..a0e686d 100644
--- a/dhall/src/core.rs
+++ b/dhall/src/core.rs
@@ -997,6 +997,7 @@ where
                 (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
                 (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
                 (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
+                (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
                 (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
                 (App(f@box Builtin(ListBuild), box t), k) => {
                         let labeled =
@@ -1065,12 +1066,22 @@ where
                         kvs = [ ("index", NaturalLit (fromIntegral n))
                               , ("value", x)
                               ]
-                App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->
-                    normalize (maybe nothing just' (toMaybe xs))
-                  where
-                    just' y = App just y
-                    toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList
             */
+                (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => {
+                    let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _|
+                        App(just.clone(), bx(y))
+                    );
+                    normalize(&e2)
+                }
+                (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), b)) => {
+                    normalize(&b)
+                }
+                (App(box Builtin(OptionalBuild), a0), g) => {
+                    let e2: Expr<_, _> = app(app(app(g,
+                            App(bx(Builtin(Optional)), a0.clone())),
+                            Lam("x", a0.clone(), bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))), OptionalLit(Some(a0), vec![]));
+                    normalize(&e2)
+                }
                 (f2, a2) => app(f2, a2),
             },
         },
-- 
cgit v1.2.3