Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
Tidy up prelude (#531)
* run `dhall format` over Prelude

the `let` expressions indented in the old way was a little annoying

* remove usage of `constructors` from example code

Some of the example code in Prelude used the now-removed `constructors`
keyword.  This removes it and runs the example through `dhall format`.
  • Loading branch information
philandstuff committed May 9, 2019
1 parent 092996d commit dbcf50c
Show file tree
Hide file tree
Showing 57 changed files with 541 additions and 558 deletions.
8 changes: 4 additions & 4 deletions Prelude/Bool/and
Expand Up @@ -10,9 +10,9 @@ Examples:
./and ([] : List Bool) = True
```
-}
let and
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True
let and
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True

in and
8 changes: 4 additions & 4 deletions Prelude/Bool/build
Expand Up @@ -9,9 +9,9 @@ Examples:
./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
let build
: (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool
= λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool)
→ f Bool True False

in build
8 changes: 4 additions & 4 deletions Prelude/Bool/even
Expand Up @@ -14,9 +14,9 @@ Examples:
./even ([] : List Bool) = True
```
-}
let even
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True
let even
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True

in even
14 changes: 7 additions & 7 deletions Prelude/Bool/fold
Expand Up @@ -9,12 +9,12 @@ Examples:
./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
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
8 changes: 4 additions & 4 deletions Prelude/Bool/odd
Expand Up @@ -14,9 +14,9 @@ Examples:
./odd ([] : List Bool) = False
```
-}
let odd
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False
let odd
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False

in odd
8 changes: 4 additions & 4 deletions Prelude/Bool/or
Expand Up @@ -10,9 +10,9 @@ Examples:
./or ([] : List Bool) = False
```
-}
let or
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False
let or
: List Bool → Bool
= λ(xs : List Bool)
→ List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False

in or
16 changes: 8 additions & 8 deletions Prelude/Bool/package.dhall
@@ -1,25 +1,25 @@
{ and =
./and sha256:0b2114fa33cd76652e4360f012bc082718944fe4c5b28c975483178f8d9b0a6d
./and sha256:0b2114fa33cd76652e4360f012bc082718944fe4c5b28c975483178f8d9b0a6d
? ./and
, build =
./build sha256:add7cb9acacac705410088d876a7e4488e046a7aded304f06c51accffd7f1b7b
./build sha256:add7cb9acacac705410088d876a7e4488e046a7aded304f06c51accffd7f1b7b
? ./build
, even =
./even sha256:72a05ee550636a3acb768360fa51ba0db0326763e0cf1ceb737f0f3607fc0fe5
./even sha256:72a05ee550636a3acb768360fa51ba0db0326763e0cf1ceb737f0f3607fc0fe5
? ./even
, fold =
./fold sha256:39f60baf3950268c2e849e91dc6279ee41cd6b81892d54020d4fcd2ce30a96ae
./fold sha256:39f60baf3950268c2e849e91dc6279ee41cd6b81892d54020d4fcd2ce30a96ae
? ./fold
, not =
./not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
./not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
? ./not
, odd =
./odd sha256:6360fca3a745de32bd186cc7b71487a6398cd47d5119064eae491872c41d1999
./odd sha256:6360fca3a745de32bd186cc7b71487a6398cd47d5119064eae491872c41d1999
? ./odd
, or =
./or sha256:5c50738e84e1c4fed8343ebd57608500e1b61ac1f502aa52d6d6edb5c20b99e4
./or sha256:5c50738e84e1c4fed8343ebd57608500e1b61ac1f502aa52d6d6edb5c20b99e4
? ./or
, show =
./show sha256:f85f6d2d921c37a2122cb2e2f8a0170e305b699debd0e6df5ef3370d806b5f61
./show sha256:f85f6d2d921c37a2122cb2e2f8a0170e305b699debd0e6df5ef3370d806b5f61
? ./show
}
2 changes: 1 addition & 1 deletion Prelude/Double/package.dhall
@@ -1,4 +1,4 @@
{ show =
./show sha256:ae645813cc4d8505a265df4d7564c95482f62bb3e07fc81681959599b6cee04f
./show sha256:ae645813cc4d8505a265df4d7564c95482f62bb3e07fc81681959599b6cee04f
? ./show
}
18 changes: 9 additions & 9 deletions Prelude/Function/compose
Expand Up @@ -8,14 +8,14 @@ Examples:
= 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)
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
2 changes: 1 addition & 1 deletion Prelude/Function/package.dhall
@@ -1,4 +1,4 @@
{ compose =
./compose sha256:65ad8bbea530b3d8968785a7cf4a9a7976b67059aa15e3b61fcba600a40ae013
./compose sha256:65ad8bbea530b3d8968785a7cf4a9a7976b67059aa15e3b61fcba600a40ae013
? ./compose
}
4 changes: 2 additions & 2 deletions Prelude/Integer/package.dhall
@@ -1,7 +1,7 @@
{ show =
./show sha256:ecf8b0594cd5181bc45d3b7ea0d44d3ba9ad5dac6ec17bb8968beb65f4b1baa9
./show sha256:ecf8b0594cd5181bc45d3b7ea0d44d3ba9ad5dac6ec17bb8968beb65f4b1baa9
? ./show
, toDouble =
./toDouble sha256:77bc5d635dc4d952f37cc96f2a681d5ac503b4e8b21fc00055b1946adb5beda7
./toDouble sha256:77bc5d635dc4d952f37cc96f2a681d5ac503b4e8b21fc00055b1946adb5beda7
? ./toDouble
}
17 changes: 8 additions & 9 deletions Prelude/JSON/Nesting
Expand Up @@ -5,17 +5,16 @@ names
For example, this Dhall code:

