Add first version of new evaluator

- Dhall.Eval: new evaluator, conversion checker and normalizer.
  There is no standalone alpha normalizer yet.
- There is a new option "new-normalize" for dhall executable, which uses
  the new normalizer.
- Type checker is unchanged.

dhall/benchmark/examples/new-normalize/ChurchEval.dhall

@@ -0,0 +1,25 @@
+
+-- new-normalize: 0.53s
+-- normalize    : 3.85s
+-- call-by-value version of new-normalize (rebuild Eval.hs with strict vApp) : 0.23s
+
+let Nat = ∀(N : Type) → (N → N) → N → N
+let n2  = λ(N : Type) → λ(s : N → N) → λ(z : N) → s (s z)
+let n5  = λ(N : Type) → λ(s : N → N) → λ(z : N) → s (s (s (s (s z))))
+
+let mul =
+  λ(a : Nat) → λ(b : Nat) → λ(N : Type) → λ(s : N → N) → λ(z : N) → a N (b N s) z
+
+let add =
+  λ(a : Nat) → λ(b : Nat) → λ(N : Type) → λ(s : N → N) → λ(z : N) → a N s (b N s z)
+
+let n10   = mul n2 n5
+let n100  = mul n10 n10
+let n1k   = mul n10 n100
+let n10k  = mul n100 n100
+let n100k = mul n10 n10k
+let n1M   = mul n10k n100
+let n5M   = mul n1M n5
+let n10M  = mul n1M n10
+
+in n1M Natural (λ (x:Natural) → x + 1) 0

dhall/benchmark/examples/new-normalize/ListBenchAltPrelude.dhall

@@ -0,0 +1,47 @@
+
+-- This runs in 0.015s with "new-normalize", runs out of memory with "normalize"
+
+let iterate =
+    λ(n : Natural)
+  → λ(a : Type)
+  → λ(f : a → a)
+  → λ(x : a)
+  → (Natural/fold n
+      (a → List a → {fst:a, snd:List a})
+	  (λ (hyp : a → List a → {fst:a, snd:List a}) →
+	   λ (x : a) → λ (xs : List a)
+	   → let tup = hyp x xs
+	     in {fst = f (tup.fst), snd = [tup.fst] # tup.snd})
+	  (λ (x : a) → λ (xs : List a) → {fst=x, snd=xs})
+	  x ([] : List a)).snd
+
+let countTo =
+  λ (x : Natural)
+  → iterate x Natural (λ (x : Natural) → x + 1) 0
+
+let sum =
+  λ (xs : List Natural)
+  → List/fold Natural xs Natural (λ (x : Natural) → λ (acc : Natural) → x + acc) 0
+
+let map
+  =   λ(a : Type)
+    → λ(b : Type)
+    → λ(f : a → b)
+    → λ(xs : List a)
+	→ List/fold a xs (List b) (λ (x : a) → λ (xs : List b) → [f x] # xs) ([] : List b)
+
+let any
+  =   λ(a : Type)
+        → λ(f : a → Bool)
+        → λ(xs : List a)
+        → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
+
+let filter
+  =   λ(a : Type)
+    → λ(f : a → Bool)
+    → λ(xs : List a)
+	→ List/fold a xs (List a)
+	    (λ (x : a) → λ (xs : List a) → if f x then [x] # xs else xs) ([] : List a)
+
+in sum (filter Natural Natural/even
+     (map Natural Natural (λ(x:Natural) → x + 10) (countTo 1000)))

dhall/benchmark/examples/new-normalize/ListBenchOldPrelude.dhall

@@ -0,0 +1,80 @@
+
+-- Runs in 0.06s with new-normalize, runs out of memory with "normalize". Old
+-- normalize is about 3x faster with old prelude, but extremely slow in either
+-- case.
+
+
+let iterate
+    =   λ(n : Natural)
+      → λ(a : Type)
+      → λ(f : a → a)
+      → λ(x : a)
+      → List/build
+        a
+        (   λ(list : Type)
+          → λ(cons : a → list → list)
+          → List/fold
+            { index : Natural, value : {} }
+            ( List/indexed
+              {}
+              ( List/build
+                {}
+                (   λ(list : Type)
+                  → λ(cons : {} → list → list)
+                  → Natural/fold n list (cons {=})
+                )
+              )
+            )
+            list
+            (   λ(y : { index : Natural, value : {} })
+              → cons (Natural/fold y.index a f x)
+            )
+        )
+
+let countTo =
+  λ (x : Natural)
+  → iterate x Natural (λ (x : Natural) → x + 1) 0
+
+let sum =
+  λ (xs : List Natural)
+  → List/fold Natural xs Natural (λ (x : Natural) → λ (acc : Natural) → x + acc) 0
+
+
+let map
+        : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b
+        =   λ(a : Type)
+          → λ(b : Type)
+          → λ(f : a → b)
+          → λ(xs : List a)
+          → List/build
+            b
+            (   λ(list : Type)
+              → λ(cons : b → list → list)
+              → List/fold a xs list (λ(x : a) → cons (f x))
+            )
+
+let any
+        : ∀(a : Type) → (a → Bool) → List a → Bool
+        =   λ(a : Type)
+          → λ(f : a → Bool)
+          → λ(xs : List a)
+          → List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
+
+let filter
+        : ∀(a : Type) → (a → Bool) → List a → List a
+        =   λ(a : Type)
+          → λ(f : a → Bool)
+          → λ(xs : List a)
+          → List/build
+            a
+            (   λ(list : Type)
+              → λ(cons : a → list → list)
+              → List/fold
+                a
+                xs
+                list
+                (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs)
+            )
+
+in sum (filter Natural Natural/even
+     (map Natural Natural (λ(x:Natural) → x + 10) (countTo 1000)))

dhall/dhall.cabal

@@ -25,6 +25,7 @@ Category: Compiler
 Extra-Source-Files:
     benchmark/deep-nested-large-record/*.dhall
     benchmark/examples/*.dhall
+    benchmark/examples/new-normalize/*.dhall
     CHANGELOG.md
     dhall-lang/Prelude/Bool/and
     dhall-lang/Prelude/Bool/build
@@ -441,7 +442,8 @@ Library
         Dhall.Repl,
         Dhall.TH,
         Dhall.Tutorial,
-        Dhall.TypeCheck
+        Dhall.TypeCheck,
+        Dhall.Eval
     Other-Modules:
         Dhall.Pretty.Internal,
         Dhall.Parser.Expression,
@@ -475,6 +477,7 @@ Test-Suite tasty
         Dhall.Test.Import
         Dhall.Test.Lint
         Dhall.Test.Normalization
+        Dhall.Test.NewNormalization
         Dhall.Test.Parser
         Dhall.Test.QuickCheck
         Dhall.Test.Regression