ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Import Prelude instead of vendoring the Prelude (#639)

Browse Source 
This uses Dhall's import system to fetch the Prelude so that we don't have
to keep a local copy of it
This commit is contained in:
Gabriel Gonzalez 2018-10-14 09:00:08 -07:00 committed by GitHub
parent 88b406b30c
commit 25a0d69797
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
215 changed files with 159 additions and 1972 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Prelude/Bool/and
View File

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

17
Prelude/Bool/build
View File

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

22
Prelude/Bool/even
View File

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

20
Prelude/Bool/fold
View File

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

12
Prelude/Bool/not
View File

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

22
Prelude/Bool/odd
View File

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

18
Prelude/Bool/or
View File

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

17
Prelude/Bool/package.dhall
View File

@ -1,17 +0,0 @@
{ and =
./and
, build =
./build
, even =
./even
, fold =
./fold
, not =
./not
, odd =
./odd
, or =
./or
, show =
./show
}

13
Prelude/Bool/show
View File

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

1
Prelude/Double/package.dhall
View File

@ -1 +0,0 @@
{ show = ./show }

13
Prelude/Double/show
View File

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

21
Prelude/Function/compose
View File

@ -1,21 +0,0 @@
{-
Compose two functions into one.
Examples:
```
./compose Natural Natural Bool (λ(n : Natural) → n + n) ../Natural/even 3
= True
```
-}
let compose
: ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
= λ(A : Type)
→ λ(B : Type)
→ λ(C : Type)
→ λ(f : A → B)
→ λ(g : B → C)
→ λ(x : A)
→ g (f x)
in compose

1
Prelude/Function/package.dhall
View File

@ -1 +0,0 @@
{ compose = ./compose }

1
Prelude/Integer/package.dhall
View File

@ -1 +0,0 @@
{ show = ./show }

14
Prelude/Integer/show
View File

@ -1,14 +0,0 @@
{-
Render an `Integer` as `Text` using the same representation as Dhall source
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"
```
-}
let show : Integer → Text = Integer/show in show

12
Prelude/Integer/toDouble
View File

@ -1,12 +0,0 @@
{-
Convert an `Integer` to the corresponding `Double`
Examples:
```
./toDouble -3 = -3.0
./toDouble +2 = 2.0
```
-}
let toDouble : Integer → Double = Integer/toDouble in toDouble

32
Prelude/JSON/Nesting
View File

@ -1,32 +0,0 @@
{-
This type is used as part of `dhall-json`'s support for preserving alternative
names
For example, this Dhall code:
```
let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
in let example = constructors Example
in let Nesting = < Inline : {} | Nested : Text >
in let nesting = constructors Nesting
in { field = "name"
, nesting = nesting.Inline {=}
, contents = example.Left { foo = 2 }
}
```
... generates this JSON:
```
{
"foo": 2,
"name": "Left"
}
```
-}
let Nesting : Type = < Inline : {} | Nested : Text > in Nesting

69
Prelude/JSON/Tagged
View File

@ -1,69 +0,0 @@
{-
This is a convenient type-level function when using `dhall-to-json`'s support
for preserving alternative names
For example, this code:
```
let map = ../List/map
in let Provisioner =
< shell :
{ inline : List Text }
| file :
{ source : Text, destination : Text }
>
in let provisioner = constructors Provisioner
in let Tagged = ./Tagged
in let nesting = constructors ./Nesting
in let wrap
: Provisioner → Tagged Provisioner
= λ(x : Provisioner)
→ { field = "type", nesting = nesting.Nested "params", contents = x }
in { provisioners =
map
Provisioner
(Tagged Provisioner)
wrap
[ provisioner.shell { inline = [ "echo foo" ] }
, provisioner.file
{ source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
]
}
```
... produces this JSON:
```
{
"provisioners": [
{
"params": {
"inline": [
"echo foo"
]
},
"type": "shell"
},
{
"params": {
"destination": "/tmp/app.tar.gz",
"source": "app.tar.gz"
},
"type": "file"
}
]
}
```
-}
let Tagged
: Type → Type
= λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a }
in Tagged

17
Prelude/JSON/keyText
View File

@ -1,17 +0,0 @@
{-
Builds a key-value record such that a List of them will be converted to a
homogeneous record by dhall-to-json and dhall-to-yaml.
Both key and value are fixed to Text.
Take a look at `Record/keyValue` for a polymorphic version.
Example:
```
./keyText "foo" "bar" = { mapKey = "foo", mapValue = "bar" }
```
-}
let keyText =
λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
in keyText

20
Prelude/JSON/keyValue
View File

@ -1,20 +0,0 @@
{-
Builds a key-value record such that a List of them will be converted to a
homogeneous record by dhall-to-json and dhall-to-yaml.
Examples:
```
./keyValue Natural "foo" 2 = { mapKey = "foo", mapValue = 2 }
./keyValue Text "bar" "baz" = { mapKey = "bar", mapValue = "baz" }
```
-}
let keyValue =
λ(v : Type)
→ λ(key : Text)
→ λ(value : v)
→ { mapKey = key, mapValue = value }
in keyValue

1
Prelude/JSON/package.dhall
View File

@ -1 +0,0 @@
{ keyText = ./keyText, keyValue = ./keyValue }

20
Prelude/List/all
View File

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

20
Prelude/List/any
View File

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

32
Prelude/List/build
View File

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

42
Prelude/List/concat
View File

@ -1,42 +0,0 @@
{-
Concatenate a `List` of `List`s into a single `List`
Examples:
```
./concat Natural
[ [0, 1, 2]
, [3, 4]
, [5, 6, 7, 8]
]
= [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
./concat Natural
( [ [] : List Natural
, [] : List Natural
, [] : List Natural
]
)
= [] : List Natural
./concat Natural ([] : List (List Natural)) = [] : List Natural
```
-}
let concat
: ∀(a : Type) → List (List a) → List a
= λ(a : Type)
→ λ(xss : List (List a))
→ List/build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ λ(nil : list)
→ List/fold
(List a)
xss
list
(λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys)
nil
)
in concat

28
Prelude/List/concatMap
View File

@ -1,28 +0,0 @@
{-
Transform a list by applying a function to each element and flattening the
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]) ([] : List Natural)
= [] : List Natural
```
-}
let concatMap
: ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b
= λ(a : Type)
→ λ(b : Type)
→ λ(f : a → List b)
→ λ(xs : List a)
→ List/build
b
( λ(list : Type)
→ λ(cons : b → list → list)
→ List/fold a xs list (λ(x : a) → List/fold b (f x) list cons)
)
in concatMap

30
Prelude/List/filter
View File

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

46
Prelude/List/fold
View File

@ -1,46 +0,0 @@
{-
`fold` is the primitive function for consuming `List`s
If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a
`fold` just replaces each `cons` and `nil` with something else
Examples:
```
./fold
Natural
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
0
= 10
λ(nil : Natural)
→ ./fold
Natural
[ 2, 3, 5 ]
Natural
(λ(x : Natural) → λ(y : Natural) → x + y)
nil
= λ(nil : Natural) → 2 + (3 + (5 + nil))
λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)
→ ./fold Natural [ 2, 3, 5 ] list cons nil
= λ(list : Type)
→ λ(cons : Natural → list → list)
→ λ(nil : list)
→ cons 2 (cons 3 (cons 5 nil))
```
-}
let fold
: ∀(a : Type)
→ List a
→ ∀(list : Type)
→ ∀(cons : a → list → list)
→ ∀(nil : list)
→ list
= List/fold
in fold

38
Prelude/List/generate
View File

@ -1,38 +0,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 0 Bool Natural/even = [] : List Bool
```
-}
let generate
: Natural → ∀(a : Type) → (Natural → a) → List a
= λ(n : Natural)
→ λ(a : Type)
→ λ(f : Natural → a)
→ List/build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type)
→ λ(cons : {} → list → list)
→ Natural/fold n list (cons {=})
)
)
)
list
(λ(x : { index : Natural, value : {} }) → cons (f x.index))
)
in generate

12
Prelude/List/head
View File

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

21
Prelude/List/indexed
View File

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

43
Prelude/List/iterate
View File

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

12
Prelude/List/last
View File

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

12
Prelude/List/length
View File

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

27
Prelude/List/map
View File

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

16
Prelude/List/null
View File

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

39
Prelude/List/package.dhall
View File

@ -1,39 +0,0 @@
{ all =
./all
, any =
./any
, build =
./build
, concat =
./concat
, concatMap =
./concatMap
, filter =
./filter
, fold =
./fold
, generate =
./generate
, head =
./head
, indexed =
./indexed
, iterate =
./iterate
, last =
./last
, length =
./length
, map =
./map
, null =
./null
, replicate =
./replicate
, reverse =
./reverse
, shifted =
./shifted
, unzip =
./unzip
}

24
Prelude/List/replicate
View File

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

12
Prelude/List/reverse
View File

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

90
Prelude/List/shifted
View File

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

55
Prelude/List/unzip
View File

@ -1,55 +0,0 @@
{-
Unzip a `List` into two separate `List`s
Examples:
```
./unzip
Text
Bool
( [ { _1 = "ABC", _2 = True }
, { _1 = "DEF", _2 = False }
, { _1 = "GHI", _2 = True }
]
)
= { _1 = [ "ABC", "DEF", "GHI" ]
, _2 = [ True, False, True ]
}
./unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
= { _1 = [] : List Text, _2 = [] : List Bool }
```
-}
let unzip
: ∀(a : Type)
→ ∀(b : Type)
→ List { _1 : a, _2 : b }
→ { _1 : List a, _2 : List b }
= λ(a : Type)
→ λ(b : Type)
→ λ(xs : List { _1 : a, _2 : b })
→ { _1 =
List/build
a
( λ(list : Type)
→ λ(cons : a → list → list)
→ List/fold
{ _1 : a, _2 : b }
xs
list
(λ(x : { _1 : a, _2 : b }) → cons x._1)
)
, _2 =
List/build
b
( λ(list : Type)
→ λ(cons : b → list → list)
→ List/fold
{ _1 : a, _2 : b }
xs
list
(λ(x : { _1 : a, _2 : b }) → cons x._2)
)
}
in unzip

40
Prelude/Monoid
View File

@ -1,39 +1 @@
{-
Any function `f` that is a `Monoid` must satisfy the following law:
```
t : Type
f : ./Monoid t
xs : List (List t)
f (./List/concat t xs) = f (./map (List t) t f xs)
```
Examples:
```
./Bool/and
: ./Monoid Bool
./Bool/or
: ./Monoid Bool
./Bool/even
: ./Monoid Bool
./Bool/odd
: ./Monoid Bool
./List/concat
: ∀(a : Type) → ./Monoid (List a)
./List/shifted
: ∀(a : Type) → ./Monoid (List { index : Natural, value : a })
./Natural/sum
: ./Monoid Natural
./Natural/product
: ./Monoid Natural
./Optional/head
: ∀(a : Type) → ./Monoid (Optional a)
./Optional/last
: ∀(a : Type) → ./Monoid (Optional a)
./Text/concat
: ./Monoid Text
```
-}
let Monoid : ∀(m : Type) → Type = λ(m : Type) → List m → m in Monoid
https://raw.githubusercontent.com/dhall-lang/Prelude/a22da69657b9316a3c51ba0bf80c9d4024db3fce/Monoid sha256:7c753f458fb433ef50e2fc517c0eaffbf21afd07186cefa92ea77173fe83304e

33
Prelude/Natural/build
View File

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

36
Prelude/Natural/enumerate
View File

@ -1,36 +0,0 @@
{-
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 0 = [] : List Natural
```
-}
let enumerate
: Natural → List Natural
= λ(n : Natural)
→ List/build
Natural
( λ(list : Type)
→ λ(cons : Natural → list → list)
→ List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type)
→ λ(cons : {} → list → list)
→ Natural/fold n list (cons {=})
)
)
)
list
(λ(x : { index : Natural, value : {} }) → cons x.index)
)
in enumerate

