Integration and fixes for NbE evaluator

- new implementation: alphaNormalize, judgmentallyEqual, normalize
- normalizeWith takes a Maybe ReifiedNormalizer argument now, and switches to
  the new evaluator whenever the input normalizer is Nothing
- QuickCheck test for isNormalized removed, because we don't support evaluation
  of ill-typed terms, which the test would require.

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

@@ -1,8 +1,4 @@
 
--- 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))))
@@ -21,5 +17,6 @@ let n100k = mul n10 n10k
 let n1M   = mul n10k n100
 let n5M   = mul n1M n5
 let n10M  = mul n1M n10
+let n20M  = mul n10M n2
 
 in n1M Natural (λ (x:Natural) → x + 1) 0

dhall/benchmark/examples/normalize/FunCompose.dhall

@@ -0,0 +1,18 @@
+
+let compose
+    : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
+    =   λ(A : Type)
+      → λ(B : Type)
+      → λ(C : Type)
+      → λ(f : A → B)
+      → λ(g : B → C)
+      → λ(x : A)
+      → g (f x)
+
+let composeN : ∀ (a : Type) → Natural → (a → a) → a → a
+    = λ (a : Type)
+	→ λ (n : Natural)
+	→ λ (f : a → a)
+	→ Natural/fold n (a → a) (compose a a a f) (λ (x : a) → x)
+
+in composeN Natural 100000 (λ (x : Natural) → x + 1) 0

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

@@ -1,9 +1,4 @@
 
--- 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)

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

@@ -1,6 +1,4 @@
 
--- This runs in 0.015s with "new-normalize", runs out of memory with "normalize"
-
 let iterate =
     λ(n : Natural)
   → λ(a : Type)
@@ -11,7 +9,7 @@ let iterate =
 	  (λ (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})
+	     in {fst = f (tup.fst), snd = tup.snd # [tup.fst]})
 	  (λ (x : a) → λ (xs : List a) → {fst=x, snd=xs})
 	  x ([] : List a)).snd
 

dhall/dhall.cabal

@@ -25,7 +25,7 @@ Category: Compiler
 Extra-Source-Files:
     benchmark/deep-nested-large-record/*.dhall
     benchmark/examples/*.dhall
-    benchmark/examples/new-normalize/*.dhall
+    benchmark/examples/normalize/*.dhall
     CHANGELOG.md
     dhall-lang/Prelude/Bool/and
     dhall-lang/Prelude/Bool/build
@@ -477,7 +477,6 @@ Test-Suite tasty
         Dhall.Test.Import
         Dhall.Test.Lint
         Dhall.Test.Normalization
-        Dhall.Test.NewNormalization
         Dhall.Test.Parser
         Dhall.Test.QuickCheck
         Dhall.Test.Regression

dhall/src/Dhall.hs

@@ -185,7 +185,7 @@ instance (Pretty s, Pretty a, Typeable s, Typeable a) => Show (InvalidType s a)
         where
           txt0 = Dhall.Util.insert invalidTypeExpected
           txt1 = Dhall.Util.insert invalidTypeExpression
-            
+
 
 instance (Pretty s, Pretty a, Typeable s, Typeable a) => Exception (InvalidType s a)
 
@@ -231,7 +231,7 @@ sourceName k s =
 -- | @since 1.16
 data EvaluateSettings = EvaluateSettings
   { _startingContext :: Dhall.Context.Context (Expr Src X)
-  , _normalizer      :: Dhall.Core.ReifiedNormalizer X
+  , _normalizer      :: Maybe (Dhall.Core.ReifiedNormalizer X)
   , _standardVersion :: StandardVersion
   }
 
@@ -242,7 +242,7 @@ data EvaluateSettings = EvaluateSettings
 defaultEvaluateSettings :: EvaluateSettings
 defaultEvaluateSettings = EvaluateSettings
   { _startingContext = Dhall.Context.empty
-  , _normalizer      = Dhall.Core.ReifiedNormalizer (const (pure Nothing))
+  , _normalizer      = Nothing
   , _standardVersion = Dhall.Binary.defaultStandardVersion
   }
 
@@ -263,11 +263,11 @@ startingContext = evaluateSettings . l
 -- @since 1.16
 normalizer
   :: (Functor f, HasEvaluateSettings s)
-  => LensLike' f s (Dhall.Core.ReifiedNormalizer X)
+  => LensLike' f s (Maybe (Dhall.Core.ReifiedNormalizer X))
 normalizer = evaluateSettings . l
   where
     l :: (Functor f)
-      => LensLike' f EvaluateSettings (Dhall.Core.ReifiedNormalizer X)
+      => LensLike' f EvaluateSettings (Maybe (Dhall.Core.ReifiedNormalizer X))
     l k s = fmap (\x -> s { _normalizer = x }) (k (_normalizer s))
 
 -- | Access the standard version (used primarily when encoding or decoding
@@ -360,10 +360,8 @@ inputWithSettings settings (Type {..}) txt = do
             _ ->
                 Annot expr' expected
     _ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) annot)
-    let normExpr = Dhall.Core.normalizeWith
-                     (Dhall.Core.getReifiedNormalizer
-                       (view normalizer settings))
-                     expr'
+    let normExpr = Dhall.Core.normalizeWith (view normalizer settings) expr'
+
     case extract normExpr  of
         Just x  -> return x
         Nothing -> Control.Exception.throwIO
@@ -450,7 +448,7 @@ inputExprWithSettings settings txt = do
     expr' <- State.evalStateT (Dhall.Import.loadWith expr) status
 
     _ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) expr')
-    pure (Dhall.Core.normalizeWith (Dhall.Core.getReifiedNormalizer (view normalizer settings)) expr')
+    pure (Dhall.Core.normalizeWith (view normalizer settings) expr')
 
 -- | Use this function to extract Haskell values directly from Dhall AST.
 --   The intended use case is to allow easy extraction of Dhall values for
@@ -834,7 +832,7 @@ instance Interpret a => Interpret (Vector a) where
 instance (Inject a, Interpret b) => Interpret (a -> b) where
     autoWith opts = Type extractOut expectedOut
       where
-        normalizer_ = Dhall.Core.getReifiedNormalizer (inputNormalizer opts)
+        normalizer_ = Just (inputNormalizer opts)
 
         extractOut e = Just (\i -> case extractIn (Dhall.Core.normalizeWith normalizer_ (App e (embed i))) of
             Just o  -> o