From 04553344b793c29f0d3f3a14e5f8269f19503d28 Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Sat, 13 Oct 2018 08:05:40 -0700 Subject: [PATCH] Import Prelude instead of vendoring the Prelude This uses Dhall's import system to fetch the Prelude so that we don't have to keep a local copy of it --- 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 | 40 +-------- 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 | 20 +---- dhall.cabal | 61 +------------ src/Dhall/Core.hs | 4 +- tests/Normalization.hs | 7 +- tests/Tests.hs | 9 +- .../normalization/examples/Bool/and/0A.dhall | 2 +- .../normalization/examples/Bool/and/1A.dhall | 2 +- .../examples/Bool/build/0A.dhall | 2 +- .../examples/Bool/build/1A.dhall | 2 +- .../normalization/examples/Bool/even/0A.dhall | 2 +- .../normalization/examples/Bool/even/1A.dhall | 2 +- .../normalization/examples/Bool/even/2A.dhall | 2 +- .../normalization/examples/Bool/even/3A.dhall | 2 +- .../normalization/examples/Bool/fold/0A.dhall | 2 +- .../normalization/examples/Bool/fold/1A.dhall | 2 +- .../normalization/examples/Bool/not/0A.dhall | 2 +- .../normalization/examples/Bool/not/1A.dhall | 2 +- .../normalization/examples/Bool/odd/0A.dhall | 2 +- .../normalization/examples/Bool/odd/1A.dhall | 2 +- .../normalization/examples/Bool/odd/2A.dhall | 2 +- .../normalization/examples/Bool/odd/3A.dhall | 2 +- tests/normalization/examples/Bool/or/0A.dhall | 2 +- tests/normalization/examples/Bool/or/1A.dhall | 2 +- .../normalization/examples/Bool/show/0A.dhall | 2 +- .../normalization/examples/Bool/show/1A.dhall | 2 +- .../examples/Double/show/0A.dhall | 2 +- .../examples/Double/show/1A.dhall | 2 +- .../examples/Integer/show/0A.dhall | 2 +- .../examples/Integer/show/1A.dhall | 2 +- .../examples/Integer/toDouble/0A.dhall | 2 +- .../examples/Integer/toDouble/1A.dhall | 2 +- .../normalization/examples/List/all/0A.dhall | 2 +- .../normalization/examples/List/all/1A.dhall | 2 +- .../normalization/examples/List/any/0A.dhall | 2 +- .../normalization/examples/List/any/1A.dhall | 2 +- .../examples/List/build/0A.dhall | 2 +- .../examples/List/build/1A.dhall | 2 +- .../examples/List/concat/0A.dhall | 2 +- .../examples/List/concat/1A.dhall | 2 +- .../examples/List/concatMap/0A.dhall | 2 +- .../examples/List/concatMap/1A.dhall | 2 +- .../examples/List/filter/0A.dhall | 2 +- .../examples/List/filter/1A.dhall | 2 +- .../normalization/examples/List/fold/0A.dhall | 2 +- .../normalization/examples/List/fold/1A.dhall | 2 +- .../normalization/examples/List/fold/2A.dhall | 2 +- .../examples/List/generate/0A.dhall | 2 +- .../examples/List/generate/1A.dhall | 2 +- .../normalization/examples/List/head/0A.dhall | 2 +- .../normalization/examples/List/head/1A.dhall | 2 +- .../examples/List/indexed/0A.dhall | 2 +- .../examples/List/indexed/1A.dhall | 2 +- .../examples/List/iterate/0A.dhall | 2 +- .../examples/List/iterate/1A.dhall | 2 +- .../normalization/examples/List/last/0A.dhall | 2 +- .../normalization/examples/List/last/1A.dhall | 2 +- .../examples/List/length/0A.dhall | 2 +- .../examples/List/length/1A.dhall | 2 +- .../normalization/examples/List/map/0A.dhall | 2 +- .../normalization/examples/List/map/1A.dhall | 2 +- .../normalization/examples/List/null/0A.dhall | 2 +- .../normalization/examples/List/null/1A.dhall | 2 +- .../examples/List/replicate/0A.dhall | 2 +- .../examples/List/replicate/1A.dhall | 2 +- .../examples/List/reverse/0A.dhall | 2 +- .../examples/List/reverse/1A.dhall | 2 +- .../examples/List/shifted/0A.dhall | 2 +- .../examples/List/shifted/1A.dhall | 2 +- .../examples/List/unzip/0A.dhall | 2 +- .../examples/List/unzip/1A.dhall | 2 +- .../examples/Natural/build/0A.dhall | 2 +- .../examples/Natural/build/1A.dhall | 2 +- .../examples/Natural/enumerate/0A.dhall | 2 +- .../examples/Natural/enumerate/1A.dhall | 2 +- .../examples/Natural/even/0A.dhall | 2 +- .../examples/Natural/even/1A.dhall | 2 +- .../examples/Natural/fold/0A.dhall | 2 +- .../examples/Natural/fold/1A.dhall | 2 +- .../examples/Natural/fold/2A.dhall | 2 +- .../examples/Natural/isZero/0A.dhall | 2 +- .../examples/Natural/isZero/1A.dhall | 2 +- .../examples/Natural/odd/0A.dhall | 2 +- .../examples/Natural/odd/1A.dhall | 2 +- .../examples/Natural/product/0A.dhall | 2 +- .../examples/Natural/product/1A.dhall | 2 +- .../examples/Natural/show/0A.dhall | 2 +- .../examples/Natural/show/1A.dhall | 2 +- .../examples/Natural/sum/0A.dhall | 2 +- .../examples/Natural/sum/1A.dhall | 2 +- .../examples/Natural/toDouble/0A.dhall | 2 +- .../examples/Natural/toDouble/1A.dhall | 2 +- .../examples/Natural/toInteger/0A.dhall | 2 +- .../examples/Natural/toInteger/1A.dhall | 2 +- .../examples/Optional/all/0A.dhall | 2 +- .../examples/Optional/all/1A.dhall | 2 +- .../examples/Optional/any/0A.dhall | 2 +- .../examples/Optional/any/1A.dhall | 2 +- .../examples/Optional/build/0A.dhall | 2 +- .../examples/Optional/build/1A.dhall | 2 +- .../examples/Optional/concat/0A.dhall | 2 +- .../examples/Optional/concat/1A.dhall | 2 +- .../examples/Optional/concat/2A.dhall | 2 +- .../examples/Optional/filter/0A.dhall | 2 +- .../examples/Optional/filter/1A.dhall | 2 +- .../examples/Optional/fold/0A.dhall | 2 +- .../examples/Optional/fold/1A.dhall | 2 +- .../examples/Optional/head/0A.dhall | 2 +- .../examples/Optional/head/1A.dhall | 2 +- .../examples/Optional/head/2A.dhall | 2 +- .../examples/Optional/last/0A.dhall | 2 +- .../examples/Optional/last/1A.dhall | 2 +- .../examples/Optional/last/2A.dhall | 2 +- .../examples/Optional/length/0A.dhall | 2 +- .../examples/Optional/length/1A.dhall | 2 +- .../examples/Optional/map/0A.dhall | 2 +- .../examples/Optional/map/1A.dhall | 2 +- .../examples/Optional/null/0A.dhall | 2 +- .../examples/Optional/null/1A.dhall | 2 +- .../examples/Optional/toList/0A.dhall | 2 +- .../examples/Optional/toList/1A.dhall | 2 +- .../examples/Optional/unzip/0A.dhall | 2 +- .../examples/Optional/unzip/1A.dhall | 2 +- .../examples/Text/concat/0A.dhall | 2 +- .../examples/Text/concat/1A.dhall | 2 +- .../examples/Text/concatMap/0A.dhall | 2 +- .../examples/Text/concatMap/1A.dhall | 2 +- .../examples/Text/concatMapSep/0A.dhall | 2 +- .../examples/Text/concatMapSep/1A.dhall | 2 +- .../examples/Text/concatSep/0A.dhall | 2 +- .../examples/Text/concatSep/1A.dhall | 2 +- tests/normalization/remoteSystemsA.dhall | 4 +- tests/typecheck/examples/Monoid/00A.dhall | 2 +- tests/typecheck/examples/Monoid/01A.dhall | 2 +- tests/typecheck/examples/Monoid/02A.dhall | 2 +- tests/typecheck/examples/Monoid/03A.dhall | 2 +- tests/typecheck/examples/Monoid/04A.dhall | 2 +- tests/typecheck/examples/Monoid/05A.dhall | 2 +- tests/typecheck/examples/Monoid/06A.dhall | 2 +- tests/typecheck/examples/Monoid/07A.dhall | 2 +- tests/typecheck/examples/Monoid/08A.dhall | 2 +- tests/typecheck/examples/Monoid/09A.dhall | 2 +- tests/typecheck/examples/Monoid/10A.dhall | 2 +- 215 files changed, 159 insertions(+), 1972 deletions(-) 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/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 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 5307ea7a9..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 index fe5bd7a06..a5854e1ee 100644 --- a/Prelude/Monoid +++ b/Prelude/Monoid @@ -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 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 2150d3edc..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 index 7b88b7920..20f0f4a9e 100644 --- a/Prelude/package.dhall +++ b/Prelude/package.dhall @@ -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 diff --git a/dhall.cabal b/dhall.cabal index cca0a896c..29a8b7dd6 100644 --- a/dhall.cabal +++ b/dhall.cabal @@ -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 , diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs index dfdb0f923..1ec5e8bb4 100644 --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -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 diff --git a/tests/Normalization.hs b/tests/Normalization.hs index 4629117b7..f70ce7ca8 100644 --- a/tests/Normalization.hs +++ b/tests/Normalization.hs @@ -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" diff --git a/tests/Tests.hs b/tests/Tests.hs index 8517800a6..f88b35c99 100644 --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -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 diff --git a/tests/normalization/examples/Bool/and/0A.dhall b/tests/normalization/examples/Bool/and/0A.dhall index 0a1cbacda..fdd0b0ef1 100644 --- a/tests/normalization/examples/Bool/and/0A.dhall +++ b/tests/normalization/examples/Bool/and/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/and [ True, False, True ] +(../../../../../Prelude/package.dhall).`Bool`.and [ True, False, True ] diff --git a/tests/normalization/examples/Bool/and/1A.dhall b/tests/normalization/examples/Bool/and/1A.dhall index ee0f982f2..67a7b9c6d 100644 --- a/tests/normalization/examples/Bool/and/1A.dhall +++ b/tests/normalization/examples/Bool/and/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/and ([] : List Bool) +(../../../../../Prelude/package.dhall).`Bool`.and ([] : List Bool) diff --git a/tests/normalization/examples/Bool/build/0A.dhall b/tests/normalization/examples/Bool/build/0A.dhall index a137a2b8c..f09208ee6 100644 --- a/tests/normalization/examples/Bool/build/0A.dhall +++ b/tests/normalization/examples/Bool/build/0A.dhall @@ -1,2 +1,2 @@ -../../../../../Prelude/Bool/build +(../../../../../Prelude/package.dhall).`Bool`.build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) diff --git a/tests/normalization/examples/Bool/build/1A.dhall b/tests/normalization/examples/Bool/build/1A.dhall index 258093b04..210e3a6fb 100644 --- a/tests/normalization/examples/Bool/build/1A.dhall +++ b/tests/normalization/examples/Bool/build/1A.dhall @@ -1,2 +1,2 @@ -../../../../../Prelude/Bool/build +(../../../../../Prelude/package.dhall).`Bool`.build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) diff --git a/tests/normalization/examples/Bool/even/0A.dhall b/tests/normalization/examples/Bool/even/0A.dhall index 5bb044bac..fcfb3c7ce 100644 --- a/tests/normalization/examples/Bool/even/0A.dhall +++ b/tests/normalization/examples/Bool/even/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/even [ False, True, False ] +(../../../../../Prelude/package.dhall).`Bool`.even [ False, True, False ] diff --git a/tests/normalization/examples/Bool/even/1A.dhall b/tests/normalization/examples/Bool/even/1A.dhall index a168aa790..bf9aea7df 100644 --- a/tests/normalization/examples/Bool/even/1A.dhall +++ b/tests/normalization/examples/Bool/even/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/even [ False, True ] +(../../../../../Prelude/package.dhall).`Bool`.even [ False, True ] diff --git a/tests/normalization/examples/Bool/even/2A.dhall b/tests/normalization/examples/Bool/even/2A.dhall index 98da17c4d..9beba3c76 100644 --- a/tests/normalization/examples/Bool/even/2A.dhall +++ b/tests/normalization/examples/Bool/even/2A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/even [ False ] +(../../../../../Prelude/package.dhall).`Bool`.even [ False ] diff --git a/tests/normalization/examples/Bool/even/3A.dhall b/tests/normalization/examples/Bool/even/3A.dhall index dcf6601d0..bb9e45d5f 100644 --- a/tests/normalization/examples/Bool/even/3A.dhall +++ b/tests/normalization/examples/Bool/even/3A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/even ([] : List Bool) +(../../../../../Prelude/package.dhall).`Bool`.even ([] : List Bool) diff --git a/tests/normalization/examples/Bool/fold/0A.dhall b/tests/normalization/examples/Bool/fold/0A.dhall index b64fe5dae..baac7f302 100644 --- a/tests/normalization/examples/Bool/fold/0A.dhall +++ b/tests/normalization/examples/Bool/fold/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/fold True Natural 0 1 +(../../../../../Prelude/package.dhall).`Bool`.fold True Natural 0 1 diff --git a/tests/normalization/examples/Bool/fold/1A.dhall b/tests/normalization/examples/Bool/fold/1A.dhall index 22418375d..dec00b8b0 100644 --- a/tests/normalization/examples/Bool/fold/1A.dhall +++ b/tests/normalization/examples/Bool/fold/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/fold False Natural 0 1 +(../../../../../Prelude/package.dhall).`Bool`.fold False Natural 0 1 diff --git a/tests/normalization/examples/Bool/not/0A.dhall b/tests/normalization/examples/Bool/not/0A.dhall index ffdcc2d2b..82275d400 100644 --- a/tests/normalization/examples/Bool/not/0A.dhall +++ b/tests/normalization/examples/Bool/not/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/not True +(../../../../../Prelude/package.dhall).`Bool`.not True diff --git a/tests/normalization/examples/Bool/not/1A.dhall b/tests/normalization/examples/Bool/not/1A.dhall index 70af9085e..bdd7e663a 100644 --- a/tests/normalization/examples/Bool/not/1A.dhall +++ b/tests/normalization/examples/Bool/not/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/not False +(../../../../../Prelude/package.dhall).`Bool`.not False diff --git a/tests/normalization/examples/Bool/odd/0A.dhall b/tests/normalization/examples/Bool/odd/0A.dhall index 5a51a9ee4..c5a93b99d 100644 --- a/tests/normalization/examples/Bool/odd/0A.dhall +++ b/tests/normalization/examples/Bool/odd/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/odd [ True, False, True ] +(../../../../../Prelude/package.dhall).`Bool`.odd [ True, False, True ] diff --git a/tests/normalization/examples/Bool/odd/1A.dhall b/tests/normalization/examples/Bool/odd/1A.dhall index 4cafcd3a1..c76356b9c 100644 --- a/tests/normalization/examples/Bool/odd/1A.dhall +++ b/tests/normalization/examples/Bool/odd/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/odd [ True, False ] +(../../../../../Prelude/package.dhall).`Bool`.odd [ True, False ] diff --git a/tests/normalization/examples/Bool/odd/2A.dhall b/tests/normalization/examples/Bool/odd/2A.dhall index 9a75653e8..c603f7c13 100644 --- a/tests/normalization/examples/Bool/odd/2A.dhall +++ b/tests/normalization/examples/Bool/odd/2A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/odd [ True ] +(../../../../../Prelude/package.dhall).`Bool`.odd [ True ] diff --git a/tests/normalization/examples/Bool/odd/3A.dhall b/tests/normalization/examples/Bool/odd/3A.dhall index b2c89bfa8..759af4cf5 100644 --- a/tests/normalization/examples/Bool/odd/3A.dhall +++ b/tests/normalization/examples/Bool/odd/3A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/odd ([] : List Bool) +(../../../../../Prelude/package.dhall).`Bool`.odd ([] : List Bool) diff --git a/tests/normalization/examples/Bool/or/0A.dhall b/tests/normalization/examples/Bool/or/0A.dhall index 9b0e6a9fc..119c757b5 100644 --- a/tests/normalization/examples/Bool/or/0A.dhall +++ b/tests/normalization/examples/Bool/or/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/or [ True, False, True ] +(../../../../../Prelude/package.dhall).`Bool`.or [ True, False, True ] diff --git a/tests/normalization/examples/Bool/or/1A.dhall b/tests/normalization/examples/Bool/or/1A.dhall index 325ca9332..24e032f29 100644 --- a/tests/normalization/examples/Bool/or/1A.dhall +++ b/tests/normalization/examples/Bool/or/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/or ([] : List Bool) +(../../../../../Prelude/package.dhall).`Bool`.or ([] : List Bool) diff --git a/tests/normalization/examples/Bool/show/0A.dhall b/tests/normalization/examples/Bool/show/0A.dhall index 030418bb8..936447fce 100644 --- a/tests/normalization/examples/Bool/show/0A.dhall +++ b/tests/normalization/examples/Bool/show/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/show True +(../../../../../Prelude/package.dhall).`Bool`.show True diff --git a/tests/normalization/examples/Bool/show/1A.dhall b/tests/normalization/examples/Bool/show/1A.dhall index a6b216e81..388f5fe21 100644 --- a/tests/normalization/examples/Bool/show/1A.dhall +++ b/tests/normalization/examples/Bool/show/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Bool/show False +(../../../../../Prelude/package.dhall).`Bool`.show False diff --git a/tests/normalization/examples/Double/show/0A.dhall b/tests/normalization/examples/Double/show/0A.dhall index 872e1921c..e88971be3 100644 --- a/tests/normalization/examples/Double/show/0A.dhall +++ b/tests/normalization/examples/Double/show/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Double/show -3.1 +(../../../../../Prelude/package.dhall).`Double`.show -3.1 diff --git a/tests/normalization/examples/Double/show/1A.dhall b/tests/normalization/examples/Double/show/1A.dhall index b8f84dedc..c7c08ec72 100644 --- a/tests/normalization/examples/Double/show/1A.dhall +++ b/tests/normalization/examples/Double/show/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Double/show 0.4 +(../../../../../Prelude/package.dhall).`Double`.show 0.4 diff --git a/tests/normalization/examples/Integer/show/0A.dhall b/tests/normalization/examples/Integer/show/0A.dhall index a6f58af4b..2dec9062c 100644 --- a/tests/normalization/examples/Integer/show/0A.dhall +++ b/tests/normalization/examples/Integer/show/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Integer/show -3 +(../../../../../Prelude/package.dhall).`Integer`.show -3 diff --git a/tests/normalization/examples/Integer/show/1A.dhall b/tests/normalization/examples/Integer/show/1A.dhall index 21f335b17..b9529b9af 100644 --- a/tests/normalization/examples/Integer/show/1A.dhall +++ b/tests/normalization/examples/Integer/show/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Integer/show +0 +(../../../../../Prelude/package.dhall).`Integer`.show +0 diff --git a/tests/normalization/examples/Integer/toDouble/0A.dhall b/tests/normalization/examples/Integer/toDouble/0A.dhall index f8a8e8b98..8f5899624 100644 --- a/tests/normalization/examples/Integer/toDouble/0A.dhall +++ b/tests/normalization/examples/Integer/toDouble/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Integer/toDouble -3 +(../../../../../Prelude/package.dhall).`Integer`.toDouble -3 diff --git a/tests/normalization/examples/Integer/toDouble/1A.dhall b/tests/normalization/examples/Integer/toDouble/1A.dhall index 849ef77ac..ebf21845a 100644 --- a/tests/normalization/examples/Integer/toDouble/1A.dhall +++ b/tests/normalization/examples/Integer/toDouble/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Integer/toDouble +2 +(../../../../../Prelude/package.dhall).`Integer`.toDouble +2 diff --git a/tests/normalization/examples/List/all/0A.dhall b/tests/normalization/examples/List/all/0A.dhall index 0ae4b493b..4286e9245 100644 --- a/tests/normalization/examples/List/all/0A.dhall +++ b/tests/normalization/examples/List/all/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/all Natural Natural/even [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`List`.all Natural Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/all/1A.dhall b/tests/normalization/examples/List/all/1A.dhall index 5e2d49fa5..ff2364434 100644 --- a/tests/normalization/examples/List/all/1A.dhall +++ b/tests/normalization/examples/List/all/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/all Natural Natural/even ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.all Natural Natural/even ([] : List Natural) diff --git a/tests/normalization/examples/List/any/0A.dhall b/tests/normalization/examples/List/any/0A.dhall index 08fa2b1f9..445ed5ce3 100644 --- a/tests/normalization/examples/List/any/0A.dhall +++ b/tests/normalization/examples/List/any/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/any Natural Natural/even [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`List`.any Natural Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/any/1A.dhall b/tests/normalization/examples/List/any/1A.dhall index 1958d7a16..0b7b8deea 100644 --- a/tests/normalization/examples/List/any/1A.dhall +++ b/tests/normalization/examples/List/any/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/any Natural Natural/even ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.any Natural Natural/even ([] : List Natural) diff --git a/tests/normalization/examples/List/build/0A.dhall b/tests/normalization/examples/List/build/0A.dhall index 58f98efdb..bd7f5051e 100644 --- a/tests/normalization/examples/List/build/0A.dhall +++ b/tests/normalization/examples/List/build/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/build +(../../../../../Prelude/package.dhall).`List`.build Text ( λ(list : Type) → λ(cons : Text → list → list) diff --git a/tests/normalization/examples/List/build/1A.dhall b/tests/normalization/examples/List/build/1A.dhall index 8a689f77c..a8f6e4121 100644 --- a/tests/normalization/examples/List/build/1A.dhall +++ b/tests/normalization/examples/List/build/1A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/build +(../../../../../Prelude/package.dhall).`List`.build Text ( λ(list : Type) → λ(cons : Text → list → list) diff --git a/tests/normalization/examples/List/concat/0A.dhall b/tests/normalization/examples/List/concat/0A.dhall index c5936e265..850627acf 100644 --- a/tests/normalization/examples/List/concat/0A.dhall +++ b/tests/normalization/examples/List/concat/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/concat Natural +(../../../../../Prelude/package.dhall).`List`.concat Natural [ [ 0, 1, 2 ] , [ 3, 4 ] , [ 5, 6, 7, 8 ] diff --git a/tests/normalization/examples/List/concat/1A.dhall b/tests/normalization/examples/List/concat/1A.dhall index 512a62e3d..c9ecae39d 100644 --- a/tests/normalization/examples/List/concat/1A.dhall +++ b/tests/normalization/examples/List/concat/1A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/concat Natural +(../../../../../Prelude/package.dhall).`List`.concat Natural [ [] : List Natural , [] : List Natural , [] : List Natural diff --git a/tests/normalization/examples/List/concatMap/0A.dhall b/tests/normalization/examples/List/concatMap/0A.dhall index 5f89cbf5d..1f0ab7917 100644 --- a/tests/normalization/examples/List/concatMap/0A.dhall +++ b/tests/normalization/examples/List/concatMap/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`List`.concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/concatMap/1A.dhall b/tests/normalization/examples/List/concatMap/1A.dhall index 027e351a2..bbfae3b42 100644 --- a/tests/normalization/examples/List/concatMap/1A.dhall +++ b/tests/normalization/examples/List/concatMap/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/concatMap Natural Natural (λ(n : Natural) → [ n, n ]) ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.concatMap Natural Natural (λ(n : Natural) → [ n, n ]) ([] : List Natural) diff --git a/tests/normalization/examples/List/filter/0A.dhall b/tests/normalization/examples/List/filter/0A.dhall index fd3112974..ce0400f86 100644 --- a/tests/normalization/examples/List/filter/0A.dhall +++ b/tests/normalization/examples/List/filter/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/filter Natural Natural/even [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`List`.filter Natural Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/filter/1A.dhall b/tests/normalization/examples/List/filter/1A.dhall index 7704d7d78..2923e1727 100644 --- a/tests/normalization/examples/List/filter/1A.dhall +++ b/tests/normalization/examples/List/filter/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/filter Natural Natural/odd [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`List`.filter Natural Natural/odd [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/fold/0A.dhall b/tests/normalization/examples/List/fold/0A.dhall index 0dc009f86..2e923cff6 100644 --- a/tests/normalization/examples/List/fold/0A.dhall +++ b/tests/normalization/examples/List/fold/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/fold +(../../../../../Prelude/package.dhall).`List`.fold Natural [ 2, 3, 5 ] Natural diff --git a/tests/normalization/examples/List/fold/1A.dhall b/tests/normalization/examples/List/fold/1A.dhall index a383d2dbd..3c17a3160 100644 --- a/tests/normalization/examples/List/fold/1A.dhall +++ b/tests/normalization/examples/List/fold/1A.dhall @@ -1,5 +1,5 @@ λ(nil : Natural) -→ ../../../../../Prelude/List/fold +→ (../../../../../Prelude/package.dhall).`List`.fold Natural [ 2, 3, 5 ] Natural diff --git a/tests/normalization/examples/List/fold/2A.dhall b/tests/normalization/examples/List/fold/2A.dhall index a71827f1d..adb3fe860 100644 --- a/tests/normalization/examples/List/fold/2A.dhall +++ b/tests/normalization/examples/List/fold/2A.dhall @@ -1,4 +1,4 @@ λ(list : Type) → λ(cons : Natural → list → list) → λ(nil : list) -→ ../../../../../Prelude/List/fold Natural [ 2, 3, 5 ] list cons nil +→ (../../../../../Prelude/package.dhall).`List`.fold Natural [ 2, 3, 5 ] list cons nil diff --git a/tests/normalization/examples/List/generate/0A.dhall b/tests/normalization/examples/List/generate/0A.dhall index c3868bd06..294411d56 100644 --- a/tests/normalization/examples/List/generate/0A.dhall +++ b/tests/normalization/examples/List/generate/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/generate 5 Bool Natural/even +(../../../../../Prelude/package.dhall).`List`.generate 5 Bool Natural/even diff --git a/tests/normalization/examples/List/generate/1A.dhall b/tests/normalization/examples/List/generate/1A.dhall index 3d1b63593..969f26a20 100644 --- a/tests/normalization/examples/List/generate/1A.dhall +++ b/tests/normalization/examples/List/generate/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/generate 0 Bool Natural/even +(../../../../../Prelude/package.dhall).`List`.generate 0 Bool Natural/even diff --git a/tests/normalization/examples/List/head/0A.dhall b/tests/normalization/examples/List/head/0A.dhall index 990746e26..57be97206 100644 --- a/tests/normalization/examples/List/head/0A.dhall +++ b/tests/normalization/examples/List/head/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/head Natural [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`List`.head Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/head/1A.dhall b/tests/normalization/examples/List/head/1A.dhall index 6be8e0bb3..638bc48d3 100644 --- a/tests/normalization/examples/List/head/1A.dhall +++ b/tests/normalization/examples/List/head/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/head Natural ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.head Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/indexed/0A.dhall b/tests/normalization/examples/List/indexed/0A.dhall index 466f86108..ecb0e8c0f 100644 --- a/tests/normalization/examples/List/indexed/0A.dhall +++ b/tests/normalization/examples/List/indexed/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/indexed Bool [ True, False, True ] +(../../../../../Prelude/package.dhall).`List`.indexed Bool [ True, False, True ] diff --git a/tests/normalization/examples/List/indexed/1A.dhall b/tests/normalization/examples/List/indexed/1A.dhall index c18fe3692..b92b3ad0f 100644 --- a/tests/normalization/examples/List/indexed/1A.dhall +++ b/tests/normalization/examples/List/indexed/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/indexed Bool ([] : List Bool) +(../../../../../Prelude/package.dhall).`List`.indexed Bool ([] : List Bool) diff --git a/tests/normalization/examples/List/iterate/0A.dhall b/tests/normalization/examples/List/iterate/0A.dhall index 59bfc597b..7931af442 100644 --- a/tests/normalization/examples/List/iterate/0A.dhall +++ b/tests/normalization/examples/List/iterate/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/iterate 10 Natural (λ(x : Natural) → x * 2) 1 +(../../../../../Prelude/package.dhall).`List`.iterate 10 Natural (λ(x : Natural) → x * 2) 1 diff --git a/tests/normalization/examples/List/iterate/1A.dhall b/tests/normalization/examples/List/iterate/1A.dhall index 65fd48a6e..573970db4 100644 --- a/tests/normalization/examples/List/iterate/1A.dhall +++ b/tests/normalization/examples/List/iterate/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/iterate 0 Natural (λ(x : Natural) → x * 2) 1 +(../../../../../Prelude/package.dhall).`List`.iterate 0 Natural (λ(x : Natural) → x * 2) 1 diff --git a/tests/normalization/examples/List/last/0A.dhall b/tests/normalization/examples/List/last/0A.dhall index d8319f787..2f2660b98 100644 --- a/tests/normalization/examples/List/last/0A.dhall +++ b/tests/normalization/examples/List/last/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/last Natural [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`List`.last Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/last/1A.dhall b/tests/normalization/examples/List/last/1A.dhall index 74a1eadaa..f9a97eefb 100644 --- a/tests/normalization/examples/List/last/1A.dhall +++ b/tests/normalization/examples/List/last/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/last Natural ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.last Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/length/0A.dhall b/tests/normalization/examples/List/length/0A.dhall index 78fe3d565..cfff3a292 100644 --- a/tests/normalization/examples/List/length/0A.dhall +++ b/tests/normalization/examples/List/length/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/length Natural [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`List`.length Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/length/1A.dhall b/tests/normalization/examples/List/length/1A.dhall index 5ffe727d7..33cd9d54d 100644 --- a/tests/normalization/examples/List/length/1A.dhall +++ b/tests/normalization/examples/List/length/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/length Natural ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.length Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/map/0A.dhall b/tests/normalization/examples/List/map/0A.dhall index a42c319ce..921c9b264 100644 --- a/tests/normalization/examples/List/map/0A.dhall +++ b/tests/normalization/examples/List/map/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/map Natural Bool Natural/even [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`List`.map Natural Bool Natural/even [ 2, 3, 5 ] diff --git a/tests/normalization/examples/List/map/1A.dhall b/tests/normalization/examples/List/map/1A.dhall index 9987e9799..39b712e9b 100644 --- a/tests/normalization/examples/List/map/1A.dhall +++ b/tests/normalization/examples/List/map/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/map Natural Bool Natural/even ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.map Natural Bool Natural/even ([] : List Natural) diff --git a/tests/normalization/examples/List/null/0A.dhall b/tests/normalization/examples/List/null/0A.dhall index 0a6580328..3c5052582 100644 --- a/tests/normalization/examples/List/null/0A.dhall +++ b/tests/normalization/examples/List/null/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/null Natural [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`List`.null Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/null/1A.dhall b/tests/normalization/examples/List/null/1A.dhall index bc75bce50..fbc77b659 100644 --- a/tests/normalization/examples/List/null/1A.dhall +++ b/tests/normalization/examples/List/null/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/null Natural ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.null Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/replicate/0A.dhall b/tests/normalization/examples/List/replicate/0A.dhall index 77c62409a..f54726232 100644 --- a/tests/normalization/examples/List/replicate/0A.dhall +++ b/tests/normalization/examples/List/replicate/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/replicate 9 Natural 1 +(../../../../../Prelude/package.dhall).`List`.replicate 9 Natural 1 diff --git a/tests/normalization/examples/List/replicate/1A.dhall b/tests/normalization/examples/List/replicate/1A.dhall index 53900de56..828f5841f 100644 --- a/tests/normalization/examples/List/replicate/1A.dhall +++ b/tests/normalization/examples/List/replicate/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/replicate 0 Natural 1 +(../../../../../Prelude/package.dhall).`List`.replicate 0 Natural 1 diff --git a/tests/normalization/examples/List/reverse/0A.dhall b/tests/normalization/examples/List/reverse/0A.dhall index eb4e6da3d..a490596bc 100644 --- a/tests/normalization/examples/List/reverse/0A.dhall +++ b/tests/normalization/examples/List/reverse/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/reverse Natural [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`List`.reverse Natural [ 0, 1, 2 ] diff --git a/tests/normalization/examples/List/reverse/1A.dhall b/tests/normalization/examples/List/reverse/1A.dhall index d88926297..fa5fa4c66 100644 --- a/tests/normalization/examples/List/reverse/1A.dhall +++ b/tests/normalization/examples/List/reverse/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/reverse Natural ([] : List Natural) +(../../../../../Prelude/package.dhall).`List`.reverse Natural ([] : List Natural) diff --git a/tests/normalization/examples/List/shifted/0A.dhall b/tests/normalization/examples/List/shifted/0A.dhall index 8f5643ecd..8fd7538f5 100644 --- a/tests/normalization/examples/List/shifted/0A.dhall +++ b/tests/normalization/examples/List/shifted/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/shifted +(../../../../../Prelude/package.dhall).`List`.shifted Bool [ [ { index = 0, value = True } , { index = 1, value = True } diff --git a/tests/normalization/examples/List/shifted/1A.dhall b/tests/normalization/examples/List/shifted/1A.dhall index 4671164ca..2f5ff48cb 100644 --- a/tests/normalization/examples/List/shifted/1A.dhall +++ b/tests/normalization/examples/List/shifted/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/shifted Bool ([] : List (List { index : Natural, value : Bool })) +(../../../../../Prelude/package.dhall).`List`.shifted Bool ([] : List (List { index : Natural, value : Bool })) diff --git a/tests/normalization/examples/List/unzip/0A.dhall b/tests/normalization/examples/List/unzip/0A.dhall index f12f645c2..5bbd931f7 100644 --- a/tests/normalization/examples/List/unzip/0A.dhall +++ b/tests/normalization/examples/List/unzip/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/List/unzip +(../../../../../Prelude/package.dhall).`List`.unzip Text Bool [ { _1 = "ABC", _2 = True } diff --git a/tests/normalization/examples/List/unzip/1A.dhall b/tests/normalization/examples/List/unzip/1A.dhall index 0b9210c3c..21fcb6e6e 100644 --- a/tests/normalization/examples/List/unzip/1A.dhall +++ b/tests/normalization/examples/List/unzip/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/List/unzip Text Bool ([] : List { _1 : Text, _2 : Bool }) +(../../../../../Prelude/package.dhall).`List`.unzip Text Bool ([] : List { _1 : Text, _2 : Bool }) diff --git a/tests/normalization/examples/Natural/build/0A.dhall b/tests/normalization/examples/Natural/build/0A.dhall index 11d06934c..5a03d24e7 100644 --- a/tests/normalization/examples/Natural/build/0A.dhall +++ b/tests/normalization/examples/Natural/build/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/Natural/build +(../../../../../Prelude/package.dhall).`Natural`.build ( λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) diff --git a/tests/normalization/examples/Natural/build/1A.dhall b/tests/normalization/examples/Natural/build/1A.dhall index c938c4ff1..4633e7af4 100644 --- a/tests/normalization/examples/Natural/build/1A.dhall +++ b/tests/normalization/examples/Natural/build/1A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/Natural/build +(../../../../../Prelude/package.dhall).`Natural`.build ( λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) diff --git a/tests/normalization/examples/Natural/enumerate/0A.dhall b/tests/normalization/examples/Natural/enumerate/0A.dhall index 4a680ead2..418a52254 100644 --- a/tests/normalization/examples/Natural/enumerate/0A.dhall +++ b/tests/normalization/examples/Natural/enumerate/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/enumerate 10 +(../../../../../Prelude/package.dhall).`Natural`.enumerate 10 diff --git a/tests/normalization/examples/Natural/enumerate/1A.dhall b/tests/normalization/examples/Natural/enumerate/1A.dhall index 955fda526..6af6ea614 100644 --- a/tests/normalization/examples/Natural/enumerate/1A.dhall +++ b/tests/normalization/examples/Natural/enumerate/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/enumerate 0 +(../../../../../Prelude/package.dhall).`Natural`.enumerate 0 diff --git a/tests/normalization/examples/Natural/even/0A.dhall b/tests/normalization/examples/Natural/even/0A.dhall index 61cbb11a1..6bd99f6fd 100644 --- a/tests/normalization/examples/Natural/even/0A.dhall +++ b/tests/normalization/examples/Natural/even/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/even 3 +(../../../../../Prelude/package.dhall).`Natural`.even 3 diff --git a/tests/normalization/examples/Natural/even/1A.dhall b/tests/normalization/examples/Natural/even/1A.dhall index c6f83d57b..001b64a01 100644 --- a/tests/normalization/examples/Natural/even/1A.dhall +++ b/tests/normalization/examples/Natural/even/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/even 0 +(../../../../../Prelude/package.dhall).`Natural`.even 0 diff --git a/tests/normalization/examples/Natural/fold/0A.dhall b/tests/normalization/examples/Natural/fold/0A.dhall index c6d9b269b..6d0a6032d 100644 --- a/tests/normalization/examples/Natural/fold/0A.dhall +++ b/tests/normalization/examples/Natural/fold/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/fold 3 Natural (λ(x : Natural) → 5 * x) 1 +(../../../../../Prelude/package.dhall).`Natural`.fold 3 Natural (λ(x : Natural) → 5 * x) 1 diff --git a/tests/normalization/examples/Natural/fold/1A.dhall b/tests/normalization/examples/Natural/fold/1A.dhall index 0b9bb8e42..2d819d222 100644 --- a/tests/normalization/examples/Natural/fold/1A.dhall +++ b/tests/normalization/examples/Natural/fold/1A.dhall @@ -1 +1 @@ -λ(zero : Natural) → ../../../../../Prelude/Natural/fold 3 Natural (λ(x : Natural) → 5 * x) zero +λ(zero : Natural) → (../../../../../Prelude/package.dhall).`Natural`.fold 3 Natural (λ(x : Natural) → 5 * x) zero diff --git a/tests/normalization/examples/Natural/fold/2A.dhall b/tests/normalization/examples/Natural/fold/2A.dhall index cb536c74d..b50172e18 100644 --- a/tests/normalization/examples/Natural/fold/2A.dhall +++ b/tests/normalization/examples/Natural/fold/2A.dhall @@ -1,4 +1,4 @@ λ(natural : Type) → λ(succ : natural → natural) → λ(zero : natural) -→ ../../../../../Prelude/Natural/fold 3 natural succ zero +→ (../../../../../Prelude/package.dhall).`Natural`.fold 3 natural succ zero diff --git a/tests/normalization/examples/Natural/isZero/0A.dhall b/tests/normalization/examples/Natural/isZero/0A.dhall index b5c0e2f2d..ab317ec39 100644 --- a/tests/normalization/examples/Natural/isZero/0A.dhall +++ b/tests/normalization/examples/Natural/isZero/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/isZero 2 +(../../../../../Prelude/package.dhall).`Natural`.isZero 2 diff --git a/tests/normalization/examples/Natural/isZero/1A.dhall b/tests/normalization/examples/Natural/isZero/1A.dhall index ded082c04..6df09a04b 100644 --- a/tests/normalization/examples/Natural/isZero/1A.dhall +++ b/tests/normalization/examples/Natural/isZero/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/isZero 0 +(../../../../../Prelude/package.dhall).`Natural`.isZero 0 diff --git a/tests/normalization/examples/Natural/odd/0A.dhall b/tests/normalization/examples/Natural/odd/0A.dhall index 05112dcfa..a8664a4ea 100644 --- a/tests/normalization/examples/Natural/odd/0A.dhall +++ b/tests/normalization/examples/Natural/odd/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/odd 3 +(../../../../../Prelude/package.dhall).`Natural`.odd 3 diff --git a/tests/normalization/examples/Natural/odd/1A.dhall b/tests/normalization/examples/Natural/odd/1A.dhall index 5443e0b59..c18134969 100644 --- a/tests/normalization/examples/Natural/odd/1A.dhall +++ b/tests/normalization/examples/Natural/odd/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/odd 0 +(../../../../../Prelude/package.dhall).`Natural`.odd 0 diff --git a/tests/normalization/examples/Natural/product/0A.dhall b/tests/normalization/examples/Natural/product/0A.dhall index 848d0564d..cb55a2416 100644 --- a/tests/normalization/examples/Natural/product/0A.dhall +++ b/tests/normalization/examples/Natural/product/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/product [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`Natural`.product [ 2, 3, 5 ] diff --git a/tests/normalization/examples/Natural/product/1A.dhall b/tests/normalization/examples/Natural/product/1A.dhall index c1eba2325..64dbcbc47 100644 --- a/tests/normalization/examples/Natural/product/1A.dhall +++ b/tests/normalization/examples/Natural/product/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/product ([] : List Natural) +(../../../../../Prelude/package.dhall).`Natural`.product ([] : List Natural) diff --git a/tests/normalization/examples/Natural/show/0A.dhall b/tests/normalization/examples/Natural/show/0A.dhall index b3752cac1..467e7936f 100644 --- a/tests/normalization/examples/Natural/show/0A.dhall +++ b/tests/normalization/examples/Natural/show/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/show 3 +(../../../../../Prelude/package.dhall).`Natural`.show 3 diff --git a/tests/normalization/examples/Natural/show/1A.dhall b/tests/normalization/examples/Natural/show/1A.dhall index 4d9cba744..4f7e7369a 100644 --- a/tests/normalization/examples/Natural/show/1A.dhall +++ b/tests/normalization/examples/Natural/show/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/show 0 +(../../../../../Prelude/package.dhall).`Natural`.show 0 diff --git a/tests/normalization/examples/Natural/sum/0A.dhall b/tests/normalization/examples/Natural/sum/0A.dhall index 6df8879ac..477bd3d67 100644 --- a/tests/normalization/examples/Natural/sum/0A.dhall +++ b/tests/normalization/examples/Natural/sum/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/sum [ 2, 3, 5 ] +(../../../../../Prelude/package.dhall).`Natural`.sum [ 2, 3, 5 ] diff --git a/tests/normalization/examples/Natural/sum/1A.dhall b/tests/normalization/examples/Natural/sum/1A.dhall index 4bc1040b7..df8896aa8 100644 --- a/tests/normalization/examples/Natural/sum/1A.dhall +++ b/tests/normalization/examples/Natural/sum/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/sum ([] : List Natural) +(../../../../../Prelude/package.dhall).`Natural`.sum ([] : List Natural) diff --git a/tests/normalization/examples/Natural/toDouble/0A.dhall b/tests/normalization/examples/Natural/toDouble/0A.dhall index 3fb3d2c40..62836c927 100644 --- a/tests/normalization/examples/Natural/toDouble/0A.dhall +++ b/tests/normalization/examples/Natural/toDouble/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/toDouble 3 +(../../../../../Prelude/package.dhall).`Natural`.toDouble 3 diff --git a/tests/normalization/examples/Natural/toDouble/1A.dhall b/tests/normalization/examples/Natural/toDouble/1A.dhall index 11ea8179b..69bc5b039 100644 --- a/tests/normalization/examples/Natural/toDouble/1A.dhall +++ b/tests/normalization/examples/Natural/toDouble/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/toDouble 0 +(../../../../../Prelude/package.dhall).`Natural`.toDouble 0 diff --git a/tests/normalization/examples/Natural/toInteger/0A.dhall b/tests/normalization/examples/Natural/toInteger/0A.dhall index 60d693733..50a24a753 100644 --- a/tests/normalization/examples/Natural/toInteger/0A.dhall +++ b/tests/normalization/examples/Natural/toInteger/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/toInteger 3 +(../../../../../Prelude/package.dhall).`Natural`.toInteger 3 diff --git a/tests/normalization/examples/Natural/toInteger/1A.dhall b/tests/normalization/examples/Natural/toInteger/1A.dhall index 9b904f569..12f56992e 100644 --- a/tests/normalization/examples/Natural/toInteger/1A.dhall +++ b/tests/normalization/examples/Natural/toInteger/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Natural/toInteger 0 +(../../../../../Prelude/package.dhall).`Natural`.toInteger 0 diff --git a/tests/normalization/examples/Optional/all/0A.dhall b/tests/normalization/examples/Optional/all/0A.dhall index 2020b0e78..a95b676c1 100644 --- a/tests/normalization/examples/Optional/all/0A.dhall +++ b/tests/normalization/examples/Optional/all/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/all Natural Natural/even (Some 3) +(../../../../../Prelude/package.dhall).`Optional`.all Natural Natural/even (Some 3) diff --git a/tests/normalization/examples/Optional/all/1A.dhall b/tests/normalization/examples/Optional/all/1A.dhall index 906390c02..a326436e2 100644 --- a/tests/normalization/examples/Optional/all/1A.dhall +++ b/tests/normalization/examples/Optional/all/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/all Natural Natural/even (None Natural) +(../../../../../Prelude/package.dhall).`Optional`.all Natural Natural/even (None Natural) diff --git a/tests/normalization/examples/Optional/any/0A.dhall b/tests/normalization/examples/Optional/any/0A.dhall index 4c693ca5b..7ff7b60e0 100644 --- a/tests/normalization/examples/Optional/any/0A.dhall +++ b/tests/normalization/examples/Optional/any/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/any Natural Natural/even (Some 2) +(../../../../../Prelude/package.dhall).`Optional`.any Natural Natural/even (Some 2) diff --git a/tests/normalization/examples/Optional/any/1A.dhall b/tests/normalization/examples/Optional/any/1A.dhall index 28c8accd2..25da85560 100644 --- a/tests/normalization/examples/Optional/any/1A.dhall +++ b/tests/normalization/examples/Optional/any/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/any Natural Natural/even (None Natural) +(../../../../../Prelude/package.dhall).`Optional`.any Natural Natural/even (None Natural) diff --git a/tests/normalization/examples/Optional/build/0A.dhall b/tests/normalization/examples/Optional/build/0A.dhall index c0b1acd43..4eb31523a 100644 --- a/tests/normalization/examples/Optional/build/0A.dhall +++ b/tests/normalization/examples/Optional/build/0A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/Optional/build +(../../../../../Prelude/package.dhall).`Optional`.build Natural ( λ(optional : Type) → λ(some : Natural → optional) diff --git a/tests/normalization/examples/Optional/build/1A.dhall b/tests/normalization/examples/Optional/build/1A.dhall index 3e5756659..ed36fefad 100644 --- a/tests/normalization/examples/Optional/build/1A.dhall +++ b/tests/normalization/examples/Optional/build/1A.dhall @@ -1,4 +1,4 @@ -../../../../../Prelude/Optional/build +(../../../../../Prelude/package.dhall).`Optional`.build Natural ( λ(optional : Type) → λ(some : Natural → optional) diff --git a/tests/normalization/examples/Optional/concat/0A.dhall b/tests/normalization/examples/Optional/concat/0A.dhall index 5ee16196f..bfd7ffb34 100644 --- a/tests/normalization/examples/Optional/concat/0A.dhall +++ b/tests/normalization/examples/Optional/concat/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/concat Natural (Some (Some 1)) +(../../../../../Prelude/package.dhall).`Optional`.concat Natural (Some (Some 1)) diff --git a/tests/normalization/examples/Optional/concat/1A.dhall b/tests/normalization/examples/Optional/concat/1A.dhall index 1a42808d5..9e79160e3 100644 --- a/tests/normalization/examples/Optional/concat/1A.dhall +++ b/tests/normalization/examples/Optional/concat/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/concat Natural (Some (None Natural)) +(../../../../../Prelude/package.dhall).`Optional`.concat Natural (Some (None Natural)) diff --git a/tests/normalization/examples/Optional/concat/2A.dhall b/tests/normalization/examples/Optional/concat/2A.dhall index c38f5cd49..d7026582a 100644 --- a/tests/normalization/examples/Optional/concat/2A.dhall +++ b/tests/normalization/examples/Optional/concat/2A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/concat Natural (None (Optional Natural)) +(../../../../../Prelude/package.dhall).`Optional`.concat Natural (None (Optional Natural)) diff --git a/tests/normalization/examples/Optional/filter/0A.dhall b/tests/normalization/examples/Optional/filter/0A.dhall index 411f9179e..d06b63eca 100644 --- a/tests/normalization/examples/Optional/filter/0A.dhall +++ b/tests/normalization/examples/Optional/filter/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/filter Natural Natural/even (Some 2) +(../../../../../Prelude/package.dhall).`Optional`.filter Natural Natural/even (Some 2) diff --git a/tests/normalization/examples/Optional/filter/1A.dhall b/tests/normalization/examples/Optional/filter/1A.dhall index fc7487288..605c90cc1 100644 --- a/tests/normalization/examples/Optional/filter/1A.dhall +++ b/tests/normalization/examples/Optional/filter/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/filter Natural Natural/odd (Some 2) +(../../../../../Prelude/package.dhall).`Optional`.filter Natural Natural/odd (Some 2) diff --git a/tests/normalization/examples/Optional/fold/0A.dhall b/tests/normalization/examples/Optional/fold/0A.dhall index 1e4dc4680..b9025cf3c 100644 --- a/tests/normalization/examples/Optional/fold/0A.dhall +++ b/tests/normalization/examples/Optional/fold/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 +(../../../../../Prelude/package.dhall).`Optional`.fold Natural (Some 2) Natural (λ(x : Natural) → x) 0 diff --git a/tests/normalization/examples/Optional/fold/1A.dhall b/tests/normalization/examples/Optional/fold/1A.dhall index 29b606374..b029868a7 100644 --- a/tests/normalization/examples/Optional/fold/1A.dhall +++ b/tests/normalization/examples/Optional/fold/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 +(../../../../../Prelude/package.dhall).`Optional`.fold Natural (None Natural) Natural (λ(x : Natural) → x) 0 diff --git a/tests/normalization/examples/Optional/head/0A.dhall b/tests/normalization/examples/Optional/head/0A.dhall index b6428c9dc..3d6e64119 100644 --- a/tests/normalization/examples/Optional/head/0A.dhall +++ b/tests/normalization/examples/Optional/head/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/head Natural [ None Natural, Some 1, Some 2 ] +(../../../../../Prelude/package.dhall).`Optional`.head Natural [ None Natural, Some 1, Some 2 ] diff --git a/tests/normalization/examples/Optional/head/1A.dhall b/tests/normalization/examples/Optional/head/1A.dhall index 6b8b816f9..ff3a5926c 100644 --- a/tests/normalization/examples/Optional/head/1A.dhall +++ b/tests/normalization/examples/Optional/head/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/head Natural [ None Natural, None Natural ] +(../../../../../Prelude/package.dhall).`Optional`.head Natural [ None Natural, None Natural ] diff --git a/tests/normalization/examples/Optional/head/2A.dhall b/tests/normalization/examples/Optional/head/2A.dhall index e54ace447..b042bf726 100644 --- a/tests/normalization/examples/Optional/head/2A.dhall +++ b/tests/normalization/examples/Optional/head/2A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/head Natural ([] : List (Optional Natural)) +(../../../../../Prelude/package.dhall).`Optional`.head Natural ([] : List (Optional Natural)) diff --git a/tests/normalization/examples/Optional/last/0A.dhall b/tests/normalization/examples/Optional/last/0A.dhall index 7a4c7ce4d..0d274bf46 100644 --- a/tests/normalization/examples/Optional/last/0A.dhall +++ b/tests/normalization/examples/Optional/last/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/last Natural [ None Natural, Some 1, Some 2 ] +(../../../../../Prelude/package.dhall).`Optional`.last Natural [ None Natural, Some 1, Some 2 ] diff --git a/tests/normalization/examples/Optional/last/1A.dhall b/tests/normalization/examples/Optional/last/1A.dhall index f1cabfadb..634b73b04 100644 --- a/tests/normalization/examples/Optional/last/1A.dhall +++ b/tests/normalization/examples/Optional/last/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/last Natural [ None Natural, None Natural ] +(../../../../../Prelude/package.dhall).`Optional`.last Natural [ None Natural, None Natural ] diff --git a/tests/normalization/examples/Optional/last/2A.dhall b/tests/normalization/examples/Optional/last/2A.dhall index 961aebb5c..6e2b27186 100644 --- a/tests/normalization/examples/Optional/last/2A.dhall +++ b/tests/normalization/examples/Optional/last/2A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/last Natural ([] : List (Optional Natural)) +(../../../../../Prelude/package.dhall).`Optional`.last Natural ([] : List (Optional Natural)) diff --git a/tests/normalization/examples/Optional/length/0A.dhall b/tests/normalization/examples/Optional/length/0A.dhall index b36940373..79cd58276 100644 --- a/tests/normalization/examples/Optional/length/0A.dhall +++ b/tests/normalization/examples/Optional/length/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/length Natural (Some 2) +(../../../../../Prelude/package.dhall).`Optional`.length Natural (Some 2) diff --git a/tests/normalization/examples/Optional/length/1A.dhall b/tests/normalization/examples/Optional/length/1A.dhall index 8446ca278..357315f92 100644 --- a/tests/normalization/examples/Optional/length/1A.dhall +++ b/tests/normalization/examples/Optional/length/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/length Natural (None Natural) +(../../../../../Prelude/package.dhall).`Optional`.length Natural (None Natural) diff --git a/tests/normalization/examples/Optional/map/0A.dhall b/tests/normalization/examples/Optional/map/0A.dhall index 3993afadf..67ece6dc4 100644 --- a/tests/normalization/examples/Optional/map/0A.dhall +++ b/tests/normalization/examples/Optional/map/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/map Natural Bool Natural/even (Some 3) +(../../../../../Prelude/package.dhall).`Optional`.map Natural Bool Natural/even (Some 3) diff --git a/tests/normalization/examples/Optional/map/1A.dhall b/tests/normalization/examples/Optional/map/1A.dhall index a68a76049..b1ba6cf34 100644 --- a/tests/normalization/examples/Optional/map/1A.dhall +++ b/tests/normalization/examples/Optional/map/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/map Natural Bool Natural/even (None Natural) +(../../../../../Prelude/package.dhall).`Optional`.map Natural Bool Natural/even (None Natural) diff --git a/tests/normalization/examples/Optional/null/0A.dhall b/tests/normalization/examples/Optional/null/0A.dhall index 16ccfef45..15d84685a 100644 --- a/tests/normalization/examples/Optional/null/0A.dhall +++ b/tests/normalization/examples/Optional/null/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/null Natural (Some 2) +(../../../../../Prelude/package.dhall).`Optional`.null Natural (Some 2) diff --git a/tests/normalization/examples/Optional/null/1A.dhall b/tests/normalization/examples/Optional/null/1A.dhall index 168001420..7826e5442 100644 --- a/tests/normalization/examples/Optional/null/1A.dhall +++ b/tests/normalization/examples/Optional/null/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/null Natural (None Natural) +(../../../../../Prelude/package.dhall).`Optional`.null Natural (None Natural) diff --git a/tests/normalization/examples/Optional/toList/0A.dhall b/tests/normalization/examples/Optional/toList/0A.dhall index c1dd7c83d..8618f7502 100644 --- a/tests/normalization/examples/Optional/toList/0A.dhall +++ b/tests/normalization/examples/Optional/toList/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/toList Natural (Some 1) +(../../../../../Prelude/package.dhall).`Optional`.toList Natural (Some 1) diff --git a/tests/normalization/examples/Optional/toList/1A.dhall b/tests/normalization/examples/Optional/toList/1A.dhall index 8d5debe95..95f8da452 100644 --- a/tests/normalization/examples/Optional/toList/1A.dhall +++ b/tests/normalization/examples/Optional/toList/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/toList Natural (None Natural) +(../../../../../Prelude/package.dhall).`Optional`.toList Natural (None Natural) diff --git a/tests/normalization/examples/Optional/unzip/0A.dhall b/tests/normalization/examples/Optional/unzip/0A.dhall index 37e13b27c..e6e93bcfa 100644 --- a/tests/normalization/examples/Optional/unzip/0A.dhall +++ b/tests/normalization/examples/Optional/unzip/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/unzip Text Bool (Some { _1 = "ABC", _2 = True }) +(../../../../../Prelude/package.dhall).`Optional`.unzip Text Bool (Some { _1 = "ABC", _2 = True }) diff --git a/tests/normalization/examples/Optional/unzip/1A.dhall b/tests/normalization/examples/Optional/unzip/1A.dhall index 7cc47430b..85a02ee1f 100644 --- a/tests/normalization/examples/Optional/unzip/1A.dhall +++ b/tests/normalization/examples/Optional/unzip/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Optional/unzip Text Bool (None { _1 : Text, _2 : Bool }) +(../../../../../Prelude/package.dhall).`Optional`.unzip Text Bool (None { _1 : Text, _2 : Bool }) diff --git a/tests/normalization/examples/Text/concat/0A.dhall b/tests/normalization/examples/Text/concat/0A.dhall index 8039564c0..7854b295f 100644 --- a/tests/normalization/examples/Text/concat/0A.dhall +++ b/tests/normalization/examples/Text/concat/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concat [ "ABC", "DEF", "GHI" ] +(../../../../../Prelude/package.dhall).`Text`.concat [ "ABC", "DEF", "GHI" ] diff --git a/tests/normalization/examples/Text/concat/1A.dhall b/tests/normalization/examples/Text/concat/1A.dhall index 999658b46..5d212adcd 100644 --- a/tests/normalization/examples/Text/concat/1A.dhall +++ b/tests/normalization/examples/Text/concat/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concat ([] : List Text) +(../../../../../Prelude/package.dhall).`Text`.concat ([] : List Text) diff --git a/tests/normalization/examples/Text/concatMap/0A.dhall b/tests/normalization/examples/Text/concatMap/0A.dhall index 72f4f8655..42beeb445 100644 --- a/tests/normalization/examples/Text/concatMap/0A.dhall +++ b/tests/normalization/examples/Text/concatMap/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`Text`.concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ] diff --git a/tests/normalization/examples/Text/concatMap/1A.dhall b/tests/normalization/examples/Text/concatMap/1A.dhall index 445fd5ef8..bc8501725 100644 --- a/tests/normalization/examples/Text/concatMap/1A.dhall +++ b/tests/normalization/examples/Text/concatMap/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural) +(../../../../../Prelude/package.dhall).`Text`.concatMap Natural (λ(n : Natural) → "${Natural/show n} ") ([] : List Natural) diff --git a/tests/normalization/examples/Text/concatMapSep/0A.dhall b/tests/normalization/examples/Text/concatMapSep/0A.dhall index ad4c29e65..213787bfe 100644 --- a/tests/normalization/examples/Text/concatMapSep/0A.dhall +++ b/tests/normalization/examples/Text/concatMapSep/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] +(../../../../../Prelude/package.dhall).`Text`.concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] diff --git a/tests/normalization/examples/Text/concatMapSep/1A.dhall b/tests/normalization/examples/Text/concatMapSep/1A.dhall index 188fb68cb..db115d1d2 100644 --- a/tests/normalization/examples/Text/concatMapSep/1A.dhall +++ b/tests/normalization/examples/Text/concatMapSep/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concatMapSep ", " Natural Natural/show ([] : List Natural) +(../../../../../Prelude/package.dhall).`Text`.concatMapSep ", " Natural Natural/show ([] : List Natural) diff --git a/tests/normalization/examples/Text/concatSep/0A.dhall b/tests/normalization/examples/Text/concatSep/0A.dhall index 519028fe9..a36d729a3 100644 --- a/tests/normalization/examples/Text/concatSep/0A.dhall +++ b/tests/normalization/examples/Text/concatSep/0A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concatSep ", " [ "ABC", "DEF", "GHI" ] +(../../../../../Prelude/package.dhall).`Text`.concatSep ", " [ "ABC", "DEF", "GHI" ] diff --git a/tests/normalization/examples/Text/concatSep/1A.dhall b/tests/normalization/examples/Text/concatSep/1A.dhall index 95d469bbd..d5deb1f34 100644 --- a/tests/normalization/examples/Text/concatSep/1A.dhall +++ b/tests/normalization/examples/Text/concatSep/1A.dhall @@ -1 +1 @@ -../../../../../Prelude/Text/concatSep ", " ([] : List Text) +(../../../../../Prelude/package.dhall).`Text`.concatSep ", " ([] : List Text) diff --git a/tests/normalization/remoteSystemsA.dhall b/tests/normalization/remoteSystemsA.dhall index b16109553..d2ee2a5a0 100644 --- a/tests/normalization/remoteSystemsA.dhall +++ b/tests/normalization/remoteSystemsA.dhall @@ -1,8 +1,8 @@ let Text/concatMap = - ../../Prelude/Text/concatMap +( ../../Prelude/package.dhall).`Text`.concatMap in let Text/concatSep = - ../../Prelude/Text/concatSep +( ../../Prelude/package.dhall).`Text`.concatSep in let Row = { cores : diff --git a/tests/typecheck/examples/Monoid/00A.dhall b/tests/typecheck/examples/Monoid/00A.dhall index 83166a85a..b6309a420 100644 --- a/tests/typecheck/examples/Monoid/00A.dhall +++ b/tests/typecheck/examples/Monoid/00A.dhall @@ -1 +1 @@ -../../../../Prelude/Bool/and +(../../../../Prelude/package.dhall).`Bool`.and diff --git a/tests/typecheck/examples/Monoid/01A.dhall b/tests/typecheck/examples/Monoid/01A.dhall index d9f1dd4a1..2a9c643a0 100644 --- a/tests/typecheck/examples/Monoid/01A.dhall +++ b/tests/typecheck/examples/Monoid/01A.dhall @@ -1 +1 @@ -../../../../Prelude/Bool/or +(../../../../Prelude/package.dhall).`Bool`.or diff --git a/tests/typecheck/examples/Monoid/02A.dhall b/tests/typecheck/examples/Monoid/02A.dhall index b28ff8637..20376d951 100644 --- a/tests/typecheck/examples/Monoid/02A.dhall +++ b/tests/typecheck/examples/Monoid/02A.dhall @@ -1 +1 @@ -../../../../Prelude/Bool/even +(../../../../Prelude/package.dhall).`Bool`.even diff --git a/tests/typecheck/examples/Monoid/03A.dhall b/tests/typecheck/examples/Monoid/03A.dhall index daa052ac7..1d0b4ac40 100644 --- a/tests/typecheck/examples/Monoid/03A.dhall +++ b/tests/typecheck/examples/Monoid/03A.dhall @@ -1 +1 @@ -../../../../Prelude/Bool/odd +(../../../../Prelude/package.dhall).`Bool`.odd diff --git a/tests/typecheck/examples/Monoid/04A.dhall b/tests/typecheck/examples/Monoid/04A.dhall index e148ce3af..9724856c7 100644 --- a/tests/typecheck/examples/Monoid/04A.dhall +++ b/tests/typecheck/examples/Monoid/04A.dhall @@ -1 +1 @@ -../../../../Prelude/List/concat +(../../../../Prelude/package.dhall).`List`.concat diff --git a/tests/typecheck/examples/Monoid/05A.dhall b/tests/typecheck/examples/Monoid/05A.dhall index 910b536da..93ffbcc22 100644 --- a/tests/typecheck/examples/Monoid/05A.dhall +++ b/tests/typecheck/examples/Monoid/05A.dhall @@ -1 +1 @@ -../../../../Prelude/List/shifted +(../../../../Prelude/package.dhall).`List`.shifted diff --git a/tests/typecheck/examples/Monoid/06A.dhall b/tests/typecheck/examples/Monoid/06A.dhall index 74b10a1a6..311084342 100644 --- a/tests/typecheck/examples/Monoid/06A.dhall +++ b/tests/typecheck/examples/Monoid/06A.dhall @@ -1 +1 @@ -../../../../Prelude/Natural/sum +(../../../../Prelude/package.dhall).`Natural`.sum diff --git a/tests/typecheck/examples/Monoid/07A.dhall b/tests/typecheck/examples/Monoid/07A.dhall index 2b213fdf9..832472680 100644 --- a/tests/typecheck/examples/Monoid/07A.dhall +++ b/tests/typecheck/examples/Monoid/07A.dhall @@ -1 +1 @@ -../../../../Prelude/Natural/product +(../../../../Prelude/package.dhall).`Natural`.product diff --git a/tests/typecheck/examples/Monoid/08A.dhall b/tests/typecheck/examples/Monoid/08A.dhall index 545cf8a95..0daa732af 100644 --- a/tests/typecheck/examples/Monoid/08A.dhall +++ b/tests/typecheck/examples/Monoid/08A.dhall @@ -1 +1 @@ -../../../../Prelude/Optional/head +(../../../../Prelude/package.dhall).`Optional`.head diff --git a/tests/typecheck/examples/Monoid/09A.dhall b/tests/typecheck/examples/Monoid/09A.dhall index b5621a0f4..3ff6920b8 100644 --- a/tests/typecheck/examples/Monoid/09A.dhall +++ b/tests/typecheck/examples/Monoid/09A.dhall @@ -1 +1 @@ -../../../../Prelude/Optional/last +(../../../../Prelude/package.dhall).`Optional`.last diff --git a/tests/typecheck/examples/Monoid/10A.dhall b/tests/typecheck/examples/Monoid/10A.dhall index 6e9454f4a..effda30e2 100644 --- a/tests/typecheck/examples/Monoid/10A.dhall +++ b/tests/typecheck/examples/Monoid/10A.dhall @@ -1 +1 @@ -../../../../Prelude/Text/concat +(../../../../Prelude/package.dhall).`Text`.concat