12
Prelude/Natural/even
View File

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

33
Prelude/Natural/fold
View File

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

12
Prelude/Natural/isZero
View File

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

12
Prelude/Natural/odd
View File

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

21
Prelude/Natural/package.dhall
View File

@ -1,21 +0,0 @@
{ build =
./build
, enumerate =
./enumerate
, even =
./even
, fold =
./fold
, isZero =
./isZero
, odd =
./odd
, product =
./product
, sum =
./sum
, show =
./show
, toInteger =
./toInteger
}

22
Prelude/Natural/product
View File

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

13
Prelude/Natural/show
View File

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

22
Prelude/Natural/sum
View File

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

16
Prelude/Natural/toDouble
View File

@ -1,16 +0,0 @@
{-
Convert a `Natural` number to the corresponding `Double`
Examples:
```
./toDouble 3 = 3.0
./toDouble 0 = 0.0
```
-}
let toDouble
: Natural → Double
= λ(n : Natural) → Integer/toDouble (Natural/toInteger n)
in toDouble

12
Prelude/Natural/toInteger
View File

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

20
Prelude/Optional/all
View File

@ -1,20 +0,0 @@
{-
Returns `False` if the supplied function returns `False` for a present element
and `True` otherwise:
Examples:
```
./all Natural Natural/even (Some 3) = False
./all Natural Natural/even (None Natural) = True
```
-}
let all
: ∀(a : Type) → (a → Bool) → Optional a → Bool
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : Optional a)
→ Optional/fold a xs Bool f True
in all

