Split out normalization code into separate files (#276)

This is part of an effort to create a language-independent compliance
test suite by splitting out actual and expected results into files that
can be shared between language implementations.

This also has the nice benefit that the Dhall code doesn't have to be embedded
and escaped within Haskell.

dhall.cabal

@@ -82,6 +82,7 @@ Extra-Source-Files:
     Prelude/Text/concatMapSep
     Prelude/Text/concatSep
     tests/format/*.dhall
+    tests/normalization/*.dhall
     tests/parser/*.dhall
     tests/regression/*.dhall
     tests/tutorial/*.dhall

tests/Normalization.hs

@@ -4,6 +4,17 @@
 module Normalization (normalizationTests) where
 
 import Data.Monoid ((<>))
+import Data.Text.Lazy (Text)
+import Dhall.Core (Expr)
+import Dhall.TypeCheck (X)
+
+import qualified Control.Exception
+import qualified Data.Text.Lazy
+import qualified Dhall.Core
+import qualified Dhall.Import
+import qualified Dhall.Parser
+import qualified Dhall.TypeCheck
+
 import Dhall.Core
 import Dhall.Context
 import Test.Tasty
@@ -11,29 +22,37 @@ import Test.Tasty.HUnit
 import Util 
 
 normalizationTests :: TestTree
-normalizationTests = testGroup "normalization" [ constantFolding
+normalizationTests =
+    testGroup "normalization"
+        [ constantFolding
         , conversions
-                                               , fusion
+        , shouldNormalize "Optional build/fold fusion" "optionalBuildFold"
         , customization
         ]
 
 constantFolding :: TestTree
-constantFolding = testGroup "folding of constants" [ naturalPlus
+constantFolding =
-                                                   , optionalFold
+    testGroup "folding of constants"
-                                                   , optionalBuild
+        [ shouldNormalize "Natural/plus"   "naturalPlus"
+        , shouldNormalize "Optional/fold"  "optionalFold"
+        , shouldNormalize "Optional/build" "optionalBuild"
         ]
 
 conversions :: TestTree
-conversions = testGroup "conversions" [ naturalShow
+conversions =
-                                      , integerShow
+    testGroup "conversions"
-                                      , doubleShow
+        [ shouldNormalize "Natural/show" "naturalShow"
-                                      , naturalToInteger
+        , shouldNormalize "Integer/show" "integerShow"
+        , shouldNormalize "Double/show"  "doubleShow"
+        , shouldNormalize "Natural/toInteger" "naturalToInteger"
         ]
 
 customization :: TestTree
-customization = testGroup "customization"
+customization =
-                 [simpleCustomization
+    testGroup "customization"
-                 ,nestedReduction]
+        [ simpleCustomization
+        , nestedReduction
+        ]
 
 simpleCustomization :: TestTree
 simpleCustomization = testCase "simpleCustomization" $ do
@@ -60,120 +79,35 @@ nestedReduction = testCase "doubleReduction" $ do
   e <- codeWith tyCtx "wurble +6"
   assertNormalizesToWith valCtx e "+5"
 
-naturalPlus :: TestTree
+should :: Text -> Text -> TestTree
-naturalPlus = testCase "natural plus" $ do
+should name basename =
-  e <- code "+1 + +2"
+    Test.Tasty.HUnit.testCase (Data.Text.Lazy.unpack name) $ do
-  e `assertNormalizesTo` "+3"
+        let actualCode   = "./tests/normalization/" <> basename <> "A.dhall"
+        let expectedCode = "./tests/normalization/" <> basename <> "B.dhall"
 
-naturalToInteger :: TestTree
+        actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of
-naturalToInteger = testCase "Natural/toInteger" $ do
+            Left  err  -> Control.Exception.throwIO err
-  e <- code "Natural/toInteger +1"
+            Right expr -> return expr
-  isNormalized e @?= False
+        actualResolved <- Dhall.Import.load actualExpr
-  normalize' e @?= "1"
+        case Dhall.TypeCheck.typeOf actualResolved of
+            Left  err -> Control.Exception.throwIO err
+            Right _   -> return ()
+        let actualNormalized = Dhall.Core.normalize actualResolved :: Expr X X
 
-naturalShow :: TestTree
+        expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of
-naturalShow = testCase "Natural/show" $ do
+            Left  err  -> Control.Exception.throwIO err
-  e <- code "Natural/show +42"
+            Right expr -> return expr
-  e `assertNormalizesTo` "\"+42\""
+        expectedResolved <- Dhall.Import.load expectedExpr
+        case Dhall.TypeCheck.typeOf expectedResolved of
+            Left  err -> Control.Exception.throwIO err
+            Right _   -> return ()
+        -- Use `denote` instead of `normalize` to enforce that the expected
+        -- expression is already in normal form
+        let expectedNormalized = Dhall.Core.denote expectedResolved
 
-integerShow :: TestTree
+        let message =
-integerShow = testCase "Integer/show" $ do
+                "The normalized expression did not match the expected output"
-  e <- code "[Integer/show 1337, Integer/show -42, Integer/show 0]"
+        Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized
-  e `assertNormalizesTo` "[ \"1337\", \"-42\", \"0\" ]"
 
-doubleShow :: TestTree
+shouldNormalize :: Text -> Text -> TestTree
-doubleShow = testCase "Double/show" $ do
+shouldNormalize name = should ("normalize " <> name <> " correctly")
-  e <- code "[Double/show -0.42, Double/show 13.37]"
-  e `assertNormalizesTo` "[ \"-0.42\", \"13.37\" ]"
-
-optionalFold :: TestTree
-optionalFold = testGroup "Optional/fold" [ just, nothing ]
-  where test label inp out = testCase label $ do
-             e <- code ("Optional/fold Text ([" <> inp <> "] : Optional Text) Natural (λ(j : Text) → +1) +2")
-             e `assertNormalizesTo` out
-        just = test "just" "\"foo\"" "+1"
-        nothing = test "nothing" "" "+2"
-
-optionalBuild :: TestTree
-optionalBuild = testGroup "Optional/build" [ optionalBuild1
-                                           , optionalBuildShadowing
-                                           , optionalBuildIrreducible
-                                           ]
-
-optionalBuild1 :: TestTree
-optionalBuild1 = testCase "reducible" $ do
-  e <- code
-    "Optional/build                  \n\
-    \Natural                         \n\
-    \(   λ(optional : Type)          \n\
-    \→   λ(just : Natural → optional)\n\
-    \→   λ(nothing : optional)       \n\
-    \→   just +1                     \n\
-    \)                               \n"
-  e `assertNormalizesTo` "[ +1 ] : Optional Natural"
-
-optionalBuildShadowing :: TestTree
-optionalBuildShadowing = testCase "handles shadowing" $ do
-  e <- code
-    "Optional/build               \n\
-    \Integer                      \n\
-    \(   λ(optional : Type)       \n\
-    \→   λ(x : Integer → optional)\n\
-    \→   λ(x : optional)          \n\
-    \→   x@1 1                    \n\
-    \)                            \n"
-  e `assertNormalizesTo` "[ 1 ] : Optional Integer"
-
-optionalBuildIrreducible :: TestTree
-optionalBuildIrreducible = testCase "irreducible" $ do
-  e <- code
-    "    λ(id : ∀(a : Type) → a → a)  \n\
-    \→   Optional/build               \n\
-    \    Bool                         \n\
-    \    (   λ(optional : Type)       \n\
-    \    →   λ(just : Bool → optional)\n\
-    \    →   λ(nothing : optional)    \n\
-    \    →   id optional (just True)  \n\
-    \    )                            \n"
-  assertNormalized e
-
-fusion :: TestTree
-fusion = testGroup "Optional build/fold fusion" [ fuseOptionalBF
-                                                , fuseOptionalFB
-                                                ]
-
-fuseOptionalBF :: TestTree
-fuseOptionalBF = testCase "fold . build" $ do
-  e0 <- code
-    "    λ(  f                        \n\
-    \    :   ∀(optional : Type)       \n\
-    \    →   ∀(just : Text → optional)\n\
-    \    →   ∀(nothing : optional)    \n\
-    \    →   optional                 \n\
-    \    )                            \n\
-    \→   Optional/fold                \n\
-    \    Text                         \n\
-    \    (   Optional/build           \n\
-    \        Text                     \n\
-    \        f                        \n\
-    \    )                            \n"
-  e1 <- code
-    "    λ(  f                        \n\
-    \    :   ∀(optional : Type)       \n\
-    \    →   ∀(just : Text → optional)\n\
-    \    →   ∀(nothing : optional)    \n\
-    \    →   optional                 \n\
-    \    )                            \n\
-    \→   f                            \n"
-  e0 `assertNormalizesTo` (Dhall.Core.pretty e1)
-
-fuseOptionalFB :: TestTree
-fuseOptionalFB = testCase "build . fold" $ do
-  test <- code
-    "Optional/build                 \n\
-    \Text                           \n\
-    \(   Optional/fold              \n\
-    \    Text                       \n\
-    \    ([\"foo\"] : Optional Text)\n\
-    \)                              \n"
-  test `assertNormalizesTo` "[ \"foo\" ] : Optional Text"

tests/normalization/doubleShowA.dhall

@@ -0,0 +1 @@
+{ example0 = Double/show -0.42, example1 = Double/show 13.37 }

tests/normalization/doubleShowB.dhall

@@ -0,0 +1 @@
+{ example0 = "-0.42", example1 = "13.37" }

tests/normalization/integerShowA.dhall

@@ -0,0 +1,4 @@
+{ example0 = Integer/show 1337
+, example1 = Integer/show -42
+, example2 = Integer/show 0
+}

tests/normalization/integerShowB.dhall

@@ -0,0 +1 @@
+{ example0 = "1337", example1 = "-42", example2 = "0" }

tests/normalization/naturalPlusA.dhall

@@ -0,0 +1 @@
++1 + +2

tests/normalization/naturalPlusB.dhall

@@ -0,0 +1 @@
++3

tests/normalization/naturalShowA.dhall

@@ -0,0 +1 @@
+Natural/show +42

tests/normalization/naturalShowB.dhall

@@ -0,0 +1 @@
+"+42"

tests/normalization/naturalToIntegerA.dhall

@@ -0,0 +1 @@
+Natural/toInteger +1

tests/normalization/naturalToIntegerB.dhall

@@ -0,0 +1 @@
+1

tests/normalization/optionalBuildA.dhall

@@ -0,0 +1,22 @@
+{ example0 =
+    Optional/build
+    Natural
+    (   λ(optional : Type)
+      → λ(just : Natural → optional)
+      → λ(nothing : optional)
+      → just +1
+    )
+, example1 =
+    Optional/build
+    Integer
+    (λ(optional : Type) → λ(x : Integer → optional) → λ(x : optional) → x@1 1)
+, example2 =
+      λ(id : ∀(a : Type) → a → a)
+    → Optional/build
+      Bool
+      (   λ(optional : Type)
+        → λ(just : Bool → optional)
+        → λ(nothing : optional)
+        → id optional (just True)
+      )
+}

tests/normalization/optionalBuildB.dhall

@@ -0,0 +1,12 @@
+{ example0 = [ +1 ] : Optional Natural
+, example1 = [ 1 ] : Optional Integer
+, example2 =
+      λ(id : ∀(a : Type) → a → a)
+    → Optional/build
+      Bool
+      (   λ(optional : Type)
+        → λ(just : Bool → optional)
+        → λ(nothing : optional)
+        → id optional (just True)
+      )
+}

tests/normalization/optionalBuildFoldA.dhall

@@ -0,0 +1,11 @@
+{ example0 =
+      λ ( f
+        :   ∀(optional : Type)
+          → ∀(just : Text → optional)
+          → ∀(nothing : optional)
+          → optional
+        )
+    → Optional/fold Text (Optional/build Text f)
+, example1 =
+    Optional/build Text (Optional/fold Text ([ "foo" ] : Optional Text))
+}

tests/normalization/optionalBuildFoldB.dhall

@@ -0,0 +1,10 @@
+{ example0 =
+      λ ( f
+        :   ∀(optional : Type)
+          → ∀(just : Text → optional)
+          → ∀(nothing : optional)
+          → optional
+        )
+    → f
+, example1 = [ "foo" ] : Optional Text
+}

tests/normalization/optionalFoldA.dhall

@@ -0,0 +1,7 @@
+    let f =
+            λ(o : Optional Text)
+          → Optional/fold Text o Natural (λ(j : Text) → +1) +2
+
+in  { example0 = f ([ "foo" ] : Optional Text)
+    , example1 = f ([] : Optional Text)
+    }

tests/normalization/optionalFoldB.dhall

@@ -0,0 +1 @@
+{ example0 = +1, example1 = +2 }