packages feed

dhall 1.10.0 → 1.11.0

raw patch · 327 files changed

+1447/−1736 lines, 327 filesdep +cryptonitedep +memorydep −cryptohashdep ~ansi-terminaldep ~exceptionsPVP ok

version bump matches the API change (PVP)

Dependencies added: cryptonite, memory

Dependencies removed: cryptohash

Dependency ranges changed: ansi-terminal, exceptions

API changes (from Hackage documentation)

- Dhall.TypeCheck: InvalidOptionalLiteral :: Int -> TypeMessage s a
+ Dhall: data Seq a :: * -> *
+ Dhall: instance Dhall.Interpret a => Dhall.Interpret (Data.Sequence.Internal.Seq a)
+ Dhall: sequence :: Type a -> Type (Seq a)
+ Dhall.Core: alphaNormalize :: Expr s a -> Expr s a
+ Dhall.Core: judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
- Dhall.Core: ListLit :: (Maybe (Expr s a)) -> (Vector (Expr s a)) -> Expr s a
+ Dhall.Core: ListLit :: (Maybe (Expr s a)) -> (Seq (Expr s a)) -> Expr s a
- Dhall.Core: OptionalLit :: (Expr s a) -> (Vector (Expr s a)) -> Expr s a
+ Dhall.Core: OptionalLit :: (Expr s a) -> (Maybe (Expr s a)) -> Expr s a
- Dhall.Core: PathHashed :: Maybe ByteString -> PathType -> PathHashed
+ Dhall.Core: PathHashed :: Maybe (Digest SHA256) -> PathType -> PathHashed
- Dhall.Core: [hash] :: PathHashed -> Maybe ByteString
+ Dhall.Core: [hash] :: PathHashed -> Maybe (Digest SHA256)
- Dhall.Core: normalize :: Expr s a -> Expr t a
+ Dhall.Core: normalize :: Eq a => Expr s a -> Expr t a
- Dhall.Core: normalizeWith :: Normalizer a -> Expr s a -> Expr t a
+ Dhall.Core: normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a
- Dhall.Import: hashExpression :: Expr s X -> ByteString
+ Dhall.Import: hashExpression :: Expr s X -> (Digest SHA256)

Files