20
Prelude/Optional/any
View File

@ -1,20 +0,0 @@
{-
Returns `True` if the supplied function returns `True` for a present element and
`False` otherwise
Examples:
```
./any Natural Natural/even (Some 2) = True
./any Natural Natural/even (None Natural) = False
```
-}
let any
: ∀(a : Type) → (a → Bool) → Optional a → Bool
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : Optional a)
→ Optional/fold a xs Bool f False
in any

36
Prelude/Optional/build
View File

@ -1,36 +0,0 @@
{-
`build` is the inverse of `fold`
Examples:
```
./build
Natural
( λ(optional : Type)
→ λ(some : Natural → optional)
→ λ(none : optional)
→ some 1
)
= Some 1
./build
Natural
( λ(optional : Type)
→ λ(some : Natural → optional)
→ λ(none : optional)
→ none
)
= None Natural
```
-}
let build
: ∀(a : Type)
→ ( ∀(optional : Type)
→ ∀(some : a → optional)
→ ∀(none : optional)
→ optional
)
→ Optional a
= Optional/build
in build

28
Prelude/Optional/concat
View File

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

32
Prelude/Optional/filter
View File

@ -1,32 +0,0 @@
{-
Only keep an `Optional` element if the supplied function returns `True`
Examples:
```
./filter Natural Natural/even (Some 2)
= Some 2
./filter Natural Natural/odd (Some 2)
= None Natural
```
-}
let filter
: ∀(a : Type) → (a → Bool) → Optional a → Optional a
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : Optional a)
→ Optional/build
a
( λ(optional : Type)
→ λ(some : a → optional)
→ λ(none : optional)
→ Optional/fold
a
xs
optional
(λ(x : a) → if f x then some x else none)
none
)
in filter

