dhall 1.2.0 → 1.3.0

raw patch · 60 files changed

+3146/−209 lines, 60 filesdep +charsetdep +tastydep +tasty-hunitdep ~basedep ~vectorPVP ok

version bump matches the API change (PVP)

Dependencies added: charset, tasty, tasty-hunit

Dependency ranges changed: base, vector

API changes (from Hackage documentation)

+ Dhall.Core: DoubleShow :: Expr s a

+ Dhall.Core: IntegerShow :: Expr s a

+ Dhall.Core: NaturalShow :: Expr s a

+ Dhall.Core: NaturalToInteger :: Expr s a

+ Dhall.Core: OptionalBuild :: Expr s a

+ Dhall.Core: Prefer :: (Expr s a) -> (Expr s a) -> Expr s a

+ Dhall.Core: instance (GHC.Classes.Eq a, GHC.Classes.Eq s) => GHC.Classes.Eq (Dhall.Core.Expr s a)

+ Dhall.Core: instance GHC.Classes.Eq Dhall.Core.Const

+ Dhall.Core: reservedIdentifiers :: HashSet String

+ Dhall.TypeCheck: instance GHC.Classes.Eq Dhall.TypeCheck.X

- Dhall.TypeCheck: MustCombineARecord :: (Expr s X) -> (Expr s X) -> TypeMessage s

+ Dhall.TypeCheck: MustCombineARecord :: Char -> (Expr s X) -> (Expr s X) -> TypeMessage s

Files

CHANGELOG.md +26/−0
Prelude/Bool/and +17/−0
Prelude/Bool/build +16/−0
Prelude/Bool/even +21/−0
Prelude/Bool/fold +19/−0
Prelude/Bool/not +15/−0
Prelude/Bool/odd +21/−0
Prelude/Bool/or +17/−0
Prelude/Bool/show +16/−0
Prelude/Double/show +16/−0
Prelude/Integer/show +16/−0
Prelude/List/all +19/−0
Prelude/List/any +19/−0
Prelude/List/build +32/−0
Prelude/List/concat +50/−0
Prelude/List/filter +29/−0
Prelude/List/fold +46/−0
Prelude/List/generate +37/−0
Prelude/List/head +15/−0
Prelude/List/indexed +20/−0
Prelude/List/iterate +42/−0
Prelude/List/last +15/−0
Prelude/List/length +15/−0
Prelude/List/map +26/−0
Prelude/List/null +15/−0
Prelude/List/replicate +23/−0
Prelude/List/reverse +15/−0
Prelude/List/shifted +80/−0
Prelude/List/unzip +55/−0
Prelude/Monoid +42/−0
Prelude/Natural/build +33/−0
Prelude/Natural/enumerate +38/−0
Prelude/Natural/even +15/−0
Prelude/Natural/fold +33/−0
Prelude/Natural/isZero +15/−0
Prelude/Natural/odd +15/−0
Prelude/Natural/product +16/−0
Prelude/Natural/show +16/−0
Prelude/Natural/sum +16/−0
Prelude/Natural/toInteger +15/−0
Prelude/Optional/build +36/−0
Prelude/Optional/concat +27/−0
Prelude/Optional/fold +21/−0
Prelude/Optional/head +36/−0
Prelude/Optional/last +36/−0
Prelude/Optional/map +26/−0
Prelude/Optional/toList +17/−0
Prelude/Optional/unzip +41/−0
Prelude/Text/concat +16/−0
dhall.cabal +74/−3
exec/Main.hs +9/−2
src/Dhall/Core.hs +199/−21
src/Dhall/Import.hs +2/−2
src/Dhall/Parser.hs +140/−123
src/Dhall/Tutorial.hs +59/−48
src/Dhall/TypeCheck.hs +40/−10
tests/Examples.hs +1136/−0
tests/Normalization.hs +156/−0
tests/Tests.hs +15/−0
tests/Util.hs +53/−0

CHANGELOG.md view

@@ -1,3 +1,29 @@+1.3.0++* BREAKING CHANGE TO THE API: Add support for new primitives, specifically:+    * `(//)` - Right-biased and shallow record merge+    * `Optional/build` (now a built-in in order to support build/fold fusion)+    * `Natural/show`+    * `Integer/show`+    * `Double/show`+    * `Natural/toInteger`+    * These all add new constructors to the `Expr` type, which would break+      exhaustive pattern matches+* BREAKING CHANGE TO THE LANGUAGE: Imported paths and URLs no longer support+  the characters: "()[]{}<>:"+    * This reduces the number of cases where you have to add a space after+      imports+    * Note that this does not exclude the `:` in the URL scheme (i.e. `http://`)+* Increase connection timeout for imports+* Variable names now allow the `-` character for all but the first character+* You can now escape identifiers with backticks+    * This lets you name identifiers so that they don't conflict with reserved+      key words+    * This is most useful when converting Dhall to other file formats (like+      JSON) where you might need to emit a field that conflicts with one of+      Dhall's reserved keywords+* New `--version` flag for the `dhall` executable+ 1.2.0  * BREAKING CHANGE: Add support for customizing derived `Interpret` instances

+ Prelude/Bool/and view

@@ -0,0 +1,17 @@+{-+The `and` function returns `False` if there are any `False` elements in the+`List` and returns `True` otherwise++Examples:++```+./and ([True, False, True] : List Bool) = False++./and ([] : List Bool) = True+```+-}+let and : List Bool → Bool+    =   λ(xs : List Bool)+    →   List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True++in  and

+ Prelude/Bool/build view

@@ -0,0 +1,16 @@+{-+`build` is the inverse of `fold`++Examples:++```+./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) = True++./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) = False+```+-}+let build : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool+    =   λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool)+    →   f Bool True False++in  build

+ Prelude/Bool/even view

@@ -0,0 +1,21 @@+{-+Returns `True` if there are an even number of `False` elements in the list and+returns `False` otherwise++Examples:++```+./even ([False, True, False] : List Bool) = True++./even ([False, True] : List Bool) = False++./even ([False] : List Bool) = False++./even ([] : List Bool) = True+```+-}+let even : List Bool → Bool+    =   λ(xs : List Bool)+    →   List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True++in  even

+ Prelude/Bool/fold view

@@ -0,0 +1,19 @@+{-+`fold` is essentially the same as `if`/`then`/else` except as a function++Examples:++```+./fold True Integer 0 1 = 0++./fold False Integer 0 1 = 1+```+-}+let fold : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool+    =   λ(b : Bool)+    →   λ(bool : Type)+    →   λ(true : bool)+    →   λ(false : bool)+    →   if b then true else false++in  fold

+ Prelude/Bool/not view

@@ -0,0 +1,15 @@+{-+Flip the value of a `Bool`++Examples:++```+./not True = False++./not False = True+```+-}+let not : Bool → Bool+    =   λ(b : Bool) → b == False++in  not

+ Prelude/Bool/odd view

@@ -0,0 +1,21 @@+{-+Returns `True` if there are an odd number of `True` elements in the list and+returns `False` otherwise++Examples:++```+./odd ([True, False, True] : List Bool) = False++./odd ([True, False] : List Bool) = True++./odd ([True] : List Bool) = True++./odd ([] : List Bool) = False+```+-}+let odd : List Bool → Bool+    =   λ(xs : List Bool)+    →   List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False++in  odd

+ Prelude/Bool/or view

@@ -0,0 +1,17 @@+{-+The `or` function returns `True` if there are any `True` elements in the `List`+and returns `False` otherwise++Examples:++```+./or ([True, False, True] : List Bool) = True++./or ([] : List Bool) = False+```+-}+let or : List Bool → Bool+    =   λ(xs : List Bool)+    →   List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False++in  or

+ Prelude/Bool/show view

@@ -0,0 +1,16 @@+{-+Render a `Bool` as `Text` using the same representation as Dhall source code+(i.e. beginning with a capital letter)++Examples:++```+./show True  = "True"++./show False = "False"+```+-}+let show : Bool → Text+    =   λ(b : Bool) → if b then "True" else "False"++in  show

+ Prelude/Double/show view

@@ -0,0 +1,16 @@+{-+Render a `Double` as `Text` using the same representation as Dhall source+code (i.e. a decimal floating point number with a leading `-` sign if negative)++Examples:++```+./show -3.1 = "-3.1"++./show  0.4 =  "0.4"+```+-}+let show : Double → Text+    =   Double/show++in  show

+ Prelude/Integer/show view

@@ -0,0 +1,16 @@+{-+Render an `Integer` as `Text` using the same representation as Dhall source+code (i.e. a decimal number with a leading `-` sign if negative)++Examples:++```+./show -3 = "-3"++./show  0 =  "0"+```+-}+let show : Integer → Text+    =   Integer/show++in  show

+ Prelude/List/all view

@@ -0,0 +1,19 @@+{-+Returns `True` if the supplied function returns `True` for all elements in the+`List`++Examples:++```+./all Natural Natural/even ([+2, +3, +5] : List Natural) = False++./all Natural Natural/even ([] : List Natural) = True+```+-}+let all : ∀(a : Type) → (a → Bool) → List a → Bool+    =   λ(a : Type)+    →   λ(f : a → Bool)+    →   λ(xs : List a)+    →   List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True++in  all

+ Prelude/List/any view

@@ -0,0 +1,19 @@+{-+Returns `True` if the supplied function returns `True` for any element in the+`List`++Examples:++```+./any Natural Natural/even ([+2, +3, +5] : List Natural) = True++./any Natural Natural/even ([] : List Natural) = False+```+-}+let any : ∀(a : Type) → (a → Bool) → List a → Bool+    =   λ(a : Type)+    →   λ(f : a → Bool)+    →   λ(xs : List a)+    →   List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False++in  any

+ Prelude/List/build view

@@ -0,0 +1,32 @@+{-+`build` is the inverse of `fold`++Examples:++```+./build+Text+(   λ(list : Type)+→   λ(cons : Text → list → list)+→   λ(nil : list)+→   cons "ABC" (cons "DEF" nil)+)+= ["ABC", "DEF"] : List Text++./build+Text+(   λ(list : Type)+→   λ(cons : Text → list → list)+→   λ(nil : list)+→   nil+)+= [] : List Text+```+-}+let build+    :   ∀(a : Type)+    →   (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)+    →   List a+    =   List/build++in  build

+ Prelude/List/concat view

@@ -0,0 +1,50 @@+{-+Concatenate a `List` of `List`s into a single `List`++Examples:++```+./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++./concat Integer+(   [   [] : List Integer+    ,   [] : List Integer+    ,   [] : List Integer+    ]   : List (List Integer)+)+= [] : List Integer++./concat Integer ([] : List (List Integer)) = [] : List Integer+```+-}+let concat : ∀(a : Type) → List (List a) → List a+    =   λ(a : Type)+    →   λ(xss : List (List a))+    →   List/build+        a+        (   λ(list : Type)+        →   λ(cons : a → list → list)+        →   λ(nil : list)+        →   List/fold+            (List a)+            xss+            list+            (   λ(xs : List a)+            →   λ(ys : list)+            →   List/fold+                a+                xs+                list+                cons+                ys+            )+            nil+        )++in  concat

+ Prelude/List/filter view

@@ -0,0 +1,29 @@+{-+Only keep elements of the list where the supplied function returns `True`++Examples:++```+./filter Natural Natural/even ([+2, +3, +5] : List Natural)+= [+2] : List Natural++./filter Natural Natural/odd ([+2, +3, +5] : List Natural)+= [+3, +5] : List Natural+```+-}+let filter : ∀(a : Type) → (a → Bool) → List a → List a+    =   λ(a : Type)+    →   λ(f : a → Bool)+    →   λ(xs : List a)+    →   List/build+        a+        (   λ(list : Type)+        →   λ(cons : a → list → list)+        →   List/fold+            a+            xs+            list+            (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs)+        )++in  filter

+ Prelude/List/fold view

@@ -0,0 +1,46 @@+{-+`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++Examples:++```+    ./fold+    Natural+    ([+2, +3, +5] : List Natural)+    Natural+    (λ(x : Natural) → λ(y : Natural) → x + y)+    +0+=   +10++    λ(nil : Natural)+→   ./fold+    Natural+    ([+2, +3, +5] : List Natural)+    Natural+    (λ(x : Natural) → λ(y : Natural) → x + y)+    nil+=   λ(nil : Natural) → +2 + +3 + +5 + nil++    λ(list : Type)+→   λ(cons : Natural → list → list)+→   λ(nil : list)+→   ./fold Natural ([+2, +3, +5] : List Natural) list cons nil+=   λ(list : Type)+→   λ(cons : Natural → list → list)+→   λ(nil : list)+→   cons +2 (cons +3 (cons +5 nil))+```+-}+let fold+    :   ∀(a : Type)+    →   List a+    →   ∀(list : Type)+    →   ∀(cons : a → list → list)+    →   ∀(nil : list)+    →   list+    =   List/fold++in  fold