```
let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
let Example = < Left : { foo : Natural } | Right : { bar : Bool } >

in let example = constructors Example
let Nesting = < Inline : {} | Nested : Text >

in let Nesting = < Inline : {} | Nested : Text >

in let nesting = constructors Nesting

in { field = "name"
, nesting = nesting.Inline {=}
, contents = example.Left { foo = 2 }
in { field =
"name"
, nesting =
Nesting.Inline {=}
, contents =
Example.Left { foo = 2 }
}
```

Expand Down
38 changes: 18 additions & 20 deletions Prelude/JSON/Tagged
Expand Up @@ -5,33 +5,31 @@ for preserving alternative names
For example, this code:

```
let map = ../List/map
let map = ../List/map

in let Provisioner =
< shell :
{ inline : List Text }
| file :
{ source : Text, destination : Text }
>
let Provisioner =
< shell :
{ inline : List Text }
| file :
{ source : Text, destination : Text }
>

in let provisioner = constructors Provisioner
let Tagged = ./Tagged

in let Tagged = ./Tagged
let Nesting = ./Nesting

in let nesting = constructors ./Nesting

in let wrap
: Provisioner → Tagged Provisioner
= λ(x : Provisioner)
→ { field = "type", nesting = nesting.Nested "params", contents = x }
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
[ Provisioner.shell { inline = [ "echo foo" ] }
, Provisioner.file
{ source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
]
}
Expand Down Expand Up @@ -62,8 +60,8 @@ in { provisioners =
```

-}
let Tagged
: Type → Type
= λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a }
let Tagged
: Type → Type
= λ(a : Type) → { field : Text, nesting : ./Nesting, contents : a }

in Tagged
4 changes: 2 additions & 2 deletions Prelude/JSON/keyText
Expand Up @@ -11,7 +11,7 @@ Example:
```
-}

let keyText =
λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
let keyText =
λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }

in keyText
10 changes: 5 additions & 5 deletions Prelude/JSON/keyValue
Expand Up @@ -11,10 +11,10 @@ Examples:
```
-}

let keyValue =
λ(v : Type)
→ λ(key : Text)
→ λ(value : v)
→ { mapKey = key, mapValue = value }
let keyValue =
λ(v : Type)
→ λ(key : Text)
→ λ(value : v)
→ { mapKey = key, mapValue = value }

in keyValue
4 changes: 2 additions & 2 deletions Prelude/JSON/package.dhall
@@ -1,7 +1,7 @@
{ keyText =
./keyText sha256:f7b6c802ca5764d03d5e9a6e48d9cb167c01392f775d9c2c87b83cdaa60ea0cc
./keyText sha256:f7b6c802ca5764d03d5e9a6e48d9cb167c01392f775d9c2c87b83cdaa60ea0cc
? ./keyText
, keyValue =
./keyValue sha256:a0a97199d280c4cce72ffcbbf93b7ceda0a569cf4d173ac98e0aaaa78034b98c
./keyValue sha256:a0a97199d280c4cce72ffcbbf93b7ceda0a569cf4d173ac98e0aaaa78034b98c
? ./keyValue
}
12 changes: 6 additions & 6 deletions Prelude/List/all
Expand Up @@ -10,11 +10,11 @@ Examples:
./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
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
12 changes: 6 additions & 6 deletions Prelude/List/any
Expand Up @@ -10,11 +10,11 @@ Examples:
./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
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
10 changes: 5 additions & 5 deletions Prelude/List/build
Expand Up @@ -23,10 +23,10 @@ Text
= [] : List Text
```
-}
let build
: ∀(a : Type)
→ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
→ List a
= List/build
let build
: ∀(a : Type)
→ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
→ List a
= List/build

in build
32 changes: 16 additions & 16 deletions Prelude/List/concat
Expand Up @@ -22,21 +22,21 @@ Examples:
./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
)
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

0 comments on commit dbcf50c

Please sign in to comment.