From 03d56ed227ee199bb8fcb257985164193e2cedda Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Mon, 10 Sep 2018 20:21:04 -0700 Subject: [PATCH] Change `Prelude/` directory to be a submodule Now that there is a separate git repository for the Prelude, we can use it as a submodule instead of mirroring the files between the two repositories --- .gitmodules | 3 ++ Prelude | 1 + Prelude/Bool/and | 18 ------- Prelude/Bool/build | 17 ------- Prelude/Bool/even | 22 --------- Prelude/Bool/fold | 20 -------- Prelude/Bool/not | 12 ----- Prelude/Bool/odd | 22 --------- Prelude/Bool/or | 18 ------- Prelude/Bool/package.dhall | 17 ------- Prelude/Bool/show | 13 ----- Prelude/Double/package.dhall | 1 - Prelude/Double/show | 13 ----- Prelude/Function/compose | 21 -------- Prelude/Function/package.dhall | 1 - Prelude/Integer/package.dhall | 1 - Prelude/Integer/show | 14 ------ Prelude/Integer/toDouble | 12 ----- Prelude/JSON/Nesting | 32 ------------ Prelude/JSON/Tagged | 69 -------------------------- Prelude/JSON/keyText | 17 ------- Prelude/JSON/keyValue | 20 -------- Prelude/JSON/package.dhall | 1 - Prelude/List/all | 20 -------- Prelude/List/any | 20 -------- Prelude/List/build | 32 ------------ Prelude/List/concat | 42 ---------------- Prelude/List/concatMap | 28 ----------- Prelude/List/filter | 30 ------------ Prelude/List/fold | 46 ----------------- Prelude/List/generate | 38 -------------- Prelude/List/head | 12 ----- Prelude/List/indexed | 21 -------- Prelude/List/iterate | 43 ---------------- Prelude/List/last | 12 ----- Prelude/List/length | 12 ----- Prelude/List/map | 27 ---------- Prelude/List/null | 16 ------ Prelude/List/package.dhall | 39 --------------- Prelude/List/replicate | 24 --------- Prelude/List/reverse | 12 ----- Prelude/List/shifted | 90 ---------------------------------- Prelude/List/unzip | 55 --------------------- Prelude/Monoid | 39 --------------- Prelude/Natural/build | 33 ------------- Prelude/Natural/enumerate | 36 -------------- Prelude/Natural/even | 12 ----- Prelude/Natural/fold | 33 ------------- Prelude/Natural/isZero | 12 ----- Prelude/Natural/odd | 12 ----- Prelude/Natural/package.dhall | 21 -------- Prelude/Natural/product | 22 --------- Prelude/Natural/show | 13 ----- Prelude/Natural/sum | 22 --------- Prelude/Natural/toDouble | 16 ------ Prelude/Natural/toInteger | 12 ----- Prelude/Optional/all | 20 -------- Prelude/Optional/any | 20 -------- Prelude/Optional/build | 36 -------------- Prelude/Optional/concat | 28 ----------- Prelude/Optional/filter | 32 ------------ Prelude/Optional/fold | 21 -------- Prelude/Optional/head | 28 ----------- Prelude/Optional/last | 28 ----------- Prelude/Optional/length | 18 ------- Prelude/Optional/map | 20 -------- Prelude/Optional/null | 18 ------- Prelude/Optional/package.dhall | 27 ---------- Prelude/Optional/toList | 18 ------- Prelude/Optional/unzip | 38 -------------- Prelude/Text/concat | 17 ------- Prelude/Text/concatMap | 21 -------- Prelude/Text/concatMapSep | 47 ------------------ Prelude/Text/concatSep | 44 ----------------- Prelude/Text/package.dhall | 9 ---- Prelude/package.dhall | 19 ------- 76 files changed, 4 insertions(+), 1772 deletions(-) create mode 100644 .gitmodules create mode 160000 Prelude delete mode 100644 Prelude/Bool/and delete mode 100644 Prelude/Bool/build delete mode 100644 Prelude/Bool/even delete mode 100644 Prelude/Bool/fold delete mode 100644 Prelude/Bool/not delete mode 100644 Prelude/Bool/odd delete mode 100644 Prelude/Bool/or delete mode 100644 Prelude/Bool/package.dhall delete mode 100644 Prelude/Bool/show delete mode 100644 Prelude/Double/package.dhall delete mode 100644 Prelude/Double/show delete mode 100644 Prelude/Function/compose delete mode 100644 Prelude/Function/package.dhall delete mode 100644 Prelude/Integer/package.dhall delete mode 100644 Prelude/Integer/show delete mode 100644 Prelude/Integer/toDouble delete mode 100644 Prelude/JSON/Nesting delete mode 100644 Prelude/JSON/Tagged delete mode 100644 Prelude/JSON/keyText delete mode 100644 Prelude/JSON/keyValue delete mode 100644 Prelude/JSON/package.dhall delete mode 100644 Prelude/List/all delete mode 100644 Prelude/List/any delete mode 100644 Prelude/List/build delete mode 100644 Prelude/List/concat delete mode 100644 Prelude/List/concatMap delete mode 100644 Prelude/List/filter delete mode 100644 Prelude/List/fold delete mode 100644 Prelude/List/generate delete mode 100644 Prelude/List/head delete mode 100644 Prelude/List/indexed delete mode 100644 Prelude/List/iterate delete mode 100644 Prelude/List/last delete mode 100644 Prelude/List/length delete mode 100644 Prelude/List/map delete mode 100644 Prelude/List/null delete mode 100644 Prelude/List/package.dhall delete mode 100644 Prelude/List/replicate delete mode 100644 Prelude/List/reverse delete mode 100644 Prelude/List/shifted delete mode 100644 Prelude/List/unzip delete mode 100644 Prelude/Monoid delete mode 100644 Prelude/Natural/build delete mode 100644 Prelude/Natural/enumerate delete mode 100644 Prelude/Natural/even delete mode 100644 Prelude/Natural/fold delete mode 100644 Prelude/Natural/isZero delete mode 100644 Prelude/Natural/odd delete mode 100644 Prelude/Natural/package.dhall delete mode 100644 Prelude/Natural/product delete mode 100644 Prelude/Natural/show delete mode 100644 Prelude/Natural/sum delete mode 100644 Prelude/Natural/toDouble delete mode 100644 Prelude/Natural/toInteger delete mode 100644 Prelude/Optional/all delete mode 100644 Prelude/Optional/any delete mode 100644 Prelude/Optional/build delete mode 100644 Prelude/Optional/concat delete mode 100644 Prelude/Optional/filter delete mode 100644 Prelude/Optional/fold delete mode 100644 Prelude/Optional/head delete mode 100644 Prelude/Optional/last delete mode 100644 Prelude/Optional/length delete mode 100644 Prelude/Optional/map delete mode 100644 Prelude/Optional/null delete mode 100644 Prelude/Optional/package.dhall delete mode 100644 Prelude/Optional/toList delete mode 100644 Prelude/Optional/unzip delete mode 100644 Prelude/Text/concat delete mode 100644 Prelude/Text/concatMap delete mode 100644 Prelude/Text/concatMapSep delete mode 100644 Prelude/Text/concatSep delete mode 100644 Prelude/Text/package.dhall delete mode 100644 Prelude/package.dhall diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 000000000..659a4aafa --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "Prelude"] + path = Prelude + url = https://github.com/dhall-lang/Prelude.git diff --git a/Prelude b/Prelude new file mode 160000 index 000000000..4e565d6ed --- /dev/null +++ b/Prelude @@ -0,0 +1 @@ +Subproject commit 4e565d6ed6a5bcb5a8afe1f6829fec59cf34f829 diff --git a/Prelude/Bool/and b/Prelude/Bool/and deleted file mode 100644 index 3d8633876..000000000 --- a/Prelude/Bool/and +++ /dev/null @@ -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 diff --git a/Prelude/Bool/build b/Prelude/Bool/build deleted file mode 100644 index 85ca48406..000000000 --- a/Prelude/Bool/build +++ /dev/null @@ -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 diff --git a/Prelude/Bool/even b/Prelude/Bool/even deleted file mode 100644 index b4eb5e953..000000000 --- a/Prelude/Bool/even +++ /dev/null @@ -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 diff --git a/Prelude/Bool/fold b/Prelude/Bool/fold deleted file mode 100644 index e8e2b5610..000000000 --- a/Prelude/Bool/fold +++ /dev/null @@ -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 diff --git a/Prelude/Bool/not b/Prelude/Bool/not deleted file mode 100644 index c0599a62e..000000000 --- a/Prelude/Bool/not +++ /dev/null @@ -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 diff --git a/Prelude/Bool/odd b/Prelude/Bool/odd deleted file mode 100644 index 8ad485a7d..000000000 --- a/Prelude/Bool/odd +++ /dev/null @@ -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 diff --git a/Prelude/Bool/or b/Prelude/Bool/or deleted file mode 100644 index e3ae1e2d1..000000000 --- a/Prelude/Bool/or +++ /dev/null @@ -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 diff --git a/Prelude/Bool/package.dhall b/Prelude/Bool/package.dhall deleted file mode 100644 index c7769405e..000000000 --- a/Prelude/Bool/package.dhall +++ /dev/null @@ -1,17 +0,0 @@ -{ and = - ./and -, build = - ./build -, even = - ./even -, fold = - ./fold -, not = - ./not -, odd = - ./odd -, or = - ./or -, show = - ./show -} diff --git a/Prelude/Bool/show b/Prelude/Bool/show deleted file mode 100644 index 18018751a..000000000 --- a/Prelude/Bool/show +++ /dev/null @@ -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 diff --git a/Prelude/Double/package.dhall b/Prelude/Double/package.dhall deleted file mode 100644 index 46f027228..000000000 --- a/Prelude/Double/package.dhall +++ /dev/null @@ -1 +0,0 @@ -{ show = ./show } diff --git a/Prelude/Double/show b/Prelude/Double/show deleted file mode 100644 index 36aae657c..000000000 --- a/Prelude/Double/show +++ /dev/null @@ -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 diff --git a/Prelude/Function/compose b/Prelude/Function/compose deleted file mode 100644 index bae6a662b..000000000 --- a/Prelude/Function/compose +++ /dev/null @@ -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 diff --git a/Prelude/Function/package.dhall b/Prelude/Function/package.dhall deleted file mode 100644 index ecb64da12..000000000 --- a/Prelude/Function/package.dhall +++ /dev/null @@ -1 +0,0 @@ -{ compose = ./compose } diff --git a/Prelude/Integer/package.dhall b/Prelude/Integer/package.dhall deleted file mode 100644 index 46f027228..000000000 --- a/Prelude/Integer/package.dhall +++ /dev/null @@ -1 +0,0 @@ -{ show = ./show } diff --git a/Prelude/Integer/show b/Prelude/Integer/show deleted file mode 100644 index 13b6eb8d6..000000000 --- a/Prelude/Integer/show +++ /dev/null @@ -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 diff --git a/Prelude/Integer/toDouble b/Prelude/Integer/toDouble deleted file mode 100644 index 8b30c78b6..000000000 --- a/Prelude/Integer/toDouble +++ /dev/null @@ -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 diff --git a/Prelude/JSON/Nesting b/Prelude/JSON/Nesting deleted file mode 100644 index bf0de5053..000000000 --- a/Prelude/JSON/Nesting +++ /dev/null @@ -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 diff --git a/Prelude/JSON/Tagged b/Prelude/JSON/Tagged deleted file mode 100644 index 9b731d6b4..000000000 --- a/Prelude/JSON/Tagged +++ /dev/null @@ -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 diff --git a/Prelude/JSON/keyText b/Prelude/JSON/keyText deleted file mode 100644 index eabb77daa..000000000 --- a/Prelude/JSON/keyText +++ /dev/null @@ -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 diff --git a/Prelude/JSON/keyValue b/Prelude/JSON/keyValue deleted file mode 100644 index 0e5e36238..000000000 --- a/Prelude/JSON/keyValue +++ /dev/null @@ -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 diff --git a/Prelude/JSON/package.dhall b/Prelude/JSON/package.dhall deleted file mode 100644 index 9c4b60591..000000000 --- a/Prelude/JSON/package.dhall +++ /dev/null @@ -1 +0,0 @@ -{ keyText = ./keyText, keyValue = ./keyValue } diff --git a/Prelude/List/all b/Prelude/List/all deleted file mode 100644 index f7456d910..000000000 --- a/Prelude/List/all +++ /dev/null @@ -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 diff --git a/Prelude/List/any b/Prelude/List/any deleted file mode 100644 index 225da845f..000000000 --- a/Prelude/List/any +++ /dev/null @@ -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 diff --git a/Prelude/List/build b/Prelude/List/build deleted file mode 100644 index c05572e5e..000000000 --- a/Prelude/List/build +++ /dev/null @@ -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 diff --git a/Prelude/List/concat b/Prelude/List/concat deleted file mode 100644 index 2f7291b76..000000000 --- a/Prelude/List/concat +++ /dev/null @@ -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 diff --git a/Prelude/List/concatMap b/Prelude/List/concatMap deleted file mode 100644 index f54f491ea..000000000 --- a/Prelude/List/concatMap +++ /dev/null @@ -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 diff --git a/Prelude/List/filter b/Prelude/List/filter deleted file mode 100644 index 3edeb5872..000000000 --- a/Prelude/List/filter +++ /dev/null @@ -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 diff --git a/Prelude/List/fold b/Prelude/List/fold deleted file mode 100644 index f0cf52095..000000000 --- a/Prelude/List/fold +++ /dev/null @@ -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 diff --git a/Prelude/List/generate b/Prelude/List/generate deleted file mode 100644 index 3397fa8b2..000000000 --- a/Prelude/List/generate +++ /dev/null @@ -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 diff --git a/Prelude/List/head b/Prelude/List/head deleted file mode 100644 index 0e2186ebd..000000000 --- a/Prelude/List/head +++ /dev/null @@ -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 diff --git a/Prelude/List/indexed b/Prelude/List/indexed deleted file mode 100644 index 06bb22714..000000000 --- a/Prelude/List/indexed +++ /dev/null @@ -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 diff --git a/Prelude/List/iterate b/Prelude/List/iterate deleted file mode 100644 index fd6e11d00..000000000 --- a/Prelude/List/iterate +++ /dev/null @@ -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 diff --git a/Prelude/List/last b/Prelude/List/last deleted file mode 100644 index ca0cf7bf1..000000000 --- a/Prelude/List/last +++ /dev/null @@ -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 diff --git a/Prelude/List/length b/Prelude/List/length deleted file mode 100644 index 397d0ce9c..000000000 --- a/Prelude/List/length +++ /dev/null @@ -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 diff --git a/Prelude/List/map b/Prelude/List/map deleted file mode 100644 index e82c40de4..000000000 --- a/Prelude/List/map +++ /dev/null @@ -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 diff --git a/Prelude/List/null b/Prelude/List/null deleted file mode 100644 index e38f92557..000000000 --- a/Prelude/List/null +++ /dev/null @@ -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 diff --git a/Prelude/List/package.dhall b/Prelude/List/package.dhall deleted file mode 100644 index 9555bbb21..000000000 --- a/Prelude/List/package.dhall +++ /dev/null @@ -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 -} diff --git a/Prelude/List/replicate b/Prelude/List/replicate deleted file mode 100644 index 3f2fede69..000000000 --- a/Prelude/List/replicate +++ /dev/null @@ -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 diff --git a/Prelude/List/reverse b/Prelude/List/reverse deleted file mode 100644 index bed5ddc6c..000000000 --- a/Prelude/List/reverse +++ /dev/null @@ -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 diff --git a/Prelude/List/shifted b/Prelude/List/shifted deleted file mode 100644 index 80551dc41..000000000 --- a/Prelude/List/shifted +++ /dev/null @@ -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 diff --git a/Prelude/List/unzip b/Prelude/List/unzip deleted file mode 100644 index 8293ced27..000000000 --- a/Prelude/List/unzip +++ /dev/null @@ -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 diff --git a/Prelude/Monoid b/Prelude/Monoid deleted file mode 100644 index fe5bd7a06..000000000 --- a/Prelude/Monoid +++ /dev/null @@ -1,39 +0,0 @@ -{- -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 diff --git a/Prelude/Natural/build b/Prelude/Natural/build deleted file mode 100644 index a01ef7ebd..000000000 --- a/Prelude/Natural/build +++ /dev/null @@ -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 diff --git a/Prelude/Natural/enumerate b/Prelude/Natural/enumerate deleted file mode 100644 index c90612f62..000000000 --- a/Prelude/Natural/enumerate +++ /dev/null @@ -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 diff --git a/Prelude/Natural/even b/Prelude/Natural/even deleted file mode 100644 index b9e7b1e7d..000000000 --- a/Prelude/Natural/even +++ /dev/null @@ -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 diff --git a/Prelude/Natural/fold b/Prelude/Natural/fold deleted file mode 100644 index 3df16be1c..000000000 --- a/Prelude/Natural/fold +++ /dev/null @@ -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 diff --git a/Prelude/Natural/isZero b/Prelude/Natural/isZero deleted file mode 100644 index 0811317f2..000000000 --- a/Prelude/Natural/isZero +++ /dev/null @@ -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 diff --git a/Prelude/Natural/odd b/Prelude/Natural/odd deleted file mode 100644 index 54d5090ac..000000000 --- a/Prelude/Natural/odd +++ /dev/null @@ -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 diff --git a/Prelude/Natural/package.dhall b/Prelude/Natural/package.dhall deleted file mode 100644 index 513cb9713..000000000 --- a/Prelude/Natural/package.dhall +++ /dev/null @@ -1,21 +0,0 @@ -{ build = - ./build -, enumerate = - ./enumerate -, even = - ./even -, fold = - ./fold -, isZero = - ./isZero -, odd = - ./odd -, product = - ./product -, sum = - ./sum -, show = - ./show -, toInteger = - ./toInteger -} diff --git a/Prelude/Natural/product b/Prelude/Natural/product deleted file mode 100644 index dcc5235cd..000000000 --- a/Prelude/Natural/product +++ /dev/null @@ -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 diff --git a/Prelude/Natural/show b/Prelude/Natural/show deleted file mode 100644 index 3e9e6be12..000000000 --- a/Prelude/Natural/show +++ /dev/null @@ -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 diff --git a/Prelude/Natural/sum b/Prelude/Natural/sum deleted file mode 100644 index 0f0f69735..000000000 --- a/Prelude/Natural/sum +++ /dev/null @@ -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 diff --git a/Prelude/Natural/toDouble b/Prelude/Natural/toDouble deleted file mode 100644 index 12f9392a2..000000000 --- a/Prelude/Natural/toDouble +++ /dev/null @@ -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 diff --git a/Prelude/Natural/toInteger b/Prelude/Natural/toInteger deleted file mode 100644 index 1d5387410..000000000 --- a/Prelude/Natural/toInteger +++ /dev/null @@ -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 diff --git a/Prelude/Optional/all b/Prelude/Optional/all deleted file mode 100644 index 0db2c8f2f..000000000 --- a/Prelude/Optional/all +++ /dev/null @@ -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 diff --git a/Prelude/Optional/any b/Prelude/Optional/any deleted file mode 100644 index 172cebc15..000000000 --- a/Prelude/Optional/any +++ /dev/null @@ -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 diff --git a/Prelude/Optional/build b/Prelude/Optional/build deleted file mode 100644 index dde5fa698..000000000 --- a/Prelude/Optional/build +++ /dev/null @@ -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 diff --git a/Prelude/Optional/concat b/Prelude/Optional/concat deleted file mode 100644 index 8bbd36f67..000000000 --- a/Prelude/Optional/concat +++ /dev/null @@ -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 diff --git a/Prelude/Optional/filter b/Prelude/Optional/filter deleted file mode 100644 index 3c0d4eb5e..000000000 --- a/Prelude/Optional/filter +++ /dev/null @@ -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 diff --git a/Prelude/Optional/fold b/Prelude/Optional/fold deleted file mode 100644 index 602fba21d..000000000 --- a/Prelude/Optional/fold +++ /dev/null @@ -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 diff --git a/Prelude/Optional/head b/Prelude/Optional/head deleted file mode 100644 index 9cbce3ca3..000000000 --- a/Prelude/Optional/head +++ /dev/null @@ -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 diff --git a/Prelude/Optional/last b/Prelude/Optional/last deleted file mode 100644 index 8c70d9ef6..000000000 --- a/Prelude/Optional/last +++ /dev/null @@ -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 diff --git a/Prelude/Optional/length b/Prelude/Optional/length deleted file mode 100644 index c8df433a6..000000000 --- a/Prelude/Optional/length +++ /dev/null @@ -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 diff --git a/Prelude/Optional/map b/Prelude/Optional/map deleted file mode 100644 index d08329e0b..000000000 --- a/Prelude/Optional/map +++ /dev/null @@ -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 diff --git a/Prelude/Optional/null b/Prelude/Optional/null deleted file mode 100644 index 6854edb13..000000000 --- a/Prelude/Optional/null +++ /dev/null @@ -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 diff --git a/Prelude/Optional/package.dhall b/Prelude/Optional/package.dhall deleted file mode 100644 index 97a4d0c50..000000000 --- a/Prelude/Optional/package.dhall +++ /dev/null @@ -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 -} diff --git a/Prelude/Optional/toList b/Prelude/Optional/toList deleted file mode 100644 index 6dc7ccb84..000000000 --- a/Prelude/Optional/toList +++ /dev/null @@ -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 diff --git a/Prelude/Optional/unzip b/Prelude/Optional/unzip deleted file mode 100644 index af4b99f99..000000000 --- a/Prelude/Optional/unzip +++ /dev/null @@ -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 diff --git a/Prelude/Text/concat b/Prelude/Text/concat deleted file mode 100644 index 7f14e5ace..000000000 --- a/Prelude/Text/concat +++ /dev/null @@ -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 diff --git a/Prelude/Text/concatMap b/Prelude/Text/concatMap deleted file mode 100644 index 86db318e3..000000000 --- a/Prelude/Text/concatMap +++ /dev/null @@ -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 diff --git a/Prelude/Text/concatMapSep b/Prelude/Text/concatMapSep deleted file mode 100644 index 5d5b0be2d..000000000 --- a/Prelude/Text/concatMapSep +++ /dev/null @@ -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 diff --git a/Prelude/Text/concatSep b/Prelude/Text/concatSep deleted file mode 100644 index d25df3887..000000000 --- a/Prelude/Text/concatSep +++ /dev/null @@ -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 diff --git a/Prelude/Text/package.dhall b/Prelude/Text/package.dhall deleted file mode 100644 index 863d06cd5..000000000 --- a/Prelude/Text/package.dhall +++ /dev/null @@ -1,9 +0,0 @@ -{ concat = - ./concat -, concatMap = - ./concatMap -, concatMapSep = - ./concatMapSep -, concatSep = - ./concatSep -} diff --git a/Prelude/package.dhall b/Prelude/package.dhall deleted file mode 100644 index 7b88b7920..000000000 --- a/Prelude/package.dhall +++ /dev/null @@ -1,19 +0,0 @@ -{ `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 -}