+ Prelude/List/generate view

@@ -0,0 +1,37 @@+{-+Build a list by calling the supplied function on all `Natural` numbers from `+0`+up to but not including the supplied `Natural` number++Examples:++```+./generate +5 Bool Natural/even = [True, False, True, False, True] : List Bool++./generate +0 Bool Natural/even = [] : List Bool+```+-}+let generate : Natural → ∀(a : Type) → (Natural → a) → List a+    =   λ(n : Natural)+    →   λ(a : Type)+    →   λ(f : Natural → a)+    →   List/build+        a+        (   λ(list : Type)+        →   λ(cons : a → list → list)+        →   List/fold+            { index : Natural, value : {} }+            (   List/indexed+                {}+                (   List/build+                    {}+                    (   λ(list : Type)+                    →   λ(cons : {} → list → list)+                    →   Natural/fold n list (cons {=})+                    )+                )+            )+            list+            (λ(x : { index : Natural, value : {} }) → cons (f x.index))+        )++in  generate

+ Prelude/List/head view

@@ -0,0 +1,15 @@+{-+Retrieve the first element of the list++Examples:++```+./head Integer ([0, 1, 2] : List Integer) = [0] : Optional Integer++./head Integer ([] : List Integer) = [] : Optional Integer+```+-}+let head : ∀(a : Type) → List a → Optional a+    =   List/head++in  head

+ Prelude/List/indexed view

@@ -0,0 +1,20 @@+{-+Tag each element of the list with its index++Examples:++```+./indexed Bool ([True, False, True] : List Bool)+=   [   { index = +0, value = True  }+    ,   { index = +1, value = False }+    ,   { index = +2, value = True  }+    ]   : List { index : Natural, value : Bool }++./indexed Bool ([] : List Bool)+= [] : List { index : Natural, value : Bool }+```+-}+let indexed : ∀(a : Type) → List a → List { index : Natural, value : a }+    =   List/indexed++in  indexed

+ Prelude/List/iterate view

@@ -0,0 +1,42 @@+{-+Generate a list of the specified length given a seed value and transition+function++Examples:++```+./iterate +10 Natural (λ(x : Natural) → x * +2) +1+= [+1, +2, +4, +8, +16, +32, +64, +128, +256, +512] : List Natural++./iterate +0 Natural (λ(x : Natural) → x * +2) +1+= [] : List Natural+```+-}+let iterate : Natural → ∀(a : Type) → (a → a) → a → List a+    =   λ(n : Natural)+    →   λ(a : Type)+    →   λ(f : a → a)+    →   λ(x : a)+    →   List/build+        a+        (   λ(list : Type)+        →   λ(cons : a → list → list)+        →   List/fold+            { index : Natural, value : {} }+            (   List/indexed+                {}+                (   List/build+                    {}+                    (   λ(list : Type)+                    →   λ(cons : {} → list → list)+                    →   Natural/fold n list (cons {=})+                    )+                )+            )+            list+            (   λ(y : { index : Natural, value : {} })+            →   cons (Natural/fold y.index a f x)+            )+        )++in  iterate

+ Prelude/List/last view

@@ -0,0 +1,15 @@+{-+Retrieve the last element of the list++Examples:++```+./last Integer ([0, 1, 2] : List Integer) = [2] : Optional Integer++./last Integer ([] : List Integer) = [] : Optional Integer+```+-}+let last : ∀(a : Type) → List a → Optional a+    =   List/last++in  last

+ Prelude/List/length view

@@ -0,0 +1,15 @@+{-+Returns the number of elements in a list++Examples:++```+./length Integer ([0, 1, 2] : List Integer) = +3++./length Integer ([] : List Integer) = +0+```+-}+let length : ∀(a : Type) → List a → Natural+    =   List/length++in  length

+ Prelude/List/map view

@@ -0,0 +1,26 @@+{-+Tranform a list by applying a function to each element++Examples:++```+./map Natural Bool Natural/even ([+2, +3, +5] : List Natural)+= [True, False, False] : List Bool++./map Natural Bool Natural/even ([] : List Natural)+= [] : List Bool+```+-}+let map : ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b+    =   λ(a : Type)+    →   λ(b : Type)+    →   λ(f : a → b)+    →   λ(xs : List a)+    →   List/build+        b+        (   λ(list : Type)+        →   λ(cons : b → list → list)+        →   List/fold a xs list (λ(x : a) → cons (f x))+        )++in  map

+ Prelude/List/null view

@@ -0,0 +1,15 @@+{-+Returns `True` if the `List` is empty and `False` otherwise++Examples:++```+./null Integer ([0, 1, 2] : List Integer) = False++./null Integer ([] : List Integer) = True+```+-}+let null : ∀(a : Type) → List a → Bool+    =   λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs)++in  null

+ Prelude/List/replicate view

@@ -0,0 +1,23 @@+{-+Build a list by copying the given element the specified number of times++Examples:++```+./replicate +9 Integer 1 = [1, 1, 1, 1, 1, 1, 1, 1, 1] : List Integer++./replicate +0 Integer 1 = [] : List Integer+```+-}+let replicate : Natural → ∀(a : Type) → a → List a+    =   λ(n : Natural)+    →   λ(a : Type)+    →   λ(x : a)+    →   List/build+        a+        (   λ(list : Type)+        →   λ(cons : a → list → list)+        →   Natural/fold n list (cons x)+        )++in  replicate

+ Prelude/List/reverse view

@@ -0,0 +1,15 @@+{-+Reverse a list++Examples:++```+./reverse Integer ([0, 1, 2] : List Integer) = [2, 1, 0] : List Integer++./reverse Integer ([] : List Integer) = [] : List Integer+```+-}+let reverse : ∀(a : Type) → List a → List a+    =   List/reverse++in  reverse

+ Prelude/List/shifted view

@@ -0,0 +1,80 @@+{-+Combine a `List` of `List`s, offsetting the `index` of each element by the+number of elements in preceding lists++Examples:++```+./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 = +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 }++./shifted Bool ([] : List (List { index : Natural, value : Bool }))+= [] : List { index : Natural, value : Bool }+```+-}+let shifted+    :   ∀(a : Type)+    →   List (List { index : Natural, value : a})+    →   List { index : Natural, value : a }+    =   λ(a : Type)+    →   λ(kvss : List (List { index : Natural, value : a }))+    →   List/build+        { index : Natural, value : a }+        (   λ(list : Type)+        →   λ(cons : { index : Natural, value : a } → list → list)+        →   λ(nil  : list)+        →   let result =+                List/fold+                (List { index : Natural, value : a })+                kvss+                { count : Natural, diff : Natural → list }+                (   λ(kvs : List { index : Natural, value : a })+                →   λ(y : { count : Natural, diff : Natural → list })+                →   let length = List/length { index : Natural, value : a } kvs+                in  { count = y.count + length+                    , diff  =+                            λ(n : Natural)+                        →   List/fold+                            { index : Natural, value : a }+                            kvs+                            list+                            (   λ(kvOld : { index : Natural, value : a })+                            →   λ(z  : list)+                            →   let kvNew =+                                    { index = kvOld.index + n+                                    , value = kvOld.value+                                    }+                            in  cons kvNew z+                            )+                            (y.diff (n + length))+                    }+                )+                { count = +0, diff = λ(_ : Natural) → nil }+            in  result.diff +0+        )++in  shifted

+ Prelude/List/unzip view

@@ -0,0 +1,55 @@+{-+Unzip a `List` into two separate `List`s++Examples:++```+./unzip+Text+Bool+(   [   { _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+    }++./unzip Text Bool ([] : List { _1 : Text, _2 : Bool })+= { _1 = [] : List Text, _2 = [] : List Bool }+```+-}+let unzip+    :   ∀(a : Type)+    →   ∀(b : Type)+    →   List { _1 : a, _2 : b }+    →   { _1 : List a, _2 : List b }+    =   λ(a : Type)+    →   λ(b : Type)+    →   λ(xs : List { _1 : a, _2 : b })+    →   { _1 =+            List/build+            a+            (   λ(list : Type)+            →   λ(cons : a → list → list)+            →   List/fold+                { _1 : a, _2 : b }+                xs+                list+                (λ(x : { _1 : a, _2 : b }) → cons x._1)+            )+        , _2 =+            List/build+            b+            (   λ(list : Type)+            →   λ(cons : b → list → list)+            →   List/fold+                { _1 : a, _2 : b }+                xs+                list+                (λ(x : { _1 : a, _2 : b }) → cons x._2)+            )+        }++in  unzip

+ Prelude/Monoid view

@@ -0,0 +1,42 @@+{-+Any function `f` that is a `Monoid` must satisfy the following law:++```+t  : Type+f  : ./Monoid t+xs : List (List t)++f (./List/concat t xs) = f (./map (List t) t f xs)+```++Examples:++```+./Bool/and+    : ./Monoid Bool+./Bool/or+    : ./Monoid Bool+./Bool/even+    : ./Monoid Bool+./Bool/odd+    : ./Monoid Bool+./List/concat+    : ∀(a : Type) → ./Monoid (List a)+./List/shifted+    : ∀(a : Type) → ./Monoid (List { index : Natural, value : a })+./Natural/sum+    : ./Monoid Natural+./Natural/product+    : ./Monoid Natural+./Optional/head+    : ∀(a : Type) → ./Monoid (Optional a)+./Optional/last+    : ∀(a : Type) → ./Monoid (Optional a)+./Text/concat+    : ./Monoid Text+```+-}+let Monoid : ∀(m : Type) → Type+    =   λ(m : Type) → List m → m++in  Monoid

+ Prelude/Natural/build view

@@ -0,0 +1,33 @@+{-+`build` is the inverse of `fold`++Examples:++```+./build+(   λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   succ (succ (succ zero))+)+= +3++./build+(   λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   zero+)+= +0+```+-}+let build+    :   (   ∀(natural : Type)+        →   ∀(succ : natural → natural)+        →   ∀(zero : natural)+        →   natural+        )+    →   Natural+    =   Natural/build++in  build

+ Prelude/Natural/enumerate view

@@ -0,0 +1,38 @@+{-+Generate a list of numbers from `+0` up to but not including the specified+number++Examples:++```+./enumerate +10 = [+0, +1, +2, +3, +4, +5, +6, +7, +8, +9] : List Natural++./enumerate +0 = [] : List Natural+```+-}+let enumerate : Natural → List Natural+    =   λ(n : Natural)+    →   List/build+        Natural+        (   λ(list : Type)+        →   λ(cons : Natural → list → list)+        →   List/fold+            { index : Natural, value : {} }+            (   List/indexed+                {}+                (   List/build+                    {}+                    (   λ(list : Type)+                    →   λ(cons : {} → list → list)+                    →   Natural/fold+                        n+                        list+                        (cons {=})+                    )+                )+            )+            list+            (λ(x : { index : Natural, value : {} }) → cons x.index)+        )++in  enumerate

+ Prelude/Natural/even view

@@ -0,0 +1,15 @@+{-+Returns `True` if a number if even and returns `False` otherwise++Examples:++```+./even +3 = False++./even +0 = True+```+-}+let even : Natural → Bool+    =   Natural/even++in  even

+ Prelude/Natural/fold view

@@ -0,0 +1,33 @@+{-+`fold` is the primitive function for consuming `Natural` numbers++If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just+replaces each `succ` and `zero` with something else++Examples:++```+./fold +3 Natural (λ(x : Natural) → +5 * x) +1 = +125++λ(zero : Natural) → ./fold +3 Natural (λ(x : Natural) → +5 * x) zero+= λ(zero : Natural) → +5 * +5 * +5 * zero++    λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   ./fold +3 natural succ zero+=   λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   succ (succ (succ zero))+```+-}+let fold+    :   Natural+    →   ∀(natural : Type)+    →   ∀(succ : natural → natural)+    →   ∀(zero : natural)+    →   natural+    =   Natural/fold++in  fold

+ Prelude/Natural/isZero view

@@ -0,0 +1,15 @@+{-+Returns `True` if a number is `+0` and returns `False` otherwise++Examples:++```+./isZero +2 = False++./isZero +0 = True+```+-}+let isZero : Natural → Bool+    =   Natural/isZero++in  isZero

+ Prelude/Natural/odd view

@@ -0,0 +1,15 @@+{-+Returns `True` if a number is odd and returns `False` otherwise++Examples:++```+./odd +3 = True++./odd +0 = False+```+-}+let odd : Natural → Bool+    =   Natural/odd++in  odd

+ Prelude/Natural/product view

@@ -0,0 +1,16 @@+{-+Multiply all the numbers in a `List`++Examples:++```+./product ([+2, +3, +5] : List Natural) = +30++./product ([] : List Natural) = +1+```+-}+let product : List Natural → Natural+    =   λ(xs : List Natural)+    →   List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) +1++in  product

