Implement a few more primitives

3 files changed, 65 insertions, 38 deletions

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index c728dd0..e335fbb 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -27,12 +27,13 @@ where
         ListHead => (2, Some(1)),
         ListLast => (2, Some(1)),
         ListReverse => (2, Some(1)),
+        ListIndexed => (2, Some(1)),
         ListBuild => (2, Some(1)),
         OptionalBuild => (2, Some(1)),
         ListFold => (5, Some(1)),
         OptionalFold => (5, Some(1)),
         NaturalBuild => (1, Some(0)),
-        NaturalFold => (1, Some(0)),
+        NaturalFold => (4, Some(0)),
         _ => (0, None),
     };
     // Abort if not enough arguments present
@@ -78,6 +79,17 @@ where
             let ys = ys.iter().rev().cloned().collect();
             rc(NEListLit(ys))
         }
+        (ListIndexed, Some(EmptyListLit(t)), _) => {
+            let t = Rc::clone(t);
+            dhall_expr!([] : List ({ index : Natural, value : t }))
+        }
+        (ListIndexed, Some(NEListLit(xs)), _) => {
+            let xs = xs.iter().cloned().enumerate().map(|(i, e)| {
+                let i = rc(NaturalLit(i));
+                dhall_expr!({ index = i, value = e })
+            }).collect();
+            rc(NEListLit(xs))
+        }
         (ListBuild, _, [a0, g, ..]) => {
             loop {
                 if let App(f2, args2) = g.as_ref() {
@@ -142,24 +154,40 @@ where
         // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
         //     normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
         // }
-        (NaturalBuild, Some(App(f2, args2)), _) => {
-            match (f2.as_ref(), args2.as_slice()) {
-                // fold/build fusion
-                (Builtin(NaturalFold), [x, rest..]) => {
-                    rc(App(x.clone(), rest.to_vec()))
-                }
-                _ => return rc(App(f, args)),
+        (NaturalBuild, _, [g, ..]) => {
+            loop {
+                if let App(f2, args2) = g.as_ref() {
+                    if let (Builtin(NaturalFold), [x, rest..]) =
+                        (f2.as_ref(), args2.as_slice())
+                    {
+                        // fold/build fusion
+                        break rc(App(x.clone(), rest.to_vec()));
+                    }
+                };
+                // TODO: use Embed to avoid reevaluating g
+                break dhall_expr!(g Natural (λ(x : Natural) -> x + 1) 0)
             }
         }
-        (NaturalFold, Some(App(f2, args2)), _) => {
-            match (f2.as_ref(), args2.as_slice()) {
-                // fold/build fusion
-                (Builtin(NaturalBuild), [x, rest..]) => {
-                    rc(App(x.clone(), rest.to_vec()))
-                }
-                _ => return rc(App(f, args)),
-            }
+        (NaturalFold, Some(NaturalLit(0)), [_, _, _, zero]) => {
+            Rc::clone(zero)
         }
+        (NaturalFold, Some(NaturalLit(n)), [_, t, succ, zero]) => {
+            let fold = rc(Builtin(NaturalFold));
+            let n = rc(NaturalLit(n-1));
+            let t = Rc::clone(t);
+            let succ = Rc::clone(succ);
+            let zero = Rc::clone(zero);
+            dhall_expr!(succ (fold n t succ zero))
+        }
+        // (NaturalFold, Some(App(f2, args2)), _) => {
+        //     match (f2.as_ref(), args2.as_slice()) {
+        //         // fold/build fusion
+        //         (Builtin(NaturalBuild), [x, rest..]) => {
+        //             rc(App(x.clone(), rest.to_vec()))
+        //         }
+        //         _ => return rc(App(f, args)),
+        //     }
+        // }
         _ => return rc(App(f, args)),
     };
     // Put the remaining arguments back and eval again. In most cases
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 387327a..62dda08 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,5 +1,4 @@
 #![allow(non_snake_case)]
-use std::collections::BTreeMap;
 use std::collections::HashSet;
 use std::fmt;
 use std::rc::Rc;
diff --git a/dhall/tests/normalization.rs b/dhall/tests/normalization.rs
index c1ea81d..9f3c547 100644
--- a/dhall/tests/normalization.rs
+++ b/dhall/tests/normalization.rs
@@ -65,14 +65,14 @@ norm!(spec_normalization_success_prelude_List_filter_1, "prelude/List/filter/1")
 norm!(spec_normalization_success_prelude_List_fold_0, "prelude/List/fold/0");
 norm!(spec_normalization_success_prelude_List_fold_1, "prelude/List/fold/1");
 norm!(spec_normalization_success_prelude_List_fold_2, "prelude/List/fold/2");
-// norm!(spec_normalization_success_prelude_List_generate_0, "prelude/List/generate/0");
-// norm!(spec_normalization_success_prelude_List_generate_1, "prelude/List/generate/1");
+norm!(spec_normalization_success_prelude_List_generate_0, "prelude/List/generate/0");
+norm!(spec_normalization_success_prelude_List_generate_1, "prelude/List/generate/1");
 norm!(spec_normalization_success_prelude_List_head_0, "prelude/List/head/0");
 norm!(spec_normalization_success_prelude_List_head_1, "prelude/List/head/1");
-// norm!(spec_normalization_success_prelude_List_indexed_0, "prelude/List/indexed/0");
-// norm!(spec_normalization_success_prelude_List_indexed_1, "prelude/List/indexed/1");
-// norm!(spec_normalization_success_prelude_List_iterate_0, "prelude/List/iterate/0");
-// norm!(spec_normalization_success_prelude_List_iterate_1, "prelude/List/iterate/1");
+norm!(spec_normalization_success_prelude_List_indexed_0, "prelude/List/indexed/0");
+norm!(spec_normalization_success_prelude_List_indexed_1, "prelude/List/indexed/1");
+norm!(spec_normalization_success_prelude_List_iterate_0, "prelude/List/iterate/0");
+norm!(spec_normalization_success_prelude_List_iterate_1, "prelude/List/iterate/1");
 norm!(spec_normalization_success_prelude_List_last_0, "prelude/List/last/0");
 norm!(spec_normalization_success_prelude_List_last_1, "prelude/List/last/1");
 norm!(spec_normalization_success_prelude_List_length_0, "prelude/List/length/0");
@@ -81,23 +81,23 @@ norm!(spec_normalization_success_prelude_List_map_0, "prelude/List/map/0");
 norm!(spec_normalization_success_prelude_List_map_1, "prelude/List/map/1");
 norm!(spec_normalization_success_prelude_List_null_0, "prelude/List/null/0");
 norm!(spec_normalization_success_prelude_List_null_1, "prelude/List/null/1");
-// norm!(spec_normalization_success_prelude_List_replicate_0, "prelude/List/replicate/0");
-// norm!(spec_normalization_success_prelude_List_replicate_1, "prelude/List/replicate/1");
+norm!(spec_normalization_success_prelude_List_replicate_0, "prelude/List/replicate/0");
+norm!(spec_normalization_success_prelude_List_replicate_1, "prelude/List/replicate/1");
 norm!(spec_normalization_success_prelude_List_reverse_0, "prelude/List/reverse/0");
 norm!(spec_normalization_success_prelude_List_reverse_1, "prelude/List/reverse/1");
 norm!(spec_normalization_success_prelude_List_shifted_0, "prelude/List/shifted/0");
 norm!(spec_normalization_success_prelude_List_shifted_1, "prelude/List/shifted/1");
 norm!(spec_normalization_success_prelude_List_unzip_0, "prelude/List/unzip/0");
 norm!(spec_normalization_success_prelude_List_unzip_1, "prelude/List/unzip/1");
-// norm!(spec_normalization_success_prelude_Natural_build_0, "prelude/Natural/build/0");
-// norm!(spec_normalization_success_prelude_Natural_build_1, "prelude/Natural/build/1");
-// norm!(spec_normalization_success_prelude_Natural_enumerate_0, "prelude/Natural/enumerate/0");
-// norm!(spec_normalization_success_prelude_Natural_enumerate_1, "prelude/Natural/enumerate/1");
+norm!(spec_normalization_success_prelude_Natural_build_0, "prelude/Natural/build/0");
+norm!(spec_normalization_success_prelude_Natural_build_1, "prelude/Natural/build/1");
+norm!(spec_normalization_success_prelude_Natural_enumerate_0, "prelude/Natural/enumerate/0");
+norm!(spec_normalization_success_prelude_Natural_enumerate_1, "prelude/Natural/enumerate/1");
 norm!(spec_normalization_success_prelude_Natural_even_0, "prelude/Natural/even/0");
 norm!(spec_normalization_success_prelude_Natural_even_1, "prelude/Natural/even/1");
-// norm!(spec_normalization_success_prelude_Natural_fold_0, "prelude/Natural/fold/0");
-// norm!(spec_normalization_success_prelude_Natural_fold_1, "prelude/Natural/fold/1");
-// norm!(spec_normalization_success_prelude_Natural_fold_2, "prelude/Natural/fold/2");
+norm!(spec_normalization_success_prelude_Natural_fold_0, "prelude/Natural/fold/0");
+norm!(spec_normalization_success_prelude_Natural_fold_1, "prelude/Natural/fold/1");
+norm!(spec_normalization_success_prelude_Natural_fold_2, "prelude/Natural/fold/2");
 norm!(spec_normalization_success_prelude_Natural_isZero_0, "prelude/Natural/isZero/0");
 norm!(spec_normalization_success_prelude_Natural_isZero_1, "prelude/Natural/isZero/1");
 norm!(spec_normalization_success_prelude_Natural_odd_0, "prelude/Natural/odd/0");
@@ -161,7 +161,7 @@ norm!(spec_normalization_success_prelude_Text_concatMap_1, "prelude/Text/concatM
 // norm!(spec_normalization_success_simple_letlet, "simple/letlet");
 norm!(spec_normalization_success_simple_listBuild, "simple/listBuild");
 norm!(spec_normalization_success_simple_multiLine, "simple/multiLine");
-// norm!(spec_normalization_success_simple_naturalBuild, "simple/naturalBuild");
+norm!(spec_normalization_success_simple_naturalBuild, "simple/naturalBuild");
 norm!(spec_normalization_success_simple_naturalPlus, "simple/naturalPlus");
 norm!(spec_normalization_success_simple_naturalShow, "simple/naturalShow");
 norm!(spec_normalization_success_simple_naturalToInteger, "simple/naturalToInteger");
@@ -215,8 +215,8 @@ norm!(spec_normalization_success_unit_ListHead, "unit/ListHead");
 norm!(spec_normalization_success_unit_ListHeadEmpty, "unit/ListHeadEmpty");
 norm!(spec_normalization_success_unit_ListHeadOne, "unit/ListHeadOne");
 norm!(spec_normalization_success_unit_ListIndexed, "unit/ListIndexed");
-// norm!(spec_normalization_success_unit_ListIndexedEmpty, "unit/ListIndexedEmpty");
-// norm!(spec_normalization_success_unit_ListIndexedOne, "unit/ListIndexedOne");
+norm!(spec_normalization_success_unit_ListIndexedEmpty, "unit/ListIndexedEmpty");
+norm!(spec_normalization_success_unit_ListIndexedOne, "unit/ListIndexedOne");
 norm!(spec_normalization_success_unit_ListLast, "unit/ListLast");
 norm!(spec_normalization_success_unit_ListLastEmpty, "unit/ListLastEmpty");
 norm!(spec_normalization_success_unit_ListLastOne, "unit/ListLastOne");
@@ -235,13 +235,13 @@ norm!(spec_normalization_success_unit_MergeWithTypeNormalizeArguments, "unit/Mer
 norm!(spec_normalization_success_unit_Natural, "unit/Natural");
 norm!(spec_normalization_success_unit_NaturalBuild, "unit/NaturalBuild");
 norm!(spec_normalization_success_unit_NaturalBuildFoldFusion, "unit/NaturalBuildFoldFusion");
-// norm!(spec_normalization_success_unit_NaturalBuildImplementation, "unit/NaturalBuildImplementation");
+norm!(spec_normalization_success_unit_NaturalBuildImplementation, "unit/NaturalBuildImplementation");
 norm!(spec_normalization_success_unit_NaturalEven, "unit/NaturalEven");
 norm!(spec_normalization_success_unit_NaturalEvenOne, "unit/NaturalEvenOne");
 norm!(spec_normalization_success_unit_NaturalEvenZero, "unit/NaturalEvenZero");
 norm!(spec_normalization_success_unit_NaturalFold, "unit/NaturalFold");
-// norm!(spec_normalization_success_unit_NaturalFoldOne, "unit/NaturalFoldOne");
-// norm!(spec_normalization_success_unit_NaturalFoldZero, "unit/NaturalFoldZero");
+norm!(spec_normalization_success_unit_NaturalFoldOne, "unit/NaturalFoldOne");
+norm!(spec_normalization_success_unit_NaturalFoldZero, "unit/NaturalFoldZero");
 norm!(spec_normalization_success_unit_NaturalIsZero, "unit/NaturalIsZero");
 norm!(spec_normalization_success_unit_NaturalIsZeroOne, "unit/NaturalIsZeroOne");
 norm!(spec_normalization_success_unit_NaturalIsZeroZero, "unit/NaturalIsZeroZero");