Switch grammar of Natural and Integer (#381)
... as standardized in https://github.com/dhall-lang/dhall-lang/pull/141 Now `Natural`s no longer require a leading `+` and non-negative `Integer`s require a leading `+` This also adds a `doctest` test suite to prevent regressions in haddock examples
This commit is contained in:
Gabriel Gonzalez
GitHub
parent
fa4569eaaf
commit
2e631db47a
|
|
@ -4,9 +4,9 @@
|
|||
Examples:
|
||||
|
||||
```
|
||||
./fold True Integer 0 1 = 0
|
||||
./fold True Natural 0 1 = 0
|
||||
|
||||
./fold False Integer 0 1 = 1
|
||||
./fold False Natural 0 1 = 1
|
||||
```
|
||||
-}
|
||||
let fold
|
||||
|
|
|
|||
|
|
@ -1,13 +1,14 @@
|
|||
{-
|
||||
Render an `Integer` as `Text` using the same representation as Dhall source
|
||||
code (i.e. a decimal number with a leading `-` sign if negative)
|
||||
code (i.e. a decimal number with a leading `-` sign if negative and a leading
|
||||
`+` sign if non-negative)
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./show -3 = "-3"
|
||||
|
||||
./show 0 = "0"
|
||||
./show +0 = "+0"
|
||||
```
|
||||
-}
|
||||
let show : Integer → Text = Integer/show in show
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for all elements in the
|
|||
Examples:
|
||||
|
||||
```
|
||||
./all Natural Natural/even [ +2, +3, +5 ] = False
|
||||
./all Natural Natural/even [ 2, 3, 5 ] = False
|
||||
|
||||
./all Natural Natural/even ([] : List Natural) = True
|
||||
```
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for any element in the
|
|||
Examples:
|
||||
|
||||
```
|
||||
./any Natural Natural/even [ +2, +3, +5 ] = True
|
||||
./any Natural Natural/even [ 2, 3, 5 ] = True
|
||||
|
||||
./any Natural Natural/even ([] : List Natural) = False
|
||||
```
|
||||
|
|
|
|||
|
|
@ -4,22 +4,22 @@ Concatenate a `List` of `List`s into a single `List`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./concat Integer
|
||||
./concat Natural
|
||||
[ [0, 1, 2]
|
||||
, [3, 4]
|
||||
, [5, 6, 7, 8]
|
||||
]
|
||||
= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
|
||||
|
||||
./concat Integer
|
||||
( [ [] : List Integer
|
||||
, [] : List Integer
|
||||
, [] : List Integer
|
||||
./concat Natural
|
||||
( [ [] : List Natural
|
||||
, [] : List Natural
|
||||
, [] : List Natural
|
||||
]
|
||||
)
|
||||
= [] : List Integer
|
||||
= [] : List Natural
|
||||
|
||||
./concat Integer ([] : List (List Integer)) = [] : List Integer
|
||||
./concat Natural ([] : List (List Natural)) = [] : List Natural
|
||||
```
|
||||
-}
|
||||
let concat
|
||||
|
|
|
|||
|
|
@ -5,8 +5,8 @@ results
|
|||
Examples:
|
||||
|
||||
```
|
||||
./concatMap Natural Natural (λ(n : Natural) → [n, n]) [+2, +3, +5]
|
||||
= [ +2, +2, +3, +3, +5, +5 ]
|
||||
./concatMap Natural Natural (λ(n : Natural) → [n, n]) [2, 3, 5]
|
||||
= [ 2, 2, 3, 3, 5, 5 ]
|
||||
|
||||
./concatMap Natural Natural (λ(n : Natural) → [n, n]) ([] : List Natural)
|
||||
= [] : List Natural
|
||||
|
|
|
|||
|
|
@ -4,11 +4,11 @@ Only keep elements of the list where the supplied function returns `True`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./filter Natural Natural/even [+2, +3, +5]
|
||||
= [ +2 ]
|
||||
./filter Natural Natural/even [ 2, 3, 5 ]
|
||||
= [ 2 ]
|
||||
|
||||
./filter Natural Natural/odd [+2, +3, +5]
|
||||
= [ +3, +5 ]
|
||||
./filter Natural Natural/odd [ 2, 3, 5 ]
|
||||
= [ 3, 5 ]
|
||||
```
|
||||
-}
|
||||
let filter
|
||||
|
|
|
|||
|
|
@ -9,29 +9,29 @@ Examples:
|
|||
```
|
||||
./fold
|
||||
Natural
|
||||
[ +2, +3, +5 ]
|
||||
[ 2, 3, 5 ]
|
||||
Natural
|
||||
(λ(x : Natural) → λ(y : Natural) → x + y)
|
||||
+0
|
||||
= +10
|
||||
0
|
||||
= 10
|
||||
|
||||
λ(nil : Natural)
|
||||
→ ./fold
|
||||
Natural
|
||||
[ +2, +3, +5 ]
|
||||
[ 2, 3, 5 ]
|
||||
Natural
|
||||
(λ(x : Natural) → λ(y : Natural) → x + y)
|
||||
nil
|
||||
= λ(nil : Natural) → +2 + +3 + +5 + nil
|
||||
= λ(nil : Natural) → 2 + 3 + 5 + nil
|
||||
|
||||
λ(list : Type)
|
||||
→ λ(cons : Natural → list → list)
|
||||
→ λ(nil : list)
|
||||
→ ./fold Natural [ +2, +3, +5 ] list cons nil
|
||||
→ ./fold Natural [ 2, 3, 5 ] list cons nil
|
||||
= λ(list : Type)
|
||||
→ λ(cons : Natural → list → list)
|
||||
→ λ(nil : list)
|
||||
→ cons +2 (cons +3 (cons +5 nil))
|
||||
→ cons 2 (cons 3 (cons 5 nil))
|
||||
```
|
||||
-}
|
||||
let fold
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
{-
|
||||
Build a list by calling the supplied function on all `Natural` numbers from `+0`
|
||||
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 ]
|
||||
./generate 5 Bool Natural/even = [ True, False, True, False, True ]
|
||||
|
||||
./generate +0 Bool Natural/even = [] : List Bool
|
||||
./generate 0 Bool Natural/even = [] : List Bool
|
||||
```
|
||||
-}
|
||||
let generate
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Retrieve the first element of the list
|
|||
Examples:
|
||||
|
||||
```
|
||||
./head Integer [ 0, 1, 2 ] = [ 0 ] : Optional Integer
|
||||
./head Natural [ 0, 1, 2 ] = [ 0 ] : Optional Natural
|
||||
|
||||
./head Integer ([] : List Integer) = [] : Optional Integer
|
||||
./head Natural ([] : List Natural) = [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let head : ∀(a : Type) → List a → Optional a = List/head in head
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@ Examples:
|
|||
|
||||
```
|
||||
./indexed Bool [ True, False, True ]
|
||||
= [ { index = +0, value = True }
|
||||
, { index = +1, value = False }
|
||||
, { index = +2, value = True }
|
||||
= [ { index = 0, value = True }
|
||||
, { index = 1, value = False }
|
||||
, { index = 2, value = True }
|
||||
] : List { index : Natural, value : Bool }
|
||||
|
||||
./indexed Bool ([] : List Bool)
|
||||
|
|
|
|||
|
|
@ -5,10 +5,10 @@ function
|
|||
Examples:
|
||||
|
||||
```
|
||||
./iterate +10 Natural (λ(x : Natural) → x * +2) +1
|
||||
= [ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]
|
||||
./iterate 10 Natural (λ(x : Natural) → x * 2) 1
|
||||
= [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
|
||||
|
||||
./iterate +0 Natural (λ(x : Natural) → x * +2) +1
|
||||
./iterate 0 Natural (λ(x : Natural) → x * 2) 1
|
||||
= [] : List Natural
|
||||
```
|
||||
-}
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Retrieve the last element of the list
|
|||
Examples:
|
||||
|
||||
```
|
||||
./last Integer [ 0, 1, 2 ] = [ 2 ] : Optional Integer
|
||||
./last Natural [ 0, 1, 2 ] = [ 2 ] : Optional Natural
|
||||
|
||||
./last Integer ([] : List Integer) = [] : Optional Integer
|
||||
./last Natural ([] : List Natural) = [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let last : ∀(a : Type) → List a → Optional a = List/last in last
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Returns the number of elements in a list
|
|||
Examples:
|
||||
|
||||
```
|
||||
./length Integer [ 0, 1, 2 ] = +3
|
||||
./length Natural [ 0, 1, 2 ] = 3
|
||||
|
||||
./length Integer ([] : List Integer) = +0
|
||||
./length Natural ([] : List Natural) = 0
|
||||
```
|
||||
-}
|
||||
let length : ∀(a : Type) → List a → Natural = List/length in length
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Transform a list by applying a function to each element
|
|||
Examples:
|
||||
|
||||
```
|
||||
./map Natural Bool Natural/even [ +2, +3, +5 ]
|
||||
./map Natural Bool Natural/even [ 2, 3, 5 ]
|
||||
= [ True, False, False ]
|
||||
|
||||
./map Natural Bool Natural/even ([] : List Natural)
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Returns `True` if the `List` is empty and `False` otherwise
|
|||
Examples:
|
||||
|
||||
```
|
||||
./null Integer [ 0, 1, 2 ] = False
|
||||
./null Natural [ 0, 1, 2 ] = False
|
||||
|
||||
./null Integer ([] : List Integer) = True
|
||||
./null Natural ([] : List Natural) = True
|
||||
```
|
||||
-}
|
||||
let null
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ 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 ]
|
||||
./replicate 9 Natural 1 = [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
|
||||
|
||||
./replicate +0 Integer 1 = [] : List Integer
|
||||
./replicate 0 Natural 1 = [] : List Natural
|
||||
```
|
||||
-}
|
||||
let replicate
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Reverse a list
|
|||
Examples:
|
||||
|
||||
```
|
||||
./reverse Integer [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Integer
|
||||
./reverse Natural [ 0, 1, 2 ] = [ 2, 1, 0 ] : List Natural
|
||||
|
||||
./reverse Integer ([] : List Integer) = [] : List Integer
|
||||
./reverse Natural ([] : List Natural) = [] : List Natural
|
||||
```
|
||||
-}
|
||||
let reverse : ∀(a : Type) → List a → List a = List/reverse in reverse
|
||||
|
|
|
|||
|
|
@ -7,28 +7,28 @@ Examples:
|
|||
```
|
||||
./shifted
|
||||
Bool
|
||||
[ [ { index = +0, value = True }
|
||||
, { index = +1, value = True }
|
||||
, { index = +2, value = True }
|
||||
[ [ { index = 0, value = True }
|
||||
, { index = 1, value = True }
|
||||
, { index = 2, value = True }
|
||||
]
|
||||
, [ { index = +0, value = False }
|
||||
, { index = +1, value = False }
|
||||
, [ { index = 0, value = False }
|
||||
, { index = 1, value = False }
|
||||
]
|
||||
, [ { index = +0, value = True }
|
||||
, { index = +1, value = True }
|
||||
, { index = +2, value = True }
|
||||
, { index = +3, value = True }
|
||||
, [ { index = 0, value = True }
|
||||
, { index = 1, value = True }
|
||||
, { index = 2, value = True }
|
||||
, { index = 3, value = True }
|
||||
]
|
||||
]
|
||||
= [ { index = +0, value = True }
|
||||
, { index = +1, value = True }
|
||||
, { index = +2, value = True }
|
||||
, { index = +3, value = False }
|
||||
, { index = +4, value = False }
|
||||
, { index = +5, value = True }
|
||||
, { index = +6, value = True }
|
||||
, { index = +7, value = True }
|
||||
, { index = +8, value = True }
|
||||
= [ { 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 }
|
||||
]
|
||||
|
||||
./shifted Bool ([] : List (List { index : Natural, value : Bool }))
|
||||
|
|
@ -79,9 +79,9 @@ Bool
|
|||
(y.diff (n + length))
|
||||
}
|
||||
)
|
||||
{ count = +0, diff = λ(_ : Natural) → nil }
|
||||
{ count = 0, diff = λ(_ : Natural) → nil }
|
||||
|
||||
in result.diff +0
|
||||
in result.diff 0
|
||||
)
|
||||
|
||||
in shifted
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Examples:
|
|||
→ λ(zero : natural)
|
||||
→ succ (succ (succ zero))
|
||||
)
|
||||
= +3
|
||||
= 3
|
||||
|
||||
./build
|
||||
( λ(natural : Type)
|
||||
|
|
@ -18,7 +18,7 @@ Examples:
|
|||
→ λ(zero : natural)
|
||||
→ zero
|
||||
)
|
||||
= +0
|
||||
= 0
|
||||
```
|
||||
-}
|
||||
let build
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
{-
|
||||
Generate a list of numbers from `+0` up to but not including the specified
|
||||
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 ]
|
||||
./enumerate 10 = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]
|
||||
|
||||
./enumerate +0 = [] : List Natural
|
||||
./enumerate 0 = [] : List Natural
|
||||
```
|
||||
-}
|
||||
let enumerate
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Returns `True` if a number if even and returns `False` otherwise
|
|||
Examples:
|
||||
|
||||
```
|
||||
./even +3 = False
|
||||
./even 3 = False
|
||||
|
||||
./even +0 = True
|
||||
./even 0 = True
|
||||
```
|
||||
-}
|
||||
let even : Natural → Bool = Natural/even in even
|
||||
|
|
|
|||
|
|
@ -1,21 +1,21 @@
|
|||
{-
|
||||
`fold` is the primitive function for consuming `Natural` numbers
|
||||
|
||||
If you treat the number `+3` as `succ (succ (succ zero))` then a `fold` just
|
||||
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
|
||||
./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
|
||||
λ(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
|
||||
→ ./fold 3 natural succ zero
|
||||
= λ(natural : Type)
|
||||
→ λ(succ : natural → natural)
|
||||
→ λ(zero : natural)
|
||||
|
|
|
|||
|
|
@ -1,12 +1,12 @@
|
|||
{-
|
||||
Returns `True` if a number is `+0` and returns `False` otherwise
|
||||
Returns `True` if a number is `0` and returns `False` otherwise
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./isZero +2 = False
|
||||
./isZero 2 = False
|
||||
|
||||
./isZero +0 = True
|
||||
./isZero 0 = True
|
||||
```
|
||||
-}
|
||||
let isZero : Natural → Bool = Natural/isZero in isZero
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Returns `True` if a number is odd and returns `False` otherwise
|
|||
Examples:
|
||||
|
||||
```
|
||||
./odd +3 = True
|
||||
./odd 3 = True
|
||||
|
||||
./odd +0 = False
|
||||
./odd 0 = False
|
||||
```
|
||||
-}
|
||||
let odd : Natural → Bool = Natural/odd in odd
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Multiply all the numbers in a `List`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./product [ +2, +3, +5 ] = +30
|
||||
./product [ 2, 3, 5 ] = 30
|
||||
|
||||
./product ([] : List Natural) = +1
|
||||
./product ([] : List Natural) = 1
|
||||
```
|
||||
-}
|
||||
let product
|
||||
|
|
@ -17,6 +17,6 @@ Examples:
|
|||
xs
|
||||
Natural
|
||||
(λ(l : Natural) → λ(r : Natural) → l * r)
|
||||
+1
|
||||
1
|
||||
|
||||
in product
|
||||
|
|
|
|||
|
|
@ -1,13 +1,13 @@
|
|||
{-
|
||||
Render a `Natural` number as `Text` using the same representation as Dhall
|
||||
source code (i.e. a decimal number with a leading `+` sign)
|
||||
source code (i.e. a decimal number)
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./show +3 = "+3"
|
||||
./show 3 = "3"
|
||||
|
||||
./show +0 = "+0"
|
||||
./show 0 = "0"
|
||||
```
|
||||
-}
|
||||
let show : Natural → Text = Natural/show in show
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Add all the numbers in a `List`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./sum [ +2, +3, +5 ] = +10
|
||||
./sum [ 2, 3, 5 ] = 10
|
||||
|
||||
./sum ([] : List Natural) = +0
|
||||
./sum ([] : List Natural) = 0
|
||||
```
|
||||
-}
|
||||
let sum
|
||||
|
|
@ -17,6 +17,6 @@ Examples:
|
|||
xs
|
||||
Natural
|
||||
(λ(l : Natural) → λ(r : Natural) → l + r)
|
||||
+0
|
||||
0
|
||||
|
||||
in sum
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Convert a `Natural` number to the corresponding `Integer`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./toInteger +3 = 3
|
||||
./toInteger 3 = +3
|
||||
|
||||
./toInteger +0 = 0
|
||||
./toInteger 0 = +0
|
||||
```
|
||||
-}
|
||||
let toInteger : Natural → Integer = Natural/toInteger in toInteger
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ and `True` otherwise:
|
|||
Examples:
|
||||
|
||||
```
|
||||
./all Natural Natural/even ([ +3 ] : Optional Natural) = False
|
||||
./all Natural Natural/even ([ 3 ] : Optional Natural) = False
|
||||
|
||||
./all Natural Natural/even ([] : Optional Natural) = True
|
||||
```
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Returns `True` if the supplied function returns `True` for a present element and
|
|||
Examples:
|
||||
|
||||
```
|
||||
./any Natural Natural/even ([ +2 ] : Optional Natural) = True
|
||||
./any Natural Natural/even ([ 2 ] : Optional Natural) = True
|
||||
|
||||
./any Natural Natural/even ([] : Optional Natural) = False
|
||||
```
|
||||
|
|
|
|||
|
|
@ -5,22 +5,22 @@ Examples:
|
|||
|
||||
```
|
||||
./build
|
||||
Integer
|
||||
Natural
|
||||
( λ(optional : Type)
|
||||
→ λ(just : Integer → optional)
|
||||
→ λ(just : Natural → optional)
|
||||
→ λ(nothing : optional)
|
||||
→ just 1
|
||||
)
|
||||
= [ 1 ] : Optional Integer
|
||||
= [ 1 ] : Optional Natural
|
||||
|
||||
./build
|
||||
Integer
|
||||
Natural
|
||||
( λ(optional : Type)
|
||||
→ λ(just : Integer → optional)
|
||||
→ λ(just : Natural → optional)
|
||||
→ λ(nothing : optional)
|
||||
→ nothing
|
||||
)
|
||||
= [] : Optional Integer
|
||||
= [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let build
|
||||
|
|
|
|||
|
|
@ -4,14 +4,14 @@ Flatten two `Optional` layers into a single `Optional` layer
|
|||
Examples:
|
||||
|
||||
```
|
||||
./concat Integer ([ [ 1 ] : Optional Integer ] : Optional (Optional Integer))
|
||||
= [ 1 ] : Optional Integer
|
||||
./concat Natural ([ [ 1 ] : Optional Natural ] : Optional (Optional Natural))
|
||||
= [ 1 ] : Optional Natural
|
||||
|
||||
./concat Integer ([ [] : Optional Integer ] : Optional (Optional Integer))
|
||||
= [] : Optional Integer
|
||||
./concat Natural ([ [] : Optional Natural ] : Optional (Optional Natural))
|
||||
= [] : Optional Natural
|
||||
|
||||
./concat Integer ([] : Optional (Optional Integer))
|
||||
= [] : Optional Integer
|
||||
./concat Natural ([] : Optional (Optional Natural))
|
||||
= [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let concat
|
||||
|
|
|
|||
|
|
@ -4,10 +4,10 @@ Only keep an `Optional` element if the supplied function returns `True`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./filter Natural Natural/even ([ +2 ] : Optional Natural)
|
||||
= [ +2 ] : Optional Natural
|
||||
./filter Natural Natural/even ([ 2 ] : Optional Natural)
|
||||
= [ 2 ] : Optional Natural
|
||||
|
||||
./filter Natural Natural/odd ([ +2 ] : Optional Natural)
|
||||
./filter Natural Natural/odd ([ 2 ] : Optional Natural)
|
||||
= [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@
|
|||
Examples:
|
||||
|
||||
```
|
||||
./fold Integer ([ 2 ] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 2
|
||||
./fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 2
|
||||
|
||||
./fold Integer ([] : Optional Integer) Integer (λ(x : Integer) → x) 0 = 0
|
||||
./fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 0
|
||||
```
|
||||
-}
|
||||
let fold
|
||||
|
|
|
|||
|
|
@ -5,20 +5,20 @@ Examples:
|
|||
|
||||
```
|
||||
./head
|
||||
Integer
|
||||
[ [ ] : Optional Integer
|
||||
, [ 1 ] : Optional Integer
|
||||
, [ 2 ] : Optional Integer
|
||||
Natural
|
||||
[ [ ] : Optional Natural
|
||||
, [ 1 ] : Optional Natural
|
||||
, [ 2 ] : Optional Natural
|
||||
]
|
||||
= [ 1 ] : Optional Integer
|
||||
= [ 1 ] : Optional Natural
|
||||
|
||||
./head
|
||||
Integer
|
||||
[ [] : Optional Integer, [] : Optional Integer ]
|
||||
= [] : Optional Integer
|
||||
Natural
|
||||
[ [] : Optional Natural, [] : Optional Natural ]
|
||||
= [] : Optional Natural
|
||||
|
||||
./head Integer ([] : List (Optional Integer))
|
||||
= [] : Optional Integer
|
||||
./head Natural ([] : List (Optional Natural))
|
||||
= [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let head
|
||||
|
|
|
|||
|
|
@ -5,20 +5,20 @@ Examples:
|
|||
|
||||
```
|
||||
./last
|
||||
Integer
|
||||
[ [ ] : Optional Integer
|
||||
, [ 1 ] : Optional Integer
|
||||
, [ 2 ] : Optional Integer
|
||||
Natural
|
||||
[ [ ] : Optional Natural
|
||||
, [ 1 ] : Optional Natural
|
||||
, [ 2 ] : Optional Natural
|
||||
]
|
||||
= [ 2 ] : Optional Integer
|
||||
= [ 2 ] : Optional Natural
|
||||
|
||||
./last
|
||||
Integer
|
||||
[ [] : Optional Integer, [] : Optional Integer ]
|
||||
= [] : Optional Integer
|
||||
Natural
|
||||
[ [] : Optional Natural, [] : Optional Natural ]
|
||||
= [] : Optional Natural
|
||||
|
||||
./last Integer ([] : List (Optional Integer))
|
||||
= [] : Optional Integer
|
||||
./last Natural ([] : List (Optional Natural))
|
||||
= [] : Optional Natural
|
||||
```
|
||||
-}
|
||||
let last
|
||||
|
|
|
|||
|
|
@ -1,18 +1,18 @@
|
|||
{-
|
||||
Returns `+1` if the `Optional` value is present and `+0` if the value is absent
|
||||
Returns `1` if the `Optional` value is present and `0` if the value is absent
|
||||
|
||||
Examples:
|
||||
|
||||
```
|
||||
./length Integer ([ 2 ] : Optional Integer) = +1
|
||||
./length Natural ([ 2 ] : Optional Natural) = 1
|
||||
|
||||
./length Integer ([] : Optional Integer) = +0
|
||||
./length Natural ([] : Optional Natural) = 0
|
||||
```
|
||||
-}
|
||||
let length
|
||||
: ∀(a : Type) → Optional a → Natural
|
||||
= λ(a : Type)
|
||||
→ λ(xs : Optional a)
|
||||
→ Optional/fold a xs Natural (λ(_ : a) → +1) +0
|
||||
→ Optional/fold a xs Natural (λ(_ : a) → 1) 0
|
||||
|
||||
in length
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Transform an `Optional` value with a function
|
|||
Examples:
|
||||
|
||||
```
|
||||
./map Natural Bool Natural/even ([ +3 ] : Optional Natural)
|
||||
./map Natural Bool Natural/even ([ 3 ] : Optional Natural)
|
||||
= [ False ] : Optional Bool
|
||||
|
||||
./map Natural Bool Natural/even ([] : Optional Natural)
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Returns `True` if the `Optional` value is absent and `False` if present
|
|||
Examples:
|
||||
|
||||
```
|
||||
./null Integer ([ 2 ] : Optional Integer) = False
|
||||
./null Natural ([ 2 ] : Optional Natural) = False
|
||||
|
||||
./null Integer ([] : Optional Integer) = True
|
||||
./null Natural ([] : Optional Natural) = True
|
||||
```
|
||||
-}
|
||||
let null
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ Convert an `Optional` value into the equivalent `List`
|
|||
Examples:
|
||||
|
||||
```
|
||||
./toList Integer ([ 1 ] : Optional Integer) = [ 1 ]
|
||||
./toList Natural ([ 1 ] : Optional Natural) = [ 1 ]
|
||||
|
||||
./toList Integer ([] : Optional Integer) = [] : List Integer
|
||||
./toList Natural ([] : Optional Natural) = [] : List Natural
|
||||
```
|
||||
-}
|
||||
let toList
|
||||
|
|
|
|||
|
|
@ -4,10 +4,10 @@ Transform each value in a `List` into `Text` and concatenate the result
|
|||
Examples:
|
||||
|
||||
```
|
||||
./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") [ 0, 1, 2 ]
|
||||
./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ]
|
||||
= "0 1 2 "
|
||||
|
||||
./concatMap Integer (λ(n : Integer) → "${Integer/show n} ") ([] : List Integer)
|
||||
./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural)
|
||||
= ""
|
||||
```
|
||||
-}
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@ separator in between each value
|
|||
Examples:
|
||||
|
||||
```
|
||||
./concatMapSep ", " Integer Integer/show [ 0, 1, 2 ] = "0, 1, 2"
|
||||
./concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] = "0, 1, 2"
|
||||
|
||||
./concatMapSep ", " Integer Integer/show ([] : List Integer) = ""
|
||||
./concatMapSep ", " Natural Natural/show ([] : List Natural) = ""
|
||||
```
|
||||
-}
|
||||
let concatMapSep
|
||||
|
|
|
|||
11
dhall.cabal
11
dhall.cabal
|
|
@ -258,7 +258,7 @@ Executable dhall-hash
|
|||
Other-Modules:
|
||||
Paths_dhall
|
||||
|
||||
Test-Suite test
|
||||
Test-Suite tasty
|
||||
Type: exitcode-stdio-1.0
|
||||
Hs-Source-Dirs: tests
|
||||
Main-Is: Tests.hs
|
||||
|
|
@ -281,3 +281,12 @@ Test-Suite test
|
|||
tasty-hunit >= 0.9.2 && < 0.11,
|
||||
text >= 0.11.1.0 && < 1.3 ,
|
||||
vector >= 0.11.0.0 && < 0.13
|
||||
|
||||
Test-Suite doctest
|
||||
Type: exitcode-stdio-1.0
|
||||
Hs-Source-Dirs: doctest
|
||||
Main-Is: Main.hs
|
||||
GHC-Options: -Wall
|
||||
Build-Depends:
|
||||
base ,
|
||||
doctest >= 0.7.0 && < 0.16
|
||||
|
|
|
|||
6
doctest/Main.hs
Normal file
6
doctest/Main.hs
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
module Main where
|
||||
|
||||
import qualified Test.DocTest
|
||||
|
||||
main :: IO ()
|
||||
main = Test.DocTest.doctest [ "-isrc", "src/Dhall.hs" ]
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
{ mkDerivation, ansi-terminal, base, bytestring, case-insensitive
|
||||
, containers, contravariant, cryptonite, deepseq, directory
|
||||
, exceptions, filepath, formatting, haskeline, http-client
|
||||
, doctest, exceptions, filepath, formatting, haskeline, http-client
|
||||
, http-client-tls, insert-ordered-containers, lens-family-core
|
||||
, megaparsec, memory, mtl, optparse-applicative, parsers
|
||||
, prettyprinter, prettyprinter-ansi-terminal, repline, scientific
|
||||
|
|
@ -26,7 +26,7 @@ mkDerivation {
|
|||
prettyprinter prettyprinter-ansi-terminal repline text
|
||||
];
|
||||
testHaskellDepends = [
|
||||
base deepseq insert-ordered-containers prettyprinter tasty
|
||||
base deepseq doctest insert-ordered-containers prettyprinter tasty
|
||||
tasty-hunit text vector
|
||||
];
|
||||
description = "A configuration language guaranteed to terminate";
|
||||
|
|
|
|||
39
src/Dhall.hs
39
src/Dhall.hs
|
|
@ -104,6 +104,9 @@ import qualified Dhall.Import
|
|||
import qualified Dhall.Parser
|
||||
import qualified Dhall.TypeCheck
|
||||
|
||||
-- $setup
|
||||
-- >>> :set -XOverloadedStrings
|
||||
|
||||
throws :: Exception e => Either e a -> IO a
|
||||
throws (Left e) = Control.Exception.throwIO e
|
||||
throws (Right r) = return r
|
||||
|
|
@ -133,7 +136,7 @@ instance Exception InvalidType
|
|||
|
||||
The first argument determines the type of value that you decode:
|
||||
|
||||
>>> input integer "2"
|
||||
>>> input integer "+2"
|
||||
2
|
||||
>>> input (vector double) "[1.0, 2.0]"
|
||||
[1.0,2.0]
|
||||
|
|
@ -235,13 +238,13 @@ rawInput (Type {..}) expr = do
|
|||
>
|
||||
>
|
||||
> ┌─────────────┐
|
||||
> │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type
|
||||
> │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type
|
||||
> └─────────────┘ checker accepts the annotation
|
||||
>
|
||||
>
|
||||
> ┌────────────────────────┐
|
||||
> │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type
|
||||
> └────────────────────────┘ checker accepts the annotation
|
||||
> ┌───────────────────────┐
|
||||
> │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type
|
||||
> └───────────────────────┘ checker accepts the annotation
|
||||
>
|
||||
>
|
||||
> ┌────────────────────┐
|
||||
|
|
@ -362,7 +365,7 @@ bool = Type {..}
|
|||
|
||||
{-| Decode a `Natural`
|
||||
|
||||
>>> input natural "+42"
|
||||
>>> input natural "42"
|
||||
42
|
||||
-}
|
||||
natural :: Type Natural
|
||||
|
|
@ -375,7 +378,7 @@ natural = Type {..}
|
|||
|
||||
{-| Decode an `Integer`
|
||||
|
||||
>>> input integer "42"
|
||||
>>> input integer "+42"
|
||||
42
|
||||
-}
|
||||
integer :: Type Integer
|
||||
|
|
@ -430,7 +433,7 @@ strictText = fmap Data.Text.Lazy.toStrict lazyText
|
|||
|
||||
{-| Decode a `Maybe`
|
||||
|
||||
>>> input (maybe integer) "[1] : Optional Integer"
|
||||
>>> input (maybe natural) "[1] : Optional Natural"
|
||||
Just 1
|
||||
-}
|
||||
maybe :: Type a -> Type (Maybe a)
|
||||
|
|
@ -443,8 +446,8 @@ maybe (Type extractIn expectedIn) = Type extractOut expectedOut
|
|||
|
||||
{-| Decode a `Seq`
|
||||
-
|
||||
>>> input (sequence integer) "[1, 2, 3]"
|
||||
[1,2,3]
|
||||
>>> input (sequence natural) "[1, 2, 3]"
|
||||
fromList [1,2,3]
|
||||
-}
|
||||
sequence :: Type a -> Type (Seq a)
|
||||
sequence (Type extractIn expectedIn) = Type extractOut expectedOut
|
||||
|
|
@ -456,7 +459,7 @@ sequence (Type extractIn expectedIn) = Type extractOut expectedOut
|
|||
|
||||
{-| Decode a list
|
||||
|
||||
>>> input (list integer) "[1, 2, 3]"
|
||||
>>> input (list natural) "[1, 2, 3]"
|
||||
[1,2,3]
|
||||
-}
|
||||
list :: Type a -> Type [a]
|
||||
|
|
@ -464,7 +467,7 @@ list = fmap Data.Foldable.toList . sequence
|
|||
|
||||
{-| Decode a `Vector`
|
||||
|
||||
>>> input (vector integer) "[1, 2, 3]"
|
||||
>>> input (vector natural) "[1, 2, 3]"
|
||||
[1,2,3]
|
||||
-}
|
||||
vector :: Type a -> Type (Vector a)
|
||||
|
|
@ -472,8 +475,8 @@ vector = fmap Data.Vector.fromList . list
|
|||
|
||||
{-| Decode `()` from an empty record.
|
||||
|
||||
>>> input unit "{=}"
|
||||
()
|
||||
>>> input unit "{=}" -- GHC doesn't print the result if it is @()@
|
||||
|
||||
-}
|
||||
unit :: Type ()
|
||||
unit = Type extractOut expectedOut
|
||||
|
|
@ -495,8 +498,8 @@ string = Data.Text.Lazy.unpack <$> lazyText
|
|||
|
||||
{-| Given a pair of `Type`s, decode a tuple-record into their pairing.
|
||||
|
||||
>>> input (pair natural bool) "{ _1 = +42, _2 = False }"
|
||||
(42, False)
|
||||
>>> input (pair natural bool) "{ _1 = 42, _2 = False }"
|
||||
(42,False)
|
||||
-}
|
||||
pair :: Type a -> Type b -> Type (a, b)
|
||||
pair l r = Type extractOut expectedOut
|
||||
|
|
@ -517,7 +520,7 @@ pair l r = Type extractOut expectedOut
|
|||
{-| Any value that implements `Interpret` can be automatically decoded based on
|
||||
the inferred return type of `input`
|
||||
|
||||
>>> input auto "[1, 2, 3]" :: IO (Vector Integer)
|
||||
>>> input auto "[1, 2, 3]" :: IO (Vector Natural)
|
||||
[1,2,3]
|
||||
|
||||
This class auto-generates a default implementation for records that
|
||||
|
|
@ -1077,7 +1080,7 @@ instance (Selector s, Inject a) => GenericInject (M1 S s (K1 i a)) where
|
|||
> , description =
|
||||
> "A configuration language guaranteed to terminate"
|
||||
> , stars =
|
||||
> +289
|
||||
> 289
|
||||
> }
|
||||
|
||||
Our parser has type 'Type' @Project@, but we can't build that out of any
|
||||
|
|
|
|||
|
|
@ -247,7 +247,7 @@ data Expr s a
|
|||
| BoolIf (Expr s a) (Expr s a) (Expr s a)
|
||||
-- | > Natural ~ Natural
|
||||
| Natural
|
||||
-- | > NaturalLit n ~ +n
|
||||
-- | > NaturalLit n ~ n
|
||||
| NaturalLit Natural
|
||||
-- | > NaturalFold ~ Natural/fold
|
||||
| NaturalFold
|
||||
|
|
@ -269,7 +269,7 @@ data Expr s a
|
|||
| NaturalTimes (Expr s a) (Expr s a)
|
||||
-- | > Integer ~ Integer
|
||||
| Integer
|
||||
-- | > IntegerLit n ~ n
|
||||
-- | > IntegerLit n ~ ±n
|
||||
| IntegerLit Integer
|
||||
-- | > IntegerShow ~ Integer/show
|
||||
| IntegerShow
|
||||
|
|
@ -1310,9 +1310,10 @@ normalizeWith ctx e0 = loop (denote e0)
|
|||
App NaturalOdd (NaturalLit n) -> BoolLit (odd n)
|
||||
App NaturalToInteger (NaturalLit n) -> IntegerLit (toInteger n)
|
||||
App NaturalShow (NaturalLit n) ->
|
||||
TextLit (Chunks [] ("+" <> buildNatural n))
|
||||
App IntegerShow (IntegerLit n) ->
|
||||
TextLit (Chunks [] (buildNumber n))
|
||||
TextLit (Chunks [] (buildNatural n))
|
||||
App IntegerShow (IntegerLit n)
|
||||
| 0 <= n -> TextLit (Chunks [] ("+" <> buildNumber n))
|
||||
| otherwise -> TextLit (Chunks [] (buildNumber n))
|
||||
App DoubleShow (DoubleLit n) ->
|
||||
TextLit (Chunks [] (buildScientific n))
|
||||
App (App OptionalBuild _A₀) g ->
|
||||
|
|
|
|||
|
|
@ -748,11 +748,15 @@ doubleLiteral = (do
|
|||
return (sign a) ) <?> "double literal"
|
||||
|
||||
integerLiteral :: Parser Integer
|
||||
integerLiteral = Text.Parser.Token.integer <?> "integer literal"
|
||||
integerLiteral = (do
|
||||
let positive = fmap (\_ -> id ) (Text.Parser.Char.char '+')
|
||||
let negative = fmap (\_ -> negate) (Text.Parser.Char.char '-')
|
||||
sign <- positive <|> negative
|
||||
a <- Text.Parser.Token.natural
|
||||
return (sign a) ) <?> "integer literal"
|
||||
|
||||
naturalLiteral :: Parser Natural
|
||||
naturalLiteral = (do
|
||||
_ <- Text.Parser.Char.char '+'
|
||||
a <- Text.Parser.Token.natural
|
||||
return (fromIntegral a) ) <?> "natural literal"
|
||||
|
||||
|
|
|
|||
|
|
@ -736,10 +736,11 @@ prettyExprF (BoolLit True) =
|
|||
builtin "True"
|
||||
prettyExprF (BoolLit False) =
|
||||
builtin "False"
|
||||
prettyExprF (IntegerLit a) =
|
||||
prettyNumber a
|
||||
prettyExprF (IntegerLit a)
|
||||
| 0 <= a = literal "+" <> prettyNumber a
|
||||
| otherwise = prettyNumber a
|
||||
prettyExprF (NaturalLit a) =
|
||||
literal "+" <> prettyNatural a
|
||||
prettyNatural a
|
||||
prettyExprF (DoubleLit a) =
|
||||
prettyScientific a
|
||||
prettyExprF (TextLit a) =
|
||||
|
|
@ -1094,10 +1095,11 @@ buildExprF (BoolLit True) =
|
|||
"True"
|
||||
buildExprF (BoolLit False) =
|
||||
"False"
|
||||
buildExprF (IntegerLit a) =
|
||||
buildNumber a
|
||||
buildExprF (IntegerLit a)
|
||||
| 0 <= a = "+" <> buildNumber a
|
||||
| otherwise = buildNumber a
|
||||
buildExprF (NaturalLit a) =
|
||||
"+" <> buildNatural a
|
||||
buildNatural a
|
||||
buildExprF (DoubleLit a) =
|
||||
buildScientific a
|
||||
buildExprF (TextLit a) =
|
||||
|
|
|
|||
|
|
@ -189,7 +189,7 @@ import Dhall
|
|||
-- >
|
||||
-- > import Dhall
|
||||
-- >
|
||||
-- > data Example = Example { foo :: Integer, bar :: Vector Double }
|
||||
-- > data Example = Example { foo :: Natural, bar :: Vector Double }
|
||||
-- > deriving (Generic, Show)
|
||||
-- >
|
||||
-- > instance Interpret Example
|
||||
|
|
@ -275,7 +275,7 @@ import Dhall
|
|||
-- >
|
||||
-- > import Dhall
|
||||
-- >
|
||||
-- > data Person = Person { age :: Integer, name :: Text }
|
||||
-- > data Person = Person { age :: Natural, name :: Text }
|
||||
-- > deriving (Generic, Show)
|
||||
-- >
|
||||
-- > instance Interpret Person
|
||||
|
|
@ -304,15 +304,24 @@ import Dhall
|
|||
-- Suppose that we try to decode a value of the wrong type, like this:
|
||||
--
|
||||
-- > >>> input auto "1" :: IO Bool
|
||||
-- > *** Exception:
|
||||
-- > *** Exception:
|
||||
-- > Error: Expression doesn't match annotation
|
||||
-- >
|
||||
-- > - Bool
|
||||
-- > + Natural
|
||||
-- >
|
||||
-- > 1 : Bool
|
||||
-- >
|
||||
-- > (input):1:1
|
||||
--
|
||||
-- The interpreter complains because the string @\"1\"@ cannot be decoded into a
|
||||
-- Haskell value of type `Bool`.
|
||||
-- Haskell value of type `Bool`. This part of the type error:
|
||||
--
|
||||
-- > - Bool
|
||||
-- > + Natural
|
||||
--
|
||||
-- ... means that the expected type was @Bool@ but the inferred type of the
|
||||
-- expression @1@ was @Natural@.
|
||||
--
|
||||
-- The code excerpt from the above error message has two components:
|
||||
--
|
||||
|
|
@ -406,7 +415,7 @@ import Dhall
|
|||
--
|
||||
-- ... then the interpreter will reject the import:
|
||||
--
|
||||
-- > >>> input auto "./file1" :: IO Integer
|
||||
-- > >>> input auto "./file1" :: IO Natural
|
||||
-- > *** Exception:
|
||||
-- > ↳ ./file1
|
||||
-- > ↳ ./file2
|
||||
|
|
@ -438,7 +447,7 @@ import Dhall
|
|||
-- You can also import Dhall expressions from environment variables, too:
|
||||
--
|
||||
-- > >>> System.Environment.setEnv "FOO" "1"
|
||||
-- > >>> input auto "env:FOO" :: IO Integer
|
||||
-- > >>> input auto "env:FOO" :: IO Natural
|
||||
-- > 1
|
||||
--
|
||||
-- You can import types, too. For example, we can change our @./bar@ file to:
|
||||
|
|
@ -494,31 +503,35 @@ import Dhall
|
|||
-- required for empty lists but optional for non-empty lists. You will get a
|
||||
-- type error if you provide an empty list without a type annotation:
|
||||
--
|
||||
-- > >>> input auto "[]" :: IO (Vector Integer)
|
||||
-- > *** Exception:
|
||||
-- > Error: Empty lists need a type annotation
|
||||
-- > >>> input auto "[]" :: IO (Vector Natural)
|
||||
-- > *** Exception:
|
||||
-- > Error: Invalid input
|
||||
-- >
|
||||
-- > []
|
||||
-- >
|
||||
-- > (input):1:1
|
||||
-- > >>> input auto "[] : List Integer" :: IO (Vector Integer)
|
||||
-- > []
|
||||
-- > (input):1:3:
|
||||
-- > |
|
||||
-- > 1 | []
|
||||
-- > | ^
|
||||
-- > unexpected end of input
|
||||
-- > expecting ':' or whitespace
|
||||
--
|
||||
-- Also, list elements must all have the same type. You will get an error if
|
||||
-- you try to store elements of different types in a list:
|
||||
--
|
||||
-- > >>> input auto "[1, True, 3]" :: IO (Vector Integer)
|
||||
-- > *** Exception:
|
||||
-- > Error: List elements should have the same type
|
||||
-- > >>> input auto "[1, True, 3]" :: IO (Vector Natural)
|
||||
-- > *** Exception:
|
||||
-- > Error: List elements should all have the same type
|
||||
-- >
|
||||
-- > [1, True, 3]
|
||||
-- > - Natural
|
||||
-- > + Bool
|
||||
-- >
|
||||
-- > (input):1:1
|
||||
-- > True
|
||||
-- >
|
||||
-- > (input):1:5
|
||||
--
|
||||
-- __Exercise:__ What is the shortest @./config@ file that you can decode using
|
||||
-- this command:
|
||||
--
|
||||
-- > >>> input auto "./config" :: IO (Vector (Vector Integer))
|
||||
-- > >>> input auto "./config" :: IO (Vector (Vector Natural))
|
||||
|
||||
-- $optional0
|
||||
--
|
||||
|
|
@ -527,19 +540,19 @@ import Dhall
|
|||
--
|
||||
-- For example, these are valid @Optional@ values:
|
||||
--
|
||||
-- > [1] : Optional Integer
|
||||
-- > [1] : Optional Natural
|
||||
-- >
|
||||
-- > [] : Optional Integer
|
||||
-- > [] : Optional Natural
|
||||
--
|
||||
-- ... but this is /not/ valid:
|
||||
--
|
||||
-- > [1, 2] : Optional Integer -- NOT valid
|
||||
-- > [1, 2] : Optional Natural -- NOT valid
|
||||
--
|
||||
-- An @Optional@ corresponds to Haskell's `Maybe` type for decoding purposes:
|
||||
--
|
||||
-- > >>> input auto "[1] : Optional Integer" :: IO (Maybe Integer)
|
||||
-- > >>> input auto "[1] : Optional Natural" :: IO (Maybe Natural)
|
||||
-- > Just 1
|
||||
-- > >>> input auto "[] : Optional Integer" :: IO (Maybe Integer)
|
||||
-- > >>> input auto "[] : Optional Natural" :: IO (Maybe Natural)
|
||||
-- > Nothing
|
||||
--
|
||||
-- You cannot omit the type annotation for @Optional@ values. The type
|
||||
|
|
@ -548,7 +561,7 @@ import Dhall
|
|||
-- __Exercise:__ What is the shortest possible @./config@ file that you can decode
|
||||
-- like this:
|
||||
--
|
||||
-- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Integer)))
|
||||
-- > >>> input auto "./config" :: IO (Maybe (Maybe (Maybe Natural)))
|
||||
-- > ???
|
||||
--
|
||||
-- __Exercise:__ Try to decode an @Optional@ value with more than one element and
|
||||
|
|
@ -569,7 +582,7 @@ import Dhall
|
|||
-- record literal has the following record type:
|
||||
--
|
||||
-- > { foo : Bool
|
||||
-- > , bar : Integer
|
||||
-- > , bar : Natural
|
||||
-- > , baz : Double
|
||||
-- > }
|
||||
--
|
||||
|
|
@ -612,7 +625,7 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > { x = 1, y = True, z = "ABC" }.{ x, y }
|
||||
-- > <Ctrl-D>
|
||||
-- > { x : Integer, y : Bool }
|
||||
-- > { x : Natural, y : Bool }
|
||||
-- >
|
||||
-- > { x = 1, y = True }
|
||||
--
|
||||
|
|
@ -714,7 +727,7 @@ import Dhall
|
|||
-- > <Ctrl-D>
|
||||
-- > ∀(n : Bool) → List Bool
|
||||
-- >
|
||||
-- > λ(n : Bool) → [n && True, n && False, n || True, n || False]
|
||||
-- > λ(n : Bool) → [ n, False, True, n ]
|
||||
--
|
||||
-- The first line says that @makeBools@ is a function of one argument named @n@
|
||||
-- that has type @Bool@ and the function returns a @List@ of @Bool@s. The @∀@
|
||||
|
|
@ -737,9 +750,14 @@ import Dhall
|
|||
--
|
||||
-- The second line of Dhall's output is our program's normal form:
|
||||
--
|
||||
-- > λ(n : Bool) → [n && True, n && False, n || True, n || False]
|
||||
-- > λ(n : Bool) → [ n, False, True, n ]
|
||||
--
|
||||
-- ... which in this case happens to be identical to our original program.
|
||||
-- ... and the interpreter was able to simplify our expression by noting that:
|
||||
--
|
||||
-- * @n && True = n@
|
||||
-- * @n && False = False@
|
||||
-- * @n || True = True@
|
||||
-- * @n || False = n@
|
||||
--
|
||||
-- To apply a function to an argument you separate the function and argument by
|
||||
-- whitespace (just like Haskell):
|
||||
|
|
@ -847,7 +865,7 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > let name = "John Doe"
|
||||
-- > in let age = 21
|
||||
-- > in "My name is ${name} and my age is ${Integer/show age}"
|
||||
-- > in "My name is ${name} and my age is ${Natural/show age}"
|
||||
-- > <Ctrl-D>
|
||||
-- > Text
|
||||
-- >
|
||||
|
|
@ -875,13 +893,13 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > { foo = 1, bar = "ABC" } // { baz = True }
|
||||
-- > <Ctrl-D>
|
||||
-- > { bar : Text, baz : Bool, foo : Integer }
|
||||
-- > { bar : Text, baz : Bool, foo : Natural }
|
||||
-- >
|
||||
-- > { bar = "ABC", baz = True, foo = 1 }
|
||||
-- > $ dhall
|
||||
-- > { foo = 1, bar = "ABC" } ⫽ { bar = True } -- Fancy unicode
|
||||
-- > <Ctrl-D>
|
||||
-- > { bar : Bool, foo : Integer }
|
||||
-- > { bar : Bool, foo : Natural }
|
||||
-- >
|
||||
-- > { bar = True, foo = 1 }
|
||||
--
|
||||
|
|
@ -926,9 +944,9 @@ import Dhall
|
|||
-- operator descends recursively into record types:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Integer }
|
||||
-- > { foo : { bar : Text } } ⩓ { foo : { baz : Bool }, qux : Natural }
|
||||
-- > <Ctrl-D>
|
||||
-- > { foo : { bar : Text, baz : Bool }, qux : Integer }
|
||||
-- > { foo : { bar : Text, baz : Bool }, qux : Natural }
|
||||
|
||||
-- $let
|
||||
--
|
||||
|
|
@ -983,10 +1001,14 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > let twice (x : Text) = x ++ x in twice "ha"
|
||||
-- > <Ctrl-D>
|
||||
-- > (stdin):1:11: error: expected: ":",
|
||||
-- > "="
|
||||
-- > let twice (x : Text) = x ++ x in twice "ha"
|
||||
-- > ^
|
||||
-- > Error: Invalid input
|
||||
-- >
|
||||
-- > (stdin):1:11:
|
||||
-- > |
|
||||
-- > 1 | let twice (x : Text) = x ++ x in twice "ha"
|
||||
-- > | ^
|
||||
-- > unexpected '('
|
||||
-- > expecting ':', '=', or the rest of label
|
||||
--
|
||||
-- The error message says that Dhall expected either a @(:)@ (i.e. the beginning
|
||||
-- of a type annotation) or a @(=)@ (the beginning of the assignment) and not a
|
||||
|
|
@ -1048,7 +1070,7 @@ import Dhall
|
|||
-- remaining alternatives. For example, both of the following union literals
|
||||
-- have the same type, which is the above union type:
|
||||
--
|
||||
-- > < Left = +0 | Right : Bool >
|
||||
-- > < Left = 0 | Right : Bool >
|
||||
--
|
||||
-- > < Right = True | Left : Natural >
|
||||
--
|
||||
|
|
@ -1070,7 +1092,7 @@ import Dhall
|
|||
-- Now our @./process@ function can handle both alternatives:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > ./process < Left = +3 | Right : Bool >
|
||||
-- > ./process < Left = 3 | Right : Bool >
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
-- >
|
||||
|
|
@ -1100,8 +1122,8 @@ import Dhall
|
|||
--
|
||||
-- So, for example:
|
||||
--
|
||||
-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = +3 | Right : Bool > : Bool
|
||||
-- > = Natural/even +3 : Bool
|
||||
-- > merge { Left = Natural/even, Right = λ(b : Bool) → b } < Left = 3 | Right : Bool > : Bool
|
||||
-- > = Natural/even 3 : Bool
|
||||
-- > = False
|
||||
--
|
||||
-- ... and similarly:
|
||||
|
|
@ -1135,8 +1157,8 @@ import Dhall
|
|||
-- > in let Person =
|
||||
-- > λ(p : { name : Text, age : Natural }) → < Person = p | Empty : {} >
|
||||
-- > in [ Empty
|
||||
-- > , Person { name = "John", age = +23 }
|
||||
-- > , Person { name = "Amy" , age = +25 }
|
||||
-- > , Person { name = "John", age = 23 }
|
||||
-- > , Person { name = "Amy" , age = 25 }
|
||||
-- > , Empty
|
||||
-- > ]
|
||||
--
|
||||
|
|
@ -1145,8 +1167,8 @@ import Dhall
|
|||
--
|
||||
-- > let MyType = constructors < Empty : {} | Person : { name : Text, age : Natural } >
|
||||
-- > in [ MyType.Empty {=}
|
||||
-- > , MyType.Person { name = "John", age = +23 }
|
||||
-- > , MyType.Person { name = "Amy" , age = +25 }
|
||||
-- > , MyType.Person { name = "John", age = 23 }
|
||||
-- > , MyType.Person { name = "Amy" , age = 25 }
|
||||
-- > ]
|
||||
--
|
||||
-- The @constructors@ keyword takes a union type argument and returns a record
|
||||
|
|
@ -1186,7 +1208,7 @@ import Dhall
|
|||
-- __Exercise__: Create a list of the following type with at least one element
|
||||
-- per alternative:
|
||||
--
|
||||
-- > List < Left : Integer | Right : Double >
|
||||
-- > List < Left : Natural | Right : Double >
|
||||
|
||||
-- $polymorphic
|
||||
--
|
||||
|
|
@ -1236,15 +1258,15 @@ import Dhall
|
|||
-- argument). The result also has type @a@.\"
|
||||
--
|
||||
-- This means that the type of the second argument changes depending on what
|
||||
-- type we provide for the first argument. When we apply @./id@ to @Integer@, we
|
||||
-- create a function that expects an @Integer@ argument:
|
||||
-- type we provide for the first argument. When we apply @./id@ to @Natural@,
|
||||
-- we create a function that expects an @Natural@ argument:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > ./id Integer
|
||||
-- > ./id Natural
|
||||
-- > <Ctrl-D>
|
||||
-- > ∀(x : Integer) → Integer
|
||||
-- > ∀(x : Natural) → Natural
|
||||
-- >
|
||||
-- > λ(x : Integer) → x
|
||||
-- > λ(x : Natural) → x
|
||||
--
|
||||
-- Similarly, when we apply @./id@ to @Bool@, we create a function that expects a
|
||||
-- @Bool@ argument:
|
||||
|
|
@ -1260,9 +1282,9 @@ import Dhall
|
|||
-- that they both work on their respective types:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > ./id Integer 4
|
||||
-- > ./id Natural 4
|
||||
-- > <Ctrl-D>
|
||||
-- > Integer
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > 4
|
||||
--
|
||||
|
|
@ -1317,11 +1339,11 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > λ(_ : Text) → 1
|
||||
-- > <Ctrl-D>
|
||||
-- > Text → Integer
|
||||
-- > Text → Natural
|
||||
-- >
|
||||
-- > λ(_ : Text) → 1
|
||||
--
|
||||
-- The type @(Text → Integer)@ is the same as @(∀(_ : Text) → Integer)@
|
||||
-- The type @(Text → Natural)@ is the same as @(∀(_ : Text) → Natural)@
|
||||
--
|
||||
-- __Exercise__ : Translate Haskell's `flip` function to Dhall
|
||||
|
||||
|
|
@ -1339,11 +1361,11 @@ import Dhall
|
|||
-- applied. For example, the following program is an anonymous function:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > \(n : Bool) -> +10 * +10
|
||||
-- > \(n : Bool) -> 10 * 10
|
||||
-- > <Ctrl-D>
|
||||
-- > ∀(n : Bool) → Natural
|
||||
-- >
|
||||
-- > λ(n : Bool) → +100
|
||||
-- > λ(n : Bool) → 100
|
||||
--
|
||||
-- ... and even though the function is still missing the first argument named
|
||||
-- @n@ the compiler is smart enough to evaluate the body of the anonymous
|
||||
|
|
@ -1354,11 +1376,11 @@ import Dhall
|
|||
--
|
||||
-- > $ dhall
|
||||
-- > let Prelude/List/map = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/map
|
||||
-- > in λ(f : Integer → Integer) → Prelude/List/map Integer Integer f [1, 2, 3]
|
||||
-- > in λ(f : Natural → Natural) → Prelude/List/map Natural Natural f [1, 2, 3]
|
||||
-- > <Ctrl-D>
|
||||
-- > ∀(f : Integer → Integer) → List Integer
|
||||
-- > ∀(f : Natural → Natural) → List Natural
|
||||
-- >
|
||||
-- > λ(f : Integer → Integer) → [f 1, f 2, f 3] : List Integer
|
||||
-- > λ(f : Natural → Natural) → [f 1, f 2, f 3] : List Natural
|
||||
--
|
||||
-- Dhall can apply our function to each element of the list even before we specify
|
||||
-- which function to apply.
|
||||
|
|
@ -1368,11 +1390,11 @@ import Dhall
|
|||
-- an @Optional@ value:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > List/head Integer ([] : List Integer)
|
||||
-- > List/head Natural ([] : List Natural)
|
||||
-- > <Ctrl-D>
|
||||
-- > Optional Integer
|
||||
-- > Optional Natural
|
||||
-- >
|
||||
-- > [] : Optional Integer
|
||||
-- > [] : Optional Natural
|
||||
--
|
||||
-- __Exercise__: The Dhall Prelude provides a @replicate@ function which you can
|
||||
-- find here:
|
||||
|
|
@ -1382,7 +1404,7 @@ import Dhall
|
|||
-- Test what the following Dhall expression normalizes to:
|
||||
--
|
||||
-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate
|
||||
-- > in replicate +10
|
||||
-- > in replicate 10
|
||||
--
|
||||
-- __Exercise__: If you have a lot of spare time, try to \"break the compiler\" by
|
||||
-- finding an input expression that crashes or loops forever (and file a bug
|
||||
|
|
@ -1461,7 +1483,7 @@ import Dhall
|
|||
-- imported Dhall value and reject the import if there is a hash mismatch:
|
||||
--
|
||||
-- > $ dhall <<< './foo'
|
||||
-- > Integer
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > 1
|
||||
--
|
||||
|
|
@ -1477,7 +1499,7 @@ import Dhall
|
|||
-- changes to whitespace or comments:
|
||||
--
|
||||
-- > $ dhall <<< './foo' # This still succeeds
|
||||
-- > Integer
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > 1
|
||||
--
|
||||
|
|
@ -1592,7 +1614,7 @@ import Dhall
|
|||
-- > index : Natural, value : a } kvs list (λ(kvOld : { index : Natural, value : a
|
||||
-- > }) → λ(z : list) → cons { index = kvOld.index + n, value = kvOld.value }
|
||||
-- > z) (y.diff (n + List/length { index : Natural, value : a } kvs)) }) { count =
|
||||
-- > +0, diff = λ(_ : Natural) → nil }).diff +0)
|
||||
-- > 0, diff = λ(_ : Natural) → nil }).diff 0)
|
||||
--
|
||||
-- ... and run the expression through the @dhall-format@ executable:
|
||||
--
|
||||
|
|
@ -1624,9 +1646,9 @@ import Dhall
|
|||
-- > (y.diff (n + List/length { index : Natural, value : a } kvs))
|
||||
-- > }
|
||||
-- > )
|
||||
-- > { count = +0, diff = λ(_ : Natural) → nil }
|
||||
-- > { count = 0, diff = λ(_ : Natural) → nil }
|
||||
-- > ).diff
|
||||
-- > +0
|
||||
-- > 0
|
||||
-- > )
|
||||
--
|
||||
-- The executable formats expressions without resolving, type-checking, or
|
||||
|
|
@ -1634,15 +1656,15 @@ import Dhall
|
|||
--
|
||||
-- > $ dhall-format
|
||||
-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate
|
||||
-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
|
||||
-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
|
||||
-- > <Ctrl-D>
|
||||
-- > let replicate =
|
||||
-- > https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate
|
||||
-- >
|
||||
-- > in replicate
|
||||
-- > +5
|
||||
-- > (List (List Integer))
|
||||
-- > (replicate +5 (List Integer) (replicate +5 Integer 1))
|
||||
-- > 5
|
||||
-- > (List (List Natural))
|
||||
-- > (replicate 5 (List Natural) (replicate 5 Natural 1))
|
||||
--
|
||||
-- You can also use the formatter to modify files in place using the
|
||||
-- @--inplace@ flag (i.e. for formatting source code):
|
||||
|
|
@ -1676,9 +1698,9 @@ import Dhall
|
|||
-- > (y.diff (n + List/length { index : Natural, value : a } kvs))
|
||||
-- > }
|
||||
-- > )
|
||||
-- > { count = +0, diff = λ(_ : Natural) → nil }
|
||||
-- > { count = 0, diff = λ(_ : Natural) → nil }
|
||||
-- > ).diff
|
||||
-- > +0
|
||||
-- > 0
|
||||
-- > )
|
||||
--
|
||||
-- Carefully note that the code formatter does not preserve all comments.
|
||||
|
|
@ -1701,47 +1723,47 @@ import Dhall
|
|||
--
|
||||
-- > $ dhall
|
||||
-- > let replicate = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/List/replicate
|
||||
-- > in replicate +5 (List (List Integer)) (replicate +5 (List Integer) (replicate +5 Integer 1))
|
||||
-- > in replicate 5 (List (List Natural)) (replicate 5 (List Natural) (replicate 5 Natural 1))
|
||||
-- > <Ctrl-D>
|
||||
-- > List (List (List Integer))
|
||||
-- > List (List (List Natural))
|
||||
-- >
|
||||
-- > [ [ [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > [ [ [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > ]
|
||||
-- > : List (List Integer)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > : List (List Natural)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > ]
|
||||
-- > : List (List Integer)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > : List (List Natural)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > ]
|
||||
-- > : List (List Integer)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > : List (List Natural)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > ]
|
||||
-- > : List (List Integer)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Integer
|
||||
-- > : List (List Natural)
|
||||
-- > , [ [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > , [ 1, 1, 1, 1, 1 ] : List Natural
|
||||
-- > ]
|
||||
-- > : List (List Integer)
|
||||
-- > : List (List Natural)
|
||||
-- > ]
|
||||
-- > : List (List (List Integer))
|
||||
-- > : List (List (List Natural))
|
||||
|
||||
-- $builtins
|
||||
--
|
||||
|
|
@ -1782,18 +1804,19 @@ import Dhall
|
|||
--
|
||||
-- First, Dhall only supports addition and multiplication on @Natural@ numbers
|
||||
-- (i.e. non-negative integers), which are not the same type of number as
|
||||
-- @Integer@s (which can be negative). A @Natural@ number is a number prefixed
|
||||
-- with the @+@ symbol. If you try to add or multiply two @Integer@s (without
|
||||
-- the @+@ prefix) you will get a type error:
|
||||
-- @Integer@s (which can be negative). An @Integer@ number is a number prefixed
|
||||
-- with either a @+@ or @-@ symbol whereas a @Natural@ number has no leading
|
||||
-- sign. If you try to add or multiply two @Integer@s you will get a type
|
||||
-- error:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > 2 + 2
|
||||
-- > +2 + +2
|
||||
-- > <Ctrl-D>
|
||||
-- > Use "dhall --explain" for detailed errors
|
||||
-- >
|
||||
-- > Error: ❰+❱ only works on ❰Natural❱s
|
||||
-- >
|
||||
-- > 2 + 2
|
||||
-- > +2 + +2
|
||||
-- >
|
||||
-- > (stdin):1:1
|
||||
--
|
||||
|
|
@ -1983,7 +2006,7 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > if True then 3 else 5
|
||||
-- > <Ctrl-D>
|
||||
-- > Integer
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > 3
|
||||
--
|
||||
|
|
@ -2005,11 +2028,12 @@ import Dhall
|
|||
|
||||
-- $natural
|
||||
--
|
||||
-- @Natural@ literals are numbers prefixed by a @+@ sign, like this:
|
||||
-- @Natural@ literals are non-negative numbers without any leading sign, like
|
||||
-- this:
|
||||
--
|
||||
-- > +4 : Natural
|
||||
-- > 4 : Natural
|
||||
--
|
||||
-- If you omit the @+@ sign then you get an @Integer@ literal, which is a
|
||||
-- If you add a @+@ or @-@ sign then you get an @Integer@ literal, which is a
|
||||
-- different type of value
|
||||
|
||||
-- $plus
|
||||
|
|
@ -2017,11 +2041,11 @@ import Dhall
|
|||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > +2 + +3
|
||||
-- > 2 + 3
|
||||
-- > <Ctrl-D>
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > +5
|
||||
-- > 5
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2033,20 +2057,20 @@ import Dhall
|
|||
--
|
||||
-- > (x + y) + z = x + (y + z)
|
||||
-- >
|
||||
-- > x + +0 = x
|
||||
-- > x + 0 = x
|
||||
-- >
|
||||
-- > +0 + x = x
|
||||
-- > 0 + x = x
|
||||
|
||||
-- $times
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > +2 * +3
|
||||
-- > 2 * 3
|
||||
-- > <Ctrl-D>
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > +6
|
||||
-- > 6
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2058,24 +2082,24 @@ import Dhall
|
|||
--
|
||||
-- > (x * y) * z = x * (y * z)
|
||||
-- >
|
||||
-- > x * +1 = x
|
||||
-- > x * 1 = x
|
||||
-- >
|
||||
-- > +1 * x = x
|
||||
-- > 1 * x = x
|
||||
-- >
|
||||
-- > (x + y) * z = (x * z) + (y * z)
|
||||
-- >
|
||||
-- > x * (y + z) = (x * y) + (x * z)
|
||||
-- >
|
||||
-- > x * +0 = +0
|
||||
-- > x * 0 = 0
|
||||
-- >
|
||||
-- > +0 * x = +0
|
||||
-- > 0 * x = 0
|
||||
|
||||
-- $even
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > Natural/even +6
|
||||
-- > Natural/even 6
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
-- >
|
||||
|
|
@ -2090,18 +2114,18 @@ import Dhall
|
|||
--
|
||||
-- > Natural/even (x + y) = Natural/even x == Natural/even y
|
||||
-- >
|
||||
-- > Natural/even +0 = True
|
||||
-- > Natural/even 0 = True
|
||||
-- >
|
||||
-- > Natural/even (x * y) = Natural/even x || Natural/even y
|
||||
-- >
|
||||
-- > Natural/even +1 = False
|
||||
-- > Natural/even 1 = False
|
||||
|
||||
-- $odd
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > Natural/odd +6
|
||||
-- > Natural/odd 6
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
-- >
|
||||
|
|
@ -2116,18 +2140,18 @@ import Dhall
|
|||
--
|
||||
-- > Natural/odd (x + y) = Natural/odd x != Natural/odd y
|
||||
-- >
|
||||
-- > Natural/odd +0 = False
|
||||
-- > Natural/odd 0 = False
|
||||
-- >
|
||||
-- > Natural/odd (x * y) = Natural/odd x && Natural/odd y
|
||||
-- >
|
||||
-- > Natural/odd +1 = True
|
||||
-- > Natural/odd 1 = True
|
||||
|
||||
-- $isZero
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > Natural/isZero +6
|
||||
-- > Natural/isZero 6
|
||||
-- > <Ctrl-D>
|
||||
-- > Bool
|
||||
-- >
|
||||
|
|
@ -2142,18 +2166,18 @@ import Dhall
|
|||
--
|
||||
-- > Natural/isZero (x + y) = Natural/isZero x && Natural/isZero y
|
||||
-- >
|
||||
-- > Natural/isZero +0 = True
|
||||
-- > Natural/isZero 0 = True
|
||||
-- >
|
||||
-- > Natural/isZero (x * y) = Natural/isZero x || Natural/isZero y
|
||||
-- >
|
||||
-- > Natural/isZero +1 = False
|
||||
-- > Natural/isZero 1 = False
|
||||
|
||||
-- $naturalFold
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > Natural/fold +40 Text (λ(t : Text) → t ++ "!") "You're welcome"
|
||||
-- > Natural/fold 40 Text (λ(t : Text) → t ++ "!") "You're welcome"
|
||||
-- > <Ctrl-D>
|
||||
-- > Text
|
||||
-- >
|
||||
|
|
@ -2168,11 +2192,11 @@ import Dhall
|
|||
--
|
||||
-- > Natural/fold (x + y) n s z = Natural/fold x n s (Natural/fold y n s z)
|
||||
-- >
|
||||
-- > Natural/fold +0 n s z = z
|
||||
-- > Natural/fold 0 n s z = z
|
||||
-- >
|
||||
-- > Natural/fold (x * y) n s = Natural/fold x n (Natural/fold y n s)
|
||||
-- >
|
||||
-- > Natural/fold +1 n s = s
|
||||
-- > Natural/fold 1 n s = s
|
||||
|
||||
-- $naturalBuild
|
||||
--
|
||||
|
|
@ -2183,7 +2207,7 @@ import Dhall
|
|||
-- > <Ctrl-D>
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > +2
|
||||
-- > 2
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2198,14 +2222,13 @@ import Dhall
|
|||
|
||||
-- $integer
|
||||
--
|
||||
-- @Integer@ literals are either prefixed with a @-@ sign (if they are negative)
|
||||
-- or no sign (if they are positive), like this:
|
||||
-- @Integer@ literals are prefixed with a @+@ (if they are non-negative) or a
|
||||
-- @-@ sign (if they are negative), like this:
|
||||
--
|
||||
-- > 3 : Integer
|
||||
-- > +3 : Integer
|
||||
-- > -2 : Integer
|
||||
--
|
||||
-- If you prefix them with a @+@ sign then they are @Natural@ literals and not
|
||||
-- @Integer@s
|
||||
-- If you omit the sign then they are @Natural@ literals and not @Integer@s
|
||||
--
|
||||
-- There are no built-in operations on @Integer@s. For all practical purposes
|
||||
-- they are opaque values within the Dhall language
|
||||
|
|
@ -2266,7 +2289,7 @@ import Dhall
|
|||
--
|
||||
-- Also, every empty @List@ must end with a mandatory type annotation, for example:
|
||||
--
|
||||
-- > [] : List Integer
|
||||
-- > [] : List Natural
|
||||
--
|
||||
-- The built-in operations on @List@s are:
|
||||
|
||||
|
|
@ -2277,7 +2300,7 @@ import Dhall
|
|||
-- > $ dhall
|
||||
-- > [1, 2, 3] # [4, 5, 6]
|
||||
-- > <Ctrl-D>
|
||||
-- > List Integer
|
||||
-- > List Natural
|
||||
-- >
|
||||
-- > [1, 2, 3, 4, 5, 6]
|
||||
--
|
||||
|
|
@ -2327,11 +2350,11 @@ import Dhall
|
|||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > List/build Integer (λ(list : Type) → λ(cons : Integer → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))
|
||||
-- > List/build Natural (λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) → cons 1 (cons 2 (cons 3 nil)))
|
||||
-- > <Ctrl-D>
|
||||
-- > List Integer
|
||||
-- > List Natural
|
||||
-- >
|
||||
-- > [1, 2, 3] : List Integer
|
||||
-- > [1, 2, 3] : List Natural
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2349,11 +2372,11 @@ import Dhall
|
|||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > List/length Integer [1, 2, 3]
|
||||
-- > List/length Natural [1, 2, 3]
|
||||
-- > <Ctrl-D>
|
||||
-- > Natural
|
||||
-- >
|
||||
-- > +3
|
||||
-- > 3
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2362,18 +2385,18 @@ import Dhall
|
|||
--
|
||||
-- Rules:
|
||||
--
|
||||
-- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + +1) +0
|
||||
-- > List/length t xs = List/fold t xs Natural (λ(_ : t) → λ(n : Natural) → n + 1) 0
|
||||
|
||||
-- $listHead
|
||||
--
|
||||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > List/head Integer [1, 2, 3]
|
||||
-- > List/head Natural [1, 2, 3]
|
||||
-- > <Ctrl-D>
|
||||
-- > Optional Integer
|
||||
-- > Optional Natural
|
||||
-- >
|
||||
-- > [1] : Optional Integer
|
||||
-- > [1] : Optional Natural
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2400,11 +2423,11 @@ import Dhall
|
|||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > List/last Integer [1, 2, 3]
|
||||
-- > List/last Natural [1, 2, 3]
|
||||
-- > <Ctrl-D>
|
||||
-- > Optional Integer
|
||||
-- > Optional Natural
|
||||
-- >
|
||||
-- > [1] : Optional Integer
|
||||
-- > [1] : Optional Natural
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2435,7 +2458,7 @@ import Dhall
|
|||
-- > <Ctrl-D>
|
||||
-- > List { index : Natural, value : Text }
|
||||
-- >
|
||||
-- > [{ index = +0, value = "ABC" }, { index = +1, value = "DEF" }, { index = +2, value = "GHI" }] : List { index : Natural, value : Text }
|
||||
-- > [{ index = 0, value = "ABC" }, { index = 1, value = "DEF" }, { index = 2, value = "GHI" }] : List { index : Natural, value : Text }
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2456,11 +2479,11 @@ import Dhall
|
|||
-- Example:
|
||||
--
|
||||
-- > $ dhall
|
||||
-- > List/reverse Integer [1, 2, 3]
|
||||
-- > List/reverse Natural [1, 2, 3]
|
||||
-- > <Ctrl-D>
|
||||
-- > List Integer
|
||||
-- > List Natural
|
||||
-- >
|
||||
-- > [3, 2, 1] : List Integer
|
||||
-- > [3, 2, 1] : List Natural
|
||||
--
|
||||
-- Type:
|
||||
--
|
||||
|
|
@ -2605,9 +2628,9 @@ import Dhall
|
|||
-- > Examples:
|
||||
-- >
|
||||
-- > ```
|
||||
-- > ./even +3 = False
|
||||
-- > ./even 3 = False
|
||||
-- >
|
||||
-- > ./even +0 = True
|
||||
-- > ./even 0 = True
|
||||
-- > ```
|
||||
-- > -}
|
||||
-- > let even : Natural → Bool
|
||||
|
|
@ -2700,11 +2723,11 @@ import Dhall
|
|||
-- > let Prelude = https://ipfs.io/ipfs/QmdtKd5Q7tebdo6rXfZed4kN6DXmErRQHJ4PsNCtca9GbB/Prelude/package.dhall
|
||||
-- >
|
||||
-- > in λ(x : Text)
|
||||
-- > → Prelude.`List`.length Text (Prelude.`List`.replicate +10 Text x)
|
||||
-- > → Prelude.`List`.length Text (Prelude.`List`.replicate 10 Text x)
|
||||
-- > <Ctrl-D>
|
||||
-- > ∀(x : Text) → Natural
|
||||
-- >
|
||||
-- > λ(x : Text) → +10
|
||||
-- > λ(x : Text) → 10
|
||||
--
|
||||
-- The organization of the package mirrors the layout of the Prelude, meaning
|
||||
-- that every directory is stored as a record whose children are the fields of
|
||||
|
|
|
|||
|
|
@ -915,9 +915,9 @@ prettyTypeMessage (UnboundVariable _) = ErrorMessages {..}
|
|||
\● You tried to define a recursive value, like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────┐ \n\
|
||||
\ │ let x = x + +1 in x │ \n\
|
||||
\ └─────────────────────┘ \n\
|
||||
\ ┌────────────────────┐ \n\
|
||||
\ │ let x = x + 1 in x │ \n\
|
||||
\ └────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ Recursive definitions are not allowed \n\
|
||||
\ \n\
|
||||
|
|
@ -961,7 +961,7 @@ prettyTypeMessage (InvalidInputType expr) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────┐ \n\
|
||||
\ │ Bool → Integer │ This is the type of a function that accepts an anonymous\n\
|
||||
\ │ Bool → Natural │ This is the type of a function that accepts an anonymous\n\
|
||||
\ └────────────────┘ input term that has type ❰Bool❱ \n\
|
||||
\ ⇧ \n\
|
||||
\ This is the type of the input term \n\
|
||||
|
|
@ -1028,8 +1028,8 @@ prettyTypeMessage (InvalidOutputType expr) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────┐ \n\
|
||||
\ │ Bool → Integer │ This is the type of a function that returns an output \n\
|
||||
\ └────────────────┘ term that has type ❰Int❱ \n\
|
||||
\ │ Bool → Natural │ This is the type of a function that returns an output \n\
|
||||
\ └────────────────┘ term that has type ❰Natural❱ \n\
|
||||
\ ⇧ \n\
|
||||
\ This is the type of the output term \n\
|
||||
\ \n\
|
||||
|
|
@ -1167,13 +1167,13 @@ prettyTypeMessage (NotAFunction expr0 expr1) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────┐ \n\
|
||||
\ │ 1 : Integer │ ❰1❱ is not a function because ❰Integer❱ is not the type of \n\
|
||||
\ │ 1 : Natural │ ❰1❱ is not a function because ❰Natural❱ is not the type of \n\
|
||||
\ └─────────────┘ a function \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
\ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ is not a function because \n\
|
||||
\ └────────────────────────┘ ❰Bool❱ is not the type of a function \n\
|
||||
\ ┌───────────────────────┐ \n\
|
||||
\ │ Natural/even 2 : Bool │ ❰Natural/even 2❱ is not a function because \n\
|
||||
\ └───────────────────────┘ ❰Bool❱ is not the type of a function \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────┐ \n\
|
||||
|
|
@ -1183,7 +1183,7 @@ prettyTypeMessage (NotAFunction expr0 expr1) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\Some common reasons why you might get this error: \n\
|
||||
\ \n\
|
||||
\● You tried to add two ❰Integer❱s without a space around the ❰+❱, like this: \n\
|
||||
\● You tried to add two ❰Natural❱s without a space around the ❰+❱, like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────┐ \n\
|
||||
|
|
@ -1202,21 +1202,17 @@ prettyTypeMessage (NotAFunction expr0 expr1) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ This is because the ❰+❱ symbol has two meanings: you use ❰+❱ to add two \n\
|
||||
\ numbers, but you also can prefix ❰Integer❱ literals with a ❰+❱ to turn them \n\
|
||||
\ into ❰Natural❱ literals (like ❰+2❱) \n\
|
||||
\ numbers, but you also can prefix ❰Natural❱ literals with a ❰+❱ to turn them \n\
|
||||
\ into ❰Integer❱ literals (like ❰+2❱) \n\
|
||||
\ \n\
|
||||
\ To fix the code, you need to put spaces around the ❰+❱ and also prefix each \n\
|
||||
\ ❰2❱ with a ❰+❱, like this: \n\
|
||||
\ To fix the code, you need to put spaces around the ❰+❱, like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────┐ \n\
|
||||
\ │ +2 + +2 │ \n\
|
||||
\ └─────────┘ \n\
|
||||
\ ┌───────┐ \n\
|
||||
\ │ 2 + 2 │ \n\
|
||||
\ └───────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ You can only add ❰Natural❱ numbers, which is why you must also change each \n\
|
||||
\ ❰2❱ to ❰+2❱ \n\
|
||||
\ \n\
|
||||
\────────────────────────────────────────────────────────────────────────────────\n\
|
||||
\ \n\
|
||||
\You tried to use the following expression as a function: \n\
|
||||
|
|
@ -1280,9 +1276,9 @@ prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}
|
|||
\ └────────────────────────┘ of argument that the anonymous function accepts \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────┐ \n\
|
||||
\ │ Natural/even +2 │ ❰+2❱ has type ❰Natural❱, which matches the type of \n\
|
||||
\ └─────────────────┘ argument that the ❰Natural/even❱ function accepts, \n\
|
||||
\ ┌────────────────┐ \n\
|
||||
\ │ Natural/even 2 │ ❰2❱ has type ❰Natural❱, which matches the type of \n\
|
||||
\ └────────────────┘ argument that the ❰Natural/even❱ function accepts, \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
|
|
@ -1316,7 +1312,7 @@ prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────┐ \n\
|
||||
\ │ List 1 │ ❰1❱ has type ❰Integer❱, but the ❰List❱ function expects an \n\
|
||||
\ │ List 1 │ ❰1❱ has type ❰Natural❱, but the ❰List❱ function expects an \n\
|
||||
\ └────────┘ argument that has kind ❰Type❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1330,17 +1326,17 @@ prettyTypeMessage (TypeMismatch expr0 expr1 expr2 expr3) = ErrorMessages {..}
|
|||
\ └───────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ ❰List/head❱ is missing the first argument, \n\
|
||||
\ which should be: ❰Integer❱ \n\
|
||||
\ which should be: ❰Natural❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\● You supply an ❰Integer❱ literal to a function that expects a ❰Natural❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────┐ \n\
|
||||
\ │ Natural/even 2 │ \n\
|
||||
\ └────────────────┘ \n\
|
||||
\ ┌─────────────────┐ \n\
|
||||
\ │ Natural/even +2 │ \n\
|
||||
\ └─────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ This should be ❰+2❱ \n\
|
||||
\ This should be ❰2❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\────────────────────────────────────────────────────────────────────────────────\n\
|
||||
|
|
@ -1388,13 +1384,13 @@ prettyTypeMessage (AnnotMismatch expr0 expr1 expr2) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────┐ \n\
|
||||
\ │ 1 : Integer │ ❰1❱ is an expression that has type ❰Integer❱, so the type \n\
|
||||
\ │ 1 : Natural │ ❰1❱ is an expression that has type ❰Natural❱, so the type \n\
|
||||
\ └─────────────┘ checker accepts the annotation \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
\ │ Natural/even +2 : Bool │ ❰Natural/even +2❱ has type ❰Bool❱, so the type \n\
|
||||
\ └────────────────────────┘ checker accepts the annotation \n\
|
||||
\ ┌───────────────────────┐ \n\
|
||||
\ │ Natural/even 2 : Bool │ ❰Natural/even 2❱ has type ❰Bool❱, so the type \n\
|
||||
\ └───────────────────────┘ checker accepts the annotation \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────┐ \n\
|
||||
|
|
@ -1587,7 +1583,7 @@ prettyTypeMessage (IfBranchMustBeTerm b expr0 expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────┐ \n\
|
||||
\ │ 1 : Integer : Type │ ❰1❱ is a term with a type (❰Integer❱) of kind ❰Type❱\n\
|
||||
\ │ 1 : Natural : Type │ ❰1❱ is a term with a type (❰Natural❱) of kind ❰Type❱\n\
|
||||
\ └────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ term \n\
|
||||
|
|
@ -1674,7 +1670,7 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────────┐ \n\
|
||||
\ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Integer❱ \n\
|
||||
\ │ λ(b : Bool) → if b then 0 else 1 │ Both branches have type ❰Natural❱ \n\
|
||||
\ └──────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1688,7 +1684,7 @@ prettyTypeMessage (IfBranchMismatch expr0 expr1 expr2 expr3) =
|
|||
\However, the following expression is " <> _NOT <> " valid: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ This branch has type ❰Integer❱ \n\
|
||||
\ This branch has type ❰Natural❱ \n\
|
||||
\ ⇩ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
\ │ if True then 0 │ \n\
|
||||
|
|
@ -1734,14 +1730,15 @@ prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────┐ \n\
|
||||
\ │ [1, 2, 3] : List Integer │ A ❰List❱ of three ❰Integer❱s \n\
|
||||
\ │ [1, 2, 3] : List Natural │ A ❰List❱ of three ❰Natural❱ numbers \n\
|
||||
\ └──────────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ The type of the ❰List❱'s elements, which are ❰Integer❱s \n\
|
||||
\ The type of the ❰List❱'s elements, which are ❰Natural❱ \n\
|
||||
\ numbers \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────┐ \n\
|
||||
\ │ [] : List Integer │ An empty ❰List❱ \n\
|
||||
\ │ [] : List Natural │ An empty ❰List❱ \n\
|
||||
\ └───────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ You must specify the type when the ❰List❱ is empty \n\
|
||||
|
|
@ -1755,7 +1752,7 @@ prettyTypeMessage (InvalidListType expr0) = ErrorMessages {..}
|
|||
\ │ ... : List 1 │ \n\
|
||||
\ └──────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ This is an ❰Integer❱ and not a ❰Type❱ \n\
|
||||
\ This is a ❰Natural❱ number and not a ❰Type❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────┐ \n\
|
||||
|
|
@ -1784,7 +1781,7 @@ prettyTypeMessage MissingListType = do
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────┐ \n\
|
||||
\ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Integer❱\n\
|
||||
\ │ [1, 2, 3] │ The compiler can infer that this list has type ❰List Natural❱\n\
|
||||
\ └───────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1792,7 +1789,7 @@ prettyTypeMessage MissingListType = do
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────┐ \n\
|
||||
\ │ [] : List Integer │ This type annotation is mandatory \n\
|
||||
\ │ [] : List Natural │ This type annotation is mandatory \n\
|
||||
\ └───────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1812,7 +1809,7 @@ prettyTypeMessage (MismatchedListElements i expr0 _expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────┐ \n\
|
||||
\ │ [1, 2, 3] │ Every element in this ❰List❱ is an ❰Integer❱ \n\
|
||||
\ │ [1, 2, 3] │ Every element in this ❰List❱ is a ❰Natural❱ number \n\
|
||||
\ └───────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1851,7 +1848,7 @@ prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────┐ \n\
|
||||
\ │ [1, 2, 3] : List Integer │ Every element in this ❰List❱ is an ❰Integer❱ \n\
|
||||
\ │ [1, 2, 3] : List Natural │ Every element in this ❰List❱ is an ❰Natural❱ \n\
|
||||
\ └──────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1859,7 +1856,7 @@ prettyTypeMessage (InvalidListElement i expr0 _expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────┐ \n\
|
||||
\ │ [1, \"ABC\", 3] : List Integer │ The second element is not an ❰Integer❱ \n\
|
||||
\ │ [1, \"ABC\", 3] : List Natural │ The second element is not an ❰Natural❱ \n\
|
||||
\ └──────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1885,14 +1882,15 @@ prettyTypeMessage (InvalidOptionalType expr0) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
\ │ [1] : Optional Integer │ An optional element that's present \n\
|
||||
\ │ [1] : Optional Natural │ An optional element that's present \n\
|
||||
\ └────────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ The type of the ❰Optional❱ element, which is an ❰Integer❱ \n\
|
||||
\ The type of the ❰Optional❱ element, which is an ❰Natural❱ \n\
|
||||
\ number \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
\ │ [] : Optional Integer │ An optional element that's absent \n\
|
||||
\ │ [] : Optional Natural │ An optional element that's absent \n\
|
||||
\ └────────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ You still specify the type even when the element is absent \n\
|
||||
|
|
@ -1906,7 +1904,7 @@ prettyTypeMessage (InvalidOptionalType expr0) = ErrorMessages {..}
|
|||
\ │ ... : Optional 1 │ \n\
|
||||
\ └──────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ This is an ❰Integer❱ and not a ❰Type❱ \n\
|
||||
\ This is a ❰Natural❱ number and not a ❰Type❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────┐ \n\
|
||||
|
|
@ -1939,15 +1937,15 @@ prettyTypeMessage (InvalidOptionalElement expr0 expr1 expr2) = ErrorMessages {..
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────┐ \n\
|
||||
\ │ [1] : Optional Integer │ ❰1❱ is an ❰Integer❱, which matches the type \n\
|
||||
\ └────────────────────────┘ \n\
|
||||
\ │ [1] : Optional Natural │ ❰1❱ is a ❰Natural❱ number, which matches the \n\
|
||||
\ └────────────────────────┘ number \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\... but this is " <> _NOT <> " a valid ❰Optional❱ value: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────────┐ \n\
|
||||
\ │ [\"ABC\"] : Optional Integer │ ❰\"ABC\"❱ is not an ❰Integer❱ \n\
|
||||
\ │ [\"ABC\"] : Optional Natural │ ❰\"ABC\"❱ is not a ❰Natural❱ number \n\
|
||||
\ └────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1977,7 +1975,7 @@ prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────────────────────┐ \n\
|
||||
\ │ { foo : Integer, bar : Integer, baz : Text } │ Every field is annotated \n\
|
||||
\ │ { foo : Natural, bar : Integer, baz : Text } │ Every field is annotated \n\
|
||||
\ └──────────────────────────────────────────────┘ with a ❰Type❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -1990,10 +1988,11 @@ prettyTypeMessage (InvalidFieldType k expr0) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────────┐ \n\
|
||||
\ │ { foo : Integer, bar : 1 } │ Invalid record type \n\
|
||||
\ │ { foo : Natural, bar : 1 } │ Invalid record type \n\
|
||||
\ └────────────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ ❰1❱ is an ❰Integer❱ and not a ❰Type❱ or ❰Kind❱ \n\
|
||||
\ ❰1❱ is a ❰Natural❱ number and not a ❰Type❱ or \n\
|
||||
\ ❰Kind❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\You provided a record type with a field named: \n\
|
||||
|
|
@ -2019,7 +2018,7 @@ prettyTypeMessage (FieldAnnotationMismatch k0 expr0 k1 expr1 c) = ErrorMessages
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────────────────────┐ \n\
|
||||
\ │ { foo : Integer, bar : Integer, baz : Text } │ Every field is annotated \n\
|
||||
\ │ { foo : Natural, bar : Integer, baz : Text } │ Every field is annotated \n\
|
||||
\ └──────────────────────────────────────────────┘ with a ❰Type❱ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -2034,7 +2033,7 @@ prettyTypeMessage (FieldAnnotationMismatch k0 expr0 k1 expr1 c) = ErrorMessages
|
|||
\ This is a ❰Type❱ annotation \n\
|
||||
\ ⇩ \n\
|
||||
\ ┌───────────────────────────────┐ \n\
|
||||
\ │ { foo : Integer, bar : Type } │ Invalid record type \n\
|
||||
\ │ { foo : Natural, bar : Type } │ Invalid record type \n\
|
||||
\ └───────────────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ ... but this is a ❰Kind❱ annotation \n\
|
||||
|
|
@ -2086,7 +2085,7 @@ prettyTypeMessage (FieldMismatch k0 expr0 k1 expr1 c) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────────────────┐ \n\
|
||||
\ │ { foo = Integer, bar = Text } │ Every field is a type \n\
|
||||
\ │ { foo = Natural, bar = Text } │ Every field is a type \n\
|
||||
\ └───────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
|
|
@ -2311,7 +2310,7 @@ prettyTypeMessage (ListAppendMismatch expr0 expr1) = ErrorMessages {..}
|
|||
\For example, the following expression is " <> _NOT <> " valid: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ These elements have type ❰Integer❱ \n\
|
||||
\ These elements have type ❰Natural❱ \n\
|
||||
\ ⇩ \n\
|
||||
\ ┌───────────────────────────┐ \n\
|
||||
\ │ [1, 2, 3] # [True, False] │ Invalid: the element types don't match \n\
|
||||
|
|
@ -2594,7 +2593,7 @@ prettyTypeMessage (MustMergeARecord expr0 expr1) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2649,7 +2648,7 @@ prettyTypeMessage (MustMergeUnion expr0 expr1) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2689,7 +2688,7 @@ prettyTypeMessage (UnusedHandler ks) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2702,11 +2701,11 @@ prettyTypeMessage (UnusedHandler ks) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 > │ The ❰Right❱ alternative is missing\n\
|
||||
\ │ in let handlers = │ \n\
|
||||
\ │ let union = < Left = 2 > │ The ❰Right❱ alternative is \n\
|
||||
\ │ in let handlers = │ missing \n\
|
||||
\ │ { Left = Natural/even │ \n\
|
||||
\ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't used\n\
|
||||
\ │ } │ \n\
|
||||
\ │ , Right = λ(x : Bool) → x │ Invalid: ❰Right❱ handler isn't \n\
|
||||
\ │ } │ used \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └───────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
|
|
@ -2729,7 +2728,7 @@ prettyTypeMessage (MissingHandler ks) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2745,7 +2744,7 @@ prettyTypeMessage (MissingHandler ks) = ErrorMessages {..}
|
|||
\ ⇩ \n\
|
||||
\ ┌─────────────────────────────────────────────────┐ \n\
|
||||
\ │ let handlers = { Left = Natural/even } │ \n\
|
||||
\ │ in let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ in let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
|
|
@ -2770,7 +2769,7 @@ prettyTypeMessage MissingMergeType =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2802,7 +2801,7 @@ prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2830,7 +2829,7 @@ prettyTypeMessage (HandlerInputTypeMismatch expr0 expr1 expr2) =
|
|||
\ ⇩ \n\
|
||||
\ ┌──────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let handlers = { Left = Natural/even | Right = λ(x : Text) → x } │ \n\
|
||||
\ │ in let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ in let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └──────────────────────────────────────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
|
|
@ -2864,7 +2863,7 @@ prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2891,7 +2890,7 @@ prettyTypeMessage (InvalidHandlerOutputType expr0 expr1 expr2) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌──────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Text │ \n\
|
||||
\ └──────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2928,7 +2927,7 @@ prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -2948,7 +2947,7 @@ prettyTypeMessage (HandlerOutputTypeMismatch key0 expr0 key1 expr1) =
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = │ \n\
|
||||
\ │ { Left = λ(x : Natural) → x │ This outputs ❰Natural❱ \n\
|
||||
\ │ , Right = λ(x : Bool ) → x │ This outputs ❰Bool❱ \n\
|
||||
|
|
@ -2982,7 +2981,7 @@ prettyTypeMessage (HandlerNotAFunction k expr0) = ErrorMessages {..}
|
|||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ let union = < Left = +2 | Right : Bool > │ \n\
|
||||
\ │ let union = < Left = 2 | Right : Bool > │ \n\
|
||||
\ │ in let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │ \n\
|
||||
\ │ in merge handlers union : Bool │ \n\
|
||||
\ └─────────────────────────────────────────────────────────────────────┘ \n\
|
||||
|
|
@ -3197,9 +3196,9 @@ prettyTypeMessage (CantInterpolate expr0 expr1) = ErrorMessages {..}
|
|||
\ └────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────────────────────────────────────────────────────────────────┐ \n\
|
||||
\ │ λ(age : Natural) → \"Age: ${Integer/show (Natural/toInteger age)}\" │ \n\
|
||||
\ └───────────────────────────────────────────────────────────────────┘ \n\
|
||||
\ ┌───────────────────────────────────────────────┐ \n\
|
||||
\ │ λ(age : Natural) → \"Age: ${Natural/show age}\" │ \n\
|
||||
\ └───────────────────────────────────────────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\Some common reasons why you might get this error: \n\
|
||||
|
|
@ -3341,9 +3340,9 @@ prettyTypeMessage (NoDependentTypes expr0 expr1) = ErrorMessages {..}
|
|||
\Similarly, this is " <> _NOT <> " legal code: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌────────────────────────────────────────────────────┐ \n\
|
||||
\ │ λ(Vector : Natural → Type → Type) → Vector +0 Text │ \n\
|
||||
\ └────────────────────────────────────────────────────┘ \n\
|
||||
\ ┌───────────────────────────────────────────────────┐ \n\
|
||||
\ │ λ(Vector : Natural → Type → Type) → Vector 0 Text │ \n\
|
||||
\ └───────────────────────────────────────────────────┘ \n\
|
||||
\ ⇧ \n\
|
||||
\ Invalid dependent type \n\
|
||||
\ \n\
|
||||
|
|
@ -3401,9 +3400,9 @@ buildNaturalOperator operator expr0 expr1 = ErrorMessages {..}
|
|||
\For example, this is a valid use of ❰" <> txt2 <> "❱: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────┐ \n\
|
||||
\ │ +3 " <> txt2 <> " +5 │ \n\
|
||||
\ └─────────┘ \n\
|
||||
\ ┌───────┐ \n\
|
||||
\ │ 3 " <> txt2 <> " 5 │ \n\
|
||||
\ └───────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\Some common reasons why you might get this error: \n\
|
||||
|
|
@ -3422,20 +3421,20 @@ buildNaturalOperator operator expr0 expr1 = ErrorMessages {..}
|
|||
\● You might have mistakenly used an ❰Integer❱ literal, which is " <> _NOT <> " allowed:\n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────┐ \n\
|
||||
\ │ 2 " <> txt2 <> " 2 │ Not valid \n\
|
||||
\ └───────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ You need to prefix each literal with a ❰+❱ to transform them into ❰Natural❱ \n\
|
||||
\ literals, like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌─────────┐ \n\
|
||||
\ │ +2 " <> txt2 <> " +2 │ Valid \n\
|
||||
\ │ +2 " <> txt2 <> " +2 │ Not valid \n\
|
||||
\ └─────────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ You need to remove the leading ❰+❱ to transform them into ❰Natural❱ literals, \n\
|
||||
\ like this: \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\ ┌───────┐ \n\
|
||||
\ │ 2 " <> txt2 <> " 2 │ Valid \n\
|
||||
\ └───────┘ \n\
|
||||
\ \n\
|
||||
\ \n\
|
||||
\────────────────────────────────────────────────────────────────────────────────\n\
|
||||
\ \n\
|
||||
\You provided this argument: \n\
|
||||
|
|
|
|||
|
|
@ -203,8 +203,8 @@ simpleCustomization = testCase "simpleCustomization" $ do
|
|||
valCtx e = case e of
|
||||
(App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalLit y)) -> Just (NaturalLit (min x y))
|
||||
_ -> Nothing
|
||||
e <- codeWith tyCtx "min (min +11 +12) +8 + +1"
|
||||
assertNormalizesToWith valCtx e "+9"
|
||||
e <- codeWith tyCtx "min (min 11 12) 8 + 1"
|
||||
assertNormalizesToWith valCtx e "9"
|
||||
|
||||
nestedReduction :: TestTree
|
||||
nestedReduction = testCase "doubleReduction" $ do
|
||||
|
|
@ -219,8 +219,8 @@ nestedReduction = testCase "doubleReduction" $ do
|
|||
(App (Var (V "fiveorless" 0)) (NaturalLit x)) -> Just
|
||||
(App (App (Var (V "min" 0)) (NaturalLit x)) (NaturalPlus (NaturalLit 3) (NaturalLit 2)))
|
||||
_ -> Nothing
|
||||
e <- codeWith tyCtx "wurble +6"
|
||||
assertNormalizesToWith valCtx e "+5"
|
||||
e <- codeWith tyCtx "wurble 6"
|
||||
assertNormalizesToWith valCtx e "5"
|
||||
|
||||
should :: Text -> Text -> TestTree
|
||||
should name basename =
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ _Interpolation_0 = Test.Tasty.HUnit.testCase "Example #0" (do
|
|||
e <- Util.code
|
||||
" let name = \"John Doe\" \n\
|
||||
\in let age = 21 \n\
|
||||
\in \"My name is ${name} and my age is ${Integer/show age}\"\n"
|
||||
\in \"My name is ${name} and my age is ${Natural/show age}\"\n"
|
||||
Util.assertNormalizesTo e "\"My name is John Doe and my age is 21\"" )
|
||||
|
||||
_Interpolation_1 :: TestTree
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/Bool/fold True Integer 0 1
|
||||
../../../../../Prelude/Bool/fold True Natural 0 1
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/Bool/fold False Integer 0 1
|
||||
../../../../../Prelude/Bool/fold False Natural 0 1
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/Integer/show 0
|
||||
../../../../../Prelude/Integer/show +0
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
"0"
|
||||
"+0"
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/all Natural Natural/even [ +2, +3, +5 ]
|
||||
../../../../../Prelude/List/all Natural Natural/even [ 2, 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/any Natural Natural/even [ +2, +3, +5 ]
|
||||
../../../../../Prelude/List/any Natural Natural/even [ 2, 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
../../../../../Prelude/List/concat Integer
|
||||
../../../../../Prelude/List/concat Natural
|
||||
[ [ 0, 1, 2 ]
|
||||
, [ 3, 4 ]
|
||||
, [ 5, 6, 7, 8 ]
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
../../../../../Prelude/List/concat Integer
|
||||
[ [] : List Integer
|
||||
, [] : List Integer
|
||||
, [] : List Integer
|
||||
../../../../../Prelude/List/concat Natural
|
||||
[ [] : List Natural
|
||||
, [] : List Natural
|
||||
, [] : List Natural
|
||||
]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[] : List Integer
|
||||
[] : List Natural
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ +2, +3, +5 ]
|
||||
../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[ +2, +2, +3, +3, +5, +5 ]
|
||||
[ 2, 2, 3, 3, 5, 5 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/filter Natural Natural/even [ +2, +3, +5 ]
|
||||
../../../../../Prelude/List/filter Natural Natural/even [ 2, 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[ +2 ]
|
||||
[ 2 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/filter Natural Natural/odd [ +2, +3, +5 ]
|
||||
../../../../../Prelude/List/filter Natural Natural/odd [ 2, 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[ +3, +5 ]
|
||||
[ 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
../../../../../Prelude/List/fold
|
||||
Natural
|
||||
[ +2, +3, +5 ]
|
||||
[ 2, 3, 5 ]
|
||||
Natural
|
||||
(λ(x : Natural) → λ(y : Natural) → x + y)
|
||||
+0
|
||||
0
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
+10
|
||||
10
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
λ(nil : Natural)
|
||||
→ ../../../../../Prelude/List/fold
|
||||
Natural
|
||||
[ +2, +3, +5 ]
|
||||
[ 2, 3, 5 ]
|
||||
Natural
|
||||
(λ(x : Natural) → λ(y : Natural) → x + y)
|
||||
nil
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
λ(nil : Natural) → +2 + +3 + +5 + nil
|
||||
λ(nil : Natural) → 2 + 3 + 5 + nil
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
λ(list : Type)
|
||||
→ λ(cons : Natural → list → list)
|
||||
→ λ(nil : list)
|
||||
→ ../../../../../Prelude/List/fold Natural [ +2, +3, +5 ] list cons nil
|
||||
→ ../../../../../Prelude/List/fold Natural [ 2, 3, 5 ] list cons nil
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
λ(list : Type)
|
||||
→ λ(cons : Natural → list → list)
|
||||
→ λ(nil : list)
|
||||
→ cons +2 (cons +3 (cons +5 nil))
|
||||
→ cons 2 (cons 3 (cons 5 nil))
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/generate +5 Bool Natural/even
|
||||
../../../../../Prelude/List/generate 5 Bool Natural/even
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/generate +0 Bool Natural/even
|
||||
../../../../../Prelude/List/generate 0 Bool Natural/even
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/head Integer [ 0, 1, 2 ]
|
||||
../../../../../Prelude/List/head Natural [ 0, 1, 2 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[ 0 ] : Optional Integer
|
||||
[ 0 ] : Optional Natural
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/head Integer ([] : List Integer)
|
||||
../../../../../Prelude/List/head Natural ([] : List Natural)
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[] : Optional Integer
|
||||
[] : Optional Natural
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/iterate +10 Natural (λ(x : Natural) → x * +2) +1
|
||||
../../../../../Prelude/List/iterate 10 Natural (λ(x : Natural) → x * 2) 1
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[ +1, +2, +4, +8, +16, +32, +64, +128, +256, +512 ]
|
||||
[ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/iterate +0 Natural (λ(x : Natural) → x * +2) +1
|
||||
../../../../../Prelude/List/iterate 0 Natural (λ(x : Natural) → x * 2) 1
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/last Integer [ 0, 1, 2 ]
|
||||
../../../../../Prelude/List/last Natural [ 0, 1, 2 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[ 2 ] : Optional Integer
|
||||
[ 2 ] : Optional Natural
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/last Integer ([] : List Integer)
|
||||
../../../../../Prelude/List/last Natural ([] : List Natural)
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[] : Optional Integer
|
||||
[] : Optional Natural
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/length Integer [ 0, 1, 2 ]
|
||||
../../../../../Prelude/List/length Natural [ 0, 1, 2 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
+3
|
||||
3
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/length Integer ([] : List Integer)
|
||||
../../../../../Prelude/List/length Natural ([] : List Natural)
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
+0
|
||||
0
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/map Natural Bool Natural/even [ +2, +3, +5 ]
|
||||
../../../../../Prelude/List/map Natural Bool Natural/even [ 2, 3, 5 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/null Integer [ 0, 1, 2 ]
|
||||
../../../../../Prelude/List/null Natural [ 0, 1, 2 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/null Integer ([] : List Integer)
|
||||
../../../../../Prelude/List/null Natural ([] : List Natural)
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/replicate +9 Integer 1
|
||||
../../../../../Prelude/List/replicate 9 Natural 1
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/replicate +0 Integer 1
|
||||
../../../../../Prelude/List/replicate 0 Natural 1
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[] : List Integer
|
||||
[] : List Natural
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/reverse Integer [ 0, 1, 2 ]
|
||||
../../../../../Prelude/List/reverse Natural [ 0, 1, 2 ]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
../../../../../Prelude/List/reverse Integer ([] : List Integer)
|
||||
../../../../../Prelude/List/reverse Natural ([] : List Natural)
|
||||
|
|
|
|||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user