21
Prelude/Optional/fold
View File

@ -1,21 +0,0 @@
{-
`fold` is the primitive function for consuming `Optional` values
Examples:
```
./fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 = 2
./fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 = 0
```
-}
let fold
: ∀(a : Type)
→ Optional a
→ ∀(optional : Type)
→ ∀(some : a → optional)
→ ∀(none : optional)
→ optional
= Optional/fold
in fold

28
Prelude/Optional/head
View File

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

28
Prelude/Optional/last
View File

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

18
Prelude/Optional/length
View File

@ -1,18 +0,0 @@
{-
Returns `1` if the `Optional` value is present and `0` if the value is absent
Examples:
```
./length Natural (Some 2) = 1
./length Natural (None Natural) = 0
```
-}
let length
: ∀(a : Type) → Optional a → Natural
= λ(a : Type)
→ λ(xs : Optional a)
→ Optional/fold a xs Natural (λ(_ : a) → 1) 0
in length

20
Prelude/Optional/map
View File

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

18
Prelude/Optional/null
View File

@ -1,18 +0,0 @@
{-
Returns `True` if the `Optional` value is absent and `False` if present
Examples:
```
./null Natural (Some 2) = False
./null Natural (None Natural) = True
```
-}
let null
: ∀(a : Type) → Optional a → Bool
= λ(a : Type)
→ λ(xs : Optional a)
→ Optional/fold a xs Bool (λ(_ : a) → False) True
in null