CHANGELOG.md view
@@ -1,3 +1,41 @@+1.11.0++* BREAKING CHANGE TO THE API: Fix `{Natural,Optional,List}/build` semantics to+  match standard+    * This is a breaking change because the `OptionalLit` and `ListLit`+      constructors changed their representations to efficiently support the+      standard semantics+    * `ListLit` now stores a `Data.Sequence.Seq` instead of a+      `Data.Vector.Vector`+    * `OptionalLit` now stores a `Maybe` instead of a `Data.Vector.Vector`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/300+* BREAKING CHANGE TO THE COMMAND LINE: `dhall` executable always formats output+    * Previously you had to opt into formatting using `--pretty`+    * Now formatting is obligatory and the `--pretty` flag is gone+    * See: https://github.com/dhall-lang/dhall-haskell/pull/303+* Feature: New `:save` command for `dhall-repl`+    * Now you can save an expression to a file: `./yourFile = someExpression`+    * See: https://github.com/dhall-lang/dhall-haskell/pull/309+* Improvement: Add new simplifications to match standard+    * See: https://github.com/dhall-lang/dhall-haskell/pull/312+    * See: https://github.com/dhall-lang/dhall-haskell/pull/316+* Improvement: Fix equivalence check to match standard+    * Practically this means that more corner cases of the language correctly+      type-check than before+* Improvement: New `--plain` flag to disable syntax highlighting+    * See: https://github.com/dhall-lang/dhall-haskell/pull/310+* Improvement: Prelude now provides an umbrella `package.dhall` import+    * This is primarily for convenience+    * See: https://github.com/dhall-lang/dhall-haskell/pull/298+* Improvement: Context is now normalized+    * See: https://github.com/dhall-lang/dhall-haskell/pull/302+* Replace `cryptohash` dependency with `cryptonite`+    * See: https://github.com/dhall-lang/dhall-haskell/commit/5d2012927a062ec8bdf2bbaba77150344f38db77+* Increase upper bound on exceptions+    * See: https://github.com/dhall-lang/dhall-haskell/pull/306+* Fix type error in tutorial+    * See: https://github.com/dhall-lang/dhall-haskell/commit/5a9126b2f684d3236fc1e8e20e206cfaf47d97db+ 1.10.0  * Feature: Records/unions can now have fields/alternatives that are types
Prelude/Bool/and view
@@ -5,7 +5,7 @@ Examples:  ```-./and ([ True, False, True ] : List Bool) = False+./and [ True, False, True ] = False  ./and ([] : List Bool) = True ```
Prelude/Bool/even view
@@ -5,11 +5,11 @@ Examples:  ```-./even ([ False, True, False ] : List Bool) = True+./even [ False, True, False ] = True -./even ([ False, True ] : List Bool) = False+./even [ False, True ] = False -./even ([ False ] : List Bool) = False+./even [ False ] = False  ./even ([] : List Bool) = True ```
Prelude/Bool/odd view
@@ -5,11 +5,11 @@ Examples:  ```-./odd ([ True, False, True ] : List Bool) = False+./odd [ True, False, True ] = False -./odd ([ True, False ] : List Bool) = True+./odd [ True, False ] = True -./odd ([ True ] : List Bool) = True+./odd [ True ] = True  ./odd ([] : List Bool) = False ```
Prelude/Bool/or view
@@ -5,7 +5,7 @@ Examples:  ```-./or ([ True, False, True ] : List Bool) = True+./or [ True, False, True ] = True  ./or ([] : List Bool) = False ```
Prelude/List/all view
@@ -5,7 +5,7 @@ Examples:  ```-./all Natural Natural/even ([ +2, +3, +5 ] : List Natural) = False+./all Natural Natural/even [ +2, +3, +5 ] = False  ./all Natural Natural/even ([] : List Natural) = True ```
Prelude/List/any view
@@ -5,7 +5,7 @@ Examples:  ```-./any Natural Natural/even ([ +2, +3, +5 ] : List Natural) = True+./any Natural Natural/even [ +2, +3, +5 ] = True  ./any Natural Natural/even ([] : List Natural) = False ```
Prelude/List/build view
@@ -11,7 +11,7 @@ →   λ(nil : list) →   cons "ABC" (cons "DEF" nil) )-= [ "ABC", "DEF" ] : List Text+= [ "ABC", "DEF" ]  ./build Text
Prelude/List/concat view
@@ -5,18 +5,17 @@  ``` ./concat Integer-(   [   [0, 1, 2]    : List Integer-    ,   [3, 4]       : List Integer-    ,   [5, 6, 7, 8] : List Integer-    ]   : List (List Integer)-)-= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] : List Integer+[   [0, 1, 2]+,   [3, 4]+,   [5, 6, 7, 8]+]+= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]  ./concat Integer (   [   [] : List Integer     ,   [] : List Integer     ,   [] : List Integer-    ]   : List (List Integer)+    ] ) = [] : List Integer
Prelude/List/concatMap view
@@ -6,7 +6,7 @@  ``` ./concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5]-= [ +2, +2, +3, +3, +5, +5 ] : List Natural+= [ +2, +2, +3, +3, +5, +5 ]  ./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural) = [] : List Natural
Prelude/List/filter view
@@ -4,11 +4,11 @@ Examples:  ```-./filter Natural Natural/even ([+2, +3, +5] : List Natural)-= [ +2 ] : List Natural+./filter Natural Natural/even [+2, +3, +5]+= [ +2 ] -./filter Natural Natural/odd ([+2, +3, +5] : List Natural)-= [ +3, +5 ] : List Natural+./filter Natural Natural/odd [+2, +3, +5]+= [ +3, +5 ] ``` -}     let filter
Prelude/List/fold view
@@ -1,15 +1,15 @@ {- `fold` is the primitive function for consuming `List`s -If you treat the list `[ x, y, z ] : List t` as `cons x (cons y (cons z nil))`,-then a `fold` just replaces each `cons` and `nil` with something else+If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a+`fold` just replaces each `cons` and `nil` with something else  Examples:  ```     ./fold     Natural-    ([ +2, +3, +5 ] : List Natural)+    [ +2, +3, +5 ]     Natural     (λ(x : Natural) → λ(y : Natural) → x + y)     +0@@ -18,7 +18,7 @@     λ(nil : Natural) →   ./fold     Natural-    ([ +2, +3, +5 ] : List Natural)+    [ +2, +3, +5 ]     Natural     (λ(x : Natural) → λ(y : Natural) → x + y)     nil@@ -27,7 +27,7 @@     λ(list : Type) →   λ(cons : Natural → list → list) →   λ(nil : list)-→   ./fold Natural ([ +2, +3, +5 ] : List Natural) list cons nil+→   ./fold Natural [ +2, +3, +5 ] list cons nil =   λ(list : Type) →   λ(cons : Natural → list → list) →   λ(nil : list)
Prelude/List/generate view
@@ -5,7 +5,7 @@ Examples:  ```-./generate +5 Bool Natural/even = [ True, False, True, False, True ] : List Bool+./generate +5 Bool Natural/even = [ True, False, True, False, True ]  ./generate +0 Bool Natural/even = [] : List Bool ```
Prelude/List/head view
@@ -4,7 +4,7 @@ Examples:  ```-./head Integer ([ 0, 1, 2 ] : List Integer) = [ 0 ] : Optional Integer+./head Integer [ 0, 1, 2 ] = [ 0 ] : Optional Integer  ./head Integer ([] : List Integer) = [] : Optional Integer ```
Prelude/List/indexed view
@@ -4,11 +4,11 @@ Examples:  ```-./indexed Bool ([ True, False, True ] : List Bool)+./indexed Bool [ True, False, True ] =   [   { index = +0, value = True  }     ,   { index = +1, value = False }     ,   { index = +2, value = True  }-    ]   : List { index : Natural, value : Bool }+    ] : List { index : Natural, value : Bool }  ./indexed Bool ([] : List Bool) = [] : List { index : Natural, value : Bool }
Prelude/List/iterate view
@@ -6,7 +6,7 @@  ``` ./iterate +10 Natural (λ(x : Natural) → x * +2) +1-= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] : List Natural+= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]  ./iterate +0 Natural (λ(x : Natural) → x * +2) +1 = [] : List Natural
Prelude/List/last view
@@ -4,7 +4,7 @@ Examples:  ```-./last Integer ([ 0, 1, 2 ] : List Integer) = [ 2 ] : Optional Integer+./last Integer [ 0, 1, 2 ] = [ 2 ] : Optional Integer  ./last Integer ([] : List Integer) = [] : Optional Integer ```
Prelude/List/length view
@@ -4,7 +4,7 @@ Examples:  ```-./length Integer ([ 0, 1, 2 ] : List Integer) = +3+./length Integer [ 0, 1, 2 ] = +3  ./length Integer ([] : List Integer) = +0 ```
Prelude/List/map view
@@ -4,8 +4,8 @@ Examples:  ```-./map Natural Bool Natural/even ([ +2, +3, +5 ] : List Natural)-= [ True, False, False ] : List Bool+./map Natural Bool Natural/even [ +2, +3, +5 ]+= [ True, False, False ]  ./map Natural Bool Natural/even ([] : List Natural) = [] : List Bool
Prelude/List/null view
@@ -4,7 +4,7 @@ Examples:  ```-./null Integer ([ 0, 1, 2 ] : List Integer) = False+./null Integer [ 0, 1, 2 ] = False  ./null Integer ([] : List Integer) = True ```
Prelude/List/replicate view
@@ -4,7 +4,7 @@ Examples:  ```-./replicate +9 Integer 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] : List Integer+./replicate +9 Integer 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]  ./replicate +0 Integer 1 = [] : List Integer ```
Prelude/List/reverse view
@@ -4,7 +4,7 @@ Examples:  ```-./reverse Integer ([ 0, 1, 2 ] : List Integer) = [ 2, 1, 0 ] : List Integer+./reverse Integer [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Integer  ./reverse Integer ([] : List Integer) = [] : List Integer ```
Prelude/List/shifted view
@@ -7,20 +7,19 @@ ``` ./shifted Bool-(   [   [   { index = +0, value = True  }-        ,   { index = +1, value = True  }-        ,   { index = +2, value = True  }-        ]   : List { index : Natural, value : Bool }-    ,   [   { index = +0, value = False }-        ,   { index = +1, value = False }-        ]   : List { index : Natural, value : Bool }-    ,   [   { index = +0, value = True  }-        ,   { index = +1, value = True  }-        ,   { index = +2, value = True  }-        ,   { index = +3, value = True  }-        ]   : List { index : Natural, value : Bool }-    ]   : List (List { index : Natural, value : Bool })-)+[   [   { index = +0, value = True  }+    ,   { index = +1, value = True  }+    ,   { index = +2, value = True  }+    ]+,   [   { index = +0, value = False }+    ,   { index = +1, value = False }+    ]+,   [   { index = +0, value = True  }+    ,   { index = +1, value = True  }+    ,   { index = +2, value = True  }+    ,   { index = +3, value = True  }+    ]+] =   [   { index = +0, value = True  }     ,   { index = +1, value = True  }     ,   { index = +2, value = True  }@@ -30,7 +29,7 @@     ,   { index = +6, value = True  }     ,   { index = +7, value = True  }     ,   { index = +8, value = True  }-    ]   : List { index : Natural, value : Bool }+    ]  ./shifted Bool ([] : List (List { index : Natural, value : Bool })) = [] : List { index : Natural, value : Bool }
Prelude/List/unzip view
@@ -10,10 +10,10 @@ (   [   { _1 = "ABC", _2 = True  }     ,   { _1 = "DEF", _2 = False }     ,   { _1 = "GHI", _2 = True  }-    ]   : List { _1 : Text, _2 : Bool }+    ] )-=   { _1 = [ "ABC", "DEF", "GHI" ] : List Text-    , _2 = [ True, False, True ] : List Bool+=   { _1 = [ "ABC", "DEF", "GHI" ]+    , _2 = [ True, False, True ]     }  ./unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
Prelude/Natural/enumerate view
@@ -5,7 +5,7 @@ Examples:  ```-./enumerate +10 = [ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] : List Natural+./enumerate +10 = [ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ]  ./enumerate +0 = [] : List Natural ```
Prelude/Natural/product view
@@ -4,7 +4,7 @@ Examples:  ```-./product ([ +2, +3, +5 ] : List Natural) = +30+./product [ +2, +3, +5 ] = +30  ./product ([] : List Natural) = +1 ```
Prelude/Natural/sum view
@@ -4,7 +4,7 @@ Examples:  ```-./sum ([ +2, +3, +5 ] : List Natural) = +10+./sum [ +2, +3, +5 ] = +10  ./sum ([] : List Natural) = +0 ```
Prelude/Optional/head view
@@ -6,17 +6,15 @@ ``` ./head Integer-(   [ [   ] : Optional Integer-    , [ 1 ] : Optional Integer-    , [ 2 ] : Optional Integer-    ]-    : List (Optional Integer)-)+[ [   ] : Optional Integer+, [ 1 ] : Optional Integer+, [ 2 ] : Optional Integer+] = [ 1 ] : Optional Integer  ./head Integer-([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))+[ [] : Optional Integer, [] : Optional Integer ] = [] : Optional Integer  ./head Integer ([] : List (Optional Integer))
Prelude/Optional/last view
@@ -6,16 +6,15 @@ ``` ./last Integer-(   [ [   ] : Optional Integer-    , [ 1 ] : Optional Integer-    , [ 2 ] : Optional Integer-    ] : List (Optional Integer)-)+[ [   ] : Optional Integer+, [ 1 ] : Optional Integer+, [ 2 ] : Optional Integer+] = [ 2 ] : Optional Integer  ./last Integer-([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))+[ [] : Optional Integer, [] : Optional Integer ] = [] : Optional Integer  ./last Integer ([] : List (Optional Integer))
Prelude/Text/concat view
@@ -4,7 +4,7 @@ Examples:  ```-./concat ([ "ABC", "DEF", "GHI" ] : List Text) = "ABCDEFGHI"+./concat [ "ABC", "DEF", "GHI" ] = "ABCDEFGHI"  ./concat ([] : List Text) = "" ```
dhall-repl/Main.hs view
@@ -20,6 +20,7 @@ import qualified Dhall.Import as Dhall import qualified Dhall.Parser as Dhall import qualified Dhall.TypeCheck as Dhall+import qualified System.Console.ANSI import qualified System.Console.Haskeline.MonadException as Haskeline import qualified System.Console.Repline as Repline import qualified System.IO@@ -97,7 +98,7 @@    modify ( \e -> e { envIt = Just ( Binding expr exprType ) } ) -  output expr+  output System.IO.stdout expr   @@ -116,7 +117,7 @@   exprType' <-     normalize exprType -  output ( Expr.Annot loaded exprType' )+  output System.IO.stdout ( Expr.Annot loaded exprType' )   @@ -181,18 +182,33 @@     )    output+    System.IO.stdout     ( Expr.Annot ( Expr.Var ( Dhall.V varName 0 ) ) t )  addBinding _ =   liftIO ( fail ":let should be of the form `:let x = y`" ) +saveBinding :: ( MonadIO m, MonadState Env m ) => [String] -> m ()+saveBinding (file : "=" : tokens) = do+  loadedExpression <- parseAndLoad (unwords tokens) +  _ <- typeCheck loadedExpression++  normalizedExpression <- normalize loadedExpression++  let handler handle = output handle normalizedExpression++  liftIO (System.IO.withFile file System.IO.WriteMode handler)+saveBinding _ = fail ":save should be of the form `:save x = y`"++ options   :: ( Haskeline.MonadException m, MonadIO m, MonadState Env m )   => Repline.Options m options =   [ ( "type", dontCrash . typeOf )   , ( "let", dontCrash . addBinding )+  , ( "save", dontCrash . saveBinding )   ]  @@ -213,20 +229,21 @@     ( \ e@SomeException{} -> liftIO ( putStrLn ( displayException e ) ) )  -output :: ( Pretty.Pretty a, MonadIO m ) => Dhall.Expr s a -> m ()-output expr = do-  let-    opts =-      Pretty.defaultLayoutOptions-        { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 }+output+    :: (Pretty.Pretty a, MonadIO m)+    => System.IO.Handle -> Dhall.Expr s a -> m ()+output handle expr = do+  let opts =+          Pretty.defaultLayoutOptions+              { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } -  liftIO-    ( Pretty.renderIO-        System.IO.stdout-        ( fmap-            Dhall.Pretty.annToAnsiStyle-            ( Pretty.layoutSmart opts ( Dhall.Pretty.prettyExpr expr ) )-        )-    )+  let stream = Pretty.layoutSmart opts (Dhall.Pretty.prettyExpr expr)+  supportsANSI <- liftIO (System.Console.ANSI.hSupportsANSI handle)+  let ansiStream =+          if supportsANSI+          then fmap Dhall.Pretty.annToAnsiStyle stream+          else Pretty.unAnnotateS stream -  liftIO ( putStrLn "" ) -- Pretty printing doesn't end with a new line+  liftIO (Pretty.renderIO handle ansiStream)++  liftIO (putStrLn "") -- Pretty printing doesn't end with a new line
dhall.cabal view
@@ -1,5 +1,5 @@ Name: dhall-Version: 1.10.0+Version: 1.11.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 8.0.1@@ -83,10 +83,68 @@     Prelude/Text/concatSep     tests/format/*.dhall     tests/normalization/*.dhall+    tests/normalization/examples/Bool/and/*.dhall+    tests/normalization/examples/Bool/build/*.dhall+    tests/normalization/examples/Bool/even/*.dhall+    tests/normalization/examples/Bool/fold/*.dhall+    tests/normalization/examples/Bool/not/*.dhall+    tests/normalization/examples/Bool/odd/*.dhall+    tests/normalization/examples/Bool/or/*.dhall+    tests/normalization/examples/Bool/show/*.dhall+    tests/normalization/examples/Double/show/*.dhall+    tests/normalization/examples/Integer/show/*.dhall+    tests/normalization/examples/List/all/*.dhall+    tests/normalization/examples/List/any/*.dhall+    tests/normalization/examples/List/build/*.dhall+    tests/normalization/examples/List/concat/*.dhall+    tests/normalization/examples/List/concatMap/*.dhall+    tests/normalization/examples/List/filter/*.dhall+    tests/normalization/examples/List/fold/*.dhall+    tests/normalization/examples/List/generate/*.dhall+    tests/normalization/examples/List/head/*.dhall+    tests/normalization/examples/List/indexed/*.dhall+    tests/normalization/examples/List/iterate/*.dhall+    tests/normalization/examples/List/last/*.dhall+    tests/normalization/examples/List/length/*.dhall+    tests/normalization/examples/List/map/*.dhall+    tests/normalization/examples/List/null/*.dhall+    tests/normalization/examples/List/replicate/*.dhall+    tests/normalization/examples/List/reverse/*.dhall+    tests/normalization/examples/List/shifted/*.dhall+    tests/normalization/examples/List/unzip/*.dhall+    tests/normalization/examples/Natural/build/*.dhall+    tests/normalization/examples/Natural/enumerate/*.dhall+    tests/normalization/examples/Natural/even/*.dhall+    tests/normalization/examples/Natural/fold/*.dhall+    tests/normalization/examples/Natural/isZero/*.dhall+    tests/normalization/examples/Natural/odd/*.dhall+    tests/normalization/examples/Natural/product/*.dhall+    tests/normalization/examples/Natural/show/*.dhall+    tests/normalization/examples/Natural/sum/*.dhall+    tests/normalization/examples/Natural/toInteger/*.dhall+    tests/normalization/examples/Optional/all/*.dhall+    tests/normalization/examples/Optional/any/*.dhall+    tests/normalization/examples/Optional/build/*.dhall+    tests/normalization/examples/Optional/concat/*.dhall+    tests/normalization/examples/Optional/filter/*.dhall+    tests/normalization/examples/Optional/fold/*.dhall+    tests/normalization/examples/Optional/head/*.dhall+    tests/normalization/examples/Optional/last/*.dhall+    tests/normalization/examples/Optional/length/*.dhall+    tests/normalization/examples/Optional/map/*.dhall+    tests/normalization/examples/Optional/null/*.dhall+    tests/normalization/examples/Optional/toList/*.dhall+    tests/normalization/examples/Optional/unzip/*.dhall+    tests/normalization/examples/Text/concat/*.dhall+    tests/normalization/examples/Text/concatMap/*.dhall+    tests/normalization/examples/Text/concatMapSep/*.dhall+    tests/normalization/examples/Text/concatSep/*.dhall+    tests/normalization/simplifications/*.dhall     tests/parser/*.dhall     tests/regression/*.dhall     tests/tutorial/*.dhall     tests/typecheck/*.dhall+    tests/typecheck/examples/Monoid/*.dhall  Source-Repository head     Type: git@@ -102,14 +160,15 @@         case-insensitive                         < 1.3 ,         containers                  >= 0.5.0.0  && < 0.6 ,         contravariant                            < 1.5 ,-        cryptohash                               < 0.12,-        exceptions                  >= 0.8.3    && < 0.9 ,+        cryptonite                  >= 0.23     && < 1.0 ,+        exceptions                  >= 0.8.3    && < 0.10,         directory                   >= 1.3      && < 1.4 ,         filepath                    >= 1.4      && < 1.5 ,         http-client                 >= 0.4.30   && < 0.6 ,         http-client-tls             >= 0.2.0    && < 0.4 ,         insert-ordered-containers   >= 0.1.0.1  && < 0.3 ,         lens-family-core            >= 1.0.0    && < 1.3 ,+        memory                      >= 0.14     && < 0.15,         parsers                     >= 0.12.4   && < 0.13,         prettyprinter               >= 1.2.0.1  && < 1.3 ,         prettyprinter-ansi-terminal >= 1.1.1    && < 1.2 ,@@ -154,6 +213,7 @@     Main-Is: Main.hs     Build-Depends:         base             >= 4        && < 5   ,+        ansi-terminal                         ,         dhall                                 ,         haskeline        >= 0.7.3.0  && < 0.8 ,         mtl              >= 2.2.1    && < 2.3 ,@@ -198,7 +258,6 @@     Main-Is: Tests.hs     GHC-Options: -Wall     Other-Modules:-        Examples         Format         Normalization         Parser
dhall/Main.hs view
@@ -36,7 +36,7 @@ data Options w = Options     { explain :: w ::: Bool <?> "Explain error messages in more detail"     , version :: w ::: Bool <?> "Display version and exit"-    , pretty  :: w ::: Bool <?> "Format output"+    , plain   :: w ::: Bool <?> "Disable syntax highlighting"     } deriving (Generic)  instance ParseRecord (Options Wrapped)@@ -46,9 +46,6 @@     Pretty.defaultLayoutOptions         { Pretty.layoutPageWidth = Pretty.AvailablePerLine 80 1.0 } -unbounded :: Pretty.LayoutOptions-unbounded = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }- main :: IO () main = do     Options {..} <- Options.Generic.unwrapRecord "Compiler for the Dhall language"@@ -96,12 +93,12 @@         let render h e = do                 let doc = prettyExpr e -                let layoutOptions = if pretty then opts else unbounded+                let layoutOptions = opts                 let stream = Pretty.layoutSmart layoutOptions doc                  supportsANSI <- System.Console.ANSI.hSupportsANSI h                 let ansiStream =-                        if supportsANSI+                        if supportsANSI && not plain                         then fmap annToAnsiStyle stream                         else Pretty.unAnnotateS stream
src/Dhall.hs view
@@ -40,8 +40,9 @@     , lazyText     , strictText     , maybe-    , vector+    , sequence     , list+    , vector     , unit     , string     , pair@@ -56,6 +57,7 @@      -- * Re-exports     , Natural+    , Seq     , Text     , Vector     , Generic@@ -67,6 +69,7 @@ import Data.Functor.Contravariant (Contravariant(..)) import Data.Monoid ((<>)) import Data.Scientific (Scientific)+import Data.Sequence (Seq) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) import Data.Typeable (Typeable)@@ -78,7 +81,7 @@ import Dhall.TypeCheck (DetailedTypeError(..), TypeError, X) import GHC.Generics import Numeric.Natural (Natural)-import Prelude hiding (maybe)+import Prelude hiding (maybe, sequence) import Text.Trifecta.Delta (Delta(..))  import qualified Control.Exception@@ -434,20 +437,18 @@ maybe :: Type a -> Type (Maybe a) maybe (Type extractIn expectedIn) = Type extractOut expectedOut   where-    extractOut (OptionalLit _ es) = traverse extractIn es'-      where-        es' = if Data.Vector.null es then Nothing else Just (Data.Vector.head es)-    extractOut _ = Nothing+    extractOut (OptionalLit _ es) = traverse extractIn es+    extractOut  _                 = Nothing      expectedOut = App Optional expectedIn -{-| Decode a `Vector`-->>> input (vector integer) "[1, 2, 3]"+{-| Decode a `Seq`+ -+>>> input (sequence integer) "[1, 2, 3]" [1,2,3] -}-vector :: Type a -> Type (Vector a)-vector (Type extractIn expectedIn) = Type extractOut expectedOut+sequence :: Type a -> Type (Seq a)+sequence (Type extractIn expectedIn) = Type extractOut expectedOut   where     extractOut (ListLit _ es) = traverse extractIn es     extractOut  _             = Nothing@@ -460,8 +461,16 @@ [1,2,3] -} list :: Type a -> Type [a]-list = fmap Data.Vector.toList . vector+list = fmap Data.Foldable.toList . sequence +{-| Decode a `Vector`++>>> input (vector integer) "[1, 2, 3]"+[1,2,3]+-}+vector :: Type a -> Type (Vector a)+vector = fmap Data.Vector.fromList . list+ {-| Decode `()` from an empty record.  >>> input unit "{=}"@@ -549,12 +558,15 @@ instance Interpret a => Interpret (Maybe a) where     autoWith opts = maybe (autoWith opts) -instance Interpret a => Interpret (Vector a) where-    autoWith opts = vector (autoWith opts)+instance Interpret a => Interpret (Seq a) where+    autoWith opts = sequence (autoWith opts)  instance Interpret a => Interpret [a] where     autoWith = fmap (fmap Data.Vector.toList) autoWith +instance Interpret a => Interpret (Vector a) where+    autoWith opts = vector (autoWith opts)+ instance (Inject a, Interpret b) => Interpret (a -> b) where     autoWith opts = Type extractOut expectedOut       where@@ -885,15 +897,15 @@     injectWith options = InputType embedOut declaredOut       where         embedOut (Just x) =-            OptionalLit declaredIn (Data.Vector.singleton (embedIn x))+            OptionalLit declaredIn (pure (embedIn x))         embedOut Nothing =-            OptionalLit declaredIn  Data.Vector.empty+            OptionalLit declaredIn  empty          InputType embedIn declaredIn = injectWith options          declaredOut = App Optional declaredIn -instance Inject a => Inject (Vector a) where+instance Inject a => Inject (Seq a) where     injectWith options = InputType embedOut declaredOut       where         embedOut xs = ListLit (Just declaredIn) (fmap embedIn xs)@@ -903,15 +915,13 @@         InputType embedIn declaredIn = injectWith options  instance Inject a => Inject [a] where-    injectWith = fmap (contramap Data.Vector.fromList) injectWith+    injectWith = fmap (contramap Data.Sequence.fromList) injectWith -instance Inject a => Inject (Data.Set.Set a) where-    injectWith = fmap (contramap go) injectWith where-        go se = Data.Vector.fromListN (Data.Set.size se) (Data.Foldable.toList se)+instance Inject a => Inject (Vector a) where+    injectWith = fmap (contramap Data.Vector.toList) injectWith -instance Inject a => Inject (Data.Sequence.Seq a) where-    injectWith = fmap (contramap go) injectWith where-        go se = Data.Vector.fromListN (Data.Sequence.length se) (Data.Foldable.toList se)+instance Inject a => Inject (Data.Set.Set a) where+    injectWith = fmap (contramap Data.Set.toList) injectWith  deriving instance (Inject a, Inject b) => Inject (a, b)
src/Dhall/Core.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes        #-} {-# LANGUAGE RecordWildCards   #-}+{-# LANGUAGE UnicodeSyntax     #-} {-# OPTIONS_GHC -Wall #-}  {-| This module contains the core calculus for the Dhall language.@@ -27,9 +28,11 @@     , Expr(..)      -- * Normalization+    , alphaNormalize     , normalize     , normalizeWith     , Normalizer+    , judgmentallyEqual     , subst     , shift     , isNormalized@@ -50,6 +53,7 @@ import Control.Applicative (Applicative(..), (<$>)) #endif import Control.Applicative (empty)+import Crypto.Hash (SHA256) import Data.Bifunctor (Bifunctor(..)) import Data.Foldable import Data.HashMap.Strict.InsOrd (InsOrdHashMap)@@ -57,29 +61,25 @@ import Data.Monoid ((<>)) import Data.String (IsString(..)) import Data.Scientific (Scientific)+import Data.Sequence (Seq, ViewL(..), ViewR(..)) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text) import Data.Text.Lazy.Builder (Builder) import Data.Text.Prettyprint.Doc (Pretty) import Data.Traversable-import Data.Vector (Vector) import {-# SOURCE #-} Dhall.Pretty.Internal import Numeric.Natural (Natural) import Prelude hiding (succ)  import qualified Control.Monad-import qualified Data.ByteString-import qualified Data.ByteString.Char8-import qualified Data.ByteString.Base16+import qualified Crypto.Hash import qualified Data.HashMap.Strict.InsOrd import qualified Data.HashSet-import qualified Data.Maybe+import qualified Data.Sequence import qualified Data.Text import qualified Data.Text.Lazy                        as Text import qualified Data.Text.Lazy.Builder                as Builder import qualified Data.Text.Prettyprint.Doc             as Pretty-import qualified Data.Vector-import qualified Data.Vector.Mutable  {-| Constants for a pure type system @@ -137,17 +137,13 @@  -- | A `PathType` extended with an optional hash for semantic integrity checks data PathHashed = PathHashed-    { hash     :: Maybe Data.ByteString.ByteString+    { hash     :: Maybe (Crypto.Hash.Digest SHA256)     , pathType :: PathType     } deriving (Eq, Ord, Show)  instance Buildable PathHashed where     build (PathHashed  Nothing p) = build p-    build (PathHashed (Just h) p) = build p <> "sha256:" <> build string <> " "-      where-        bytes = Data.ByteString.Base16.encode h--        string = Data.ByteString.Char8.unpack bytes+    build (PathHashed (Just h) p) = build p <> "sha256:" <> build (show h) <> " "  -- | Path to an external resource data Path = Path@@ -283,7 +279,7 @@     | List     -- | > ListLit (Just t ) [x, y, z]              ~  [x, y, z] : List t     --   > ListLit  Nothing  [x, y, z]              ~  [x, y, z]-    | ListLit (Maybe (Expr s a)) (Vector (Expr s a))+    | ListLit (Maybe (Expr s a)) (Seq (Expr s a))     -- | > ListAppend x y                           ~  x # y     | ListAppend (Expr s a) (Expr s a)     -- | > ListBuild                                ~  List/build@@ -302,9 +298,9 @@     | ListReverse     -- | > Optional                                 ~  Optional     | Optional-    -- | > OptionalLit t [e]                        ~  [e] : Optional t-    --   > OptionalLit t []                         ~  []  : Optional t-    | OptionalLit (Expr s a) (Vector (Expr s a))+    -- | > OptionalLit t (Just e)                   ~  [e] : Optional t+    --   > OptionalLit t Nothing                    ~  []  : Optional t+    | OptionalLit (Expr s a) (Maybe (Expr s a))     -- | > OptionalFold                             ~  Optional/fold     | OptionalFold     -- | > OptionalBuild                            ~  Optional/build@@ -851,6 +847,258 @@ -- and `subst` does nothing to a closed expression subst _ _ (Embed p) = Embed p +{-| α-normalize an expression by renaming all variables to @\"_\"@ and using+    De Bruijn indices to distinguish them+-}+alphaNormalize :: Expr s a -> Expr s a+alphaNormalize (Const c) =+    Const c+alphaNormalize (Var v) =+    Var v+alphaNormalize (Lam x _A₀ b₀) =+    Lam "_" _A₁ b₃+  where+    _A₁ = alphaNormalize _A₀++    v₀ = Var (V "_" 0)+    v₁ = shift 1 (V x 0) v₀+    b₁ = subst (V x 0) v₁ b₀+    b₂ = shift (-1) (V x 0) b₁+    b₃ = alphaNormalize b₂+alphaNormalize (Pi x _A₀ _B₀) =+    Pi "_" _A₁ _B₃+  where+    _A₁ = alphaNormalize _A₀++    v₀  = Var (V "_" 0)+    v₁  = shift 1 (V x 0) v₀+    _B₁ = subst (V x 0) v₁ _B₀+    _B₂ = shift (-1) (V x 0) _B₁+    _B₃ = alphaNormalize _B₂+alphaNormalize (App f₀ a₀) =+    App f₁ a₁+  where+    f₁ = alphaNormalize f₀++    a₁ = alphaNormalize a₀+alphaNormalize (Let x (Just _A₀) a₀ b₀) =+    Let x (Just _A₁) a₁ b₃+  where+    _A₁ = alphaNormalize _A₀++    a₁ = alphaNormalize a₀++    v₀ = Var (V "_" 0)+    v₁ = shift 1 (V x 0) v₀+    b₁ = subst (V x 0) v₁ b₀+    b₂ = shift (-1) (V x 0) b₁+    b₃ = alphaNormalize b₂+alphaNormalize (Let x Nothing a₀ b₀) =+    Let x Nothing a₁ b₃+  where+    a₁ = alphaNormalize a₀++    v₀ = Var (V "_" 0)+    v₁ = shift 1 (V x 0) v₀+    b₁ = subst (V x 0) v₁ b₀+    b₂ = shift (-1) (V x 0) b₁+    b₃ = alphaNormalize b₂+alphaNormalize (Annot t₀ _T₀) =+    Annot t₁ _T₁+  where+    t₁ = alphaNormalize t₀++    _T₁ = alphaNormalize _T₀+alphaNormalize Bool =+    Bool+alphaNormalize (BoolLit b) =+    BoolLit b+alphaNormalize (BoolAnd l₀ r₀) =+    BoolAnd l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (BoolOr l₀ r₀) =+    BoolOr l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (BoolEQ l₀ r₀) =+    BoolEQ l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (BoolNE l₀ r₀) =+    BoolNE l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (BoolIf t₀ l₀ r₀) =+    BoolIf t₁ l₁ r₁+  where+    t₁ = alphaNormalize t₀++    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize Natural =+    Natural+alphaNormalize (NaturalLit n) =+    NaturalLit n+alphaNormalize NaturalFold =+    NaturalFold+alphaNormalize NaturalBuild =+    NaturalBuild+alphaNormalize NaturalIsZero =+    NaturalIsZero+alphaNormalize NaturalEven =+    NaturalEven+alphaNormalize NaturalOdd =+    NaturalOdd+alphaNormalize NaturalToInteger =+    NaturalToInteger+alphaNormalize NaturalShow =+    NaturalShow+alphaNormalize (NaturalPlus l₀ r₀) =+    NaturalPlus l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (NaturalTimes l₀ r₀) =+    NaturalTimes l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize Integer =+    Integer+alphaNormalize (IntegerLit n) =+    IntegerLit n+alphaNormalize IntegerShow =+    IntegerShow+alphaNormalize Double =+    Double+alphaNormalize (DoubleLit n) =+    DoubleLit n+alphaNormalize DoubleShow =+    DoubleShow+alphaNormalize Text =+    Text+alphaNormalize (TextLit (Chunks xys₀ z)) =+    TextLit (Chunks xys₁ z)+  where+    xys₁ = do+        (x, y₀) <- xys₀+        let y₁ = alphaNormalize y₀+        return (x, y₁)+alphaNormalize (TextAppend l₀ r₀) =+    TextAppend l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize List =+    List+alphaNormalize (ListLit (Just _T₀) ts₀) =+    ListLit (Just _T₁) ts₁+  where+    _T₁ = alphaNormalize _T₀++    ts₁ = fmap alphaNormalize ts₀+alphaNormalize (ListLit Nothing ts₀) =+    ListLit Nothing ts₁+  where+    ts₁ = fmap alphaNormalize ts₀+alphaNormalize (ListAppend l₀ r₀) =+    ListAppend l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize ListBuild =+    ListBuild+alphaNormalize ListFold =+    ListFold+alphaNormalize ListLength =+    ListLength+alphaNormalize ListHead =+    ListHead+alphaNormalize ListLast =+    ListLast+alphaNormalize ListIndexed =+    ListIndexed+alphaNormalize ListReverse =+    ListReverse+alphaNormalize Optional =+    Optional+alphaNormalize (OptionalLit _T₀ ts₀) =+    OptionalLit _T₁ ts₁+  where+    _T₁ = alphaNormalize _T₀++    ts₁ = fmap alphaNormalize ts₀+alphaNormalize OptionalFold =+    OptionalFold+alphaNormalize OptionalBuild =+    OptionalBuild+alphaNormalize (Record kts₀) =+    Record kts₁+  where+    kts₁ = fmap alphaNormalize kts₀+alphaNormalize (RecordLit kvs₀) =+    RecordLit kvs₁+  where+    kvs₁ = fmap alphaNormalize kvs₀+alphaNormalize (Union kts₀) =+    Union kts₁+  where+    kts₁ = fmap alphaNormalize kts₀+alphaNormalize (UnionLit k v₀ kts₀) =+    UnionLit k v₁ kts₁+  where+    v₁ = alphaNormalize v₀++    kts₁ = fmap alphaNormalize kts₀+alphaNormalize (Combine l₀ r₀) =+    Combine l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (Prefer l₀ r₀) =+    Prefer l₁ r₁+  where+    l₁ = alphaNormalize l₀++    r₁ = alphaNormalize r₀+alphaNormalize (Merge t₀ u₀ _T₀) =+    Merge t₁ u₁ _T₁+  where+    t₁ = alphaNormalize t₀++    u₁ = alphaNormalize u₀++    _T₁ = fmap alphaNormalize _T₀+alphaNormalize (Constructors u₀) =+    Constructors u₁+  where+    u₁ = alphaNormalize u₀+alphaNormalize (Field e₀ a) =+    Field e₁ a+  where+    e₁ = alphaNormalize e₀+alphaNormalize (Note s e₀) =+    Note s e₁+  where+    e₁ = alphaNormalize e₀+alphaNormalize (Embed a) =+    Embed a+ {-| Reduce an expression to its normal form, performing beta reduction      `normalize` does not type-check the expression.  You may want to type-check@@ -860,7 +1108,7 @@     However, `normalize` will not fail if the expression is ill-typed and will     leave ill-typed sub-expressions unevaluated. -}-normalize ::  Expr s a -> Expr t a+normalize :: Eq a => Expr s a -> Expr t a normalize = normalizeWith (const Nothing)  {-| This function is used to determine whether folds like @Natural/fold@ or@@ -949,30 +1197,22 @@  {-| Reduce an expression to its normal form, performing beta reduction and applying     any custom definitions.-   +     `normalizeWith` is designed to be used with function `typeWith`. The `typeWith`-    function allows typing of Dhall functions in a custom typing context whereas -    `normalizeWith` allows evaluating Dhall expressions in a custom context. +    function allows typing of Dhall functions in a custom typing context whereas+    `normalizeWith` allows evaluating Dhall expressions in a custom context.      To be more precise `normalizeWith` applies the given normalizer when it finds an     application term that it cannot reduce by other means.      Note that the context used in normalization will determine the properties of normalization.     That is, if the functions in custom context are not total then the Dhall language, evaluated-    with those functions is not total either.  -   +    with those functions is not total either.+ -}-normalizeWith :: Normalizer a -> Expr s a -> Expr t a+normalizeWith :: Eq a => Normalizer a -> Expr s a -> Expr t a normalizeWith ctx e0 = loop (denote e0)  where-    -- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of-    -- `loop`.  In theory, this might change a failing repro case into-    -- a successful one, but the risk of that is low enough to not warrant-    -- the `Show` constraint.  I care more about proving at the type level-    -- that the @a@ and @s@ type parameters are never used- e'' = bimap (\_ -> ()) (\_ -> ()) e0-- text = "NormalizeWith.loop (" <> Data.Text.pack (show e'') <> ")"  loop e =  case e of     Const k -> Const k     Var v -> Var v@@ -991,16 +1231,14 @@             b'  = subst (V x 0) a' b             b'' = shift (-1) (V x 0) b'         f' -> case App f' a' of-            -- fold/build fusion for `List`+            -- build/fold fusion for `List`             App (App ListBuild _) (App (App ListFold _) e') -> loop e'-            App (App ListFold _) (App (App ListBuild _) e') -> loop e'-            -- fold/build fusion for `Natural`++            -- build/fold fusion for `Natural`             App NaturalBuild (App NaturalFold e') -> loop e'-            App NaturalFold (App NaturalBuild e') -> loop e' -            -- fold/build fusion for `Optional`+            -- build/fold fusion for `Optional`             App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'-            App (App OptionalFold _) (App (App OptionalBuild _) e') -> loop e'              App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero ->                 if boundedType (loop t) then strict else lazy@@ -1013,23 +1251,11 @@                  lazyLoop !0 = zero                 lazyLoop !n = App succ' (lazyLoop (n - 1))-            App NaturalBuild k-                | check     -> NaturalLit n-                | otherwise -> App f' a'+            App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)               where-                labeled =-                    loop (App (App (App k Natural) "Succ") "Zero")+                succ = Lam "x" Natural (NaturalPlus "x" (NaturalLit 1)) -                n = go 0 labeled-                  where-                    go !m (App (Var "Succ") e') = go (m + 1) e'-                    go !m (Var "Zero")          = m-                    go !_  _                    = internalError text-                check = go labeled-                  where-                    go (App (Var "Succ") e') = go e'-                    go (Var "Zero")          = True-                    go  _                    = False+                zero = NaturalLit 0             App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)             App NaturalEven (NaturalLit n) -> BoolLit (even n)             App NaturalOdd (NaturalLit n) -> BoolLit (odd n)@@ -1040,44 +1266,35 @@                 TextLit (Chunks [] (buildNumber n))             App DoubleShow (DoubleLit n) ->                 TextLit (Chunks [] (buildScientific n))-            App (App OptionalBuild t) k-                | check     -> OptionalLit t k'-                | otherwise -> App f' a'+            App (App OptionalBuild _A₀) g ->+                loop (App (App (App g optional) just) nothing)               where-                labeled = loop (App (App (App k (App Optional t)) "Just") "Nothing")+                _A₁ = shift 1 "a" _A₀ -                k' = go labeled-                  where-                    go (App (Var "Just") e') = pure e'-                    go (Var "Nothing")       = empty-                    go  _                    = internalError text-                check = go labeled-                  where-                    go (App (Var "Just") _) = True-                    go (Var "Nothing")      = True-                    go  _                   = False-            App (App ListBuild t) k-                | check     -> ListLit (Just t) (buildVector k')-                | otherwise -> App f' a'+                optional = App Optional _A₀++                just = Lam "a" _A₀ (OptionalLit _A₁ (pure "a"))++                nothing = OptionalLit _A₀ empty+            App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)               where-                labeled =-                    loop (App (App (App k (App List t)) "Cons") "Nil")+                _A₁ = shift 1 "a" _A₀ -                k' cons nil = go labeled-                  where-                    go (App (App (Var "Cons") x) e') = cons x (go e')-                    go (Var "Nil")                   = nil-                    go  _                            = internalError text-                check = go labeled-                  where-                    go (App (App (Var "Cons") _) e') = go e'-                    go (Var "Nil")                   = True-                    go  _                            = False+                list = App List _A₀++                cons =+                    Lam "a" _A₀+                        (Lam "as"+                            (App List _A₁)+                            (ListAppend (ListLit Nothing (pure "a")) "as")+                        )++                nil = ListLit (Just _A₀) empty             App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil ->                 if boundedType (loop t) then strict else lazy               where-                strict =       Data.Vector.foldr strictCons strictNil xs-                lazy   = loop (Data.Vector.foldr   lazyCons   lazyNil xs)+                strict =       foldr strictCons strictNil xs+                lazy   = loop (foldr   lazyCons   lazyNil xs)                  strictNil = loop nil                 lazyNil   =      nil@@ -1085,35 +1302,42 @@                 strictCons y ys = loop (App (App cons y) ys)                 lazyCons   y ys =       App (App cons y) ys             App (App ListLength _) (ListLit _ ys) ->-                NaturalLit (fromIntegral (Data.Vector.length ys))-            App (App ListHead t) (ListLit _ ys) ->-                loop (OptionalLit t (Data.Vector.take 1 ys))-            App (App ListLast t) (ListLit _ ys) ->-                loop (OptionalLit t y)+                NaturalLit (fromIntegral (Data.Sequence.length ys))+            App (App ListHead t) (ListLit _ ys) -> loop (OptionalLit t m)               where-                y = if Data.Vector.null ys-                    then Data.Vector.empty-                    else Data.Vector.singleton (Data.Vector.last ys)-            App (App ListIndexed t) (ListLit _ xs) ->-                loop (ListLit (Just t') (fmap adapt (Data.Vector.indexed xs)))+                m = case Data.Sequence.viewl ys of+                        y :< _ -> Just y+                        _      -> Nothing+            App (App ListLast t) (ListLit _ ys) -> loop (OptionalLit t m)               where-                t' = Record (Data.HashMap.Strict.InsOrd.fromList kts)+                m = case Data.Sequence.viewr ys of+                        _ :> y -> Just y+                        _      -> Nothing+            App (App ListIndexed _A₀) (ListLit _A₁ as₀) ->+                loop (ListLit (Just _A₂) as₁)+              where+                as₁ = Data.Sequence.mapWithIndex adapt as₀++                _A₂ = Record (Data.HashMap.Strict.InsOrd.fromList kts)                   where                     kts = [ ("index", Natural)-                          , ("value", t)+                          , ("value", _A₀)                           ]-                adapt (n, x) = RecordLit (Data.HashMap.Strict.InsOrd.fromList kvs)++                adapt n a_ =+                    RecordLit (Data.HashMap.Strict.InsOrd.fromList kvs)                   where                     kvs = [ ("index", NaturalLit (fromIntegral n))-                          , ("value", x)+                          , ("value", a_)                           ]             App (App ListReverse t) (ListLit _ xs) ->-                loop (ListLit (Just t) (Data.Vector.reverse xs))+                loop (ListLit m (Data.Sequence.reverse xs))+              where+                m = if Data.Sequence.null xs then Just t else Nothing             App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing ->-                loop (maybe nothing just' (toMaybe xs))+                loop (maybe nothing just' xs)               where-                just' y = App just y-                toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList+                just' = App just             _ ->  case ctx (App f' a') of                     Nothing -> App f' a'                     Just app' -> loop app'@@ -1127,53 +1351,46 @@     Annot x _ -> loop x     Bool -> Bool     BoolLit b -> BoolLit b-    BoolAnd x y ->-        case x' of-            BoolLit xn ->-                case y' of-                    BoolLit yn -> BoolLit (xn && yn)-                    _ -> BoolAnd x' y'-            _ -> BoolAnd x' y'+    BoolAnd x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y-    BoolOr x y ->-        case x' of-            BoolLit xn ->-                case y' of-                    BoolLit yn -> BoolLit (xn || yn)-                    _ -> BoolOr x' y'-            _ -> BoolOr x' y'+        decide (BoolLit True )  r              = r+        decide (BoolLit False)  _              = BoolLit False+        decide  l              (BoolLit True ) = l+        decide  _              (BoolLit False) = BoolLit False+        decide  l               r+            | judgmentallyEqual l r = l+            | otherwise             = BoolAnd l r+    BoolOr x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y-    BoolEQ x y ->-        case x' of-            BoolLit xn ->-                case y' of-                    BoolLit yn -> BoolLit (xn == yn)-                    _ -> BoolEQ x' y'-            _ -> BoolEQ x' y'+        decide (BoolLit False)  r              = r+        decide (BoolLit True )  _              = BoolLit True+        decide  l              (BoolLit False) = l+        decide  _              (BoolLit True ) = BoolLit True+        decide  l               r+            | judgmentallyEqual l r = l+            | otherwise             = BoolOr l r+    BoolEQ x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y-    BoolNE x y ->-        case x' of-            BoolLit xn ->-                case y' of-                    BoolLit yn -> BoolLit (xn /= yn)-                    _ -> BoolNE x' y'-            _ -> BoolNE x' y'+        decide (BoolLit True )  r              = r+        decide  l              (BoolLit True ) = l+        decide  l               r+            | judgmentallyEqual l r = BoolLit True+            | otherwise             = BoolEQ l r+    BoolNE x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y-    BoolIf b true false -> case loop b of-        BoolLit True  -> true'-        BoolLit False -> false'-        b'            -> BoolIf b' true' false'+        decide (BoolLit False)  r              = r+        decide  l              (BoolLit False) = l+        decide  l               r+            | judgmentallyEqual l r = BoolLit False+            | otherwise             = BoolNE l r+    BoolIf bool true false -> decide (loop bool) (loop true) (loop false)       where-        true'  = loop true-        false' = loop false+        decide (BoolLit True )  l              _              = l+        decide (BoolLit False)  _              r              = r+        decide  b              (BoolLit True) (BoolLit False) = b+        decide  b               l              r+            | judgmentallyEqual l r = l+            | otherwise             = BoolIf b l r     Natural -> Natural     NaturalLit n -> NaturalLit n     NaturalFold -> NaturalFold@@ -1183,26 +1400,20 @@     NaturalOdd -> NaturalOdd     NaturalToInteger -> NaturalToInteger     NaturalShow -> NaturalShow-    NaturalPlus  x y ->-        case x' of-            NaturalLit xn ->-                case y' of-                    NaturalLit yn -> NaturalLit (xn + yn)-                    _ -> NaturalPlus x' y'-            _ -> NaturalPlus x' y'+    NaturalPlus x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y-    NaturalTimes x y ->-        case x' of-            NaturalLit xn ->-                case y' of-                    NaturalLit yn -> NaturalLit (xn * yn)-                    _ -> NaturalTimes x' y'-            _ -> NaturalTimes x' y'+        decide (NaturalLit 0)  r             = r+        decide  l             (NaturalLit 0) = l+        decide (NaturalLit m) (NaturalLit n) = NaturalLit (m + n)+        decide  l              r             = NaturalPlus l r+    NaturalTimes x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y+        decide (NaturalLit 1)  r             = r+        decide  l             (NaturalLit 1) = l+        decide (NaturalLit 0)  _             = NaturalLit 0+        decide  _             (NaturalLit 0) = NaturalLit 0+        decide (NaturalLit m) (NaturalLit n) = NaturalLit (m * n)+        decide  l              r             = NaturalTimes l r     Integer -> Integer     IntegerLit n -> IntegerLit n     IntegerShow -> IntegerShow@@ -1220,31 +1431,26 @@         process (x, y) = case loop y of             TextLit c -> [Chunks [] x, c]             y'        -> [Chunks [(x, y')] mempty]-    TextAppend x y   ->-        case x' of-            TextLit xt ->-                case y' of-                    TextLit yt -> TextLit (xt <> yt)-                    _ -> TextAppend x' y'-            _ -> TextAppend x' y'+    TextAppend x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y+        isEmpty (Chunks [] "") = True+        isEmpty  _             = False++        decide (TextLit m)  r          | isEmpty m = r+        decide  l          (TextLit n) | isEmpty n = l+        decide (TextLit m) (TextLit n)             = TextLit (m <> n)+        decide  l           r                      = TextAppend l r     List -> List     ListLit t es -> ListLit t' es'       where         t'  = fmap loop t         es' = fmap loop es-    ListAppend x y ->-        case x' of-            ListLit t xs ->-                case y' of-                    ListLit _ ys -> ListLit t (xs <> ys)-                    _ -> ListAppend x' y'-            _ -> ListAppend x' y'+    ListAppend x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y+        decide (ListLit _ m)  r            | Data.Sequence.null m = r+        decide  l            (ListLit _ n) | Data.Sequence.null n = l+        decide (ListLit t m) (ListLit _ n)                        = ListLit t (m <> n)+        decide  l             r                                   = ListAppend l r     ListBuild -> ListBuild     ListFold -> ListFold     ListLength -> ListLength@@ -1272,26 +1478,26 @@       where         v'   =      loop v         kvs' = fmap loop kvs-    Combine x0 y0 ->-        let combine x y = case x of-                RecordLit kvsX -> case y of-                    RecordLit kvsY ->-                        let kvs = Data.HashMap.Strict.InsOrd.unionWith combine kvsX kvsY-                        in  RecordLit (fmap loop kvs)-                    _ -> Combine x y-                _ -> Combine x y-        in  combine (loop x0) (loop y0)-    Prefer x y ->-        case x' of-            RecordLit kvsX ->-                case y' of-                    RecordLit kvsY ->-                        RecordLit (fmap loop (Data.HashMap.Strict.InsOrd.union kvsY kvsX))-                    _ -> Prefer x' y'-            _ -> Prefer x' y'+    Combine x y -> decide (loop x) (loop y)       where-        x' = loop x-        y' = loop y+        decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m =+            r+        decide l (RecordLit n) | Data.HashMap.Strict.InsOrd.null n =+            l+        decide (RecordLit m) (RecordLit n) =+            RecordLit (Data.HashMap.Strict.InsOrd.unionWith decide m n)+        decide l r =+            Combine l r+    Prefer x y -> decide (loop x) (loop y)+      where+        decide (RecordLit m) r | Data.HashMap.Strict.InsOrd.null m =+            r+        decide l (RecordLit n) | Data.HashMap.Strict.InsOrd.null n =+            l+        decide (RecordLit m) (RecordLit n) =+            RecordLit (Data.HashMap.Strict.InsOrd.union n m)+        decide l r =+            Prefer l r     Merge x y t      ->         case x' of             RecordLit kvsX ->@@ -1328,13 +1534,22 @@     Note _ e' -> loop e'     Embed a -> Embed a +{-| Returns `True` if two expressions are α-equivalent and β-equivalent and+    `False` otherwise+-}+judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool+judgmentallyEqual eL0 eR0 = alphaBetaNormalize eL0 == alphaBetaNormalize eR0+  where+    alphaBetaNormalize :: Eq a => Expr s a -> Expr () a+    alphaBetaNormalize = alphaNormalize . normalize+ -- | Use this to wrap you embedded functions (see `normalizeWith`) to make them --   polymorphic enough to be used. type Normalizer a = forall s. Expr s a -> Maybe (Expr s a)  -- | Check if an expression is in a normal form given a context of evaluation.---   Unlike `isNormalized`, this will fully normalize and traverse through the expression. ---   +--   Unlike `isNormalized`, this will fully normalize and traverse through the expression.+-- --   It is much more efficient to use `isNormalized`. isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool isNormalizedWith ctx e = e == (normalizeWith ctx e)@@ -1350,28 +1565,17 @@     App f a -> isNormalized f && isNormalized a && case App f a of         App (Lam _ _ _) _ -> False -        -- fold/build fusion for `List`+        -- build/fold fusion for `List`         App (App ListBuild _) (App (App ListFold _) _) -> False-        App (App ListFold _) (App (App ListBuild _) _) -> False -        -- fold/build fusion for `Natural`+        -- build/fold fusion for `Natural`         App NaturalBuild (App NaturalFold _) -> False-        App NaturalFold (App NaturalBuild _) -> False -        -- fold/build fusion for `Optional`+        -- build/fold fusion for `Optional`         App (App OptionalBuild _) (App (App OptionalFold _) _) -> False-        App (App OptionalFold _) (App (App OptionalBuild _) _) -> False          App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False-        App NaturalBuild k0 -> isNormalized k0 && not (check0 k0)-          where-            check0 (Lam _ _ (Lam succ _ (Lam zero _ k))) = check1 succ zero k-            check0 _ = False--            check1 succ zero (App (Var (V succ' n)) k) =-                succ == succ' && n == (if succ == zero then 1 else 0) && check1 succ zero k-            check1 _ zero (Var (V zero' 0)) = zero == zero'-            check1 _ _ _ = False+        App NaturalBuild _ -> False         App NaturalIsZero (NaturalLit _) -> False         App NaturalEven (NaturalLit _) -> False         App NaturalOdd (NaturalLit _) -> False@@ -1379,24 +1583,8 @@         App NaturalToInteger (NaturalLit _) -> False         App IntegerShow (IntegerLit _) -> False         App DoubleShow (DoubleLit _) -> False-        App (App OptionalBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0)-          where-            check0 (Lam _ _ (Lam just _ (Lam nothing _ k))) = check1 just nothing k-            check0 _ = False--            check1 just nothing (App (Var (V just' n)) _) =-                just == just' && n == (if just == nothing then 1 else 0)-            check1 _ nothing (Var (V nothing' 0)) = nothing == nothing'-            check1 _ _ _ = False-        App (App ListBuild t) k0 -> isNormalized t && isNormalized k0 && not (check0 k0)-          where-            check0 (Lam _ _ (Lam cons _ (Lam nil _ k))) = check1 cons nil k-            check0 _ = False--            check1 cons nil (App (Var (V cons' n)) k) =-                cons == cons' && n == (if cons == nil then 1 else 0) && check1 cons nil k-            check1 _ nil (Var (V nil' 0)) = nil == nil'-            check1 _ _ _ = False+        App (App OptionalBuild _) _ -> False+        App (App ListBuild _) _ -> False         App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ ->             False         App (App ListLength _) (ListLit _ _) -> False@@ -1564,25 +1752,6 @@     , Data.Text.unpack text <> "                                                       "     , "```                                                                             "     ] )--buildVector :: (forall x . (a -> x -> x) -> x -> x) -> Vector a-buildVector f = Data.Vector.reverse (Data.Vector.create (do-    let cons a st = do-            (len, cap, mv) <- st-            if len < cap-                then do-                    Data.Vector.Mutable.write mv len a-                    return (len + 1, cap, mv)-                else do-                    let cap' = 2 * cap-                    mv' <- Data.Vector.Mutable.unsafeGrow mv cap'-                    Data.Vector.Mutable.write mv' len a-                    return (len + 1, cap', mv')-    let nil = do-            mv <- Data.Vector.Mutable.unsafeNew 1-            return (0, 1, mv)-    (len, _, mv) <- f cons nil-    return (Data.Vector.Mutable.slice 0 len mv) ))  -- | The set of reserved identifiers for the Dhall language reservedIdentifiers :: HashSet Text
src/Dhall/Import.hs view
@@ -71,7 +71,7 @@     > $ export BAZ='λ(x : Bool) → x == False'     > $ dhall <<< "{ foo = env:FOO , bar = env:BAR , baz = env:BAZ }"     > { bar : Text, baz : ∀(x : Bool) → Bool, foo : Integer }-    > +    >     > { bar = "Hi", baz = λ(x : Bool) → x == False, foo = 1 }      If you wish to import the raw contents of a path as @Text@ then add@@ -79,19 +79,19 @@      > $ dhall <<< "http://example.com as Text"     > Text-    > +    >     > "<!doctype html>\n<html>\n<head>\n    <title>Example Domain</title>\n\n    <meta     >  charset=\"utf-8\" />\n    <meta http-equiv=\"Content-type\" content=\"text/html-    > ; charset=utf-8\" />\n    <meta name=\"viewport\" content=\"width=device-width, +    > ; charset=utf-8\" />\n    <meta name=\"viewport\" content=\"width=device-width,     > initial-scale=1\" />\n    <style type=\"text/css\">\n    body {\n        backgro     > und-color: #f0f0f2;\n        margin: 0;\n        padding: 0;\n        font-famil-    > y: \"Open Sans\", \"Helvetica Neue\", Helvetica, Arial, sans-serif;\n        \n +    > y: \"Open Sans\", \"Helvetica Neue\", Helvetica, Arial, sans-serif;\n        \n     >    }\n    div {\n        width: 600px;\n        margin: 5em auto;\n        paddi     > ng: 50px;\n        background-color: #fff;\n        border-radius: 1em;\n    }\n     >     a:link, a:visited {\n        color: #38488f;\n        text-decoration: none;     > \n    }\n    @media (max-width: 700px) {\n        body {\n            background     > -color: #fff;\n        }\n        div {\n            width: auto;\n            m-    > argin: 0 auto;\n            border-radius: 0;\n            padding: 1em;\n      +    > argin: 0 auto;\n            border-radius: 0;\n            padding: 1em;\n     >   }\n    }\n    </style>    \n</head>\n\n<body>\n<div>\n    <h1>Example Domain</     > h1>\n    <p>This domain is established to be used for illustrative examples in d     > ocuments. You may use this\n    domain in examples without prior coordination or@@ -124,6 +124,7 @@ import Control.Monad.Catch (throwM, MonadCatch(catch)) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Trans.State.Strict (StateT)+import Crypto.Hash (SHA256) import Data.ByteString.Lazy (ByteString) import Data.CaseInsensitive (CI) import Data.Map (Map)@@ -160,12 +161,13 @@ import Text.Trifecta.Delta (Delta(..))  import qualified Control.Monad.Trans.State.Strict as State-import qualified Crypto.Hash.SHA256+import qualified Crypto.Hash+import qualified Data.ByteArray import qualified Data.ByteString-import qualified Data.ByteString.Base16 import qualified Data.ByteString.Char8 import qualified Data.ByteString.Lazy import qualified Data.CaseInsensitive+import qualified Data.Foldable import qualified Data.List                        as List import qualified Data.HashMap.Strict.InsOrd import qualified Data.Map.Strict                  as Map@@ -175,7 +177,6 @@ import qualified Data.Text.Lazy.Builder           as Builder import qualified Data.Text.Lazy.Encoding import qualified Data.Text.Lazy.IO-import qualified Data.Vector import qualified Dhall.Core import qualified Dhall.Parser import qualified Dhall.Context@@ -481,7 +482,7 @@   -> Maybe [(CI Data.ByteString.ByteString, Data.ByteString.ByteString)] toHeaders (ListLit _ hs) = do     hs' <- mapM toHeader hs-    return (Data.Vector.toList hs')+    return (Data.Foldable.toList hs') toHeaders  _             = do     empty @@ -534,8 +535,8 @@  -- | Exception thrown when an integrity check fails data HashMismatch = HashMismatch-    { expectedHash :: Data.ByteString.ByteString-    , actualHash   :: Data.ByteString.ByteString+    { expectedHash :: Crypto.Hash.Digest SHA256+    , actualHash   :: Crypto.Hash.Digest SHA256     } deriving (Typeable)  instance Exception HashMismatch@@ -547,14 +548,11 @@         <>  "\n"         <>  "Expected hash:\n"         <>  "\n"-        <>  "↳ " <> toString expectedHash <> "\n"+        <>  "↳ " <> show expectedHash <> "\n"         <>  "\n"         <>  "Actual hash:\n"         <>  "\n"-        <>  "↳ " <> toString actualHash <> "\n"-      where-        toString =-            Data.ByteString.Char8.unpack . Data.ByteString.Base16.encode+        <>  "↳ " <> show actualHash <> "\n"  parseFromFileEx     :: Text.Trifecta.Parser a@@ -849,8 +847,8 @@ load = loadWithContext Dhall.Context.empty  -- | Hash a fully resolved expression-hashExpression :: Expr s X -> Data.ByteString.ByteString-hashExpression expr = Crypto.Hash.SHA256.hashlazy actualBytes+hashExpression :: Expr s X -> (Crypto.Hash.Digest SHA256)+hashExpression expr = Crypto.Hash.hashlazy actualBytes   where     text = Dhall.Core.pretty (Dhall.Core.normalize expr)     actualBytes = Data.Text.Lazy.Encoding.encodeUtf8 text@@ -866,7 +864,7 @@   where     bytes = hashExpression expr -    bytes16 = Data.ByteString.Base16.encode bytes+    bytes16 = Data.ByteArray.convert bytes      -- Notes that `decodeUtf8` is partial, but the base16-encoded bytestring     -- should always successfully decode
src/Dhall/Parser.hs view
@@ -44,7 +44,7 @@ import Text.Trifecta.Delta (Delta)  import qualified Control.Monad-import qualified Data.ByteString.Base16.Lazy+import qualified Crypto.Hash import qualified Data.ByteString.Lazy import qualified Data.Char import qualified Data.HashMap.Strict.InsOrd@@ -56,7 +56,6 @@ import qualified Data.Text.Lazy import qualified Data.Text.Lazy.Builder import qualified Data.Text.Lazy.Encoding-import qualified Data.Vector import qualified Text.Parser.Char import qualified Text.Parser.Combinators import qualified Text.Parser.Token@@ -1070,15 +1069,15 @@     _colon     a <- alternative0 <|> alternative1     b <- selectorExpression embedded-    return (a b empty)+    return (a b)   where     alternative0 = do         _List-        return (\a b -> ListLit (Just a) b)+        return (\a -> ListLit (Just a) empty)      alternative1 = do         _Optional-        return OptionalLit+        return (\a -> OptionalLit a empty)  nonEmptyOptional :: Parser a -> Parser (Expr Src a) nonEmptyOptional embedded = do@@ -1459,7 +1458,7 @@     a <- expression embedded     b <- many (do _comma; expression embedded)     _closeBracket-    return (ListLit Nothing (Data.Vector.fromList (a:b))) ) <?> "list literal"+    return (ListLit Nothing (Data.Sequence.fromList (a:b))) ) <?> "list literal"  completeExpression :: Parser a -> Parser (Expr Src a) completeExpression embedded = do@@ -1510,10 +1509,9 @@         whitespace         let lazyText = Data.Text.Lazy.Builder.toLazyText builder         let lazyBytes = Data.Text.Lazy.Encoding.encodeUtf8 lazyText-        let (hash, suffix) = Data.ByteString.Base16.Lazy.decode lazyBytes-        if Data.ByteString.Lazy.null suffix-            then return (Data.ByteString.Lazy.toStrict hash)-            else fail "Invalid sha256 hash"+        case Crypto.Hash.digestFromByteString (Data.ByteString.Lazy.toStrict lazyBytes) of+          Nothing -> fail "Invalid sha256 hash"+          Just h -> pure h  import_ :: Parser Path import_ = (do
src/Dhall/Pretty/Internal.hs view
@@ -46,7 +46,6 @@ import qualified Data.Text.Lazy.Builder                as Builder import qualified Data.Text.Prettyprint.Doc             as Pretty import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty-import qualified Data.Vector  {-| Annotation type used to tag elements in a pretty-printed document for     syntax highlighting purposes@@ -433,13 +432,13 @@     docs d =         [ prettyExprB d ] prettyExprB (ListLit Nothing b) =-    list (map prettyExprA (Data.Vector.toList b))+    list (map prettyExprA (Data.Foldable.toList b)) prettyExprB (ListLit (Just a) b) =-        list (map prettyExprA (Data.Vector.toList b))+        list (map prettyExprA (Data.Foldable.toList b))     <>  " : "     <>  prettyExprD (App List a) prettyExprB (OptionalLit a b) =-        list (map prettyExprA (Data.Vector.toList b))+        list (map prettyExprA (Data.Foldable.toList b))     <>  " : "     <>  prettyExprD (App Optional a) prettyExprB (Merge a b (Just c)) =@@ -702,7 +701,7 @@ prettyExprF (UnionLit a b c) =     prettyUnionLit a b c prettyExprF (ListLit Nothing b) =-    list (map prettyExprA (Data.Vector.toList b))+    list (map prettyExprA (Data.Foldable.toList b)) prettyExprF (Embed a) =     Pretty.pretty a prettyExprF (Note _ b) =@@ -886,11 +885,11 @@     <>  " in "     <>  buildExprB d buildExprB (ListLit Nothing b) =-    "[" <> buildElems (Data.Vector.toList b) <> "]"+    "[" <> buildElems (Data.Foldable.toList b) <> "]" buildExprB (ListLit (Just a) b) =-    "[" <> buildElems (Data.Vector.toList b) <> "] : List "  <> buildExprE a+    "[" <> buildElems (Data.Foldable.toList b) <> "] : List "  <> buildExprE a buildExprB (OptionalLit a b) =-    "[" <> buildElems (Data.Vector.toList b) <> "] : Optional "  <> buildExprE a+    "[" <> buildElems (Data.Foldable.toList b) <> "] : Optional "  <> buildExprE a buildExprB (Merge a b (Just c)) =     "merge " <> buildExprE a <> " " <> buildExprE b <> " : " <> buildExprD c buildExprB (Merge a b Nothing) =@@ -1054,7 +1053,7 @@ buildExprF (UnionLit a b c) =     buildUnionLit a b c buildExprF (ListLit Nothing b) =-    "[" <> buildElems (Data.Vector.toList b) <> "]"+    "[" <> buildElems (Data.Foldable.toList b) <> "]" buildExprF (Embed a) =     build a buildExprF (Note _ b) =
src/Dhall/Tutorial.hs view
@@ -474,12 +474,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: ----- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not> -- -- Visit that link and read the documentation.  Then try to guess what this -- code returns: ----- > >>> input auto "https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool+-- > >>> input auto "https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess@@ -966,7 +966,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall--- > let not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not+-- > let not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not -- > in  not True -- > <Ctrl-D> -- > Bool@@ -1115,7 +1115,7 @@ -- common pattern: -- -- >     let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >--- > in  [   MyType.Empty {}+-- > in  [   MyType.Empty {=} -- >     ,   MyType.Person { name = "John", age = +23 } -- >     ,   MyType.Person { name = "Amy" , age = +25 } -- >     ]@@ -1324,7 +1324,7 @@ -- complex example: -- -- > $ dhall--- >     let Prelude/List/map = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map+-- >     let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- > in  λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3] -- > <Ctrl-D> -- > ∀(f : Integer → Integer) → List Integer@@ -1348,11 +1348,11 @@ -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: ----- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate>+-- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate> -- -- Test what the following Dhall expression normalizes to: ----- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate+-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate -- > in  replicate +10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by@@ -1604,22 +1604,22 @@ -- normalizing them: -- -- > $ dhall-format--- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate  -- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) -- > <Ctrl-D> -- >     let replicate =--- >           https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- >           https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate  -- >  -- > in  replicate -- >     +5 -- >     (List (List Integer)) -- >     (replicate +5 (List Integer) (replicate +5 Integer 1)) ----- If you want to evaluate and format an expression then you can combine the--- @dhall@ and @dhall-format@ executables:+-- If you want to evaluate and format an expression then you can use the+-- @--pretty@ flag of the @dhall@ executable: ----- > $ dhall | dhall-format--- > let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate +-- > $ dhall --pretty+-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate  -- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1)) -- > <Ctrl-D> -- > List (List (List Integer))@@ -2283,7 +2283,7 @@ -- -- Rules: ----- > let Prelude/List/concat = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat+-- > let Prelude/List/concat = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat -- > -- > List/fold a (Prelude/List/concat a xss) b c -- >     = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)@@ -2352,10 +2352,10 @@ -- -- Rules: ----- > let Prelude/Optional/head  = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/head--- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat--- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap--- > let Prelude/List/map       = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map+-- > let Prelude/Optional/head  = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/head+-- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat+-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap+-- > let Prelude/List/map       = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- >  -- > List/head a (Prelude/List/concat a xss) = -- >     Prelude/Optional/head a (Prelude/List/map (List a) (Optional a) (List/head a) xss)@@ -2383,10 +2383,10 @@ -- -- Rules: ----- > let Prelude/Optional/last  = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Optional/last--- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat--- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap--- > let Prelude/List/map       = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map+-- > let Prelude/Optional/last  = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Optional/last+-- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat+-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap+-- > let Prelude/List/map       = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- >  -- > List/last a (Prelude/List/concat a xss) = -- >     Prelude/Optional/last a (Prelude/List/map (List a) (Optional a) (List/last a) xss)@@ -2414,9 +2414,9 @@ -- -- Rules: ----- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/shifted--- > let Prelude/List/concat  = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat--- > let Prelude/List/map     = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map+-- > let Prelude/List/shifted = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/shifted+-- > let Prelude/List/concat  = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat+-- > let Prelude/List/map     = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map -- >  -- > List/indexed a (Prelude/List/concat a xss) = -- >     Prelude/List/shifted a (Prelude/List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)@@ -2439,9 +2439,9 @@ -- -- Rules: ----- > let Prelude/List/map       = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/map--- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concat--- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/concatMap+-- > let Prelude/List/map       = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map+-- > let Prelude/List/concat    = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concat+-- > let Prelude/List/concatMap = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/concatMap -- >  -- > List/reverse a (Prelude/List/concat a xss) -- >     = Prelude/List/concat a (List/reverse (List a) (Prelude/List/map (List a) (List a) (List/reverse a) xss))@@ -2499,7 +2499,7 @@ -- -- ... which currenty redirects to: ----- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude>+-- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude> -- -- There is nothing \"official\" or \"standard\" about this Prelude other than -- the fact that it is mentioned in this tutorial.  The \"Prelude\" is just a@@ -2510,12 +2510,12 @@ -- subdirectories.  For example, the @Bool@ subdirectory has a @not@ file -- located here: ----- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not> -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents ----- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not+-- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2548,7 +2548,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall--- > https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not True+-- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not True -- > <Ctrl-D> -- > Bool -- > @@ -2557,7 +2557,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall--- > let Bool/not = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Bool/not+-- > let Bool/not = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Bool/not -- > in  Bool/not True -- > <Ctrl-D> -- > Bool@@ -2568,7 +2568,7 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: ----- > $ curl https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Natural/even+-- > $ curl https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > @@ -2589,7 +2589,7 @@ -- using local relative paths instead of URLs.  For example, you can use @wget@, -- like this: ----- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/+-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool@@ -2653,15 +2653,36 @@ -- locally like this: -- -- > $ ipfs mount--- > $ cd /ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude+-- > $ cd /ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: ----- <https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude>+-- <https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude> -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial+--+-- You can also import the entire Prelude as a single large record for+-- convenience:+--+-- > $ dhall+-- >     let Prelude = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall+-- >+-- > in    λ(x : Text)+-- >     → Prelude.`List`.length Text (Prelude.`List`.replicate +10 Text x)+-- > <Ctrl-D>+-- > ∀(x : Text) → Natural+-- >+-- > λ(x : Text) → +10+--+-- The organization of the package mirrors the layout of the Prelude, meaning+-- that every directory is stored as a record whose children are the fields of+-- that record.+--+-- __Exercise__: Browse the Prelude by running:+--+-- > $ dhall --pretty <<< 'https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall'  -- $conclusion --
src/Dhall/TypeCheck.hs view
@@ -23,8 +23,8 @@  import Control.Exception (Exception) import Data.Foldable (forM_, toList)-import Data.HashMap.Strict.InsOrd (InsOrdHashMap) import Data.Monoid ((<>))+import Data.Sequence (Seq, ViewL(..)) import Data.Set (Set) import Data.Text.Buildable (Buildable(..)) import Data.Text.Lazy (Text)@@ -35,16 +35,19 @@ import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..)) import Dhall.Context (Context) -import qualified Control.Monad.Trans.State.Strict as State-import qualified Data.HashMap.Strict+import qualified Data.Foldable import qualified Data.HashMap.Strict.InsOrd+import qualified Data.Sequence import qualified Data.Set import qualified Data.Text.Lazy                   as Text import qualified Data.Text.Lazy.Builder           as Builder-import qualified Data.Vector import qualified Dhall.Context import qualified Dhall.Core +traverseWithIndex_ :: Applicative f => (Int -> a -> f b) -> Seq a -> f ()+traverseWithIndex_ k xs =+    Data.Foldable.sequenceA_ (Data.Sequence.mapWithIndex k xs)+ axiom :: Const -> Either (TypeError s a) Const axiom Type = return Kind axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) Untyped)@@ -55,75 +58,6 @@ rule Kind Kind = return Kind rule Kind Type = return Type -match :: Var -> Var -> [(Text, Text)] -> Bool-match (V xL nL) (V xR nR)             []  =-    xL == xR  && nL == nR-match (V xL 0 ) (V xR 0 ) ((xL', xR'):_ )-    | xL == xL' && xR == xR' = True-match (V xL nL) (V xR nR) ((xL', xR'):xs) =-    match (V xL nL') (V xR nR') xs-  where-    nL' = if xL == xL' then nL - 1 else nL-    nR' = if xR == xR' then nR - 1 else nR--toSortedList :: InsOrdHashMap k v -> [(k, v)]-toSortedList =-    Data.HashMap.Strict.toList . Data.HashMap.Strict.InsOrd.toHashMap--propEqual :: Eq a => Expr s a -> Expr t a -> Bool-propEqual eL0 eR0 =-    State.evalState-        (go (Dhall.Core.normalize eL0) (Dhall.Core.normalize eR0))-        []-  where-    go (Const Type) (Const Type) = return True-    go (Const Kind) (Const Kind) = return True-    go (Var vL) (Var vR) = do-        ctx <- State.get-        return (match vL vR ctx)-    go (Pi xL tL bL) (Pi xR tR bR) = do-        ctx <- State.get-        eq1 <- go tL tR-        if eq1-            then do-                State.put ((xL, xR):ctx)-                eq2 <- go bL bR-                State.put ctx-                return eq2-            else return False-    go (App fL aL) (App fR aR) = do-        b1 <- go fL fR-        if b1 then go aL aR else return False-    go Bool Bool = return True-    go Natural Natural = return True-    go Integer Integer = return True-    go Double Double = return True-    go Text Text = return True-    go List List = return True-    go Optional Optional = return True-    go (Record ktsL0) (Record ktsR0) = do-        let loop ((kL, tL):ktsL) ((kR, tR):ktsR)-                | kL == kR = do-                    b <- go tL tR-                    if b-                        then loop ktsL ktsR-                        else return False-            loop [] [] = return True-            loop _  _  = return False-        loop (toSortedList ktsL0) (toSortedList ktsR0)-    go (Union ktsL0) (Union ktsR0) = do-        let loop ((kL, tL):ktsL) ((kR, tR):ktsR)-                | kL == kR = do-                    b <- go tL tR-                    if b-                        then loop ktsL ktsR-                        else return False-            loop [] [] = return True-            loop _  _  = return False-        loop (toSortedList ktsL0) (toSortedList ktsR0)-    go (Embed eL) (Embed eR) = return (eL == eR)-    go _ _ = return False- {-| Type-check an expression and return the expression's type if type-checking     succeeds or an error if type-checking fails @@ -162,7 +96,7 @@                 return a     loop ctx   (Lam x _A  b     ) = do         _ <- loop ctx _A-        let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx)+        let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A) ctx)         _B <- loop ctx' b         let p = Pi x _A _B         _t <- loop ctx p@@ -174,7 +108,7 @@             _       -> Left (TypeError ctx e (InvalidInputType _A))          _ <- loop ctx _A-        let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x _A ctx)+        let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A) ctx)         tB <- fmap Dhall.Core.normalize (loop ctx' _B)         kB <- case tB of             Const k -> return k@@ -189,7 +123,7 @@             Pi x _A _B -> return (x, _A, _B)             _          -> Left (TypeError ctx e (NotAFunction f tf))         _A' <- loop ctx a-        if propEqual _A _A'+        if Dhall.Core.judgmentallyEqual _A _A'             then do                 let a'   = Dhall.Core.shift   1  (V x 0) a                 let _B'  = Dhall.Core.subst (V x 0) a' _B@@ -206,7 +140,7 @@                 _ <- loop ctx _A0                 let nf_A0 = Dhall.Core.normalize _A0                 let nf_A1 = Dhall.Core.normalize _A1-                if propEqual _A0 _A1+                if Dhall.Core.judgmentallyEqual _A0 _A1                     then return ()                     else Left (TypeError ctx e (AnnotMismatch a0 nf_A0 nf_A1))             Nothing -> return ()@@ -219,7 +153,7 @@         _ <- loop ctx t          t' <- loop ctx x-        if propEqual t t'+        if Dhall.Core.judgmentallyEqual t t'             then do                 return t             else do@@ -295,7 +229,7 @@             Const Type -> return ()             _          -> Left (TypeError ctx e (IfBranchMustBeTerm False z tz ttz)) -        if propEqual ty tz+        if Dhall.Core.judgmentallyEqual ty tz             then return ()             else Left (TypeError ctx e (IfBranchMismatch y z ty tz))         return ty@@ -384,17 +318,16 @@     loop _      List              = do         return (Pi "_" (Const Type) (Const Type))     loop ctx e@(ListLit  Nothing  xs) = do-        if Data.Vector.null xs-            then Left (TypeError ctx e MissingListType)-            else do-                t <- loop ctx (Data.Vector.head xs)+        case Data.Sequence.viewl xs of+            x0 :< _ -> do+                t <- loop ctx x0                 s <- fmap Dhall.Core.normalize (loop ctx t)                 case s of                     Const Type -> return ()                     _ -> Left (TypeError ctx e (InvalidListType t))-                flip Data.Vector.imapM_ xs (\i x -> do+                flip traverseWithIndex_ xs (\i x -> do                     t' <- loop ctx x-                    if propEqual t t'+                    if Dhall.Core.judgmentallyEqual t t'                         then return ()                         else do                             let nf_t  = Dhall.Core.normalize t@@ -402,14 +335,15 @@                             let err   = MismatchedListElements i nf_t x nf_t'                             Left (TypeError ctx x err) )                 return (App List t)+            _ -> Left (TypeError ctx e MissingListType)     loop ctx e@(ListLit (Just t ) xs) = do         s <- fmap Dhall.Core.normalize (loop ctx t)         case s of             Const Type -> return ()             _ -> Left (TypeError ctx e (InvalidListType t))-        flip Data.Vector.imapM_ xs (\i x -> do+        flip traverseWithIndex_ xs (\i x -> do             t' <- loop ctx x-            if propEqual t t'+            if Dhall.Core.judgmentallyEqual t t'                 then return ()                 else do                     let nf_t  = Dhall.Core.normalize t@@ -427,7 +361,7 @@             App List er -> return er             _           -> Left (TypeError ctx e (CantListAppend r tr)) -        if propEqual el er+        if Dhall.Core.judgmentallyEqual el er             then return (App List el)             else Left (TypeError ctx e (ListAppendMismatch el er))     loop _      ListBuild         = do@@ -466,13 +400,9 @@         case s of             Const Type -> return ()             _ -> Left (TypeError ctx e (InvalidOptionalType t))-        let n = Data.Vector.length xs-        if 2 <= n-            then Left (TypeError ctx e (InvalidOptionalLiteral n))-            else return ()         forM_ xs (\x -> do             t' <- loop ctx x-            if propEqual t t'+            if Dhall.Core.judgmentallyEqual t t'                 then return ()                 else do                     let nf_t  = Dhall.Core.normalize t@@ -527,7 +457,7 @@             Just _  -> Left (TypeError ctx e (DuplicateAlternative k))             Nothing -> return ()         t <- loop ctx v-        let union = Union (Data.HashMap.Strict.InsOrd.insert k t kts)+        let union = Union (Data.HashMap.Strict.InsOrd.insert k (Dhall.Core.normalize t) kts)         _ <- loop ctx union         return union     loop ctx e@(Combine kvsX kvsY) = do@@ -600,10 +530,10 @@                     Just tX  ->                         case tX of                             Pi _ tY' t' -> do-                                if propEqual tY tY'+                                if Dhall.Core.judgmentallyEqual tY tY'                                     then return ()                                     else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))-                                if propEqual t t'+                                if Dhall.Core.judgmentallyEqual t t'                                     then return ()                                     else Left (TypeError ctx e (InvalidHandlerOutputType kY t t'))                             _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))@@ -639,10 +569,10 @@                     Just tX  ->                         case tX of                             Pi _ tY' t' -> do-                                if propEqual tY tY'+                                if Dhall.Core.judgmentallyEqual tY tY'                                     then return ()                                     else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY'))-                                if propEqual t t'+                                if Dhall.Core.judgmentallyEqual t t'                                     then return ()                                     else Left (TypeError ctx e (HandlerOutputTypeMismatch kX t kY t'))                             _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX))@@ -710,7 +640,6 @@     | InvalidListElement Int (Expr s a) (Expr s a) (Expr s a)     | InvalidListType (Expr s a)     | InvalidOptionalElement (Expr s a) (Expr s a) (Expr s a)-    | InvalidOptionalLiteral Int     | InvalidOptionalType (Expr s a)     | InvalidPredicate (Expr s a) (Expr s a)     | IfBranchMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)@@ -1890,70 +1819,6 @@         txt0 = build expr0         txt1 = build expr1         txt2 = build expr2--prettyTypeMessage (InvalidOptionalLiteral n) = ErrorMessages {..}-  where-    short = "Multiple ❰Optional❱ elements not allowed"--    long =-        "Explanation: The syntax for ❰Optional❱ values resembles the syntax for ❰List❱s: \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────┐                                                   \n\-        \    │ [] : Optional Integer │  An ❰Optional❱ value which is absent              \n\-        \    └───────────────────────┘                                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────┐                                                   \n\-        \    │ [] : List     Integer │  An empty (0-element) ❰List❱                      \n\-        \    └───────────────────────┘                                                   \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌────────────────────────┐                                                  \n\-        \    │ [1] : Optional Integer │  An ❰Optional❱ value which is present            \n\-        \    └────────────────────────┘                                                  \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌────────────────────────┐                                                  \n\-        \    │ [1] : List     Integer │  A singleton (1-element) ❰List❱                  \n\-        \    └────────────────────────┘                                                  \n\-        \                                                                                \n\-        \                                                                                \n\-        \However, an ❰Optional❱ value can " <> _NOT <> " have more than one element, whereas a\n\-        \❰List❱ can have multiple elements:                                              \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────────┐                                               \n\-        \    │ [1, 2] : Optional Integer │  Invalid: multiple elements " <> _NOT <> " allowed\n\-        \    └───────────────────────────┘                                               \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌───────────────────────────┐                                               \n\-        \    │ [1, 2] : List     Integer │  Valid: multiple elements allowed             \n\-        \    └───────────────────────────┘                                               \n\-        \                                                                                \n\-        \                                                                                \n\-        \Some common reasons why you might get this error:                               \n\-        \                                                                                \n\-        \● You accidentally typed ❰Optional❱ when you meant ❰List❱, like this:           \n\-        \                                                                                \n\-        \                                                                                \n\-        \    ┌────────────────────────────────────────────────────┐                      \n\-        \    │ List/length Integer ([1, 2, 3] : Optional Integer) │                      \n\-        \    └────────────────────────────────────────────────────┘                      \n\-        \                                       ⇧                                        \n\-        \                                       This should be ❰List❱ instead            \n\-        \                                                                                \n\-        \                                                                                \n\-        \────────────────────────────────────────────────────────────────────────────────\n\-        \                                                                                \n\-        \Your ❰Optional❱ value had this many elements:                                   \n\-        \                                                                                \n\-        \↳ " <> txt0 <> "                                                                \n\-        \                                                                                \n\-        \... when an ❰Optional❱ value can only have at most one element                  \n"-      where-        txt0 = build n  prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..}   where
− tests/Examples.hs 
@@ -1,1070 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--module Examples where--import qualified Test.Tasty-import qualified Test.Tasty.HUnit-import qualified Util--import Test.Tasty (TestTree)--exampleTests :: TestTree-exampleTests =-    Test.Tasty.testGroup "examples"-        [ Test.Tasty.testGroup "Bool"-            [ Test.Tasty.testGroup "and"-                [ _Bool_and_0-                , _Bool_and_1-                ]-            , Test.Tasty.testGroup "build"-                [ _Bool_build_0-                , _Bool_build_1-                ]-            , Test.Tasty.testGroup "even"-                [ _Bool_even_0-                , _Bool_even_1-                , _Bool_even_2-                , _Bool_even_3-                ]-            , Test.Tasty.testGroup "fold"-                [ _Bool_fold_0-                , _Bool_fold_1-                ]-            , Test.Tasty.testGroup "not"-                [ _Bool_not_0-                , _Bool_not_1-                ]-            , Test.Tasty.testGroup "odd"-                [ _Bool_odd_0-                , _Bool_odd_1-                , _Bool_odd_2-                , _Bool_odd_3-                ]-            , Test.Tasty.testGroup "or"-                [ _Bool_or_0-                , _Bool_or_1-                ]-            , Test.Tasty.testGroup "show"-                [ _Bool_show_0-                , _Bool_show_1-                ]-            ]-        , Test.Tasty.testGroup "Double"-            [ Test.Tasty.testGroup "show"-                [ _Double_show_0-                , _Double_show_1-                ]-            ]-        , Test.Tasty.testGroup "Integer"-            [ Test.Tasty.testGroup "show"-                [ _Integer_show_0-                , _Integer_show_1-                ]-            ]-        , Test.Tasty.testGroup "List"-            [ Test.Tasty.testGroup "all"-                [ _List_all_0-                , _List_all_1-                ]-            , Test.Tasty.testGroup "any"-                [ _List_any_0-                , _List_any_1-                ]-            , Test.Tasty.testGroup "build"-                [ _List_build_0-                , _List_build_1-                ]-            , Test.Tasty.testGroup "concat"-                [ _List_concat_0-                , _List_concat_1-                ]-            , Test.Tasty.testGroup "concatMap"-                [ _List_concatMap_0-                , _List_concatMap_1-                ]-            , Test.Tasty.testGroup "filter"-                [ _List_filter_0-                , _List_filter_1-                ]-            , Test.Tasty.testGroup "fold"-                [ _List_fold_0-                , _List_fold_1-                , _List_fold_2-                ]-            , Test.Tasty.testGroup "generate"-                [ _List_generate_0-                , _List_generate_1-                ]-            , Test.Tasty.testGroup "head"-                [ _List_head_0-                , _List_head_1-                ]-            , Test.Tasty.testGroup "indexed"-                [ _List_indexed_0-                , _List_indexed_1-                ]-            , Test.Tasty.testGroup "iterate"-                [ _List_iterate_0-                , _List_iterate_1-                ]-            , Test.Tasty.testGroup "last"-                [ _List_last_0-                , _List_last_1-                ]-            , Test.Tasty.testGroup "length"-                [ _List_length_0-                , _List_length_1-                ]-            , Test.Tasty.testGroup "map"-                [ _List_map_0-                , _List_map_1-                ]-            , Test.Tasty.testGroup "null"-                [ _List_null_0-                , _List_null_1-                ]-            , Test.Tasty.testGroup "replicate"-                [ _List_replicate_0-                , _List_replicate_1-                ]-            , Test.Tasty.testGroup "reverse"-                [ _List_reverse_0-                , _List_reverse_1-                ]-            , Test.Tasty.testGroup "shifted"-                [ _List_shifted_0-                , _List_shifted_1-                ]-            , Test.Tasty.testGroup "unzip"-                [ _List_unzip_0-                , _List_unzip_1-                ]-            ]-        , Test.Tasty.testGroup "Monoid"-            [ _Monoid_00-            , _Monoid_01-            , _Monoid_02-            , _Monoid_03-            , _Monoid_04-            , _Monoid_05-            , _Monoid_06-            , _Monoid_07-            , _Monoid_08-            , _Monoid_09-            , _Monoid_10-            ]-        , Test.Tasty.testGroup "Natural"-            [ Test.Tasty.testGroup "build"-                [ _Natural_build_0-                , _Natural_build_1-                ]-            , Test.Tasty.testGroup "enumerate"-                [ _Natural_enumerate_0-                , _Natural_enumerate_1-                ]-            , Test.Tasty.testGroup "even"-                [ _Natural_even_0-                , _Natural_even_1-                ]-            , Test.Tasty.testGroup "fold"-                [ _Natural_fold_0-                , _Natural_fold_1-                , _Natural_fold_2-                ]-            , Test.Tasty.testGroup "isZero"-                [ _Natural_isZero_0-                , _Natural_isZero_1-                ]-            , Test.Tasty.testGroup "odd"-                [ _Natural_odd_0-                , _Natural_odd_1-                ]-            , Test.Tasty.testGroup "product"-                [ _Natural_product_0-                , _Natural_product_1-                ]-            , Test.Tasty.testGroup "show"-                [ _Natural_show_0-                , _Natural_show_1-                ]-            , Test.Tasty.testGroup "sum"-                [ _Natural_sum_0-                , _Natural_sum_1-                ]-            , Test.Tasty.testGroup "toInteger"-                [ _Natural_toInteger_0-                , _Natural_toInteger_1-                ]-            ]-        , Test.Tasty.testGroup "Optional"-            [ Test.Tasty.testGroup "all"-                [ _Optional_all_0-                , _Optional_all_1-                ]-            , Test.Tasty.testGroup "any"-                [ _Optional_any_0-                , _Optional_any_1-                ]-            , Test.Tasty.testGroup "build"-                [ _Optional_build_0-                , _Optional_build_1-                ]-            , Test.Tasty.testGroup "concat"-                [ _Optional_concat_0-                , _Optional_concat_1-                , _Optional_concat_2-                ]-            , Test.Tasty.testGroup "filter"-                [ _Optional_filter_0-                , _Optional_filter_1-                ]-            , Test.Tasty.testGroup "fold"-                [ _Optional_fold_0-                , _Optional_fold_1-                ]-            , Test.Tasty.testGroup "head"-                [ _Optional_head_0-                , _Optional_head_1-                , _Optional_head_2-                ]-            , Test.Tasty.testGroup "last"-                [ _Optional_last_0-                , _Optional_last_1-                , _Optional_last_2-                ]-            , Test.Tasty.testGroup "length"-                [ _Optional_length_0-                , _Optional_length_1-                ]-            , Test.Tasty.testGroup "null"-                [ _Optional_null_0-                , _Optional_null_1-                ]-            , Test.Tasty.testGroup "map"-                [ _Optional_map_0-                , _Optional_map_1-                ]-            , Test.Tasty.testGroup "toList"-                [ _Optional_toList_0-                , _Optional_toList_1-                ]-            , Test.Tasty.testGroup "unzip"-                [ _Optional_unzip_0-                , _Optional_unzip_1-                ]-            ]-        , Test.Tasty.testGroup "Text"-            [ Test.Tasty.testGroup "concat"-                [ _Text_concat_0-                , _Text_concat_1-                ]-            , Test.Tasty.testGroup "concatMap"-                [ _Text_concatMap_0-                , _Text_concatMap_1-                ]-            , Test.Tasty.testGroup "concatMapSep"-                [ _Text_concatMapSep_0-                , _Text_concatMapSep_1-                ]-            , Test.Tasty.testGroup "concatSep"-                [ _Text_concatSep_0-                , _Text_concatSep_1-                ]-            ]-        ]--_Bool_and_0 :: TestTree-_Bool_and_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/and ([ True, False, True ] : List Bool)"-    Util.assertNormalizesTo e "False" )--_Bool_and_1 :: TestTree-_Bool_and_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/and ([] : List Bool)"-    Util.assertNormalizesTo e "True" )--_Bool_build_0 :: TestTree-_Bool_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Bool/build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true)"-    Util.assertNormalizesTo e "True" )--_Bool_build_1 :: TestTree-_Bool_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Bool/build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)"-    Util.assertNormalizesTo e "False" )--_Bool_even_0 :: TestTree-_Bool_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/even ([ False, True, False ] : List Bool)"-    Util.assertNormalizesTo e "True" )--_Bool_even_1 :: TestTree-_Bool_even_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/even ([ False, True ] : List Bool)"-    Util.assertNormalizesTo e "False" )--_Bool_even_2 :: TestTree-_Bool_even_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code "./Prelude/Bool/even ([ False ] : List Bool)"-    Util.assertNormalizesTo e "False" )--_Bool_even_3 :: TestTree-_Bool_even_3 = Test.Tasty.HUnit.testCase "Example #3" (do-    e <- Util.code "./Prelude/Bool/even ([] : List Bool)"-    Util.assertNormalizesTo e "True" )--_Bool_fold_0 :: TestTree-_Bool_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/fold True Integer 0 1"-    Util.assertNormalizesTo e "0" )--_Bool_fold_1 :: TestTree-_Bool_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/fold False Integer 0 1"-    Util.assertNormalizesTo e "1" )--_Bool_not_0 :: TestTree-_Bool_not_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/not True"-    Util.assertNormalizesTo e "False" )--_Bool_not_1 :: TestTree-_Bool_not_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/not False"-    Util.assertNormalizesTo e "True" )--_Bool_odd_0 :: TestTree-_Bool_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/odd ([ True, False, True ] : List Bool)"-    Util.assertNormalizesTo e "False" )--_Bool_odd_1 :: TestTree-_Bool_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/odd ([ True, False ] : List Bool)"-    Util.assertNormalizesTo e "True" )--_Bool_odd_2 :: TestTree-_Bool_odd_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code "./Prelude/Bool/odd ([ True ] : List Bool)"-    Util.assertNormalizesTo e "True" )--_Bool_odd_3 :: TestTree-_Bool_odd_3 = Test.Tasty.HUnit.testCase "Example #3" (do-    e <- Util.code "./Prelude/Bool/odd ([] : List Bool)"-    Util.assertNormalizesTo e "False" )--_Bool_or_0 :: TestTree-_Bool_or_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/or ([ True, False, True ] : List Bool)"-    Util.assertNormalizesTo e "True" )--_Bool_or_1 :: TestTree-_Bool_or_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/or ([] : List Bool)"-    Util.assertNormalizesTo e "False" )--_Bool_show_0 :: TestTree-_Bool_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Bool/show True"-    Util.assertNormalizesTo e "\"True\"" )--_Bool_show_1 :: TestTree-_Bool_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Bool/show False"-    Util.assertNormalizesTo e "\"False\"" )--_Double_show_0 :: TestTree-_Double_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Double/show -3.1"-    Util.assertNormalizesTo e "\"-3.1\"" )--_Double_show_1 :: TestTree-_Double_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Double/show 0.4"-    Util.assertNormalizesTo e "\"0.4\"" )--_Integer_show_0 :: TestTree-_Integer_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Integer/show -3"-    Util.assertNormalizesTo e "\"-3\"" )--_Integer_show_1 :: TestTree-_Integer_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Integer/show 0"-    Util.assertNormalizesTo e "\"0\"" )--_List_all_0 :: TestTree-_List_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/all Natural Natural/even ([ +2, +3, +5 ] : List Natural)"-    Util.assertNormalizesTo e "False" )--_List_all_1 :: TestTree-_List_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/all Natural Natural/even ([] : List Natural)"-    Util.assertNormalizesTo e "True" )--_List_any_0 :: TestTree-_List_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/any Natural Natural/even ([ +2, +3, +5 ] : List Natural)"-    Util.assertNormalizesTo e "True" )--_List_any_1 :: TestTree-_List_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/any Natural Natural/even ([] : List Natural)"-    Util.assertNormalizesTo e "False" )--_List_build_0 :: TestTree-_List_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/build               \n\-        \Text                               \n\-        \(   λ(list : Type)                 \n\-        \→   λ(cons : Text → list → list)   \n\-        \→   λ(nil : list)                  \n\-        \→   cons \"ABC\" (cons \"DEF\" nil)\n\-        \)                                  \n"-    Util.assertNormalizesTo e "[ \"ABC\", \"DEF\" ] : List Text" )--_List_build_1 :: TestTree-_List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/List/build            \n\-        \Text                            \n\-        \(   λ(list : Type)              \n\-        \→   λ(cons : Text → list → list)\n\-        \→   λ(nil : list)               \n\-        \→   nil                         \n\-        \)                               \n"-    Util.assertNormalizesTo e "[] : List Text" )--_List_concat_0 :: TestTree-_List_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/concat Integer      \n\-        \(   [   [0, 1, 2]    : List Integer\n\-        \    ,   [3, 4]       : List Integer\n\-        \    ,   [5, 6, 7, 8] : List Integer\n\-        \    ]   : List (List Integer)      \n\-        \)                                  \n"-    Util.assertNormalizesTo e "[ 0, 1, 2, 3, 4, 5, 6, 7, 8 ] : List Integer" )--_List_concat_1 :: TestTree-_List_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/List/concat Integer\n\-        \(   [   [] : List Integer    \n\-        \    ,   [] : List Integer    \n\-        \    ,   [] : List Integer    \n\-        \    ]   : List (List Integer)\n\-        \)                            \n"-    Util.assertNormalizesTo e "[] : List Integer" )--_List_concatMap_0 :: TestTree-_List_concatMap_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5]"-    Util.assertNormalizesTo e "[ +2, +2, +3, +3, +5, +5 ] : List Natural" )--_List_concatMap_1 :: TestTree-_List_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/List/concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural)"-    Util.assertNormalizesTo e "[] : List Natural" )--_List_filter_0 :: TestTree-_List_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/filter Natural Natural/even ([+2, +3, +5] : List Natural)"-    Util.assertNormalizesTo e "[ +2 ] : List Natural" )--_List_filter_1 :: TestTree-_List_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/filter Natural Natural/odd ([+2, +3, +5] : List Natural)"-    Util.assertNormalizesTo e "[ +3, +5 ] : List Natural" )--_List_fold_0 :: TestTree-_List_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/fold                      \n\-        \Natural                                  \n\-        \([ +2, +3, +5 ] : List Natural)          \n\-        \Natural                                  \n\-        \(λ(x : Natural) → λ(y : Natural) → x + y)\n\-        \+0                                       \n"-    Util.assertNormalizesTo e "+10" )--_List_fold_1 :: TestTree-_List_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "    λ(nil : Natural)                         \n\-        \→   ./Prelude/List/fold                      \n\-        \    Natural                                  \n\-        \    ([ +2, +3, +5 ] : List Natural)          \n\-        \    Natural                                  \n\-        \    (λ(x : Natural) → λ(y : Natural) → x + y)\n\-        \    nil                                      \n"-    Util.assertNormalizesTo e "λ(nil : Natural) → +2 + +3 + +5 + nil" )--_List_fold_2 :: TestTree-_List_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code-        "    λ(list : Type)                                                         \n\-        \→   λ(cons : Natural → list → list)                                        \n\-        \→   λ(nil : list)                                                          \n\-        \→   ./Prelude/List/fold Natural ([ +2, +3, +5 ] : List Natural) list cons nil\n"-    Util.assertNormalizesTo e "λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons +2 (cons +3 (cons +5 nil))" )--_List_generate_0 :: TestTree-_List_generate_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/generate +5 Bool Natural/even"-    Util.assertNormalizesTo e "[ True, False, True, False, True ] : List Bool" )--_List_generate_1 :: TestTree-_List_generate_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/generate +0 Bool Natural/even"-    Util.assertNormalizesTo e "[] : List Bool" )--_List_head_0 :: TestTree-_List_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/head Integer ([ 0, 1, 2 ] : List Integer)"-    Util.assertNormalizesTo e "[ 0 ] : Optional Integer" )--_List_head_1 :: TestTree-_List_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/head Integer ([] : List Integer)"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_List_indexed_0 :: TestTree-_List_indexed_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/indexed Bool ([ True, False, True ] : List Bool)"-    Util.assertNormalizesTo e "[ { index = +0, value = True }, { index = +1, value = False }, { index = +2, value = True } ] : List { index : Natural, value : Bool }" )--_List_indexed_1 :: TestTree-_List_indexed_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/indexed Bool ([] : List Bool)"-    Util.assertNormalizesTo e "[] : List { index : Natural, value : Bool }" )--_List_iterate_0 :: TestTree-_List_iterate_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1"-    Util.assertNormalizesTo e "[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ] : List Natural" )--_List_iterate_1 :: TestTree-_List_iterate_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1"-    Util.assertNormalizesTo e "[] : List Natural" )--_List_last_0 :: TestTree-_List_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/last Integer ([ 0, 1, 2 ] : List Integer)"-    Util.assertNormalizesTo e "[ 2 ] : Optional Integer" )--_List_last_1 :: TestTree-_List_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/last Integer ([] : List Integer)"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_List_length_0 :: TestTree-_List_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/length Integer ([ 0, 1, 2 ] : List Integer)"-    Util.assertNormalizesTo e "+3" )--_List_length_1 :: TestTree-_List_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/length Integer ([] : List Integer)"-    Util.assertNormalizesTo e "+0" )--_List_map_0 :: TestTree-_List_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/map Natural Bool Natural/even ([ +2, +3, +5 ] : List Natural)"-    Util.assertNormalizesTo e "[ True, False, False ] : List Bool" )--_List_map_1 :: TestTree-_List_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/map Natural Bool Natural/even ([] : List Natural)"-    Util.assertNormalizesTo e "[] : List Bool" )--_List_null_0 :: TestTree-_List_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/null Integer ([ 0, 1, 2 ] : List Integer)"-    Util.assertNormalizesTo e "False" )--_List_null_1 :: TestTree-_List_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/null Integer ([] : List Integer)"-    Util.assertNormalizesTo e "True" )--_List_replicate_0 :: TestTree-_List_replicate_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/replicate +9 Integer 1"-    Util.assertNormalizesTo e "[ 1, 1, 1, 1, 1, 1, 1, 1, 1 ] : List Integer" )--_List_replicate_1 :: TestTree-_List_replicate_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/replicate +0 Integer 1"-    Util.assertNormalizesTo e "[] : List Integer" )--_List_reverse_0 :: TestTree-_List_reverse_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/List/reverse Integer ([0, 1, 2] : List Integer)"-    Util.assertNormalizesTo e "[ 2, 1, 0 ] : List Integer" )--_List_reverse_1 :: TestTree-_List_reverse_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/reverse Integer ([] : List Integer)"-    Util.assertNormalizesTo e "[] : List Integer" )--_List_shifted_0 :: TestTree-_List_shifted_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/shifted                                 \n\-        \Bool                                                   \n\-        \(   [   [   { index = +0, value = True  }              \n\-        \        ,   { index = +1, value = True  }              \n\-        \        ,   { index = +2, value = True  }              \n\-        \        ]   : List { index : Natural, value : Bool }   \n\-        \    ,   [   { index = +0, value = False }              \n\-        \        ,   { index = +1, value = False }              \n\-        \        ]   : List { index : Natural, value : Bool }   \n\-        \    ,   [   { index = +0, value = True  }              \n\-        \        ,   { index = +1, value = True  }              \n\-        \        ,   { index = +2, value = True  }              \n\-        \        ,   { index = +3, value = True  }              \n\-        \        ]   : List { index : Natural, value : Bool }   \n\-        \    ]   : List (List { index : Natural, value : Bool })\n\-        \)                                                      \n"-    Util.assertNormalizesTo e "[ { index = +0, value = True }, { index = +1, value = True }, { index = +2, value = True }, { index = +3, value = False }, { index = +4, value = False }, { index = +5, value = True }, { index = +6, value = True }, { index = +7, value = True }, { index = +8, value = True } ] : List { index : Natural, value : Bool }" )--_List_shifted_1 :: TestTree-_List_shifted_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/List/shifted Bool ([] : List (List { index : Natural, value : Bool }))"-    Util.assertNormalizesTo e "[] : List { index : Natural, value : Bool }" )--_List_unzip_0 :: TestTree-_List_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/List/unzip                   \n\-        \Text                                   \n\-        \Bool                                   \n\-        \(   [   { _1 = \"ABC\", _2 = True  }   \n\-        \    ,   { _1 = \"DEF\", _2 = False }   \n\-        \    ,   { _1 = \"GHI\", _2 = True  }   \n\-        \    ]   : List { _1 : Text, _2 : Bool }\n\-        \)                                      \n"-    Util.assertNormalizesTo e "{ _1 = [ \"ABC\", \"DEF\", \"GHI\" ] : List Text, _2 = [ True, False, True ] : List Bool }" )--_List_unzip_1 :: TestTree-_List_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/List/unzip Text Bool ([] : List { _1 : Text, _2 : Bool })"-    Util.assertNormalizesTo e "{ _1 = [] : List Text, _2 = [] : List Bool }" )--_Monoid_00 :: TestTree-_Monoid_00 = Test.Tasty.HUnit.testCase "Example #0"-    (Util.assertTypeChecks "./Prelude/Bool/and : ./Prelude/Monoid Bool")--_Monoid_01 :: TestTree-_Monoid_01 = Test.Tasty.HUnit.testCase "Example #1"-    (Util.assertTypeChecks "./Prelude/Bool/or : ./Prelude/Monoid Bool")--_Monoid_02 :: TestTree-_Monoid_02 = Test.Tasty.HUnit.testCase "Example #2"-    (Util.assertTypeChecks "./Prelude/Bool/even : ./Prelude/Monoid Bool")--_Monoid_03 :: TestTree-_Monoid_03 = Test.Tasty.HUnit.testCase "Example #3"-    (Util.assertTypeChecks "./Prelude/Bool/odd : ./Prelude/Monoid Bool")--_Monoid_04 :: TestTree-_Monoid_04 = Test.Tasty.HUnit.testCase "Example #4"-    (Util.assertTypeChecks-        "./Prelude/List/concat : ∀(a : Type) → ./Prelude/Monoid (List a)" )--_Monoid_05 :: TestTree-_Monoid_05 = Test.Tasty.HUnit.testCase "Example #5"-    (Util.assertTypeChecks-        "./Prelude/List/shifted                                                    \n\-        \    : ∀(a : Type) → ./Prelude/Monoid (List { index : Natural, value : a })\n" )--_Monoid_06 :: TestTree-_Monoid_06 = Test.Tasty.HUnit.testCase "Example #6"-    (Util.assertTypeChecks "./Prelude/Natural/sum : ./Prelude/Monoid Natural")--_Monoid_07 :: TestTree-_Monoid_07 = Test.Tasty.HUnit.testCase "Example #7"-    (Util.assertTypeChecks "./Prelude/Natural/product : ./Prelude/Monoid Natural")--_Monoid_08 :: TestTree-_Monoid_08 = Test.Tasty.HUnit.testCase "Example #8"-    (Util.assertTypeChecks-        "./Prelude/Optional/head : ∀(a : Type) → ./Prelude/Monoid (Optional a)" )--_Monoid_09 :: TestTree-_Monoid_09 = Test.Tasty.HUnit.testCase "Example #9"-    (Util.assertTypeChecks-        "./Prelude/Optional/last : ∀(a : Type) → ./Prelude/Monoid (Optional a)" )--_Monoid_10 :: TestTree-_Monoid_10 = Test.Tasty.HUnit.testCase "Example #10"-    (Util.assertTypeChecks "./Prelude/Text/concat : ./Prelude/Monoid Text")--_Natural_build_0 :: TestTree-_Natural_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Natural/build        \n\-        \(   λ(natural : Type)          \n\-        \→   λ(succ : natural → natural)\n\-        \→   λ(zero : natural)          \n\-        \→   succ (succ (succ zero))    \n\-        \)                              \n"-    Util.assertNormalizesTo e "+3" )--_Natural_build_1 :: TestTree-_Natural_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Natural/build        \n\-        \(   λ(natural : Type)          \n\-        \→   λ(succ : natural → natural)\n\-        \→   λ(zero : natural)          \n\-        \→   zero                       \n\-        \)                              \n"-    Util.assertNormalizesTo e "+0" )--_Natural_enumerate_0 :: TestTree-_Natural_enumerate_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/enumerate +10"-    Util.assertNormalizesTo e "[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ] : List Natural" )--_Natural_enumerate_1 :: TestTree-_Natural_enumerate_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/enumerate +0"-    Util.assertNormalizesTo e "[] : List Natural" )--_Natural_even_0 :: TestTree-_Natural_even_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/even +3"-    Util.assertNormalizesTo e "False" )--_Natural_even_1 :: TestTree-_Natural_even_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/even +0"-    Util.assertNormalizesTo e "True" )--_Natural_fold_0 :: TestTree-_Natural_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1"-    Util.assertNormalizesTo e "+125" )--_Natural_fold_1 :: TestTree-_Natural_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "λ(zero : Natural) → ./Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero"-    Util.assertNormalizesTo e "λ(zero : Natural) → +5 * +5 * +5 * zero" )--_Natural_fold_2 :: TestTree-_Natural_fold_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code-        "    λ(natural : Type)                          \n\-        \→   λ(succ : natural → natural)                \n\-        \→   λ(zero : natural)                          \n\-        \→   ./Prelude/Natural/fold +3 natural succ zero\n"-    Util.assertNormalizesTo e "λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ (succ zero))" )--_Natural_isZero_0 :: TestTree-_Natural_isZero_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/isZero +2"-    Util.assertNormalizesTo e "False" )--_Natural_isZero_1 :: TestTree-_Natural_isZero_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/isZero +0"-    Util.assertNormalizesTo e "True" )--_Natural_odd_0 :: TestTree-_Natural_odd_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/odd +3"-    Util.assertNormalizesTo e "True" )--_Natural_odd_1 :: TestTree-_Natural_odd_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/odd +0"-    Util.assertNormalizesTo e "False" )--_Natural_product_0 :: TestTree-_Natural_product_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/product ([ +2, +3, +5 ] : List Natural)"-    Util.assertNormalizesTo e "+30" )--_Natural_product_1 :: TestTree-_Natural_product_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/product ([] : List Natural)"-    Util.assertNormalizesTo e "+1" )--_Natural_show_0 :: TestTree-_Natural_show_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/show +3"-    Util.assertNormalizesTo e "\"+3\"" )--_Natural_show_1 :: TestTree-_Natural_show_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/show +0"-    Util.assertNormalizesTo e "\"+0\"" )--_Natural_sum_0 :: TestTree-_Natural_sum_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/sum ([ +2, +3, +5 ] : List Natural)"-    Util.assertNormalizesTo e "+10" )--_Natural_sum_1 :: TestTree-_Natural_sum_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/sum ([] : List Natural)"-    Util.assertNormalizesTo e "+0" )--_Natural_toInteger_0 :: TestTree-_Natural_toInteger_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Natural/toInteger +3"-    Util.assertNormalizesTo e "3" )--_Natural_toInteger_1 :: TestTree-_Natural_toInteger_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Natural/toInteger +0"-    Util.assertNormalizesTo e "0" )--_Optional_all_0 :: TestTree-_Optional_all_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Optional/all Natural Natural/even ([ +3 ] : Optional Natural)"-    Util.assertNormalizesTo e "False" )--_Optional_all_1 :: TestTree-_Optional_all_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Optional/all Natural Natural/even ([] : Optional Natural)"-    Util.assertNormalizesTo e "True" )--_Optional_any_0 :: TestTree-_Optional_any_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Optional/any Natural Natural/even ([ +2 ] : Optional Natural)"-    Util.assertNormalizesTo e "True" )--_Optional_any_1 :: TestTree-_Optional_any_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Optional/any Natural Natural/even ([] : Optional Natural)"-    Util.assertNormalizesTo e "False" )--_Optional_build_0 :: TestTree-_Optional_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/build        \n\-        \Integer                         \n\-        \(   λ(optional : Type)          \n\-        \→   λ(just : Integer → optional)\n\-        \→   λ(nothing : optional)       \n\-        \→   just 1                      \n\-        \)                               \n"-    Util.assertNormalizesTo e "[ 1 ] : Optional Integer" )--_Optional_build_1 :: TestTree-_Optional_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/build        \n\-        \Integer                         \n\-        \(   λ(optional : Type)          \n\-        \→   λ(just : Integer → optional)\n\-        \→   λ(nothing : optional)       \n\-        \→   nothing                     \n\-        \)                               \n"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_concat_0 :: TestTree-_Optional_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer))"-    Util.assertNormalizesTo e "[ 1 ] : Optional Integer" )--_Optional_concat_1 :: TestTree-_Optional_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer))"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_concat_2 :: TestTree-_Optional_concat_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code "./Prelude/Optional/concat Integer ([] : Optional (Optional Integer))"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_filter_0 :: TestTree-_Optional_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/filter Natural Natural/even ([ +2 ] : Optional Natural)"-    Util.assertNormalizesTo e "[ +2 ] : Optional Natural" )--_Optional_filter_1 :: TestTree-_Optional_filter_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Optional/filter Natural Natural/odd ([ +2 ] : Optional Natural)"-    Util.assertNormalizesTo e "[] : Optional Natural" )--_Optional_fold_0 :: TestTree-_Optional_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0"-    Util.assertNormalizesTo e "2" )--_Optional_fold_1 :: TestTree-_Optional_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/fold Integer ([]  : Optional Integer) Integer (λ(x : Integer) → x) 0"-    Util.assertNormalizesTo e "0" )--_Optional_head_0 :: TestTree-_Optional_head_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/head        \n\-        \Integer                        \n\-        \(   [ []    : Optional Integer \n\-        \    , [ 1 ] : Optional Integer \n\-        \    , [ 2 ] : Optional Integer \n\-        \    ] : List (Optional Integer)\n\-        \)                              \n"-    Util.assertNormalizesTo e "[ 1 ] : Optional Integer" )--_Optional_head_1 :: TestTree-_Optional_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/head                                                     \n\-        \Integer                                                                     \n\-        \([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))\n"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_head_2 :: TestTree-_Optional_head_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code "./Prelude/Optional/head Integer ([] : List (Optional Integer))"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_last_0 :: TestTree-_Optional_last_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/last        \n\-        \Integer                        \n\-        \(   [ [] : Optional Integer    \n\-        \    , [1] : Optional Integer   \n\-        \    , [2] : Optional Integer   \n\-        \    ] : List (Optional Integer)\n\-        \)                              \n"-    Util.assertNormalizesTo e "[ 2 ] : Optional Integer" )--_Optional_last_1 :: TestTree-_Optional_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/last                                                     \n\-        \Integer                                                                     \n\-        \([ [] : Optional Integer, [] : Optional Integer ] : List (Optional Integer))\n"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_last_2 :: TestTree-_Optional_last_2 = Test.Tasty.HUnit.testCase "Example #2" (do-    e <- Util.code "./Prelude/Optional/last Integer ([] : List (Optional Integer))"-    Util.assertNormalizesTo e "[] : Optional Integer" )--_Optional_map_0 :: TestTree-_Optional_map_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/map Natural Bool Natural/even ([ +3 ] : Optional Natural)"-    Util.assertNormalizesTo e "[ False ] : Optional Bool" )--_Optional_map_1 :: TestTree-_Optional_map_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural)"-    Util.assertNormalizesTo e "[] : Optional Bool" )--_Optional_length_0 :: TestTree-_Optional_length_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/length Integer ([ 2 ] : Optional Integer)"-    Util.assertNormalizesTo e "+1" )--_Optional_length_1 :: TestTree-_Optional_length_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Optional/length Integer ([] : Optional Integer)"-    Util.assertNormalizesTo e "+0" )--_Optional_null_0 :: TestTree-_Optional_null_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Optional/null Integer ([ 2]  : Optional Integer)"-    Util.assertNormalizesTo e "False" )--_Optional_null_1 :: TestTree-_Optional_null_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Optional/null Integer ([] : Optional Integer)"-    Util.assertNormalizesTo e "True" )--_Optional_toList_0 :: TestTree-_Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/toList Integer ([ 1 ] : Optional Integer)"-    Util.assertNormalizesTo e "[ 1 ]" )--_Optional_toList_1 :: TestTree-_Optional_toList_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Optional/toList Integer ([] : Optional Integer)"-    Util.assertNormalizesTo e "[] : List Integer" )--_Optional_unzip_0 :: TestTree-_Optional_unzip_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Optional/unzip                                              \n\-        \Text                                                                  \n\-        \Bool                                                                  \n\-        \([ { _1 = \"ABC\", _2 = True  } ] : Optional { _1 : Text, _2 : Bool })\n"-    Util.assertNormalizesTo e "{ _1 = [ \"ABC\" ] : Optional Text, _2 = [ True ] : Optional Bool }" )--_Optional_unzip_1 :: TestTree-_Optional_unzip_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Optional/unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool })"-    Util.assertNormalizesTo e "{ _1 = [] : Optional Text, _2 = [] : Optional Bool }" )--_Text_concat_0 :: TestTree-_Text_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Text/concat ([ \"ABC\", \"DEF\", \"GHI\" ] : List Text)"-    Util.assertNormalizesTo e "\"ABCDEFGHI\"" )--_Text_concat_1 :: TestTree-_Text_concat_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Text/concat ([] : List Text)"-    Util.assertNormalizesTo e "\"\"" )--_Text_concatMap_0 :: TestTree-_Text_concatMap_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code-        "./Prelude/Text/concatMap Integer (λ(n : Integer) → \"${Integer/show n} \") [ 0, 1, 2 ]"-    Util.assertNormalizesTo e "\"0 1 2 \"" )--_Text_concatMap_1 :: TestTree-_Text_concatMap_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Text/concatMap Integer (λ(n : Integer) → \"${Integer/show n} \") ([] : List Integer)"-    Util.assertNormalizesTo e "\"\"" )--_Text_concatMapSep_0 :: TestTree-_Text_concatMapSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Text/concatMapSep \", \" Integer Integer/show [ 0, 1, 2 ]"-    Util.assertNormalizesTo e "\"0, 1, 2\"" )--_Text_concatMapSep_1 :: TestTree-_Text_concatMapSep_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code-        "./Prelude/Text/concatMapSep \", \" Integer Integer/show ([] : List Integer)"-    Util.assertNormalizesTo e "\"\"" )--_Text_concatSep_0 :: TestTree-_Text_concatSep_0 = Test.Tasty.HUnit.testCase "Example #0" (do-    e <- Util.code "./Prelude/Text/concatSep \", \" [ \"ABC\", \"DEF\", \"GHI\" ]"-    Util.assertNormalizesTo e "\"ABC, DEF, GHI\"" )--_Text_concatSep_1 :: TestTree-_Text_concatSep_1 = Test.Tasty.HUnit.testCase "Example #1" (do-    e <- Util.code "./Prelude/Text/concatSep \", \" ([] : List Text)"-    Util.assertNormalizesTo e "\"\"" )
tests/Normalization.hs view
@@ -24,11 +24,145 @@ normalizationTests :: TestTree normalizationTests =     testGroup "normalization"-        [ constantFolding+        [ examples+        , simplifications+        , constantFolding         , conversions         , shouldNormalize "Optional build/fold fusion" "optionalBuildFold"         , customization         , shouldNormalize "a remote-systems.conf builder" "remoteSystems"+        ]++examples :: TestTree+examples =+    testGroup "Prelude examples"+        [ shouldNormalize "Bool/and" "./examples/Bool/and/0"+        , shouldNormalize "Bool/and" "./examples/Bool/and/1"+        , shouldNormalize "Bool/build" "./examples/Bool/build/0"+        , shouldNormalize "Bool/build" "./examples/Bool/build/1"+        , shouldNormalize "Bool/even" "./examples/Bool/even/0"+        , shouldNormalize "Bool/even" "./examples/Bool/even/1"+        , shouldNormalize "Bool/even" "./examples/Bool/even/2"+        , shouldNormalize "Bool/even" "./examples/Bool/even/3"+        , shouldNormalize "Bool/fold" "./examples/Bool/fold/0"+        , shouldNormalize "Bool/fold" "./examples/Bool/fold/1"+        , shouldNormalize "Bool/not" "./examples/Bool/not/0"+        , shouldNormalize "Bool/not" "./examples/Bool/not/1"+        , shouldNormalize "Bool/odd" "./examples/Bool/odd/0"+        , shouldNormalize "Bool/odd" "./examples/Bool/odd/1"+        , shouldNormalize "Bool/odd" "./examples/Bool/odd/2"+        , shouldNormalize "Bool/odd" "./examples/Bool/odd/3"+        , shouldNormalize "Bool/or" "./examples/Bool/or/0"+        , shouldNormalize "Bool/or" "./examples/Bool/or/1"+        , shouldNormalize "Bool/show" "./examples/Bool/show/0"+        , shouldNormalize "Bool/show" "./examples/Bool/show/1"+        , shouldNormalize "Double/show" "./examples/Double/show/0"+        , shouldNormalize "Double/show" "./examples/Double/show/1"+        , shouldNormalize "Integer/show" "./examples/Integer/show/0"+        , shouldNormalize "Integer/show" "./examples/Integer/show/1"+        , shouldNormalize "List/all" "./examples/List/all/0"+        , shouldNormalize "List/all" "./examples/List/all/1"+        , shouldNormalize "List/any" "./examples/List/any/0"+        , shouldNormalize "List/any" "./examples/List/any/1"+        , shouldNormalize "List/build" "./examples/List/build/0"+        , shouldNormalize "List/build" "./examples/List/build/1"+        , shouldNormalize "List/concat" "./examples/List/concat/0"+        , shouldNormalize "List/concat" "./examples/List/concat/1"+        , shouldNormalize "List/concatMap" "./examples/List/concatMap/0"+        , shouldNormalize "List/concatMap" "./examples/List/concatMap/1"+        , shouldNormalize "List/filter" "./examples/List/filter/0"+        , shouldNormalize "List/filter" "./examples/List/filter/1"+        , shouldNormalize "List/fold" "./examples/List/fold/0"+        , shouldNormalize "List/fold" "./examples/List/fold/1"+        , shouldNormalize "List/fold" "./examples/List/fold/2"+        , shouldNormalize "List/generate" "./examples/List/generate/0"+        , shouldNormalize "List/generate" "./examples/List/generate/1"+        , shouldNormalize "List/head" "./examples/List/head/0"+        , shouldNormalize "List/head" "./examples/List/head/1"+        , shouldNormalize "List/iterate" "./examples/List/iterate/0"+        , shouldNormalize "List/iterate" "./examples/List/iterate/1"+        , shouldNormalize "List/last" "./examples/List/last/0"+        , shouldNormalize "List/last" "./examples/List/last/1"+        , shouldNormalize "List/length" "./examples/List/length/0"+        , shouldNormalize "List/length" "./examples/List/length/1"+        , shouldNormalize "List/map" "./examples/List/map/0"+        , shouldNormalize "List/map" "./examples/List/map/1"+        , shouldNormalize "List/null" "./examples/List/null/0"+        , shouldNormalize "List/null" "./examples/List/null/1"+        , shouldNormalize "List/replicate" "./examples/List/replicate/0"+        , shouldNormalize "List/replicate" "./examples/List/replicate/1"+        , shouldNormalize "List/reverse" "./examples/List/reverse/0"+        , shouldNormalize "List/reverse" "./examples/List/reverse/1"+        , shouldNormalize "List/shifted" "./examples/List/shifted/0"+        , shouldNormalize "List/shifted" "./examples/List/shifted/1"+        , shouldNormalize "List/unzip" "./examples/List/unzip/0"+        , shouldNormalize "List/unzip" "./examples/List/unzip/1"+        , shouldNormalize "Natural/build" "./examples/Natural/build/0"+        , shouldNormalize "Natural/build" "./examples/Natural/build/1"+        , shouldNormalize "Natural/enumerate" "./examples/Natural/enumerate/0"+        , shouldNormalize "Natural/enumerate" "./examples/Natural/enumerate/1"+        , shouldNormalize "Natural/even" "./examples/Natural/even/0"+        , shouldNormalize "Natural/even" "./examples/Natural/even/1"+        , shouldNormalize "Natural/fold" "./examples/Natural/fold/0"+        , shouldNormalize "Natural/fold" "./examples/Natural/fold/1"+        , shouldNormalize "Natural/fold" "./examples/Natural/fold/2"+        , shouldNormalize "Natural/isZero" "./examples/Natural/isZero/0"+        , shouldNormalize "Natural/isZero" "./examples/Natural/isZero/1"+        , shouldNormalize "Natural/odd" "./examples/Natural/odd/0"+        , shouldNormalize "Natural/odd" "./examples/Natural/odd/1"+        , shouldNormalize "Natural/product" "./examples/Natural/product/0"+        , shouldNormalize "Natural/product" "./examples/Natural/product/1"+        , shouldNormalize "Natural/show" "./examples/Natural/show/0"+        , shouldNormalize "Natural/show" "./examples/Natural/show/1"+        , shouldNormalize "Natural/sum" "./examples/Natural/sum/0"+        , shouldNormalize "Natural/sum" "./examples/Natural/sum/1"+        , shouldNormalize "Natural/toInteger" "./examples/Natural/toInteger/0"+        , shouldNormalize "Natural/toInteger" "./examples/Natural/toInteger/1"+        , shouldNormalize "Optional/all" "./examples/Optional/all/0"+        , shouldNormalize "Optional/all" "./examples/Optional/all/1"+        , shouldNormalize "Optional/any" "./examples/Optional/any/0"+        , shouldNormalize "Optional/any" "./examples/Optional/any/1"+        , shouldNormalize "Optional/build" "./examples/Optional/build/0"+        , shouldNormalize "Optional/build" "./examples/Optional/build/1"+        , shouldNormalize "Optional/concat" "./examples/Optional/concat/0"+        , shouldNormalize "Optional/concat" "./examples/Optional/concat/1"+        , shouldNormalize "Optional/concat" "./examples/Optional/concat/2"+        , shouldNormalize "Optional/filter" "./examples/Optional/filter/0"+        , shouldNormalize "Optional/filter" "./examples/Optional/filter/1"+        , shouldNormalize "Optional/fold" "./examples/Optional/fold/0"+        , shouldNormalize "Optional/fold" "./examples/Optional/fold/1"+        , shouldNormalize "Optional/head" "./examples/Optional/head/0"+        , shouldNormalize "Optional/head" "./examples/Optional/head/1"+        , shouldNormalize "Optional/last" "./examples/Optional/last/0"+        , shouldNormalize "Optional/last" "./examples/Optional/last/1"+        , shouldNormalize "Optional/length" "./examples/Optional/length/0"+        , shouldNormalize "Optional/length" "./examples/Optional/length/1"+        , shouldNormalize "Optional/map" "./examples/Optional/map/0"+        , shouldNormalize "Optional/map" "./examples/Optional/map/1"+        , shouldNormalize "Optional/null" "./examples/Optional/null/0"+        , shouldNormalize "Optional/null" "./examples/Optional/null/1"+        , shouldNormalize "Optional/toList" "./examples/Optional/toList/0"+        , shouldNormalize "Optional/toList" "./examples/Optional/toList/1"+        , shouldNormalize "Optional/unzip" "./examples/Optional/unzip/0"+        , shouldNormalize "Optional/unzip" "./examples/Optional/unzip/1"+        , shouldNormalize "Text/concat" "./examples/Text/concat/0"+        , shouldNormalize "Text/concat" "./examples/Text/concat/1"+        , shouldNormalize "Text/concatMap" "./examples/Text/concatMap/0"+        , shouldNormalize "Text/concatMap" "./examples/Text/concatMap/1"+        , shouldNormalize "Text/concatMapSep" "./examples/Text/concatMapSep/0"+        , shouldNormalize "Text/concatMapSep" "./examples/Text/concatMapSep/1"+        , shouldNormalize "Text/concatSep" "./examples/Text/concatSep/0"+        , shouldNormalize "Text/concatSep" "./examples/Text/concatSep/1"+        ]++simplifications :: TestTree+simplifications =+    testGroup "Simplifications"+        [ shouldNormalize "if/then/else" "./simplifications/ifThenElse"+        , shouldNormalize "||" "./simplifications/or"+        , shouldNormalize "&&" "./simplifications/and"+        , shouldNormalize "==" "./simplifications/eq"+        , shouldNormalize "!=" "./simplifications/ne"         ]  constantFolding :: TestTree
tests/Tests.hs view
@@ -1,7 +1,6 @@ module Main where  import Normalization (normalizationTests)-import Examples (exampleTests) import Parser (parserTests) import Regression (regressionTests) import Tutorial (tutorialTests)@@ -13,7 +12,6 @@ allTests =     testGroup "Dhall Tests"         [ normalizationTests-        , exampleTests         , parserTests         , regressionTests         , tutorialTests
tests/TypeCheck.hs view
@@ -4,8 +4,6 @@  import Data.Monoid (mempty, (<>)) import Data.Text.Lazy (Text)-import Dhall.Core (Expr)-import Dhall.TypeCheck (X) import Test.Tasty (TestTree)  import qualified Control.Exception@@ -20,12 +18,28 @@ typecheckTests :: TestTree typecheckTests =     Test.Tasty.testGroup "typecheck tests"-        [ should+        [ Test.Tasty.testGroup "Prelude examples"+            [ should "Monoid" "./examples/Monoid/00"+            , should "Monoid" "./examples/Monoid/01"+            , should "Monoid" "./examples/Monoid/02"+            , should "Monoid" "./examples/Monoid/03"+            , should "Monoid" "./examples/Monoid/04"+            , should "Monoid" "./examples/Monoid/05"+            , should "Monoid" "./examples/Monoid/06"+            , should "Monoid" "./examples/Monoid/07"+            , should "Monoid" "./examples/Monoid/08"+            , should "Monoid" "./examples/Monoid/09"+            , should "Monoid" "./examples/Monoid/10"+            ]+        , should             "allow type-valued fields in a record"             "fieldsAreTypes"         , should             "allow type-valued alternatives in a union"             "alternativesAreTypes"+        , should+            "allow anonymous functions in types to be judgmentally equal"+            "anonymousFunctionsInTypes"         ]  should :: Text -> Text -> TestTree@@ -37,17 +51,13 @@         actualExpr <- case Dhall.Parser.exprFromText mempty actualCode of             Left  err  -> Control.Exception.throwIO err             Right expr -> return expr-        actualResolved <- Dhall.Import.load actualExpr-        actualType <- case Dhall.TypeCheck.typeOf actualResolved of-            Left  err  -> Control.Exception.throwIO err-            Right expr -> return expr-        let actualNormalized = Dhall.Core.normalize actualType :: Expr X X-         expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of             Left  err  -> Control.Exception.throwIO err             Right expr -> return expr-        expectedResolved <- Dhall.Import.load expectedExpr-        let expectedNormalized = Dhall.Core.normalize expectedResolved -        let message = "The expression's type did not match the expected type"-        Test.Tasty.HUnit.assertEqual message expectedNormalized actualNormalized+        let annotatedExpr = Dhall.Core.Annot actualExpr expectedExpr++        resolvedExpr <- Dhall.Import.load annotatedExpr+        case Dhall.TypeCheck.typeOf resolvedExpr of+            Left  err -> Control.Exception.throwIO err+            Right _   -> return ()
+ tests/normalization/examples/Bool/and/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/and [ True, False, True ]
+ tests/normalization/examples/Bool/and/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/and/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/and ([] : List Bool)
+ tests/normalization/examples/Bool/and/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/build/0A.dhall view
@@ -0,0 +1,2 @@+../../../../../Prelude/Bool/build +(λ(bool : Type) → λ(true : bool) → λ(false : bool) → true)
+ tests/normalization/examples/Bool/build/0B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/build/1A.dhall view
@@ -0,0 +1,2 @@+../../../../../Prelude/Bool/build +(λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)
+ tests/normalization/examples/Bool/build/1B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/even/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/even [ False, True, False ]
+ tests/normalization/examples/Bool/even/0B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/even/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/even [ False, True ]
+ tests/normalization/examples/Bool/even/1B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/even/2A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/even [ False ]
+ tests/normalization/examples/Bool/even/2B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/even/3A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/even ([] : List Bool)
+ tests/normalization/examples/Bool/even/3B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/fold/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/fold True Integer 0 1
+ tests/normalization/examples/Bool/fold/0B.dhall view
@@ -0,0 +1,1 @@+0
+ tests/normalization/examples/Bool/fold/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/fold False Integer 0 1
+ tests/normalization/examples/Bool/fold/1B.dhall view
@@ -0,0 +1,1 @@+1
+ tests/normalization/examples/Bool/not/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/not True
+ tests/normalization/examples/Bool/not/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/not/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/not False
+ tests/normalization/examples/Bool/not/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/odd/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/odd [ True, False, True ]
+ tests/normalization/examples/Bool/odd/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/odd/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/odd [ True, False ]
+ tests/normalization/examples/Bool/odd/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/odd/2A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/odd [ True ]
+ tests/normalization/examples/Bool/odd/2B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/odd/3A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/odd ([] : List Bool)
+ tests/normalization/examples/Bool/odd/3B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/or/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/or [ True, False, True ]
+ tests/normalization/examples/Bool/or/0B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Bool/or/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/or ([] : List Bool)
+ tests/normalization/examples/Bool/or/1B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Bool/show/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/show True
+ tests/normalization/examples/Bool/show/0B.dhall view
@@ -0,0 +1,1 @@+"True"
+ tests/normalization/examples/Bool/show/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Bool/show False
+ tests/normalization/examples/Bool/show/1B.dhall view
@@ -0,0 +1,1 @@+"False"
+ tests/normalization/examples/Double/show/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Double/show -3.1
+ tests/normalization/examples/Double/show/0B.dhall view
@@ -0,0 +1,1 @@+"-3.1"
+ tests/normalization/examples/Double/show/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Double/show 0.4
+ tests/normalization/examples/Double/show/1B.dhall view
@@ -0,0 +1,1 @@+"0.4"
+ tests/normalization/examples/Integer/show/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Integer/show -3
+ tests/normalization/examples/Integer/show/0B.dhall view
@@ -0,0 +1,1 @@+"-3"
+ tests/normalization/examples/Integer/show/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Integer/show 0
+ tests/normalization/examples/Integer/show/1B.dhall view
@@ -0,0 +1,1 @@+"0"
+ tests/normalization/examples/List/all/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/all Natural Natural/even [ +2, +3, +5 ]
+ tests/normalization/examples/List/all/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/List/all/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/all Natural Natural/even ([] : List Natural)
+ tests/normalization/examples/List/all/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/List/any/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/any Natural Natural/even [ +2, +3, +5 ]
+ tests/normalization/examples/List/any/0B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/List/any/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/any Natural Natural/even ([] : List Natural)
+ tests/normalization/examples/List/any/1B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/List/build/0A.dhall view
@@ -0,0 +1,7 @@+../../../../../Prelude/List/build+Text+( λ(list : Type)+→ λ(cons : Text → list → list)+→ λ(nil : list)+→ cons "ABC" (cons "DEF" nil)+)
+ tests/normalization/examples/List/build/0B.dhall view
@@ -0,0 +1,1 @@+[ "ABC", "DEF" ]
+ tests/normalization/examples/List/build/1A.dhall view
@@ -0,0 +1,7 @@+../../../../../Prelude/List/build+Text+( λ(list : Type)+→ λ(cons : Text → list → list)+→ λ(nil : list)+→ nil+)
+ tests/normalization/examples/List/build/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Text
+ tests/normalization/examples/List/concat/0A.dhall view
@@ -0,0 +1,5 @@+../../../../../Prelude/List/concat Integer+[ [ 0, 1, 2 ]+, [ 3, 4 ]+, [ 5, 6, 7, 8 ]+]
+ tests/normalization/examples/List/concat/0B.dhall view
@@ -0,0 +1,1 @@+[ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
+ tests/normalization/examples/List/concat/1A.dhall view
@@ -0,0 +1,5 @@+../../../../../Prelude/List/concat Integer+[ [] : List Integer+, [] : List Integer+, [] : List Integer+]
+ tests/normalization/examples/List/concat/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Integer
+ tests/normalization/examples/List/concatMap/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ +2, +3, +5 ]
+ tests/normalization/examples/List/concatMap/0B.dhall view
@@ -0,0 +1,1 @@+[ +2, +2, +3, +3, +5, +5 ]
+ tests/normalization/examples/List/concatMap/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) ([] : List Natural)
+ tests/normalization/examples/List/concatMap/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Natural
+ tests/normalization/examples/List/filter/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/filter Natural Natural/even [ +2, +3, +5 ]
+ tests/normalization/examples/List/filter/0B.dhall view
@@ -0,0 +1,1 @@+[ +2 ]
+ tests/normalization/examples/List/filter/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/filter Natural Natural/odd [ +2, +3, +5 ]
+ tests/normalization/examples/List/filter/1B.dhall view
@@ -0,0 +1,1 @@+[ +3, +5 ]
+ tests/normalization/examples/List/fold/0A.dhall view
@@ -0,0 +1,6 @@+../../../../../Prelude/List/fold+Natural+[ +2, +3, +5 ]+Natural+(λ(x : Natural) → λ(y : Natural) → x + y)++0
+ tests/normalization/examples/List/fold/0B.dhall view
@@ -0,0 +1,1 @@++10
+ tests/normalization/examples/List/fold/1A.dhall view
@@ -0,0 +1,7 @@+  λ(nil : Natural)+→ ../../../../../Prelude/List/fold+  Natural+  [ +2, +3, +5 ]+  Natural+  (λ(x : Natural) → λ(y : Natural) → x + y)+  nil
+ tests/normalization/examples/List/fold/1B.dhall view
@@ -0,0 +1,1 @@+λ(nil : Natural) → +2 + +3 + +5 + nil
+ tests/normalization/examples/List/fold/2A.dhall view
@@ -0,0 +1,4 @@+  λ(list : Type)+→ λ(cons : Natural → list → list)+→ λ(nil : list)+→ ../../../../../Prelude/List/fold Natural [ +2, +3, +5 ] list cons nil
+ tests/normalization/examples/List/fold/2B.dhall view
@@ -0,0 +1,4 @@+  λ(list : Type)+→ λ(cons : Natural → list → list)+→ λ(nil : list)+→ cons +2 (cons +3 (cons +5 nil))
+ tests/normalization/examples/List/generate/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/generate +5 Bool Natural/even
+ tests/normalization/examples/List/generate/0B.dhall view
@@ -0,0 +1,1 @@+[ True, False, True, False, True ]
+ tests/normalization/examples/List/generate/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/generate +0 Bool Natural/even
+ tests/normalization/examples/List/generate/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Bool
+ tests/normalization/examples/List/head/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/head Integer [ 0, 1, 2 ]
+ tests/normalization/examples/List/head/0B.dhall view
@@ -0,0 +1,1 @@+[ 0 ] : Optional Integer
+ tests/normalization/examples/List/head/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/head Integer ([] : List Integer)
+ tests/normalization/examples/List/head/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/List/indexed/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/indexed Bool ([] : List Bool)
+ tests/normalization/examples/List/indexed/0B.dhall view
@@ -0,0 +1,4 @@+[ { index = +0, value = True }+, { index = +1, value = False }+, { index = +2, valu;e = True }+]
+ tests/normalization/examples/List/indexed/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/indexed Bool ([] : List Bool)
+ tests/normalization/examples/List/indexed/1B.dhall view
@@ -0,0 +1,1 @@+[] : List { index : Natural, value : Bool }
+ tests/normalization/examples/List/iterate/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1
+ tests/normalization/examples/List/iterate/0B.dhall view
@@ -0,0 +1,1 @@+[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]
+ tests/normalization/examples/List/iterate/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1
+ tests/normalization/examples/List/iterate/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Natural
+ tests/normalization/examples/List/last/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/last Integer [ 0, 1, 2 ]
+ tests/normalization/examples/List/last/0B.dhall view
@@ -0,0 +1,1 @@+[ 2 ] : Optional Integer
+ tests/normalization/examples/List/last/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/last Integer ([] : List Integer)
+ tests/normalization/examples/List/last/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/List/length/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/length Integer [ 0, 1, 2 ]
+ tests/normalization/examples/List/length/0B.dhall view
@@ -0,0 +1,1 @@++3
+ tests/normalization/examples/List/length/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/length Integer ([] : List Integer)
+ tests/normalization/examples/List/length/1B.dhall view
@@ -0,0 +1,1 @@++0
+ tests/normalization/examples/List/map/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/map Natural Bool Natural/even [ +2, +3, +5 ]
+ tests/normalization/examples/List/map/0B.dhall view
@@ -0,0 +1,1 @@+[ True, False, False ]
+ tests/normalization/examples/List/map/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/map Natural Bool Natural/even ([] : List Natural)
+ tests/normalization/examples/List/map/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Bool
+ tests/normalization/examples/List/null/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/null Integer [ 0, 1, 2 ]
+ tests/normalization/examples/List/null/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/List/null/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/null Integer ([] : List Integer)
+ tests/normalization/examples/List/null/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/List/replicate/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/replicate +9 Integer 1
+ tests/normalization/examples/List/replicate/0B.dhall view
@@ -0,0 +1,1 @@+[ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
+ tests/normalization/examples/List/replicate/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/replicate +0 Integer 1
+ tests/normalization/examples/List/replicate/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Integer
+ tests/normalization/examples/List/reverse/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/reverse Integer [ 0, 1, 2 ]
+ tests/normalization/examples/List/reverse/0B.dhall view
@@ -0,0 +1,1 @@+[ 2, 1, 0 ]
+ tests/normalization/examples/List/reverse/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/reverse Integer ([] : List Integer)
+ tests/normalization/examples/List/reverse/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Integer
+ tests/normalization/examples/List/shifted/0A.dhall view
@@ -0,0 +1,15 @@+../../../../../Prelude/List/shifted+Bool+[ [ { index = +0, value = True }+  , { index = +1, value = True }+  , { index = +2, value = False }+  ]+, [ { index = +0, value = False }+  , { index = +1, value = False }+  ]+, [ { index = +0, value = True }+  , { index = +1, value = True }+  , { index = +2, value = True }+  , { index = +3, value = True }+  ]+]
+ tests/normalization/examples/List/shifted/0B.dhall view
@@ -0,0 +1,10 @@+[ { index = +0, value = True }+, { index = +1, value = True }+, { index = +2, value = False }+, { index = +3, value = False }+, { index = +4, value = False }+, { index = +5, value = True }+, { index = +6, value = True }+, { index = +7, value = True }+, { index = +8, value = True }+]
+ tests/normalization/examples/List/shifted/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/shifted Bool ([] : List (List { index : Natural, value : Bool }))
+ tests/normalization/examples/List/shifted/1B.dhall view
@@ -0,0 +1,1 @@+[] : List { index : Natural, value : Bool }
+ tests/normalization/examples/List/unzip/0A.dhall view
@@ -0,0 +1,7 @@+../../../../../Prelude/List/unzip+Text+Bool+[ { _1 = "ABC", _2 = True }+, { _1 = "DEF", _2 = False }+, { _1 = "GHI", _2 = True }+]
+ tests/normalization/examples/List/unzip/0B.dhall view
@@ -0,0 +1,1 @@+{ _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }
+ tests/normalization/examples/List/unzip/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/List/unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
+ tests/normalization/examples/List/unzip/1B.dhall view
@@ -0,0 +1,1 @@+{ _1 = [] : List Text, _2 = [] : List Bool }
+ tests/normalization/examples/Natural/build/0A.dhall view
@@ -0,0 +1,6 @@+../../../../../Prelude/Natural/build+( λ(natural : Type)+→ λ(succ : natural → natural)+→ λ(zero : natural)+→ succ (succ (succ zero))+)
+ tests/normalization/examples/Natural/build/0B.dhall view
@@ -0,0 +1,1 @@++3
+ tests/normalization/examples/Natural/build/1A.dhall view
@@ -0,0 +1,6 @@+../../../../../Prelude/Natural/build+( λ(natural : Type)+→ λ(succ : natural → natural)+→ λ(zero : natural)+→ zero+)
+ tests/normalization/examples/Natural/build/1B.dhall view
@@ -0,0 +1,1 @@++0
+ tests/normalization/examples/Natural/enumerate/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/enumerate +10
+ tests/normalization/examples/Natural/enumerate/0B.dhall view
@@ -0,0 +1,1 @@+[ +0, +1, +2, +3, +4, +5, +6, +7, +8, +9 ]
+ tests/normalization/examples/Natural/enumerate/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/enumerate +0
+ tests/normalization/examples/Natural/enumerate/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Natural
+ tests/normalization/examples/Natural/even/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/even +3
+ tests/normalization/examples/Natural/even/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Natural/even/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/even +0
+ tests/normalization/examples/Natural/even/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Natural/fold/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) +1
+ tests/normalization/examples/Natural/fold/0B.dhall view
@@ -0,0 +1,1 @@++125
+ tests/normalization/examples/Natural/fold/1A.dhall view
@@ -0,0 +1,1 @@+λ(zero : Natural) → ../../../../../Prelude/Natural/fold +3 Natural (λ(x : Natural) → +5 * x) zero
+ tests/normalization/examples/Natural/fold/1B.dhall view
@@ -0,0 +1,1 @@+λ(zero : Natural) → +5 * +5 * +5 * zero
+ tests/normalization/examples/Natural/fold/2A.dhall view
@@ -0,0 +1,4 @@+  λ(natural : Type)+→ λ(succ : natural → natural)+→ λ(zero : natural)+→ ../../../../../Prelude/Natural/fold +3 natural succ zero
+ tests/normalization/examples/Natural/fold/2B.dhall view
@@ -0,0 +1,1 @@+λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) → succ (succ (succ zero))
+ tests/normalization/examples/Natural/isZero/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/isZero +2
+ tests/normalization/examples/Natural/isZero/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Natural/isZero/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/isZero +0
+ tests/normalization/examples/Natural/isZero/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Natural/odd/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/odd +3
+ tests/normalization/examples/Natural/odd/0B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Natural/odd/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/odd +0
+ tests/normalization/examples/Natural/odd/1B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Natural/product/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/product [ +2, +3, +5 ]
+ tests/normalization/examples/Natural/product/0B.dhall view
@@ -0,0 +1,1 @@++30
+ tests/normalization/examples/Natural/product/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/product ([] : List Natural)
+ tests/normalization/examples/Natural/product/1B.dhall view
@@ -0,0 +1,1 @@++1
+ tests/normalization/examples/Natural/show/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/show +3
+ tests/normalization/examples/Natural/show/0B.dhall view
@@ -0,0 +1,1 @@+"+3"
+ tests/normalization/examples/Natural/show/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/show +0
+ tests/normalization/examples/Natural/show/1B.dhall view
@@ -0,0 +1,1 @@+"+0"
+ tests/normalization/examples/Natural/sum/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/sum [ +2, +3, +5 ]
+ tests/normalization/examples/Natural/sum/0B.dhall view
@@ -0,0 +1,1 @@++10
+ tests/normalization/examples/Natural/sum/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/sum ([] : List Natural)
+ tests/normalization/examples/Natural/sum/1B.dhall view
@@ -0,0 +1,1 @@++0
+ tests/normalization/examples/Natural/toInteger/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/toInteger +3
+ tests/normalization/examples/Natural/toInteger/0B.dhall view
@@ -0,0 +1,1 @@+3
+ tests/normalization/examples/Natural/toInteger/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Natural/toInteger +0
+ tests/normalization/examples/Natural/toInteger/1B.dhall view
@@ -0,0 +1,1 @@+0
+ tests/normalization/examples/Optional/all/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/all Natural Natural/even ([ +3 ] : Optional Natural)
+ tests/normalization/examples/Optional/all/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Optional/all/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/all Natural Natural/even ([] : Optional Natural)
+ tests/normalization/examples/Optional/all/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Optional/any/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/any Natural Natural/even ([ +2 ] : Optional Natural)
+ tests/normalization/examples/Optional/any/0B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Optional/any/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/any Natural Natural/even ([] : Optional Natural)
+ tests/normalization/examples/Optional/any/1B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Optional/build/0A.dhall view
@@ -0,0 +1,7 @@+../../../../../Prelude/Optional/build+Integer+( λ(optional : Type)+→ λ(just : Integer → optional)+→ λ(nothing : optional)+→ just 1+)
+ tests/normalization/examples/Optional/build/0B.dhall view
@@ -0,0 +1,1 @@+[ 1 ] : Optional Integer
+ tests/normalization/examples/Optional/build/1A.dhall view
@@ -0,0 +1,7 @@+../../../../../Prelude/Optional/build+Integer+( λ(optional : Type)+→ λ(just : Integer → optional)+→ λ(nothing : optional)+→ nothing+)
+ tests/normalization/examples/Optional/build/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/Optional/concat/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer))
+ tests/normalization/examples/Optional/concat/0B.dhall view
@@ -0,0 +1,1 @@+[ 1 ] : Optional Integer
+ tests/normalization/examples/Optional/concat/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer))
+ tests/normalization/examples/Optional/concat/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/Optional/concat/2A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/concat Integer ([ [] : Optional Integer ]: Optional (Optional Integer))
+ tests/normalization/examples/Optional/concat/2B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/Optional/filter/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/filter Natural Natural/even ([ +2 ] : Optional Natural)
+ tests/normalization/examples/Optional/filter/0B.dhall view
@@ -0,0 +1,1 @@+[ +2 ] : Optional Natural
+ tests/normalization/examples/Optional/filter/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/filter Natural Natural/odd ([ +2 ] : Optional Natural)
+ tests/normalization/examples/Optional/filter/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Natural
+ tests/normalization/examples/Optional/fold/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0
+ tests/normalization/examples/Optional/fold/0B.dhall view
@@ -0,0 +1,1 @@+2
+ tests/normalization/examples/Optional/fold/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0
+ tests/normalization/examples/Optional/fold/1B.dhall view
@@ -0,0 +1,1 @@+0
+ tests/normalization/examples/Optional/head/0A.dhall view
@@ -0,0 +1,6 @@+../../../../../Prelude/Optional/head+Integer+[ []    : Optional Integer+, [ 1 ] : Optional Integer+, [ 2 ] : Optional Integer+]
+ tests/normalization/examples/Optional/head/0B.dhall view
@@ -0,0 +1,1 @@+[ 1 ] : Optional Integer
+ tests/normalization/examples/Optional/head/1A.dhall view
@@ -0,0 +1,3 @@+../../../../../Prelude/Optional/head+Integer+[ [] : Optional Integer, [] : Optional Integer ]
+ tests/normalization/examples/Optional/head/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/Optional/last/0A.dhall view
@@ -0,0 +1,7 @@+../../../../../Prelude/Optional/last+Integer+( [ [] : Optional Integer+  , [ 1 ] : Optional Integer+  , [ 2 ] : Optional Integer+  ]+)
+ tests/normalization/examples/Optional/last/0B.dhall view
@@ -0,0 +1,1 @@+[ 2 ] : Optional Integer
+ tests/normalization/examples/Optional/last/1A.dhall view
@@ -0,0 +1,3 @@+../../../../../Prelude/Optional/last+Integer+[ [] : Optional Integer, [] : Optional Integer ]
+ tests/normalization/examples/Optional/last/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/Optional/last/2A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/last Integer ([] : List (Optional Integer))
+ tests/normalization/examples/Optional/last/2B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Integer
+ tests/normalization/examples/Optional/length/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/length Integer ([ 2 ] : Optional Integer)
+ tests/normalization/examples/Optional/length/0B.dhall view
@@ -0,0 +1,1 @@++1
+ tests/normalization/examples/Optional/length/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/length Integer ([] : Optional Integer)
+ tests/normalization/examples/Optional/length/1B.dhall view
@@ -0,0 +1,1 @@++0
+ tests/normalization/examples/Optional/map/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/map Natural Bool Natural/even ([ +3 ] : Optional Natural)
+ tests/normalization/examples/Optional/map/0B.dhall view
@@ -0,0 +1,1 @@+[ False ] : Optional Bool
+ tests/normalization/examples/Optional/map/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural)
+ tests/normalization/examples/Optional/map/1B.dhall view
@@ -0,0 +1,1 @@+[] : Optional Bool
+ tests/normalization/examples/Optional/null/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/null Integer ([ 2 ] : Optional Integer)
+ tests/normalization/examples/Optional/null/0B.dhall view
@@ -0,0 +1,1 @@+False
+ tests/normalization/examples/Optional/null/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/null Integer ([] : Optional Integer)
+ tests/normalization/examples/Optional/null/1B.dhall view
@@ -0,0 +1,1 @@+True
+ tests/normalization/examples/Optional/toList/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/toList Integer ([ 1 ] : Optional Integer)
+ tests/normalization/examples/Optional/toList/0B.dhall view
@@ -0,0 +1,1 @@+[ 1 ]
+ tests/normalization/examples/Optional/toList/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/toList Integer ([] : Optional Integer)
+ tests/normalization/examples/Optional/toList/1B.dhall view
@@ -0,0 +1,1 @@+[] : List Integer
+ tests/normalization/examples/Optional/unzip/0A.dhall view
@@ -0,0 +1,4 @@+../../../../../Prelude/Optional/unzip+Text+Bool+([ { _1 = "ABC", _2 = True } ] : Optional { _1 : Text, _2 : Bool })
+ tests/normalization/examples/Optional/unzip/0B.dhall view
@@ -0,0 +1,1 @@+{ _1 = [ "ABC" ] : Optional Text, _2 = [ True ] : Optional Bool }
+ tests/normalization/examples/Optional/unzip/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Optional/unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool })
+ tests/normalization/examples/Optional/unzip/1B.dhall view
@@ -0,0 +1,1 @@+{ _1 = [] : Optional Text, _2 = [] : Optional Bool }
+ tests/normalization/examples/Text/concat/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concat [ "ABC", "DEF", "GHI" ]
+ tests/normalization/examples/Text/concat/0B.dhall view
@@ -0,0 +1,1 @@+"ABCDEFGHI"
+ tests/normalization/examples/Text/concat/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concat ([] : List Text)
+ tests/normalization/examples/Text/concat/1B.dhall view
@@ -0,0 +1,1 @@+""
+ tests/normalization/examples/Text/concatMap/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ]
+ tests/normalization/examples/Text/concatMap/0B.dhall view
@@ -0,0 +1,1 @@+"0 1 2 "
+ tests/normalization/examples/Text/concatMap/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer)
+ tests/normalization/examples/Text/concatMap/1B.dhall view
@@ -0,0 +1,1 @@+""
+ tests/normalization/examples/Text/concatMapSep/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show [ 0, 1, 2 ]
+ tests/normalization/examples/Text/concatMapSep/0B.dhall view
@@ -0,0 +1,1 @@+"0, 1, 2"
+ tests/normalization/examples/Text/concatMapSep/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concatMapSep ", " Integer Integer/show ([] : List Integer)
+ tests/normalization/examples/Text/concatMapSep/1B.dhall view
@@ -0,0 +1,1 @@+""
+ tests/normalization/examples/Text/concatSep/0A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concatSep ", " [ "ABC", "DEF", "GHI" ]
+ tests/normalization/examples/Text/concatSep/0B.dhall view
@@ -0,0 +1,1 @@+"ABC, DEF, GHI"
+ tests/normalization/examples/Text/concatSep/1A.dhall view
@@ -0,0 +1,1 @@+../../../../../Prelude/Text/concatSep ", " ([] : List Text)
+ tests/normalization/examples/Text/concatSep/1B.dhall view
@@ -0,0 +1,1 @@+""
+ tests/normalization/listBuildA.dhall view
@@ -0,0 +1,22 @@+{ example0 =+    List/build+    Bool+    (   λ(list : Type)+      → λ(cons : Bool → list → list)+      → λ(nil : list)+      → cons True (cons False nil)+    )+, example1 =+    List/build+    Bool+    (λ(x : Type) → λ(x : Bool → x → x) → λ(x : x@1) → x@1 True (x@1 False x))+, example2 =+      λ(id : ∀(a : Type) → a → a)+    → List/build+      Bool+      (   λ(list : Type)+        → λ(cons : Bool → list → list)+        → λ(nil : list)+        → id list (cons True (cons False nil))+      )+}
+ tests/normalization/listBuildB.dhall view
@@ -0,0 +1,7 @@+{ example0 =+    [ True, False ] : List Bool+, example1 =+    [ True, False ] : List Bool+, example2 =+    λ(id : ∀(a : Type) → a → a) → id (List Bool) [ True, False ]+}
+ tests/normalization/naturalBuildA.dhall view
@@ -0,0 +1,18 @@+{ example0 =+    Natural/build+    (   λ(natural : Type)+      → λ(succ : natural → natural)+      → λ(zero : natural)+      → succ zero+    )+, example1 =+    Natural/build (λ(x : Type) → λ(x : x → x) → λ(x : x@1) → x@1 x)+, example2 =+      λ(id : ∀(a : Type) → a → a)+    → Natural/build+      (   λ(natural : Type)+        → λ(succ : natural → natural)+        → λ(zero : natural)+        → id natural (succ zero)+      )+}
+ tests/normalization/naturalBuildB.dhall view
@@ -0,0 +1,7 @@+{ example0 =+    +1+, example1 =+    +1+, example2 =+    λ(id : ∀(a : Type) → a → a) → id Natural +1+}
tests/normalization/optionalBuildA.dhall view
@@ -19,4 +19,14 @@         → λ(nothing : optional)         → id optional (just True)       )+, example3 =+      λ(a : Type)+    → λ(x : a)+    → Optional/build+      a+      (   λ(optional : Type)+        → λ(just : a → optional)+        → λ(nothing : optional)+        → just x+      ) }
tests/normalization/optionalBuildB.dhall view
@@ -1,12 +1,9 @@-{ example0 = [ +1 ] : Optional Natural-, example1 = [ 1 ] : Optional Integer+{ 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)-      )+    λ(id : ∀(a : Type) → a → a) → id (Optional Bool) ([ True ] : Optional Bool)+, example3 =+    λ(a : Type) → λ(x : a) → [ x ] : Optional a }
tests/normalization/optionalBuildFoldA.dhall view
@@ -1,11 +1,1 @@-{ 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))-}+Optional/build Text (Optional/fold Text ([ "foo" ] : Optional Text))
tests/normalization/optionalBuildFoldB.dhall view
@@ -1,10 +1,1 @@-{ example0 =-      λ ( f-        :   ∀(optional : Type)-          → ∀(just : Text → optional)-          → ∀(nothing : optional)-          → optional-        )-    → f-, example1 = [ "foo" ] : Optional Text-}+[ "foo" ] : Optional Text
tests/normalization/remoteSystemsA.dhall view
@@ -1,8 +1,8 @@     let Text/concatMap =-          https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Text/concatMap +          ../../Prelude/Text/concatMap   in  let Text/concatSep =-          https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/Text/concatSep +          ../../Prelude/Text/concatSep   in  let Row =           { cores :
+ tests/normalization/simplifications/andA.dhall view
@@ -0,0 +1,6 @@+{ example0 = λ(x : Bool) → x && True+, example1 = λ(x : Bool) → True && x+, example2 = λ(x : Bool) → x && False+, example3 = λ(x : Bool) → False && x+, example4 = λ(x : Bool) → x && x+}
+ tests/normalization/simplifications/andB.dhall view
@@ -0,0 +1,6 @@+{ example0 = λ(x : Bool) → x+, example1 = λ(x : Bool) → x+, example2 = λ(x : Bool) → False+, example3 = λ(x : Bool) → False+, example4 = λ(x : Bool) → x+}
+ tests/normalization/simplifications/eqA.dhall view
@@ -0,0 +1,4 @@+{ example0 = λ(x : Bool) → x == True+, example1 = λ(x : Bool) → True == x+, example2 = λ(x : Bool) → x == x+}
+ tests/normalization/simplifications/eqB.dhall view
@@ -0,0 +1,4 @@+{ example0 = λ(x : Bool) → x+, example1 = λ(x : Bool) → x+, example2 = λ(x : Bool) → True+}
+ tests/normalization/simplifications/ifThenElseA.dhall view
@@ -0,0 +1,3 @@+{ example0 = λ(x : Bool) → if x then True else False+, example1 = λ(x : Bool) → λ(y : Text) → if x then y else y+}
+ tests/normalization/simplifications/ifThenElseB.dhall view
@@ -0,0 +1,3 @@+{ example0 = λ(x : Bool) → x+, example1 = λ(x : Bool) → λ(y : Text) → y+}
+ tests/normalization/simplifications/neA.dhall view
@@ -0,0 +1,4 @@+{ example0 = λ(x : Bool) → x != False+, example1 = λ(x : Bool) → False != x+, example2 = λ(x : Bool) → x != x+}
+ tests/normalization/simplifications/neB.dhall view
@@ -0,0 +1,4 @@+{ example0 = λ(x : Bool) → x+, example1 = λ(x : Bool) → x+, example2 = λ(x : Bool) → False+}
+ tests/normalization/simplifications/orA.dhall view
@@ -0,0 +1,6 @@+{ example0 = λ(x : Bool) → x || True+, example1 = λ(x : Bool) → True || x+, example2 = λ(x : Bool) → x || False+, example3 = λ(x : Bool) → False || x+, example4 = λ(x : Bool) → x || x+}
+ tests/normalization/simplifications/orB.dhall view
@@ -0,0 +1,6 @@+{ example0 = λ(x : Bool) → True+, example1 = λ(x : Bool) → True+, example2 = λ(x : Bool) → x+, example3 = λ(x : Bool) → x+, example4 = λ(x : Bool) → x+}
+ tests/typecheck/anonymousFunctionsInTypesA.dhall view
@@ -0,0 +1,5 @@+    let anonymousFunction = λ(a : Type) → List a++in    λ(HigherOrderType : (Type → Type) → Type)+    → λ(x : HigherOrderType anonymousFunction)+    → (x : HigherOrderType anonymousFunction)
+ tests/typecheck/anonymousFunctionsInTypesB.dhall view
@@ -0,0 +1,4 @@+  ∀(HigherOrderType : (Type → Type) → Type)+→ ∀(x : HigherOrderType (λ(a : Type) → List a))+→ HigherOrderType (λ(a : Type) → List a)+
+ tests/typecheck/examples/Monoid/00A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Bool/and
+ tests/typecheck/examples/Monoid/00B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Bool
+ tests/typecheck/examples/Monoid/01A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Bool/or
+ tests/typecheck/examples/Monoid/01B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Bool
+ tests/typecheck/examples/Monoid/02A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Bool/even
+ tests/typecheck/examples/Monoid/02B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Bool
+ tests/typecheck/examples/Monoid/03A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Bool/odd
+ tests/typecheck/examples/Monoid/03B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Bool
+ tests/typecheck/examples/Monoid/04A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/List/concat
+ tests/typecheck/examples/Monoid/04B.dhall view
@@ -0,0 +1,1 @@+∀(a : Type) → ../../../../Prelude/Monoid (List a)
+ tests/typecheck/examples/Monoid/05A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/List/shifted
+ tests/typecheck/examples/Monoid/05B.dhall view
@@ -0,0 +1,1 @@+∀(a : Type) → ../../../../Prelude/Monoid (List { index : Natural, value : a })
+ tests/typecheck/examples/Monoid/06A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Natural/sum
+ tests/typecheck/examples/Monoid/06B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Natural
+ tests/typecheck/examples/Monoid/07A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Natural/product
+ tests/typecheck/examples/Monoid/07B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Natural
+ tests/typecheck/examples/Monoid/08A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Optional/head
+ tests/typecheck/examples/Monoid/08B.dhall view
@@ -0,0 +1,1 @@+∀(a : Type) → ../../../../Prelude/Monoid (Optional a)
+ tests/typecheck/examples/Monoid/09A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Optional/last
+ tests/typecheck/examples/Monoid/09B.dhall view
@@ -0,0 +1,1 @@+∀(a : Type) → ../../../../Prelude/Monoid (Optional a)
+ tests/typecheck/examples/Monoid/10A.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Text/concat
+ tests/typecheck/examples/Monoid/10B.dhall view
@@ -0,0 +1,1 @@+../../../../Prelude/Monoid Text