+ Prelude/Natural/show view

@@ -0,0 +1,16 @@+{-+Render a `Natural` number as `Text` using the same representation as Dhall+source code (i.e. a decimal number with a leading `+` sign)++Examples:++```+./show +3 = "+3"++./show +0 = "+0"+```+-}+let show : Natural → Text+    =   Natural/show++in  show

+ Prelude/Natural/sum view

@@ -0,0 +1,16 @@+{-+Add all the numbers in a `List`++Examples:++```+./sum ([+2, +3, +5] : List Natural) = +10++./sum ([] : List Natural) = +0+```+-}+let sum : List Natural → Natural+    =   λ(xs : List Natural)+    →   List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) +0++in  sum

+ Prelude/Natural/toInteger view

@@ -0,0 +1,15 @@+{-+Convert a `Natural` number to the corresponding `Integer`++Examples:++```+./toInteger +3 = 3++./toInteger +0 = 0+```+-}+let toInteger : Natural → Integer+    =   Natural/toInteger++in  toInteger

+ Prelude/Optional/build view

@@ -0,0 +1,36 @@+{-+`build` is the inverse of `fold`++Examples:++```+./build+Integer+(   λ(optional : Type)+→   λ(just : Integer → optional)+→   λ(nothing : optional)+→   just 1+)+= [1] : Optional Integer++./build+Integer+(   λ(optional : Type)+→   λ(just : Integer → optional)+→   λ(nothing : optional)+→   nothing+)+= [] : Optional Integer+```+-}+let build+    :   ∀(a : Type)+    →   (   ∀(optional : Type)+        →   ∀(just : a → optional)+        →   ∀(nothing : optional)+        →   optional+        )+    →   Optional a+    =   Optional/build++in  build

+ Prelude/Optional/concat view

@@ -0,0 +1,27 @@+{-+Flatten two `Optional` layers into a single `Optional` layer++Examples:++```+./concat Integer ([[1] : Optional Integer] : Optional (Optional Integer))+= [1] : Optional Integer++./concat Integer ([[] : Optional Integer] : Optional (Optional Integer))+= [] : Optional Integer++./concat Integer ([] : Optional (Optional Integer))+= [] : Optional Integer+```+-}+let concat : ∀(a : Type) → Optional (Optional a) → Optional a+    =   λ(a : Type)+    →   λ(x : Optional (Optional a))+    →   Optional/fold+        (Optional a)+        x+        (Optional a)+        (λ(y : Optional a) → y)+        ([] : Optional a)++in  concat

+ Prelude/Optional/fold view

@@ -0,0 +1,21 @@+{-+`fold` is the primitive function for consuming `Optional` values++Examples:++```+./fold Integer ([2] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2++./fold Integer ([]  : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0+```+-}+let fold+    :   ∀(a : Type)+    →   Optional a+    →   ∀(optional : Type)+    →   ∀(just : a → optional)+    →   ∀(nothing : optional)+    →   optional+    =   Optional/fold++in  fold

+ Prelude/Optional/head view

@@ -0,0 +1,36 @@+{-+Returns the first non-empty `Optional` value in a `List`++Examples:++```+./head+Integer+(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]+    : List (Optional Integer)+)+= [1] : Optional Integer++./head+Integer+([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))+= [] : Optional Integer++./head Integer ([] : List (Optional Integer))+= [] : Optional Integer+```+-}+let head : ∀(a : Type) → List (Optional a) → Optional a+    =   λ(a : Type)+    →   λ(xs : List (Optional a))+    →   List/fold+        (Optional a)+        xs+        (Optional a)+        (   λ(l : Optional a)+        →   λ(r : Optional a)+        →   Optional/fold a l (Optional a) (λ(x : a) → [x] : Optional a) r+        )+        ([] : Optional a)++in  head

+ Prelude/Optional/last view

@@ -0,0 +1,36 @@+{-+Returns the last non-empty `Optional` value in a `List`++Examples:++```+./last+Integer+(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]+    : List (Optional Integer)+)+= [2] : Optional Integer++./last+Integer+([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))+= [] : Optional Integer++./last Integer ([] : List (Optional Integer))+= [] : Optional Integer+```+-}+let last : ∀(a : Type) → List (Optional a) → Optional a+    =   λ(a : Type)+    →   λ(xs : List (Optional a))+    →   List/fold+        (Optional a)+        xs+        (Optional a)+        (   λ(l : Optional a)+        →   λ(r : Optional a)+        →   Optional/fold a r (Optional a) (λ(x : a) → [x] : Optional a) l+        )+        ([] : Optional a)++in  last

+ Prelude/Optional/map view

@@ -0,0 +1,26 @@+{-+Transform an `Optional` value with a function++Examples:++```+./map Natural Bool Natural/even ([+3] : Optional Natural)+= [False] : Optional Bool++./map Natural Bool Natural/even ([] : Optional Natural)+= [] : Optional Bool+```+-}+let map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b+    =   λ(a : Type)+    →   λ(b : Type)+    →   λ(f : a → b)+    →   λ(o : Optional a)+    →   Optional/fold+        a+        o+        (Optional b)+        (λ(x : a) → [f x] : Optional b)+        ([] : Optional b)++in  map

+ Prelude/Optional/toList view

@@ -0,0 +1,17 @@+{-+Convert an `Optional` value into the equivalent `List`++Examples:++```+./toList Integer ([1] : Optional Integer) = [1] : List Integer++./toList Integer ([] : Optional Integer) = [] : List Integer+```+-}+let toList : ∀(a : Type) → Optional a → List a+    =   λ(a : Type)+    →   λ(o : Optional a)+    →   Optional/fold a o (List a) (λ(x : a) → [x] : List a) ([] : List a)++in  toList

+ Prelude/Optional/unzip view

@@ -0,0 +1,41 @@+{-+Unzip an `Optional` value into two separate `Optional` values++Examples:++```+./unzip+Text+Bool+([{ _1 = "ABC", _2 = True  }] : Optional { _1 : Text, _2 : Bool })+= { _1 = ["ABC"] : Optional Text, _2 = [True] : Optional Bool }++./unzip Text Bool ([] : Optional { _1 : Text, _2 : Bool })+= { _1 = [] : Optional Text, _2 = [] : Optional Bool }+```+-}+let unzip+    :   ∀(a : Type)+    →   ∀(b : Type)+    →   Optional { _1 : a, _2 : b }+    →   { _1 : Optional a, _2 : Optional b }+    =   λ(a : Type)+    →   λ(b : Type)+    →   λ(xs : Optional { _1 : a, _2 : b })+    →   { _1 =+            Optional/fold+            { _1 : a, _2 : b }+            xs+            (Optional a)+            (λ(x : { _1 : a, _2 : b }) → [x._1] : Optional a)+            ([] : Optional a)+        , _2 =+            Optional/fold+            { _1 : a, _2 : b }+            xs+            (Optional b)+            (λ(x : { _1 : a, _2 : b }) → [x._2] : Optional b)+            ([] : Optional b)+        }++in  unzip

+ Prelude/Text/concat view

@@ -0,0 +1,16 @@+{-+Concatenate all the `Text` values in a `List`++Examples:++```+./concat (["ABC", "DEF", "GHI"] : List Text) = "ABCDEFGHI"++./concat ([] : List Text) = ""+```+-}+let concat : List Text → Text+    =   λ(xs : List Text)+    →   List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) ""++in  concat

dhall.cabal view

@@ -1,5 +1,5 @@ Name: dhall-Version: 1.2.0+Version: 1.3.0 Cabal-Version: >=1.8.0.2 Build-Type: Simple Tested-With: GHC == 7.10.2, GHC == 8.0.1@@ -22,7 +22,57 @@     .     Read "Dhall.Tutorial" to learn how to use this library Category: Compiler-Extra-Source-Files: CHANGELOG.md+Extra-Source-Files:+    CHANGELOG.md+    Prelude/Bool/and+    Prelude/Bool/build+    Prelude/Bool/even+    Prelude/Bool/fold+    Prelude/Bool/not+    Prelude/Bool/odd+    Prelude/Bool/or+    Prelude/Bool/show+    Prelude/Double/show+    Prelude/Integer/show+    Prelude/List/all+    Prelude/List/any+    Prelude/List/build+    Prelude/List/concat+    Prelude/List/filter+    Prelude/List/fold+    Prelude/List/generate+    Prelude/List/head+    Prelude/List/indexed+    Prelude/List/iterate+    Prelude/List/last+    Prelude/List/length+    Prelude/List/map+    Prelude/List/null+    Prelude/List/replicate+    Prelude/List/reverse+    Prelude/List/shifted+    Prelude/List/unzip+    Prelude/Monoid+    Prelude/Natural/build+    Prelude/Natural/enumerate+    Prelude/Natural/even+    Prelude/Natural/fold+    Prelude/Natural/isZero+    Prelude/Natural/odd+    Prelude/Natural/product+    Prelude/Natural/show+    Prelude/Natural/sum+    Prelude/Natural/toInteger+    Prelude/Optional/build+    Prelude/Optional/concat+    Prelude/Optional/fold+    Prelude/Optional/head+    Prelude/Optional/last+    Prelude/Optional/map+    Prelude/Optional/toList+    Prelude/Optional/unzip+    Prelude/Text/concat+ Source-Repository head     Type: git     Location: https://github.com/Gabriel439/Haskell-Dhall-Library@@ -33,6 +83,7 @@         base                 >= 4.8.0.0  && < 5   ,         ansi-wl-pprint                      < 0.7 ,         bytestring                          < 0.11,+        charset                             < 0.4 ,         containers           >= 0.5.0.0  && < 0.6 ,         http-client          >= 0.4.30   && < 0.6 ,         http-client-tls      >= 0.2.0    && < 0.4 ,@@ -46,7 +97,7 @@         transformers         >= 0.2.0.0  && < 0.6 ,         trifecta             >= 1.6      && < 1.7 ,         unordered-containers >= 0.1.3.0  && < 0.3 ,-        vector               >= 0.11.0.0 && < 0.12+        vector               >= 0.11.0.0 && < 0.13     Exposed-Modules:         Dhall,         Dhall.Context,@@ -67,3 +118,23 @@         trifecta         >= 1.6      && < 1.7,         text             >= 0.11.1.0 && < 1.3     GHC-Options: -Wall+    Other-Modules:+        Paths_dhall++Test-Suite test+    Type: exitcode-stdio-1.0+    Hs-Source-Dirs: tests+    Main-Is: Tests.hs+    GHC-Options: -Wall+    Other-Modules:+        Examples+        Normalization+        Util+    Build-Depends:+        base               >= 4        && < 5   ,+        dhall                                   ,+        neat-interpolation >= 0.3.2.1  && < 0.4 ,+        tasty              >= 0.11.2   && < 0.12,+        tasty-hunit        >= 0.9.2    && < 0.10,+        text               >= 0.11.1.0 && < 1.3 ,+        vector             >= 0.11.0.0 && < 0.12

exec/Main.hs view

@@ -7,16 +7,20 @@ module Main where  import Control.Exception (SomeException)+import Control.Monad (when) import Data.Monoid (mempty)+import Data.Version (showVersion) import Dhall.Core (pretty, normalize) import Dhall.Import (Imported(..), load) import Dhall.Parser (Src, exprFromText) import Dhall.TypeCheck (DetailedTypeError(..), TypeError) import Options.Generic (Generic, ParseRecord, type (<?>)(..)) import System.IO (stderr)-import System.Exit (exitFailure)+import System.Exit (exitFailure, exitSuccess) import Text.Trifecta.Delta (Delta(..)) +import qualified Paths_dhall as Meta+ import qualified Control.Exception import qualified Data.Text.Lazy.IO import qualified Dhall.TypeCheck@@ -27,6 +31,7 @@  data Options = Options     { explain :: Bool <?> "Explain error messages in more detail"+    , version :: Bool <?> "Display version and exit"     } deriving (Generic)  instance ParseRecord Options@@ -34,7 +39,9 @@ main :: IO () main = do     options <- Options.Generic.getRecord "Compiler for the Dhall language"-+    when (unHelpful (version options)) $ do+      putStrLn (showVersion Meta.version)+      exitSuccess     let handle =                 Control.Exception.handle handler2             .   Control.Exception.handle handler1

src/Dhall/Core.hs view