27
Prelude/Optional/package.dhall
View File

@ -1,27 +0,0 @@
{ all =
./all
, any =
./any
, build =
./build
, concat =
./concat
, filter =
./filter
, fold =
./fold
, head =
./head
, last =
./last
, length =
./length
, map =
./map
, null =
./null
, toList =
./toList
, unzip =
./unzip
}

18
Prelude/Optional/toList
View File

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

38
Prelude/Optional/unzip
View File

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

17
Prelude/Text/concat
View File

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

21
Prelude/Text/concatMap
View File

@ -1,21 +0,0 @@
{-
Transform each value in a `List` into `Text` and concatenate the result
Examples:
```
./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ]
= "0 1 2 "
./concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural)
= ""
```
-}
let concatMap
: ∀(a : Type) → (a → Text) → List a → Text
= λ(a : Type)
→ λ(f : a → Text)
→ λ(xs : List a)
→ List/fold a xs Text (λ(x : a) → λ(y : Text) → f x ++ y) ""
in concatMap

47
Prelude/Text/concatMapSep
View File

@ -1,47 +0,0 @@
{-
Transform each value in a `List` to `Text` and then concatenate them with a
separator in between each value
Examples:
```
./concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] = "0, 1, 2"
./concatMapSep ", " Natural Natural/show ([] : List Natural) = ""
```
-}
let concatMapSep
: ∀(separator : Text) → ∀(a : Type) → (a → Text) → List a → Text
= λ(separator : Text)
→ λ(a : Type)
→ λ(f : a → Text)
→ λ(elements : List a)
→ let status =
List/fold
a
elements
< Empty : {} | NonEmpty : Text >
( λ(element : a)
→ λ(status : < Empty : {} | NonEmpty : Text >)
→ merge
{ Empty =
λ(_ : {}) → < NonEmpty = f element | Empty : {} >
, NonEmpty =
λ(result : Text)
→ < NonEmpty =
f element ++ separator ++ result
| Empty :
{}
>
}
status
: < Empty : {} | NonEmpty : Text >
)
< Empty = {=} | NonEmpty : Text >
in merge
{ Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result }
status
: Text
in concatMapSep

44
Prelude/Text/concatSep
View File

@ -1,44 +0,0 @@
{-
Concatenate a `List` of `Text` values with a separator in between each value
Examples:
```
./concatSep ", " [ "ABC", "DEF", "GHI" ] = "ABC, DEF, GHI"
./concatSep ", " ([] : List Text) = ""
```
-}
let concatSep
: ∀(separator : Text) → ∀(elements : List Text) → Text
= λ(separator : Text)
→ λ(elements : List Text)
→ let status =
List/fold
Text
elements
< Empty : {} | NonEmpty : Text >
( λ(element : Text)
→ λ(status : < Empty : {} | NonEmpty : Text >)
→ merge
{ Empty =
λ(_ : {}) → < NonEmpty = element | Empty : {} >
, NonEmpty =
λ(result : Text)
→ < NonEmpty =
element ++ separator ++ result
| Empty :
{}
>
}
status
: < Empty : {} | NonEmpty : Text >
)
< Empty = {=} | NonEmpty : Text >
in merge
{ Empty = λ(_ : {}) → "", NonEmpty = λ(result : Text) → result }
status
: Text
in concatSep

9
Prelude/Text/package.dhall
View File

@ -1,9 +0,0 @@
{ concat =
./concat
, concatMap =
./concatMap
, concatMapSep =
./concatMapSep
, concatSep =
./concatSep
}

20
Prelude/package.dhall
View File

@ -1,19 +1 @@
{ `Bool` =
./Bool/package.dhall
, `Double` =
./Double/package.dhall
, Function =
./Function/package.dhall
, `Integer` =
./Integer/package.dhall
, `List` =
./List/package.dhall
, `Natural` =
./Natural/package.dhall
, `Optional` =
./Optional/package.dhall
, JSON =
./JSON/package.dhall
, `Text` =
./Text/package.dhall
}
https://raw.githubusercontent.com/dhall-lang/Prelude/e9c90396c02f9eb0fe66c00c544615cbfa068f34/package.dhall sha256:9fbb8a6db3360fa30086ea8462dc36087f0e4f87af2a1f802a8befdc5a08f809

