Permalink
Browse files

Migrate Prelude into `dhall-lang` repository (#247)

... as suggested here:

#240 (comment)
  • Loading branch information...
Gabriel439 committed Oct 21, 2018
1 parent cab6775 commit 0a7f596d03b3ea760a96a8e03935f4baa64274e1
Showing with 1,780 additions and 8 deletions.
  1. +6 −8 .github/CONTRIBUTING.md
  2. +18 −0 Prelude/Bool/and
  3. +17 −0 Prelude/Bool/build
  4. +22 −0 Prelude/Bool/even
  5. +20 −0 Prelude/Bool/fold
  6. +12 −0 Prelude/Bool/not
  7. +22 −0 Prelude/Bool/odd
  8. +18 −0 Prelude/Bool/or
  9. +17 −0 Prelude/Bool/package.dhall
  10. +13 −0 Prelude/Bool/show
  11. +1 −0 Prelude/Double/package.dhall
  12. +13 −0 Prelude/Double/show
  13. +21 −0 Prelude/Function/compose
  14. +1 −0 Prelude/Function/package.dhall
  15. +1 −0 Prelude/Integer/package.dhall
  16. +14 −0 Prelude/Integer/show
  17. +12 −0 Prelude/Integer/toDouble
  18. +32 −0 Prelude/JSON/Nesting
  19. +69 −0 Prelude/JSON/Tagged
  20. +17 −0 Prelude/JSON/keyText
  21. +20 −0 Prelude/JSON/keyValue
  22. +1 −0 Prelude/JSON/package.dhall
  23. +20 −0 Prelude/List/all
  24. +20 −0 Prelude/List/any
  25. +32 −0 Prelude/List/build
  26. +42 −0 Prelude/List/concat
  27. +28 −0 Prelude/List/concatMap
  28. +30 −0 Prelude/List/filter
  29. +46 −0 Prelude/List/fold
  30. +38 −0 Prelude/List/generate
  31. +12 −0 Prelude/List/head
  32. +21 −0 Prelude/List/indexed
  33. +43 −0 Prelude/List/iterate
  34. +12 −0 Prelude/List/last
  35. +12 −0 Prelude/List/length
  36. +27 −0 Prelude/List/map
  37. +16 −0 Prelude/List/null
  38. +39 −0 Prelude/List/package.dhall
  39. +24 −0 Prelude/List/replicate
  40. +12 −0 Prelude/List/reverse
  41. +90 −0 Prelude/List/shifted
  42. +55 −0 Prelude/List/unzip
  43. +39 −0 Prelude/Monoid
  44. +33 −0 Prelude/Natural/build
  45. +36 −0 Prelude/Natural/enumerate
  46. +12 −0 Prelude/Natural/even
  47. +33 −0 Prelude/Natural/fold
  48. +12 −0 Prelude/Natural/isZero
  49. +12 −0 Prelude/Natural/odd
  50. +23 −0 Prelude/Natural/package.dhall
  51. +22 −0 Prelude/Natural/product
  52. +13 −0 Prelude/Natural/show
  53. +22 −0 Prelude/Natural/sum
  54. +16 −0 Prelude/Natural/toDouble
  55. +12 −0 Prelude/Natural/toInteger
  56. +20 −0 Prelude/Optional/all
  57. +20 −0 Prelude/Optional/any
  58. +36 −0 Prelude/Optional/build
  59. +28 −0 Prelude/Optional/concat
  60. +32 −0 Prelude/Optional/filter
  61. +21 −0 Prelude/Optional/fold
  62. +28 −0 Prelude/Optional/head
  63. +28 −0 Prelude/Optional/last
  64. +18 −0 Prelude/Optional/length
  65. +20 −0 Prelude/Optional/map
  66. +18 −0 Prelude/Optional/null
  67. +27 −0 Prelude/Optional/package.dhall
  68. +18 −0 Prelude/Optional/toList
  69. +38 −0 Prelude/Optional/unzip
  70. +17 −0 Prelude/Text/concat
  71. +21 −0 Prelude/Text/concatMap
  72. +47 −0 Prelude/Text/concatMapSep
  73. +44 −0 Prelude/Text/concatSep
  74. +9 −0 Prelude/Text/package.dhall
  75. +19 −0 Prelude/package.dhall
@@ -6,9 +6,7 @@ This repository hosts language-independent features of the Dhall ecosystem:
* The [Dhall standard][standard] grammar and semantics
* [Dhall infrastructure][infrastructure]
The one exception is the [Prelude][prelude], which lives in a separate
repository for ease of distribution.
* The [Prelude][prelude] of shared utility functions
Issues on this repository typically discuss language design and proposed
changes to the language that are not specific to an integration.
@@ -75,10 +73,10 @@ your idea and if your idea is approved then you can ask somebody (including
## How do changes get approved?
Changes only require approval if they change the [standard][standard]. Anybody
with the "commit bit" (i.e. write access to this repository) can merge a pull
request after a 24 hour waiting period. See below for more details about how
to obtain the commit bit.
Changes only require approval if they change the [standard][standard] or
[Prelude][prelude]. Anybody with the "commit bit" (i.e. write access to this
repository) can merge a pull request after a 24 hour waiting period. See below
for more details about how to obtain the commit bit.
Language changes are voted on by actively maintained implementations of the
Dhall language. Each implementation gets one vote.
@@ -140,9 +138,9 @@ Learn by doing and get your hands dirty!
[infrastructure]: https://github.com/dhall-lang/dhall-lang/tree/master/nixops
[standard]: https://github.com/dhall-lang/dhall-lang/tree/master/standard
[prelude]: https://github.com/dhall-lang/dhall-lang/tree/master/Prelude
[dhall-haskell-issues]: https://github.com/dhall-lang/dhall-haskell/issues
[dhall-lang-issues]: https://github.com/dhall-lang/dhall-lang/issues
[dhall-lang-pulls]: https://github.com/dhall-lang/dhall-lang/pulls
[dhall-json-issues]: https://github.com/dhall-lang/dhall-json/issues
[stack-overflow]: https://stackoverflow.com/
[prelude]: https://github.com/dhall-lang/Prelude
@@ -0,0 +1,18 @@
{-
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
@@ -0,0 +1,17 @@
{-
`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
@@ -0,0 +1,22 @@
{-
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
@@ -0,0 +1,20 @@
{-
`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
@@ -0,0 +1,12 @@
{-
Flip the value of a `Bool`
Examples:
```
./not True = False
./not False = True
```
-}
let not : Bool → Bool = λ(b : Bool) → b == False in not
@@ -0,0 +1,22 @@
{-
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
@@ -0,0 +1,18 @@
{-
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
@@ -0,0 +1,17 @@
{ and =
./and
, build =
./build
, even =
./even
, fold =
./fold
, not =
./not
, odd =
./odd
, or =
./or
, show =
./show
}
@@ -0,0 +1,13 @@
{-
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
@@ -0,0 +1 @@
{ show = ./show }
@@ -0,0 +1,13 @@
{-
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
@@ -0,0 +1,21 @@
{-
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
@@ -0,0 +1 @@
{ compose = ./compose }
@@ -0,0 +1 @@
{ show = ./show, toDouble = ./toDouble }
@@ -0,0 +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 and a leading
`+` sign if non-negative)
Examples:
```
./show -3 = "-3"
./show +0 = "+0"
```
-}
let show : Integer → Text = Integer/show in show
@@ -0,0 +1,12 @@
{-
Convert an `Integer` to the corresponding `Double`
Examples:
```
./toDouble -3 = -3.0
./toDouble +2 = 2.0
```
-}
let toDouble : Integer → Double = Integer/toDouble in toDouble
@@ -0,0 +1,32 @@
{-
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
@@ -0,0 +1,69 @@
{-
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
@@ -0,0 +1,17 @@
{-
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
Oops, something went wrong.

0 comments on commit 0a7f596

Please sign in to comment.