@@ -36,14 +36,17 @@      -- * Miscellaneous     , internalError+    , reservedIdentifiers     ) where  #if MIN_VERSION_base(4,8,0) #else import Control.Applicative (Applicative(..), (<$>)) #endif+import Control.Applicative (empty) import Data.Bifunctor (Bifunctor(..)) import Data.Foldable+import Data.HashSet (HashSet) import Data.Map (Map) import Data.Monoid ((<>)) import Data.String (IsString(..))@@ -57,6 +60,7 @@ import Prelude hiding (FilePath, succ)  import qualified Control.Monad+import qualified Data.HashSet import qualified Data.Map import qualified Data.Maybe import qualified Data.Text@@ -84,7 +88,7 @@     Note that Dhall does not support functions from terms to types and therefore     Dhall is not a dependently typed language -}-data Const = Type | Kind deriving (Show, Bounded, Enum)+data Const = Type | Kind deriving (Show, Eq, Bounded, Enum)  instance Buildable Const where     build = buildConst@@ -182,7 +186,7 @@     = Const Const     -- | > Var (V x 0)                              ~  x     --   > Var (V x n)                              ~  x@n-    | Var Var             +    | Var Var     -- | > Lam x     A b                            ~  λ(x : A) -> b     | Lam Text (Expr s a) (Expr s a)     -- | > Pi "_" A B                               ~        A  -> B@@ -223,6 +227,10 @@     | NaturalEven     -- | > NaturalOdd                               ~  Natural/odd     | NaturalOdd+    -- | > NaturalToInteger                         ~  Natural/toInteger+    | NaturalToInteger+    -- | > NaturalShow                              ~  Natural/show+    | NaturalShow     -- | > NaturalPlus x y                          ~  x + y     | NaturalPlus (Expr s a) (Expr s a)     -- | > NaturalTimes x y                         ~  x * y@@ -231,10 +239,14 @@     | Integer     -- | > IntegerLit n                             ~  n     | IntegerLit Integer+    -- | > IntegerShow                              ~  Integer/show+    | IntegerShow     -- | > Double                                   ~  Double     | Double     -- | > DoubleLit n                              ~  n     | DoubleLit Double+    -- | > DoubleShow                               ~  Double/show+    | DoubleShow     -- | > Text                                     ~  Text     | Text     -- | > TextLit t                                ~  t@@ -253,7 +265,7 @@     -- | > ListLength                               ~  List/length     | ListLength     -- | > ListHead                                 ~  List/head-    | ListHead +    | ListHead     -- | > ListLast                                 ~  List/last     | ListLast     -- | > ListIndexed                              ~  List/indexed@@ -267,16 +279,20 @@     | OptionalLit (Expr s a) (Vector (Expr s a))     -- | > OptionalFold                             ~  Optional/fold     | OptionalFold+    -- | > OptionalBuild                            ~  Optional/build+    | OptionalBuild     -- | > Record            [(k1, t1), (k2, t2)]   ~  { k1 : t1, k2 : t1 }     | Record    (Map Text (Expr s a))     -- | > RecordLit         [(k1, v1), (k2, v2)]   ~  { k1 = v1, k2 = v2 }     | RecordLit (Map Text (Expr s a))     -- | > Union             [(k1, t1), (k2, t2)]   ~  < k1 : t1 | k2 : t2 >     | Union     (Map Text (Expr s a))-    -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1 | k2 : t2 | k3 : t3 > +    -- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)]   ~  < k1 = t1 | k2 : t2 | k3 : t3 >     | UnionLit Text (Expr s a) (Map Text (Expr s a))     -- | > Combine x y                              ~  x ∧ y     | Combine (Expr s a) (Expr s a)+    -- | > CombineRight x y                         ~  x ⫽ y+    | Prefer (Expr s a) (Expr s a)     -- | > Merge x y t                              ~  merge x y : t     | Merge (Expr s a) (Expr s a) (Expr s a)     -- | > Field e x                                ~  e.x@@ -285,7 +301,7 @@     | Note s (Expr s a)     -- | > Embed path                               ~  path     | Embed a-    deriving (Functor, Foldable, Traversable, Show)+    deriving (Functor, Foldable, Traversable, Show, Eq)  instance Applicative (Expr s) where     pure = Embed@@ -316,12 +332,16 @@     NaturalIsZero    >>= _ = NaturalIsZero     NaturalEven      >>= _ = NaturalEven     NaturalOdd       >>= _ = NaturalOdd+    NaturalToInteger >>= _ = NaturalToInteger+    NaturalShow      >>= _ = NaturalShow     NaturalPlus  a b >>= k = NaturalPlus  (a >>= k) (b >>= k)     NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)     Integer          >>= _ = Integer     IntegerLit a     >>= _ = IntegerLit a+    IntegerShow      >>= _ = IntegerShow     Double           >>= _ = Double     DoubleLit a      >>= _ = DoubleLit a+    DoubleShow       >>= _ = DoubleShow     Text             >>= _ = Text     TextLit a        >>= _ = TextLit a     TextAppend a b   >>= k = TextAppend (a >>= k) (b >>= k)@@ -337,11 +357,13 @@     Optional         >>= _ = Optional     OptionalLit a b  >>= k = OptionalLit (a >>= k) (fmap (>>= k) b)     OptionalFold     >>= _ = OptionalFold+    OptionalBuild    >>= _ = OptionalBuild     Record    a      >>= k = Record (fmap (>>= k) a)     RecordLit a      >>= k = RecordLit (fmap (>>= k) a)     Union     a      >>= k = Union (fmap (>>= k) a)     UnionLit a b c   >>= k = UnionLit a (b >>= k) (fmap (>>= k) c)     Combine a b      >>= k = Combine (a >>= k) (b >>= k)+    Prefer a b       >>= k = Prefer (a >>= k) (b >>= k)     Merge a b c      >>= k = Merge (a >>= k) (b >>= k) (c >>= k)     Field a b        >>= k = Field (a >>= k) b     Note a b         >>= k = Note a (b >>= k)@@ -369,12 +391,16 @@     first _  NaturalIsZero     = NaturalIsZero     first _  NaturalEven       = NaturalEven     first _  NaturalOdd        = NaturalOdd+    first _  NaturalToInteger  = NaturalToInteger+    first _  NaturalShow       = NaturalShow     first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)     first k (NaturalTimes a b) = NaturalTimes (first k a) (first k b)     first _  Integer           = Integer     first _ (IntegerLit a    ) = IntegerLit a+    first _  IntegerShow       = IntegerShow     first _  Double            = Double     first _ (DoubleLit a     ) = DoubleLit a+    first _  DoubleShow        = DoubleShow     first _  Text              = Text     first _ (TextLit a       ) = TextLit a     first k (TextAppend a b  ) = TextAppend (first k a) (first k b)@@ -390,11 +416,13 @@     first _  Optional          = Optional     first k (OptionalLit a b ) = OptionalLit (first k a) (fmap (first k) b)     first _  OptionalFold      = OptionalFold+    first _  OptionalBuild     = OptionalBuild     first k (Record a        ) = Record (fmap (first k) a)     first k (RecordLit a     ) = RecordLit (fmap (first k) a)     first k (Union a         ) = Union (fmap (first k) a)     first k (UnionLit a b c  ) = UnionLit a (first k b) (fmap (first k) c)     first k (Combine a b     ) = Combine (first k a) (first k b)+    first k (Prefer a b      ) = Prefer (first k a) (first k b)     first k (Merge a b c     ) = Merge (first k a) (first k b) (first k c)     first k (Field a b       ) = Field (first k a) b     first k (Note a b        ) = Note (k a) (first k b)@@ -422,7 +450,10 @@  -- | Builder corresponding to the @label@ token in "Dhall.Parser" buildLabel :: Text -> Builder-buildLabel = build+buildLabel label =+    if Data.HashSet.member label reservedIdentifiersText+    then "`" <> build label <> "`"+    else build label  -- | Builder corresponding to the @number@ token in "Dhall.Parser" buildNumber :: Integer -> Builder@@ -536,28 +567,34 @@  -- | Builder corresponding to the @exprC4@ parser in "Dhall.Parser" buildExprC4 :: Buildable a => Expr s a -> Builder-buildExprC4 (Combine a b) = buildExprC5 a <> " ∧ " <> buildExprC4 b-buildExprC4 (Note    _ b) = buildExprC4 b-buildExprC4  a            = buildExprC5 a+buildExprC4 (Combine   a b) = buildExprC5 a <> " ∧ " <> buildExprC4 b+buildExprC4 (Note      _ b) = buildExprC4 b+buildExprC4  a              = buildExprC5 a  -- | Builder corresponding to the @exprC5@ parser in "Dhall.Parser" buildExprC5 :: Buildable a => Expr s a -> Builder-buildExprC5 (NaturalTimes a b) = buildExprC6 a <> " * " <> buildExprC5 b-buildExprC5 (Note         _ b) = buildExprC5 b-buildExprC5  a                 = buildExprC6 a+buildExprC5 (Prefer a b) = buildExprC6 a <> " ⫽ " <> buildExprC5 b+buildExprC5 (Note   _ b) = buildExprC5 b+buildExprC5  a           = buildExprC6 a  -- | Builder corresponding to the @exprC6@ parser in "Dhall.Parser" buildExprC6 :: Buildable a => Expr s a -> Builder-buildExprC6 (BoolEQ a b) = buildExprC7 a <> " == " <> buildExprC6 b-buildExprC6 (Note   _ b) = buildExprC6 b-buildExprC6  a           = buildExprC7 a+buildExprC6 (NaturalTimes a b) = buildExprC7 a <> " * " <> buildExprC6 b+buildExprC6 (Note         _ b) = buildExprC6 b+buildExprC6  a                 = buildExprC7 a  -- | Builder corresponding to the @exprC7@ parser in "Dhall.Parser" buildExprC7 :: Buildable a => Expr s a -> Builder-buildExprC7 (BoolNE a b) = buildExprD  a <> " != " <> buildExprC7 b+buildExprC7 (BoolEQ a b) = buildExprC8 a <> " == " <> buildExprC7 b buildExprC7 (Note   _ b) = buildExprC7 b-buildExprC7  a           = buildExprD  a+buildExprC7  a           = buildExprC8 a +-- | Builder corresponding to the @exprC8@ parser in "Dhall.Parser"+buildExprC8 :: Buildable a => Expr s a -> Builder+buildExprC8 (BoolNE a b) = buildExprD  a <> " != " <> buildExprC8 b+buildExprC8 (Note   _ b) = buildExprC8 b+buildExprC8  a           = buildExprD  a+ -- | Builder corresponding to the @exprD@ parser in "Dhall.Parser" buildExprD :: Buildable a => Expr s a -> Builder buildExprD (App  a b) = buildExprD a <> " " <> buildExprE b@@ -590,10 +627,18 @@     "Natural/even" buildExprF NaturalOdd =     "Natural/odd"+buildExprF NaturalToInteger =+    "Natural/toInteger"+buildExprF NaturalShow =+    "Natural/show" buildExprF Integer =     "Integer"+buildExprF IntegerShow =+    "Integer/show" buildExprF Double =     "Double"+buildExprF DoubleShow =+    "Double/show" buildExprF Text =     "Text" buildExprF List =@@ -616,6 +661,8 @@     "Optional" buildExprF OptionalFold =     "Optional/fold"+buildExprF OptionalBuild =+    "Optional/build" buildExprF (BoolLit True) =     "True" buildExprF (BoolLit False) =@@ -861,6 +908,8 @@ shift _ _ NaturalIsZero = NaturalIsZero shift _ _ NaturalEven = NaturalEven shift _ _ NaturalOdd = NaturalOdd+shift _ _ NaturalToInteger = NaturalToInteger+shift _ _ NaturalShow = NaturalShow shift d v (NaturalPlus a b) = NaturalPlus a' b'   where     a' = shift d v a@@ -871,8 +920,10 @@     b' = shift d v b shift _ _ Integer = Integer shift _ _ (IntegerLit a) = IntegerLit a+shift _ _ IntegerShow = IntegerShow shift _ _ Double = Double shift _ _ (DoubleLit a) = DoubleLit a+shift _ _ DoubleShow = DoubleShow shift _ _ Text = Text shift _ _ (TextLit a) = TextLit a shift d v (TextAppend a b) = TextAppend a' b'@@ -897,6 +948,7 @@     a' =       shift d v  a     b' = fmap (shift d v) b shift _ _ OptionalFold = OptionalFold+shift _ _ OptionalBuild = OptionalBuild shift d v (Record a) = Record a'   where     a' = fmap (shift d v) a@@ -914,6 +966,10 @@   where     a' = shift d v a     b' = shift d v b+shift d v (Prefer a b) = Prefer a' b'+  where+    a' = shift d v a+    b' = shift d v b shift d v (Merge a b c) = Merge a' b' c'   where     a' = shift d v a@@ -992,6 +1048,8 @@ subst _ _ NaturalIsZero = NaturalIsZero subst _ _ NaturalEven = NaturalEven subst _ _ NaturalOdd = NaturalOdd+subst _ _ NaturalToInteger = NaturalToInteger+subst _ _ NaturalShow = NaturalShow subst x e (NaturalPlus a b) = NaturalPlus a' b'   where     a' = subst x e a@@ -1002,8 +1060,10 @@     b' = subst x e b subst _ _ Integer = Integer subst _ _ (IntegerLit a) = IntegerLit a+subst _ _ IntegerShow = IntegerShow subst _ _ Double = Double subst _ _ (DoubleLit a) = DoubleLit a+subst _ _ DoubleShow = DoubleShow subst _ _ Text = Text subst _ _ (TextLit a) = TextLit a subst x e (TextAppend a b) = TextAppend a' b'@@ -1028,6 +1088,7 @@     a' =       subst x e  a     b' = fmap (subst x e) b subst _ _ OptionalFold = OptionalFold+subst _ _ OptionalBuild = OptionalBuild subst x e (Record       kts) = Record                   (fmap (subst x e) kts) subst x e (RecordLit    kvs) = RecordLit                (fmap (subst x e) kvs) subst x e (Union        kts) = Union                    (fmap (subst x e) kts)@@ -1036,6 +1097,10 @@   where     a' = subst x e a     b' = subst x e b+subst x e (Prefer a b) = Prefer a' b'+  where+    a' = subst x e a+    b' = subst x e b subst x e (Merge a b c) = Merge a' b' c'   where     a' = subst x e a@@ -1082,11 +1147,14 @@             -- fold/build fusion for `List`             App (App ListBuild _) (App (App ListFold _) e') -> normalize e'             App (App ListFold _) (App (App ListBuild _) e') -> normalize e'-             -- fold/build fusion for `Natural`             App NaturalBuild (App NaturalFold e') -> normalize e'             App NaturalFold (App NaturalBuild e') -> normalize e' +            -- fold/build fusion for `Optional`+            App (App OptionalBuild _) (App (App OptionalFold _) e') -> normalize e'+            App (App OptionalFold _) (App (App OptionalBuild _) e') -> normalize e'+             App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->                 normalize (go n0)               where@@ -1112,6 +1180,26 @@             App NaturalIsZero (NaturalLit n) -> BoolLit (n == 0)             App NaturalEven (NaturalLit n) -> BoolLit (even n)             App NaturalOdd (NaturalLit n) -> BoolLit (odd n)+            App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n)+            App NaturalShow (NaturalLit n) -> TextLit ("+" <> buildNatural n)+            App IntegerShow (IntegerLit n) -> TextLit (buildNumber n)+            App DoubleShow (DoubleLit n) -> TextLit (buildDouble n)+            App (App OptionalBuild t) k+                | check     -> OptionalLit t k'+                | otherwise -> App f' a'+              where+                labeled = normalize (App (App (App k (App Optional t)) "Just") "Nothing")++                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'@@ -1228,6 +1316,8 @@     NaturalIsZero -> NaturalIsZero     NaturalEven -> NaturalEven     NaturalOdd -> NaturalOdd+    NaturalToInteger -> NaturalToInteger+    NaturalShow -> NaturalShow     NaturalPlus  x y ->         case x' of             NaturalLit xn ->@@ -1250,8 +1340,10 @@         y' = normalize y     Integer -> Integer     IntegerLit n -> IntegerLit n+    IntegerShow -> IntegerShow     Double -> Double     DoubleLit n -> DoubleLit n+    DoubleShow -> DoubleShow     Text -> Text     TextLit t -> TextLit t     TextAppend x y   ->@@ -1282,6 +1374,7 @@         t'  =      normalize t         es' = fmap normalize es     OptionalFold -> OptionalFold+    OptionalBuild -> OptionalBuild     Record kts -> Record kts'       where         kts' = fmap normalize kts@@ -1304,6 +1397,17 @@                     _ -> Combine x y                 _ -> Combine x y         in  combine (normalize x0) (normalize y0)+    Prefer x y ->+        case x' of+            RecordLit kvsX ->+                case y' of+                    RecordLit kvsY ->+                        RecordLit (fmap normalize (Data.Map.union kvsY kvsX))+                    _ -> Prefer x' y'+            _ -> Prefer x' y'+      where+        x' = normalize x+        y' = normalize y     Merge x y t      ->         case x' of             RecordLit kvsX ->@@ -1347,6 +1451,7 @@     App f a -> isNormalized f && isNormalized a && case App f a of         App (Lam _ _ _) _ -> False +        -- fold/build fusion for `List`         App (App ListBuild _) (App (App ListFold _) _) -> False         App (App ListFold _) (App (App ListBuild _) _) -> False @@ -1354,6 +1459,10 @@         App NaturalBuild (App NaturalFold _) -> False         App NaturalFold (App NaturalBuild _) -> False +        -- fold/build 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@@ -1367,6 +1476,19 @@         App NaturalIsZero (NaturalLit _) -> False         App NaturalEven (NaturalLit _) -> False         App NaturalOdd (NaturalLit _) -> False+        App NaturalShow (NaturalLit _) -> False+        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@@ -1428,6 +1550,8 @@     NaturalIsZero -> True     NaturalEven -> True     NaturalOdd -> True+    NaturalShow -> True+    NaturalToInteger -> True     NaturalPlus x y -> isNormalized x && isNormalized y &&         case x of             NaturalLit _ ->@@ -1444,8 +1568,10 @@             _ -> True     Integer -> True     IntegerLit _ -> True+    IntegerShow -> True     Double -> True     DoubleLit _ -> True+    DoubleShow -> True     Text -> True     TextLit _ -> True     TextAppend x y -> isNormalized x && isNormalized y &&@@ -1467,17 +1593,25 @@     Optional -> True     OptionalLit t es -> isNormalized t && all isNormalized es     OptionalFold -> True+    OptionalBuild -> True     Record kts -> all isNormalized kts     RecordLit kvs -> all isNormalized kvs     Union kts -> all isNormalized kts     UnionLit _ v kvs -> isNormalized v && all isNormalized kvs-    Combine x0 y0 -> isNormalized x0 && isNormalized y0 && combine x0 y0+    Combine x y -> isNormalized x && isNormalized y && combine       where-        combine x y = case x of+        combine = case x of             RecordLit _ -> case y of                 RecordLit _ -> False                 _ -> True             _ -> True+    Prefer x y -> isNormalized x && isNormalized y && combine+      where+        combine = case x of+            RecordLit _ -> case y of+                RecordLit _ -> False+                _ -> True+            _ -> True     Merge x y t -> isNormalized x && isNormalized y && isNormalized t &&         case x of             RecordLit kvsX ->@@ -1488,7 +1622,7 @@                             Nothing -> True                     _ -> True             _ -> True-    Field r x -> isNormalized r && +    Field r x -> isNormalized r &&         case r of             RecordLit kvs ->                 case Data.Map.lookup x kvs of@@ -1539,3 +1673,47 @@             return (0, 1, mv)     (len, _, mv) <- f cons nil     return (Data.Vector.Mutable.slice 0 len mv) ))++reservedIdentifiers :: HashSet String+reservedIdentifiers =+    Data.HashSet.fromList+        [ "let"+        , "in"+        , "Type"+        , "Kind"+        , "forall"+        , "Bool"+        , "True"+        , "False"+        , "merge"+        , "if"+        , "then"+        , "else"+        , "as"+        , "Natural"+        , "Natural/fold"+        , "Natural/build"+        , "Natural/isZero"+        , "Natural/even"+        , "Natural/odd"+        , "Natural/toInteger"+        , "Natural/show"+        , "Integer"+        , "Integer/show"+        , "Double"+        , "Double/show"+        , "Text"+        , "List"+        , "List/build"+        , "List/fold"+        , "List/length"+        , "List/head"+        , "List/last"+        , "List/indexed"+        , "List/reverse"+        , "Optional"+        , "Optional/fold"+        ]++reservedIdentifiersText :: HashSet Text+reservedIdentifiersText = Data.HashSet.map Text.pack reservedIdentifiers