61
dhall.cabal
View File

@ -24,65 +24,8 @@ Description:
Category: Compiler
Extra-Source-Files:
CHANGELOG.md
Prelude/Bool/and
Prelude/Bool/build
Prelude/Bool/even
Prelude/Bool/fold
Prelude/Bool/not
Prelude/Bool/odd
Prelude/Bool/or
Prelude/Bool/show
Prelude/Double/show
Prelude/Integer/show
Prelude/Integer/toDouble
Prelude/List/all
Prelude/List/any
Prelude/List/build
Prelude/List/concat
Prelude/List/concatMap
Prelude/List/filter
Prelude/List/fold
Prelude/List/generate
Prelude/List/head
Prelude/List/indexed
Prelude/List/iterate
Prelude/List/last
Prelude/List/length
Prelude/List/map
Prelude/List/null
Prelude/List/replicate
Prelude/List/reverse
Prelude/List/shifted
Prelude/List/unzip
Prelude/package.dhall
Prelude/Monoid
Prelude/Natural/build
Prelude/Natural/enumerate
Prelude/Natural/even
Prelude/Natural/fold
Prelude/Natural/isZero
Prelude/Natural/odd
Prelude/Natural/product
Prelude/Natural/show
Prelude/Natural/sum
Prelude/Natural/toDouble
Prelude/Natural/toInteger
Prelude/Optional/all
Prelude/Optional/any
Prelude/Optional/build
Prelude/Optional/concat
Prelude/Optional/filter
Prelude/Optional/fold
Prelude/Optional/head
Prelude/Optional/last
Prelude/Optional/length
Prelude/Optional/map
Prelude/Optional/null
Prelude/Optional/toList
Prelude/Optional/unzip
Prelude/Text/concat
Prelude/Text/concatMap
Prelude/Text/concatMapSep
Prelude/Text/concatSep
tests/format/*.dhall
tests/normalization/tutorial/combineTypes/*.dhall
tests/normalization/tutorial/projection/*.dhall
@ -269,6 +212,8 @@ Test-Suite tasty
containers ,
deepseq >= 1.2.0.1 && < 1.5 ,
dhall ,
directory ,
filepath ,
prettyprinter ,
QuickCheck >= 2.10 && < 2.13,
quickcheck-instances >= 0.3.12 && < 0.4 ,

4
src/Dhall/Core.hs
View File

@ -1721,7 +1721,9 @@ normalizeWith ctx e0 = loop (denote e0)
decide (TextLit m) (TextLit n) = TextLit (m <> n)
decide l r = TextAppend l r
List -> List
ListLit t es -> ListLit t' es'
ListLit t es
| Data.Sequence.null es -> ListLit t' es'
| otherwise -> ListLit Nothing es'
where
t' = fmap loop t
es' = fmap loop es

7
tests/Normalization.hs
View File

@ -246,7 +246,9 @@ should name basename =
case Dhall.TypeCheck.typeOf actualResolved of
Left err -> Control.Exception.throwIO err
Right _ -> return ()
let actualNormalized = Dhall.Core.normalize actualResolved :: Expr X X
let actualNormalized =
Dhall.Core.alphaNormalize
(Dhall.Core.normalize actualResolved :: Expr X X)
expectedExpr <- case Dhall.Parser.exprFromText mempty expectedCode of
Left err -> Control.Exception.throwIO err
@ -257,7 +259,8 @@ should name basename =
Right _ -> return ()
-- Use `denote` instead of `normalize` to enforce that the expected
-- expression is already in normal form
let expectedNormalized = Dhall.Core.denote expectedResolved
let expectedNormalized =
Dhall.Core.alphaNormalize (Dhall.Core.denote expectedResolved)
let message =
"The normalized expression did not match the expected output"

9
tests/Tests.hs
View File

@ -8,8 +8,12 @@ import Tutorial (tutorialTests)
import TypeCheck (typecheckTests)
import Format (formatTests)
import Import (importTests)
import System.FilePath ((</>))
import Test.Tasty
import qualified System.Directory
import qualified System.Environment
allTests :: TestTree
allTests =
testGroup "Dhall Tests"
@ -24,4 +28,7 @@ allTests =
]
main :: IO ()
main = defaultMain allTests
main = do
pwd <- System.Directory.getCurrentDirectory
System.Environment.setEnv "XDG_CACHE_HOME" (pwd </> ".cache")
defaultMain allTests

2
tests/normalization/examples/Bool/and/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/and [ True, False, True ]
(../../../../../Prelude/package.dhall).`Bool`.and [ True, False, True ]

2
tests/normalization/examples/Bool/and/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/and ([] : List Bool)
(../../../../../Prelude/package.dhall).`Bool`.and ([] : List Bool)

2
tests/normalization/examples/Bool/build/0A.dhall
View File

@ -1,2 +1,2 @@
../../../../../Prelude/Bool/build
(../../../../../Prelude/package.dhall).`Bool`.build
(λ(bool : Type) → λ(true : bool) → λ(false : bool) → true)

2
tests/normalization/examples/Bool/build/1A.dhall
View File

@ -1,2 +1,2 @@
../../../../../Prelude/Bool/build
(../../../../../Prelude/package.dhall).`Bool`.build
(λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)

2
tests/normalization/examples/Bool/even/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/even [ False, True, False ]
(../../../../../Prelude/package.dhall).`Bool`.even [ False, True, False ]

2
tests/normalization/examples/Bool/even/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/even [ False, True ]
(../../../../../Prelude/package.dhall).`Bool`.even [ False, True ]

2
tests/normalization/examples/Bool/even/2A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/even [ False ]
(../../../../../Prelude/package.dhall).`Bool`.even [ False ]

2
tests/normalization/examples/Bool/even/3A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/even ([] : List Bool)
(../../../../../Prelude/package.dhall).`Bool`.even ([] : List Bool)

2
tests/normalization/examples/Bool/fold/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/fold True Natural 0 1
(../../../../../Prelude/package.dhall).`Bool`.fold True Natural 0 1

2
tests/normalization/examples/Bool/fold/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/fold False Natural 0 1
(../../../../../Prelude/package.dhall).`Bool`.fold False Natural 0 1

2
tests/normalization/examples/Bool/not/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/not True
(../../../../../Prelude/package.dhall).`Bool`.not True

2
tests/normalization/examples/Bool/not/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/not False
(../../../../../Prelude/package.dhall).`Bool`.not False

2
tests/normalization/examples/Bool/odd/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/odd [ True, False, True ]
(../../../../../Prelude/package.dhall).`Bool`.odd [ True, False, True ]

2
tests/normalization/examples/Bool/odd/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/odd [ True, False ]
(../../../../../Prelude/package.dhall).`Bool`.odd [ True, False ]

2
tests/normalization/examples/Bool/odd/2A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/odd [ True ]
(../../../../../Prelude/package.dhall).`Bool`.odd [ True ]

2
tests/normalization/examples/Bool/odd/3A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/odd ([] : List Bool)
(../../../../../Prelude/package.dhall).`Bool`.odd ([] : List Bool)

2
tests/normalization/examples/Bool/or/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/or [ True, False, True ]
(../../../../../Prelude/package.dhall).`Bool`.or [ True, False, True ]

2
tests/normalization/examples/Bool/or/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/or ([] : List Bool)
(../../../../../Prelude/package.dhall).`Bool`.or ([] : List Bool)

2
tests/normalization/examples/Bool/show/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/show True
(../../../../../Prelude/package.dhall).`Bool`.show True

2
tests/normalization/examples/Bool/show/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Bool/show False
(../../../../../Prelude/package.dhall).`Bool`.show False

2
tests/normalization/examples/Double/show/0A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Double/show -3.1
(../../../../../Prelude/package.dhall).`Double`.show -3.1

2
tests/normalization/examples/Double/show/1A.dhall
View File

@ -1 +1 @@
../../../../../Prelude/Double/show 0.4
(../../../../../Prelude/package.dhall).`Double`.show 0.4

Some files were not shown because too many files have changed in this diff Show More