src/Dhall/Import.hs view

@@ -325,9 +325,9 @@         Nothing -> do             let settings = HTTP.tlsManagerSettings #if MIN_VERSION_http_client(0,5,0)-                    { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro 1000000 }  -- 1 second+                    { HTTP.managerResponseTimeout = HTTP.responseTimeoutMicro (30 * 1000 * 1000) }  -- 30 seconds #else-                    { HTTP.managerResponseTimeout = Just 1000000 }  -- 1 second+                    { HTTP.managerResponseTimeout = Just (30 * 1000 * 1000) }  -- 30 seconds #endif             m <- liftIO (HTTP.newManager settings)             zoom manager (State.put (Just m))

src/Dhall/Parser.hs view

@@ -22,6 +22,7 @@ import Control.Exception (Exception) import Control.Monad (MonadPlus) import Data.ByteString (ByteString)+import Data.CharSet (CharSet) import Data.Map (Map) import Data.Monoid ((<>)) import Data.Sequence (ViewL(..))@@ -41,7 +42,7 @@ import Text.Trifecta.Delta (Delta)  import qualified Data.Char-import qualified Data.HashSet+import qualified Data.CharSet import qualified Data.Map import qualified Data.ByteString.Lazy import qualified Data.List@@ -92,7 +93,7 @@  instance TokenParsing Parser where     someSpace =-        Text.Parser.Token.Style.buildSomeSpaceParser +        Text.Parser.Token.Style.buildSomeSpaceParser             (Parser someSpace)             Text.Parser.Token.Style.haskellCommentStyle @@ -113,41 +114,8 @@     , _styleStart    =         Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ "_")     , _styleLetter   =-        Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_/")-    , _styleReserved = Data.HashSet.fromList-        [ "let"-        , "in"-        , "Type"-        , "Kind"-        , "forall"-        , "Bool"-        , "True"-        , "False"-        , "merge"-        , "if"-        , "then"-        , "else"-        , "as"-        , "Natural"-        , "Natural/fold"-        , "Natural/build"-        , "Natural/isZero"-        , "Natural/even"-        , "Natural/odd"-        , "Integer"-        , "Double"-        , "Text"-        , "List"-        , "List/build"-        , "List/fold"-        , "List/length"-        , "List/head"-        , "List/last"-        , "List/indexed"-        , "List/reverse"-        , "Optional"-        , "Optional/fold"-        ]+        Text.Parser.Char.oneOf (['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ "_-/")+    , _styleReserved = reservedIdentifiers     , _styleHighlight         = Identifier     , _styleReservedHighlight = ReservedIdentifier     }@@ -262,9 +230,21 @@ combine :: Parser () combine = symbol "/\\" <|> symbol "∧" +prefer :: Parser ()+prefer = symbol "//" <|> symbol "⫽"+ label :: Parser Text-label = Text.Parser.Token.ident identifierStyle <?> "label"+label = (normalIdentifier <|> escapedIdentifier) <?> "label"+  where+    normalIdentifier = Text.Parser.Token.ident identifierStyle +    escapedIdentifier = Text.Parser.Token.token (do+        _  <- Text.Parser.Char.char '`'+        c  <- Text.Parser.Token._styleStart  identifierStyle+        cs <- many (Text.Parser.Token._styleLetter identifierStyle)+        _  <- Text.Parser.Char.char '`'+        return (Data.Text.Lazy.pack (c:cs)) )+ -- | Parser for a top-level Dhall expression expr :: Parser (Expr Src Path) expr = exprA import_@@ -389,14 +369,15 @@         a <- pA         try (do _ <- pOp <?> "operator"; b <- pB; return (op a b)) <|> pure a ) -    exprC0 = chain exprC1 (symbol "||") BoolOr       exprC0-    exprC2 = chain exprC3 (symbol "++") TextAppend   exprC2-    exprC1 = chain exprC2 (symbol "+" ) NaturalPlus  exprC1-    exprC3 = chain exprC4 (symbol "&&") BoolAnd      exprC3-    exprC4 = chain exprC5  combine      Combine      exprC4-    exprC5 = chain exprC6 (symbol "*" ) NaturalTimes exprC5-    exprC6 = chain exprC7 (symbol "==") BoolEQ       exprC6-    exprC7 = chain (exprD embedded)  (symbol "!=") BoolNE       exprC7+    exprC0 = chain  exprC1          (symbol "||") BoolOr       exprC0+    exprC1 = chain  exprC2          (symbol "+" ) NaturalPlus  exprC1+    exprC2 = chain  exprC3          (symbol "++") TextAppend   exprC2+    exprC3 = chain  exprC4          (symbol "&&") BoolAnd      exprC3+    exprC4 = chain  exprC5           combine      Combine      exprC4+    exprC5 = chain  exprC6           prefer       Prefer       exprC5+    exprC6 = chain  exprC7          (symbol "*" ) NaturalTimes exprC6+    exprC7 = chain  exprC8          (symbol "==") BoolEQ       exprC7+    exprC8 = chain (exprD embedded) (symbol "!=") BoolNE       exprC8  -- We can't use left-recursion to define `exprD` otherwise the parser will -- loop infinitely. However, I'd still like to use left-recursion in the@@ -426,177 +407,202 @@  exprF :: Show a => Parser a -> Parser (Expr Src a) exprF embedded = choice-    [   noted (try exprF26)-    ,   noted (try exprF25)-    ,   noted      exprF24-    ,   noted      exprF27-    ,   noted (try exprF28)-    ,   noted      exprF29-    ,   noted (try exprF30)-    ,   noted      exprF31-    ,   noted      exprF32-    ,   noted      exprF33+    [   noted (try exprParseDouble)+    ,   noted (try exprNaturalLit)+    ,   noted      exprIntegerLit+    ,   noted      exprStringLiteral+    ,   noted (try exprRecordType)+    ,   noted      exprRecordLiteral+    ,   noted (try exprUnionType)+    ,   noted      exprUnionLiteral+    ,   noted      exprListLiteral+    ,   noted      exprImport     ,   (choice-            [   noted      exprF03-            ,   noted      exprF04-            ,   noted      exprF05-            ,   noted      exprF06-            ,   noted      exprF07-            ,   noted      exprF12-            ,   noted      exprF13-            ,   noted      exprF14-            ,   noted      exprF15-            ,   noted      exprF16-            ,   noted      exprF17-            ,   noted      exprF18-            ,   noted      exprF20-            ,   noted      exprF21-            ,   noted      exprF19-            ,   noted      exprF02-            ,   noted      exprF08-            ,   noted      exprF09-            ,   noted      exprF10-            ,   noted      exprF11-            ,   noted      exprF22-            ,   noted      exprF23-            ,   noted      exprF01+            [   noted      exprNaturalFold+            ,   noted      exprNaturalBuild+            ,   noted      exprNaturalIsZero+            ,   noted      exprNaturalEven+            ,   noted      exprNaturalOdd+            ,   noted      exprNaturalToInteger+            ,   noted      exprNaturalShow+            ,   noted      exprIntegerShow+            ,   noted      exprDoubleShow+            ,   noted      exprListBuild+            ,   noted      exprListFold+            ,   noted      exprListLength+            ,   noted      exprListHead+            ,   noted      exprListLast+            ,   noted      exprListIndexed+            ,   noted      exprListReverse+            ,   noted      exprOptionalFold+            ,   noted      exprOptionalBuild+            ,   noted      exprBool+            ,   noted      exprOptional+            ,   noted      exprNatural+            ,   noted      exprInteger+            ,   noted      exprDouble+            ,   noted      exprText+            ,   noted      exprList+            ,   noted      exprBoolLitTrue+            ,   noted      exprBoolLitFalse+            ,   noted      exprConst             ]         ) <?> "built-in value"-    ,   noted      exprF00-    ,              exprF34+    ,   noted      exprVar+    ,              exprParens     ]   where-    exprF00 = do+    exprVar = do         a <- var         return (Var a) -    exprF01 = do+    exprConst = do         a <- const         return (Const a) -    exprF02 = do+    exprNatural = do         reserve "Natural"         return Natural -    exprF03 = do+    exprNaturalFold = do         reserve "Natural/fold"         return NaturalFold -    exprF04 = do+    exprNaturalBuild = do         reserve "Natural/build"         return NaturalBuild -    exprF05 = do+    exprNaturalIsZero = do         reserve "Natural/isZero"         return NaturalIsZero -    exprF06 = do+    exprNaturalEven = do         reserve "Natural/even"         return NaturalEven -    exprF07 = do+    exprNaturalOdd = do         reserve "Natural/odd"         return NaturalOdd -    exprF08 = do+    exprNaturalToInteger = do+        reserve "Natural/toInteger"+        return NaturalToInteger++    exprNaturalShow = do+        reserve "Natural/show"+        return NaturalShow++    exprInteger = do         reserve "Integer"         return Integer -    exprF09 = do+    exprIntegerShow = do+        reserve "Integer/show"+        return IntegerShow++    exprDouble = do         reserve "Double"         return Double -    exprF10 = do+    exprDoubleShow = do+        reserve "Double/show"+        return DoubleShow++    exprText = do         reserve "Text"         return Text -    exprF11 = do+    exprList = do         reserve "List"         return List -    exprF12 = do+    exprListBuild = do         reserve "List/build"         return ListBuild -    exprF13 = do+    exprListFold = do         reserve "List/fold"         return ListFold -    exprF14 = do+    exprListLength = do         reserve "List/length"         return ListLength -    exprF15 = do+    exprListHead = do         reserve "List/head"         return ListHead -    exprF16 = do+    exprListLast = do         reserve "List/last"         return ListLast -    exprF17 = do+    exprListIndexed = do         reserve "List/indexed"         return ListIndexed -    exprF18 = do+    exprListReverse = do         reserve "List/reverse"         return ListReverse -    exprF19 = do+    exprOptional = do         reserve "Optional"         return Optional -    exprF20 = do+    exprOptionalFold = do         reserve "Optional/fold"         return OptionalFold -    exprF21 = do+    exprOptionalBuild = do+        reserve "Optional/build"+        return OptionalBuild++    exprBool = do         reserve "Bool"         return Bool -    exprF22 = do+    exprBoolLitTrue = do         reserve "True"         return (BoolLit True) -    exprF23 = do+    exprBoolLitFalse = do         reserve "False"         return (BoolLit False) -    exprF24 = do+    exprIntegerLit = do         a <- Text.Parser.Token.integer         return (IntegerLit a) -    exprF25 = (do+    exprNaturalLit = (do         _ <- Text.Parser.Char.char '+'         a <- Text.Parser.Token.natural         return (NaturalLit (fromIntegral a)) ) <?> "natural" -    exprF26 = do+    exprParseDouble = do         sign <-  fmap (\_ -> negate) (Text.Parser.Char.char '-')              <|> fmap (\_ -> id    ) (Text.Parser.Char.char '+')              <|> pure id         a <- Text.Parser.Token.double         return (DoubleLit (sign a)) -    exprF27 = do+    exprStringLiteral = do         a <- stringLiteral         return (TextLit a) -    exprF28 = record embedded <?> "record type"+    exprRecordType = record embedded <?> "record type" -    exprF29 = recordLit embedded <?> "record literal"+    exprRecordLiteral = recordLit embedded <?> "record literal" -    exprF30 = union embedded <?> "union type"+    exprUnionType = union embedded <?> "union type" -    exprF31 = unionLit embedded <?> "union literal"+    exprUnionLiteral = unionLit embedded <?> "union literal" -    exprF32 = listLit embedded <?> "list literal"+    exprListLiteral = listLit embedded <?> "list literal" -    exprF33 = do+    exprImport = do         a <- embedded <?> "import"         return (Embed a) -    exprF34 = do+    exprParens = do         symbol "("         a <- exprA embedded         symbol ")"@@ -734,6 +740,16 @@     pathMode <- rawText <|> pure Code     return (Path {..}) +pathChar :: Char -> Bool+pathChar c =+    not+    (   Data.Char.isSpace c+    ||  Data.CharSet.member c disallowedPathChars+    )++disallowedPathChars :: CharSet+disallowedPathChars = Data.CharSet.fromList "()[]{}<>:"+ file :: Parser PathType file =  try (token file0)     <|>      token file1@@ -742,26 +758,27 @@   where     file0 = do         a <- Text.Parser.Char.string "/"-        b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+        b <- many (Text.Parser.Char.satisfy pathChar)         case b of             '\\':_ -> empty -- So that "/\" parses as the operator and not a path+            '/' :_ -> empty -- So that "//" parses as the operator and not a path             _      -> return ()         return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b)))      file1 = do         a <- Text.Parser.Char.string "./"-        b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+        b <- many (Text.Parser.Char.satisfy pathChar)         return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b)))      file2 = do         a <- Text.Parser.Char.string "../"-        b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+        b <- many (Text.Parser.Char.satisfy pathChar)         return (File Homeless (Filesystem.Path.CurrentOS.decodeString (a <> b)))      file3 = do         _ <- Text.Parser.Char.string "~"         _ <- some (Text.Parser.Char.string "/")-        b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+        b <- many (Text.Parser.Char.satisfy pathChar)         return (File Home (Filesystem.Path.CurrentOS.decodeString b))  url :: Parser PathType@@ -770,18 +787,18 @@   where     url0 = do         a <- Text.Parser.Char.string "https://"-        b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+        b <- many (Text.Parser.Char.satisfy pathChar)         return (URL (Data.Text.Lazy.pack (a <> b)))      url1 = do         a <- Text.Parser.Char.string "http://"-        b <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+        b <- many (Text.Parser.Char.satisfy pathChar)         return (URL (Data.Text.Lazy.pack (a <> b)))  env :: Parser PathType env = do     _ <- Text.Parser.Char.string "env:"-    a <- many (Text.Parser.Char.satisfy (not . Data.Char.isSpace))+    a <- many (Text.Parser.Char.satisfy pathChar)     return (Env (Data.Text.Lazy.pack a))  -- | A parsing error

src/Dhall/Tutorial.hs view

@@ -456,12 +456,12 @@ -- -- __Exercise:__ There is a @not@ function hosted online here: ----- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not> -- -- Visit that link and read the documentation.  Then try to guess what this -- code returns: ----- > >>> input auto "https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool+-- > >>> input auto "https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not https://ipfs.io/ipfs/QmVf6hhTCXc9y2pRvhUmLk3AZYEgjeAz5PNwjt1GBYqsVB" :: IO Bool -- > ??? -- -- Run the code to test your guess@@ -766,37 +766,40 @@  -- $combine ----- You can combine two records, using the @(/\\)@ operator or the--- corresponding Unicode @(∧)@ (U+2227) operator:+-- You can combine two records, using either the @(//)@ operator or the+-- @(/\\)@ operator. --+-- The @(//)@ operator (or @(⫽)@ U+2AFD) combines the fields of both records,+-- preferring fields from the right record if they share fields in common:+-- -- > $ dhall--- > { foo = 1, bar = "ABC" } /\ { baz = True }+-- > { foo = 1, bar = "ABC" } // { baz = True } -- > <Ctrl-D> -- > { bar : Text, baz : Bool, foo : Integer } -- >  -- > { bar = "ABC", baz = True, foo = 1 }--- -- > $ dhall--- > { foo = 1, bar = "ABC" } ∧ { baz = True }  -- Fancy unicode+-- > { foo = 1, bar = "ABC" } ⫽ { bar = True }  -- Fancy unicode -- > <Ctrl-D>--- > { bar : Text, baz : Bool, foo : Integer }+-- > { bar : Bool, foo : Integer } -- > --- > { bar = "ABC", baz = True, foo = 1 }+-- > { bar = True, foo = 1 } -- -- Note that the order of record fields does not matter.  The compiler--- automatically sorts the fields when normalizing expressions.+-- automatically sorts the fields. ----- The @(∧)@ operator also merges records recursively.  For example:+-- The @(/\\)@ operator (or @(∧)@ U+2227) also lets you combine records, but+-- behaves differently if the records share fields in common.  The operator+-- combines shared fields recursively if they are both records: -- -- > $ dhall--- > { foo = { bar = True }, baz = "ABC" } ∧ { foo = { qux = 1.0 } }+-- > { foo = { bar = True }, baz = "ABC" } /\ { foo = { qux = 1.0 } } -- > <Ctrl-D> -- > { baz : Text, foo : { bar : Bool, qux : Double } } -- >  -- > { baz = "ABC", foo = { bar = True, qux = 1.0 } } ----- However, you cannot combine two records if they share a field that is not a--- record:+-- ... but fails with a type error if either shared field is not a record: -- -- > $ dhall -- > { foo = 1, bar = "ABC" } ∧ { foo = True }@@ -809,8 +812,8 @@ -- >  -- > (stdin):1:1 ----- __Exercise__: Combine any record with the empty record.  What do you expect to--- happen?+-- __Exercise__: Combine any record with the empty record.  What do you expect+-- to happen?  -- $let --@@ -901,7 +904,7 @@ -- You can also use @let@ expressions to rename imports, like this: -- -- > $ dhall--- > let not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not+-- > let not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not -- > in  not True -- > <Ctrl-D> -- > Bool@@ -1182,7 +1185,7 @@ -- complex example: -- -- > $ dhall--- >     let List/map = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- >     let List/map = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- > in  λ(f : Integer → Integer) → List/map Integer Integer f [1, 2, 3] -- > <Ctrl-D> -- > ∀(f : Integer → Integer) → List Integer@@ -1206,11 +1209,11 @@ -- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can -- find here: ----- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate>+-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate> -- -- Test what the following Dhall expression normalizes to: ----- > let replicate = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/replicate+-- > let replicate = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/replicate -- > in  replicate +10 -- -- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by@@ -1760,7 +1763,7 @@ -- -- Rules: ----- > let List/concat = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat+-- > let List/concat = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat -- > -- > List/fold a (List/concat a xss) b c -- >     = List/fold (List a) xss b (λ(x : List a) → List/fold a x b c)@@ -1829,10 +1832,10 @@ -- -- Rules: ----- > let Optional/head  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/head--- > let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat--- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap--- > let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > let Optional/head  = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/head+-- > let List/concat    = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat+-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap+-- > let List/map       = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- >  -- > List/head a (List/concat a xss) = -- >     Optional/head a (List/map (List a) (Optional a) (List/head a) xss)@@ -1860,10 +1863,10 @@ -- -- Rules: ----- > let Optional/last  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Optional/last--- > let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat--- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap--- > let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > let Optional/last  = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Optional/last+-- > let List/concat    = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat+-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap+-- > let List/map       = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- >  -- > List/last a (List/concat a xss) = -- >     Optional/last a (List/map (List a) (Optional a) (List/last a) xss)@@ -1891,9 +1894,9 @@ -- -- Rules: ----- > let List/shifted = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/shifted--- > let List/concat  = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat--- > let List/map     = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map+-- > let List/shifted = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/shifted+-- > let List/concat  = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat+-- > let List/map     = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map -- >  -- > List/indexed a (List/concat a xss) = -- >     List/shifted a (List/map (List a) (List { index : Natural, value : a }) (List/indexed a) xss)@@ -1916,9 +1919,9 @@ -- -- Rules: ----- > let List/map       = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/map--- > let List/concat    = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concat--- > let List/concatMap = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/List/concatMap+-- > let List/map       = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/map+-- > let List/concat    = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concat+-- > let List/concatMap = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/List/concatMap -- >  -- > List/reverse a (List/concat a xss) -- >     = List/concat a (List/reverse (List a) (List/map (List a) (List a) (List/reverse a) xss))@@ -1972,7 +1975,7 @@ -- -- There is also a Prelude available at: ----- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude>+-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/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@@ -1983,12 +1986,12 @@ -- subdirectories.  For example, the @Bool@ subdirectory has a @not@ file -- located here: ----- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not>+-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not> -- -- The @not@ function is just a UTF8-encoded text file hosted online with the -- following contents ----- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not+-- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not -- > {- -- > Flip the value of a `Bool` -- > @@ -2021,7 +2024,7 @@ -- You can use this @not@ function either directly: -- -- > $ dhall--- > https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not True+-- > https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not True -- > <Ctrl-D> -- > Bool -- > @@ -2030,7 +2033,7 @@ -- ... or assign the URL to a shorter name: -- -- > $ dhall--- > let Bool/not = https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Bool/not+-- > let Bool/not = https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Bool/not -- > in  Bool/not True -- > <Ctrl-D> -- > Bool@@ -2041,7 +2044,7 @@ -- consistency and documentation, such as @Prelude\/Natural\/even@, which -- re-exports the built-in @Natural/even@ function: ----- > $ curl https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/Natural/even+-- > $ curl https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/Natural/even -- > {- -- > Returns `True` if a number if even and returns `False` otherwise -- > @@ -2062,7 +2065,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/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude/+-- > $ wget -np -nH -r --cut-dirs=2 https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude/ -- > $ tree Prelude -- > Prelude -- > ├── Bool@@ -2072,7 +2075,12 @@ -- > │   ├── fold -- > │   ├── not -- > │   ├── odd--- > │   └── or+-- > │   ├── or+-- > │   └── show+-- > ├── Double+-- > │   └── show+-- > ├── Integer+-- > │   └── show -- > ├── List -- > │   ├── all -- > │   ├── any@@ -2101,7 +2109,9 @@ -- > │   ├── isZero -- > │   ├── odd -- > │   ├── product--- > │   └── sum+-- > │   ├── show+-- > │   ├── sum+-- > │   └── toInteger -- > ├── Optional -- > │   ├── build -- > │   ├── concat@@ -2111,19 +2121,20 @@ -- > │   ├── map -- > │   ├── toList -- > │   └── unzip--- > └── Text--- >     └── concat+-- > ├── Text+-- > │   └── concat+-- > └── index.html -- -- ... or if you have an @ipfs@ daemon running, you can mount the Prelude -- locally like this: -- -- > $ ipfs mount--- > $ cd /ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude+-- > $ cd /ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude -- -- Browse the Prelude online to learn more by seeing what functions are -- available and reading their inline documentation: ----- <https://ipfs.io/ipfs/QmcTbCdS21pCxXysTzEiucDuwwLWbLUWNSKwkJVfwpy2zK/Prelude>+-- <https://ipfs.io/ipfs/Qmbh2ifwcpX9a384vJMehySbV7rdvYhzVbL5ySs84k8BgY/Prelude> -- -- __Exercise__: Try to use a new Prelude function that has not been covered -- previously in this tutorial

src/Dhall/TypeCheck.hs view

@@ -308,6 +308,10 @@     return (Pi "_" Natural Bool) typeWith _      NaturalOdd        = do     return (Pi "_" Natural Bool)+typeWith _      NaturalToInteger  = do+    return (Pi "_" Natural Integer)+typeWith _      NaturalShow  = do+    return (Pi "_" Natural Text) typeWith ctx e@(NaturalPlus  l r) = do     tl <- fmap Dhall.Core.normalize (typeWith ctx l)     case tl of@@ -334,10 +338,14 @@     return (Const Type) typeWith _     (IntegerLit _    ) = do     return Integer+typeWith _      IntegerShow  = do+    return (Pi "_" Integer Text) typeWith _      Double            = do     return (Const Type) typeWith _     (DoubleLit _     ) = do     return Double+typeWith _     DoubleShow         = do+    return (Pi "_" Double Text) typeWith _      Text              = do     return (Const Type) typeWith _     (TextLit _       ) = do@@ -444,6 +452,13 @@                 (Pi "optional" (Const Type)                     (Pi "just" (Pi "_" "a" "optional")                         (Pi "nothing" "optional" "optional") ) ) ) )+typeWith _      OptionalBuild     = do+    return+        (Pi "a" (Const Type)+            (Pi "_" f (App Optional "a") ) )+    where f = Pi "optional" (Const Type)+                  (Pi "just" (Pi "_" "a" "optional")+                      (Pi "nothing" "optional" "optional") ) typeWith ctx e@(Record    kts   ) = do     let process (k, t) = do             s <- fmap Dhall.Core.normalize (typeWith ctx t)@@ -482,12 +497,12 @@     tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX)     ktsX  <- case tKvsX of         Record kts -> return kts-        _          -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX))+        _          -> Left (TypeError ctx e (MustCombineARecord '∧' kvsX tKvsX))      tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY)     ktsY  <- case tKvsY of         Record kts -> return kts-        _          -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY))+        _          -> Left (TypeError ctx e (MustCombineARecord '∧' kvsY tKvsY))      let combineTypes ktsL ktsR = do             let ks =@@ -506,6 +521,17 @@             return (Record (Data.Map.fromList kts))      combineTypes ktsX ktsY+typeWith ctx e@(Prefer kvsX kvsY) = do+    tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX)+    ktsX  <- case tKvsX of+        Record kts -> return kts+        _          -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsX tKvsX))++    tKvsY <- fmap Dhall.Core.normalize (typeWith ctx kvsY)+    ktsY  <- case tKvsY of+        Record kts -> return kts+        _          -> Left (TypeError ctx e (MustCombineARecord '⫽' kvsY tKvsY))+    return (Record (Data.Map.union ktsY ktsX)) typeWith ctx e@(Merge kvsX kvsY t) = do     tKvsX <- fmap Dhall.Core.normalize (typeWith ctx kvsX)     ktsX  <- case tKvsX of@@ -569,6 +595,9 @@ instance Show X where     show = absurd +instance Eq X where+  _ == _ = True+ instance Buildable X where     build = absurd @@ -596,7 +625,7 @@     | InvalidAlternative Text (Expr s X)     | InvalidAlternativeType Text (Expr s X)     | DuplicateAlternative Text-    | MustCombineARecord (Expr s X) (Expr s X)+    | MustCombineARecord Char (Expr s X) (Expr s X)     | FieldCollision Text     | MustMergeARecord (Expr s X) (Expr s X)     | MustMergeUnion (Expr s X) (Expr s X)@@ -2086,22 +2115,22 @@       where         txt0 = Text.toStrict (Dhall.Core.pretty k) -prettyTypeMessage (MustCombineARecord expr0 expr1) = ErrorMessages {..}+prettyTypeMessage (MustCombineARecord c expr0 expr1) = ErrorMessages {..}   where     short = "You can only combine records"      long =         Builder.fromText [NeatInterpolation.text|-Explanation: You can combine records using the ❰∧❱ operator, like this:+Explanation: You can combine records using the ❰$op❱ operator, like this:       ┌───────────────────────────────────────────┐-    │ { foo = 1, bar = "ABC" } ∧ { baz = True } │+    │ { foo = 1, bar = "ABC" } $op { baz = True } │     └───────────────────────────────────────────┘       ┌─────────────────────────────────────────────┐-    │ λ(r : { foo : Bool }) → r ∧ { bar = "ABC" } │+    │ λ(r : { foo : Bool }) → r $op { bar = "ABC" } │     └─────────────────────────────────────────────┘  @@ -2111,21 +2140,21 @@       ┌──────────────────────────────┐-    │ { foo = 1, bar = "ABC" } ∧ 1 │+    │ { foo = 1, bar = "ABC" } $op 1 │     └──────────────────────────────┘                                  ⇧                                  Invalid: Not a record       ┌───────────────────────────────────────────┐-    │ { foo = 1, bar = "ABC" } ∧ { baz : Bool } │+    │ { foo = 1, bar = "ABC" } $op { baz : Bool } │     └───────────────────────────────────────────┘                                  ⇧                                  Invalid: This is a record type and not a record       ┌───────────────────────────────────────────┐-    │ { foo = 1, bar = "ABC" } ∧ < baz = True > │+    │ { foo = 1, bar = "ABC" } $op < baz = True > │     └───────────────────────────────────────────┘                                  ⇧                                  Invalid: This is a union and not a record@@ -2140,6 +2169,7 @@ ↳ $txt1 |]       where+        op   = Data.Text.singleton c         txt0 = Text.toStrict (Dhall.Core.pretty expr0)         txt1 = Text.toStrict (Dhall.Core.pretty expr1)

+ tests/Examples.hs view

@@ -0,0 +1,1136 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes       #-}++module Examples where++import qualified NeatInterpolation+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 "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 "build"+                [ _Optional_build_0+                , _Optional_build_1+                ]+            , Test.Tasty.testGroup "concat"+                [ _Optional_concat_0+                , _Optional_concat_1+                , _Optional_concat_2+                ]+            , 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 "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+                ]+            ]+        ]++_Bool_and_0 :: TestTree+_Bool_and_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/List/build+Text+(   λ(list : Type)+→   λ(cons : Text → list → list)+→   λ(nil : list)+→   cons "ABC" (cons "DEF" nil)+)+|]+    Util.assertNormalizesTo e "[\"ABC\", \"DEF\"] : List Text" )++_List_build_1 :: TestTree+_List_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/List/build+Text+(   λ(list : Type)+→   λ(cons : Text → list → list)+→   λ(nil : list)+→   nil+)+|]+    Util.assertNormalizesTo e "[] : List Text" )++_List_concat_0 :: TestTree+_List_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/List/concat Integer+(   [   [0, 1, 2]    : List Integer+    ,   [3, 4]       : List Integer+    ,   [5, 6, 7, 8] : List Integer+    ]   : List (List Integer)+)+|]+    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 [NeatInterpolation.text|+./Prelude/List/concat Integer+(   [   [] : List Integer+    ,   [] : List Integer+    ,   [] : List Integer+    ]   : List (List Integer)+)+|]+    Util.assertNormalizesTo e "[] : List Integer" )++_List_filter_0 :: TestTree+_List_filter_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+    ./Prelude/List/fold+    Natural+    ([+2, +3, +5] : List Natural)+    Natural+    (λ(x : Natural) → λ(y : Natural) → x + y)+    +0+|]+    Util.assertNormalizesTo e "+10" )++_List_fold_1 :: TestTree+_List_fold_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+    λ(nil : Natural)+→   ./Prelude/List/fold+    Natural+    ([+2, +3, +5] : List Natural)+    Natural+    (λ(x : Natural) → λ(y : Natural) → x + y)+    nil+|]+    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 [NeatInterpolation.text|+    λ(list : Type)+→   λ(cons : Natural → list → list)+→   λ(nil : list)+→   ./Prelude/List/fold Natural ([+2, +3, +5] : List Natural) list cons nil+|]+    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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/List/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 })+)+|]+    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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/List/unzip+Text+Bool+(   [   { _1 = "ABC", _2 = True  }+    ,   { _1 = "DEF", _2 = False }+    ,   { _1 = "GHI", _2 = True  }+    ]   : List { _1 : Text, _2 : Bool }+)+|]+    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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Bool/and+    : ./Prelude/Monoid Bool+|] )++_Monoid_01 :: TestTree+_Monoid_01 = Test.Tasty.HUnit.testCase "Example #1"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Bool/or+    : ./Prelude/Monoid Bool+|] )++_Monoid_02 :: TestTree+_Monoid_02 = Test.Tasty.HUnit.testCase "Example #2"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Bool/even+    : ./Prelude/Monoid Bool+|] )++_Monoid_03 :: TestTree+_Monoid_03 = Test.Tasty.HUnit.testCase "Example #3"+    (Util.assertTypeChecks[NeatInterpolation.text|+./Prelude/Bool/odd+    : ./Prelude/Monoid Bool+|] )++_Monoid_04 :: TestTree+_Monoid_04 = Test.Tasty.HUnit.testCase "Example #4"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/List/concat+    : ∀(a : Type) → ./Prelude/Monoid (List a)+|] )++_Monoid_05 :: TestTree+_Monoid_05 = Test.Tasty.HUnit.testCase "Example #5"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/List/shifted+    : ∀(a : Type) → ./Prelude/Monoid (List { index : Natural, value : a })+|] )++_Monoid_06 :: TestTree+_Monoid_06 = Test.Tasty.HUnit.testCase "Example #6"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Natural/sum+    : ./Prelude/Monoid Natural+|] )++_Monoid_07 :: TestTree+_Monoid_07 = Test.Tasty.HUnit.testCase "Example #7"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Natural/product+    : ./Prelude/Monoid Natural+|] )++_Monoid_08 :: TestTree+_Monoid_08 = Test.Tasty.HUnit.testCase "Example #8"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Optional/head+    : ∀(a : Type) → ./Prelude/Monoid (Optional a)+|] )++_Monoid_09 :: TestTree+_Monoid_09 = Test.Tasty.HUnit.testCase "Example #9"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Optional/last+    : ∀(a : Type) → ./Prelude/Monoid (Optional a)+|] )++_Monoid_10 :: TestTree+_Monoid_10 = Test.Tasty.HUnit.testCase "Example #10"+    (Util.assertTypeChecks [NeatInterpolation.text|+./Prelude/Text/concat+    : ./Prelude/Monoid Text+|] )++_Natural_build_0 :: TestTree+_Natural_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Natural/build+(   λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   succ (succ (succ zero))+)+|]+    Util.assertNormalizesTo e "+3" )++_Natural_build_1 :: TestTree+_Natural_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Natural/build+(   λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   zero+)+|]+    Util.assertNormalizesTo e "+0" )++_Natural_enumerate_0 :: TestTree+_Natural_enumerate_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+λ(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 [NeatInterpolation.text|+    λ(natural : Type)+→   λ(succ : natural → natural)+→   λ(zero : natural)+→   ./Prelude/Natural/fold +3 natural succ zero+|]+    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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Natural/toInteger +0+|]+    Util.assertNormalizesTo e "0" )++_Optional_build_0 :: TestTree+_Optional_build_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Optional/build+Integer+(   λ(optional : Type)+→   λ(just : Integer → optional)+→   λ(nothing : optional)+→   just 1+)+|]+    Util.assertNormalizesTo e "[1] : Optional Integer" )++_Optional_build_1 :: TestTree+_Optional_build_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Optional/build+Integer+(   λ(optional : Type)+→   λ(just : Integer → optional)+→   λ(nothing : optional)+→   nothing+)+|]+    Util.assertNormalizesTo e "[] : Optional Integer" )++_Optional_concat_0 :: TestTree+_Optional_concat_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Optional/concat Integer ([] : Optional (Optional Integer))+|]+    Util.assertNormalizesTo e "[] : Optional Integer" )++_Optional_fold_0 :: TestTree+_Optional_fold_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Optional/head+Integer+(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]+    : List (Optional Integer)+)+|]+    Util.assertNormalizesTo e "[1] : Optional Integer" )++_Optional_head_1 :: TestTree+_Optional_head_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Optional/head+Integer+([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))+|]+    Util.assertNormalizesTo e "[] : Optional Integer" )++_Optional_head_2 :: TestTree+_Optional_head_2 = Test.Tasty.HUnit.testCase "Example #2" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Optional/last+Integer+(   [[] : Optional Integer, [1] : Optional Integer, [2] : Optional Integer]+    : List (Optional Integer)+)+|]+    Util.assertNormalizesTo e "[2] : Optional Integer" )++_Optional_last_1 :: TestTree+_Optional_last_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Optional/last+Integer+([[] : Optional Integer, [] : Optional Integer] : List (Optional Integer))+|]+    Util.assertNormalizesTo e "[] : Optional Integer" )++_Optional_last_2 :: TestTree+_Optional_last_2 = Test.Tasty.HUnit.testCase "Example #2" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Optional/map Natural Bool Natural/even ([] : Optional Natural)+|]+    Util.assertNormalizesTo e "[] : Optional Bool" )++_Optional_toList_0 :: TestTree+_Optional_toList_0 = Test.Tasty.HUnit.testCase "Example #0" (do+    e <- Util.code [NeatInterpolation.text|+./Prelude/Optional/toList Integer ([1] : Optional Integer)+|]+    Util.assertNormalizesTo e "[1] : List Integer" )++_Optional_toList_1 :: TestTree+_Optional_toList_1 = Test.Tasty.HUnit.testCase "Example #1" (do+    e <- Util.code [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Optional/unzip+Text+Bool+([{ _1 = "ABC", _2 = True  }] : Optional { _1 : Text, _2 : Bool })+|]+    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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./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 [NeatInterpolation.text|+./Prelude/Text/concat ([] : List Text)+|]+    Util.assertNormalizesTo e "\"\"" )

+ tests/Normalization.hs view

@@ -0,0 +1,156 @@+{-# LANGUAGE OverloadedLists   #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE QuasiQuotes       #-}++module Normalization (normalizationTests) where++import           Dhall.Core+import qualified NeatInterpolation+import           Test.Tasty+import           Test.Tasty.HUnit+import           Util (code, normalize', assertNormalizesTo, assertNormalized)++normalizationTests :: TestTree+normalizationTests = testGroup "normalization" [ constantFolding+                                               , conversions+                                               , fusion+                                               ]++constantFolding :: TestTree+constantFolding = testGroup "folding of constants" [ naturalPlus+                                                   , optionalFold+                                                   , optionalBuild+                                                   ]++conversions :: TestTree+conversions = testGroup "conversions" [ naturalShow+                                      , integerShow+                                      , doubleShow+                                      , naturalToInteger+                                      ]++naturalPlus :: TestTree+naturalPlus = testCase "natural plus" $ do+  e <- code "+1 + +2"+  e `assertNormalizesTo` "+3"++naturalToInteger :: TestTree+naturalToInteger = testCase "Natural/toInteger" $ do+  e <- code "Natural/toInteger +1"+  isNormalized e @?= False+  normalize' e @?= "1"++naturalShow :: TestTree+naturalShow = testCase "Natural/show" $ do+  e <- code "Natural/show +42"+  e `assertNormalizesTo` "\"+42\""++integerShow :: TestTree+integerShow = testCase "Integer/show" $ do+  e <- code "[Integer/show 1337, Integer/show -42, Integer/show 0]"+  e `assertNormalizesTo` "[\"1337\", \"-42\", \"0\"]"++doubleShow :: TestTree+doubleShow = testCase "Double/show" $ do+  e <- code "[Double/show -0.42, Double/show 13.37]"+  e `assertNormalizesTo` "[\"-0.42\", \"13.37\"]"++optionalFold :: TestTree+optionalFold = testGroup "Optional/fold" [ just, nothing ]+  where test label inp out = testCase label $ do+             e <- code [NeatInterpolation.text|+                         Optional/fold Text ([$inp] : Optional Text) Natural (λ(j : Text) → +1) +2+                       |]+             e `assertNormalizesTo` out+        just = test "just" "\"foo\"" "+1"+        nothing = test "nothing" "" "+2"++optionalBuild :: TestTree+optionalBuild = testGroup "Optional/build" [ optionalBuild1+                                           , optionalBuildShadowing+                                           , optionalBuildIrreducible+                                           ]++optionalBuild1 :: TestTree+optionalBuild1 = testCase "reducible" $ do+  e <- code [NeatInterpolation.text|+Optional/build+Natural+(   λ(optional : Type)+→   λ(just : Natural → optional)+→   λ(nothing : optional)+→   just +1+)+|]+  e `assertNormalizesTo` "[+1] : Optional Natural"++optionalBuildShadowing :: TestTree+optionalBuildShadowing = testCase "handles shadowing" $ do+  e <- code [NeatInterpolation.text|+Optional/build+Integer+(   λ(optional : Type)+→   λ(x : Integer → optional)+→   λ(x : optional)+→   x@1 1+)+|]+  e `assertNormalizesTo` "[1] : Optional Integer"++optionalBuildIrreducible :: TestTree+optionalBuildIrreducible = testCase "irreducible" $ do+  e <- code [NeatInterpolation.text|+    λ(id : ∀(a : Type) → a → a)+→   Optional/build+    Bool+    (   λ(optional : Type)+    →   λ(just : Bool → optional)+    →   λ(nothing : optional)+    →   id optional (just True)+    )+|]+  assertNormalized e++fusion :: TestTree+fusion = testGroup "Optional build/fold fusion" [ fuseOptionalBF+                                                , fuseOptionalFB+                                                ]++fuseOptionalBF :: TestTree+fuseOptionalBF = testCase "fold . build" $ do+  e0 <- code [NeatInterpolation.text|+    λ(  f+    :   ∀(optional : Type)+    →   ∀(just : Text → optional)+    →   ∀(nothing : optional)+    →   optional+    )+→   Optional/fold+    Text+    (   Optional/build+        Text+        f+    )+|]+  e1 <- code [NeatInterpolation.text|+    λ(  f+    :   ∀(optional : Type)+    →   ∀(just : Text → optional)+    →   ∀(nothing : optional)+    →   optional+    )+→   f+|]+  e0 `assertNormalizesTo` (Dhall.Core.pretty e1)++fuseOptionalFB :: TestTree+fuseOptionalFB = testCase "build . fold" $ do+  test <- code [NeatInterpolation.text|+Optional/build+Text+(   Optional/fold+    Text+    (["foo"] : Optional Text)+)+|]+  test `assertNormalizesTo` "[\"foo\"] : Optional Text"

+ tests/Tests.hs view

@@ -0,0 +1,15 @@+module Main where++import Normalization (normalizationTests)+import Examples (exampleTests)+import Test.Tasty++allTests :: TestTree+allTests =+    testGroup "Dhall Tests"+        [ normalizationTests+        , exampleTests+        ]++main :: IO ()+main = defaultMain allTests

+ tests/Util.hs view

@@ -0,0 +1,53 @@+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE OverloadedStrings #-}+module Util+    ( code+    , normalize'+    , assertNormalizesTo+    , assertNormalized+    , assertTypeChecks+    ) where++import qualified Control.Exception+import qualified Data.Functor+import           Data.Text (Text)+import qualified Data.Text.Lazy+import qualified Dhall.Core+import           Dhall.Core (Expr)+import qualified Dhall.Import+import qualified Dhall.Parser+import           Dhall.Parser (Src)+import qualified Dhall.TypeCheck+import           Dhall.TypeCheck (X)+import           Test.Tasty.HUnit++normalize' :: Expr Src X -> Data.Text.Lazy.Text+normalize' = Dhall.Core.pretty . Dhall.Core.normalize++code :: Data.Text.Text -> IO (Expr Src X)+code strictText = do+    let lazyText = Data.Text.Lazy.fromStrict strictText+    expr0 <- case Dhall.Parser.exprFromText mempty lazyText of+        Left parseError -> Control.Exception.throwIO parseError+        Right expr0     -> return expr0+    expr1 <- Dhall.Import.load expr0+    case Dhall.TypeCheck.typeOf expr1 of+        Left typeError -> Control.Exception.throwIO typeError+        Right _        -> return ()+    return expr1++assertNormalizesTo :: Expr Src X -> Data.Text.Lazy.Text -> IO ()+assertNormalizesTo e expected = do+  assertBool msg (not $ Dhall.Core.isNormalized e)+  normalize' e @?= expected+  where msg = "Given expression is already in normal form"++assertNormalized :: Expr Src X -> IO ()+assertNormalized e = do+  assertBool msg1 (Dhall.Core.isNormalized e)+  assertEqual msg2 (normalize' e) (Dhall.Core.pretty e)+  where msg1 = "Expression was not in normal form"+        msg2 = "Normalization is not supposed to change the expression"++assertTypeChecks :: Text -> IO ()+assertTypeChecks text = Data.Functor.void (code text)