diff --git a/Bool/and.dhall b/Bool/and.dhall
deleted file mode 100644
index 6b4e35c..0000000
--- a/Bool/and.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
-{-|
-The `and` function returns `False` if there are any `False` elements in the
-`List` and returns `True` otherwise
--}
-let and
- : List Bool → Bool
- = λ(xs : List Bool) →
- List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True
-
-let example0 = assert : and [ True, False, True ] ≡ False
-
-let example1 = assert : and ([] : List Bool) ≡ True
-
-in and
diff --git a/Bool/build.dhall b/Bool/build.dhall
deleted file mode 100644
index 03f3c81..0000000
--- a/Bool/build.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
---| `build` is the inverse of `fold`
-let build
- : (∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool
- = λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) →
- f Bool True False
-
-let example0 =
- assert
- : build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) ≡ True
-
-let example1 =
- assert
- : build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false)
- ≡ False
-
-in build
diff --git a/Bool/even.dhall b/Bool/even.dhall
deleted file mode 100644
index 9f5515e..0000000
--- a/Bool/even.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-{-|
-Returns `True` if there are an even number of `False` elements in the list and
-returns `False` otherwise.
-
-This function is the `Monoid` for the `==` operation.
--}
-let even
- : List Bool → Bool
- = λ(xs : List Bool) →
- List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True
-
-let example0 = assert : even [ False, True, False ] ≡ True
-
-let example1 = assert : even [ False, True ] ≡ False
-
-let example2 = assert : even [ False ] ≡ False
-
-let example3 = assert : even ([] : List Bool) ≡ True
-
-in even
diff --git a/Bool/fold.dhall b/Bool/fold.dhall
deleted file mode 100644
index 5bfcfbf..0000000
--- a/Bool/fold.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
---| `fold` is essentially the same as `if`/`then`/`else` except as a function
-let fold
- : ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
- = λ(b : Bool) →
- λ(bool : Type) →
- λ(true : bool) →
- λ(false : bool) →
- if b then true else false
-
-let example0 = assert : fold True Natural 0 1 ≡ 0
-
-let example1 = assert : fold False Natural 0 1 ≡ 1
-
-in fold
diff --git a/Bool/not.dhall b/Bool/not.dhall
deleted file mode 100644
index 3d58e9e..0000000
--- a/Bool/not.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Flip the value of a `Bool`
-let not
- : Bool → Bool
- = λ(b : Bool) → b == False
-
-let example0 = assert : not True ≡ False
-
-let example1 = assert : not False ≡ True
-
-in not
diff --git a/Bool/odd.dhall b/Bool/odd.dhall
deleted file mode 100644
index 2c0d1d9..0000000
--- a/Bool/odd.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-{-|
-Returns `True` if there are an odd number of `True` elements in the list and
-returns `False` otherwise.
-
-This function is the `Monoid` for the `!=` operation.
--}
-let odd
- : List Bool → Bool
- = λ(xs : List Bool) →
- List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False
-
-let example0 = assert : odd [ True, False, True ] ≡ False
-
-let example1 = assert : odd [ True, False ] ≡ True
-
-let example2 = assert : odd [ True ] ≡ True
-
-let example3 = assert : odd ([] : List Bool) ≡ False
-
-in odd
diff --git a/Bool/or.dhall b/Bool/or.dhall
deleted file mode 100644
index 6f1642c..0000000
--- a/Bool/or.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
-{-|
-The `or` function returns `True` if there are any `True` elements in the `List`
-and returns `False` otherwise
--}
-let or
- : List Bool → Bool
- = λ(xs : List Bool) →
- List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False
-
-let example0 = assert : or [ True, False, True ] ≡ True
-
-let example1 = assert : or ([] : List Bool) ≡ False
-
-in or
diff --git a/Bool/package.dhall b/Bool/package.dhall
index 883ac99..e15fef4 100644
--- a/Bool/package.dhall
+++ b/Bool/package.dhall
@@ -1,12 +1 @@
-λ(nix : ../NixPrelude.dhall) →
- { Type = Bool
- , and = ./and.dhall
- , build = ./build.dhall
- , even = ./even.dhall
- , fold = ./fold.dhall
- , fromAny = ./fromAny.dhall nix
- , not = ./not.dhall
- , odd = ./odd.dhall
- , or = ./or.dhall
- , show = ./show.dhall
- }
+λ(nix : ../NixPrelude.dhall) → { Type = Bool, fromAny = ./fromAny.dhall nix }
diff --git a/Bool/show.dhall b/Bool/show.dhall
deleted file mode 100644
index 434001e..0000000
--- a/Bool/show.dhall
+++ /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)
--}
-let show
- : Bool → Text
- = λ(b : Bool) → if b then "True" else "False"
-
-let example0 = assert : show True ≡ "True"
-
-let example1 = assert : show False ≡ "False"
-
-in show
diff --git a/Double/package.dhall b/Double/package.dhall
index 4f0f0b8..eebe615 100644
--- a/Double/package.dhall
+++ b/Double/package.dhall
@@ -23,7 +23,6 @@
, nonPositive = ./nonPositive.dhall nix
, positive = ./positive.dhall nix
, product = ./product.dhall nix
- , show = ./show.dhall
, sort = ./sort.dhall nix
, subtract = ./subtract.dhall nix
, sum = ./sum.dhall nix
diff --git a/Double/show.dhall b/Double/show.dhall
deleted file mode 100644
index 443515d..0000000
--- a/Double/show.dhall
+++ /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)
--}
-let show
- : Double → Text
- = Double/show
-
-let example0 = assert : show -3.1 ≡ "-3.1"
-
-let example1 = assert : show 0.4 ≡ "0.4"
-
-in show
diff --git a/Function/compose.dhall b/Function/compose.dhall
deleted file mode 100644
index 3931702..0000000
--- a/Function/compose.dhall
+++ /dev/null
@@ -1,17 +0,0 @@
---| Compose two functions into one.
-let compose
- : ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
- = λ(A : Type) →
- λ(B : Type) →
- λ(C : Type) →
- λ(f : A → B) →
- λ(g : B → C) →
- λ(x : A) →
- g (f x)
-
-let example0 =
- assert
- : compose Natural Natural Bool (λ(n : Natural) → n + n) Natural/even 3
- ≡ True
-
-in compose
diff --git a/Function/identity.dhall b/Function/identity.dhall
deleted file mode 100644
index 40d3a67..0000000
--- a/Function/identity.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| The identity function simply returns its input
-let identity
- : ∀(a : Type) → ∀(x : a) → a
- = λ(a : Type) → λ(x : a) → x
-
-let example0 = assert : identity Natural 1 ≡ 1
-
-let example1 = assert : identity Bool ≡ (λ(x : Bool) → x)
-
-in identity
diff --git a/Function/package.dhall b/Function/package.dhall
deleted file mode 100644
index ddd5532..0000000
--- a/Function/package.dhall
+++ /dev/null
@@ -1 +0,0 @@
-{ compose = ./compose.dhall, identity = ./identity.dhall }
diff --git a/Integer/abs.dhall b/Integer/abs.dhall
deleted file mode 100644
index f32770a..0000000
--- a/Integer/abs.dhall
+++ /dev/null
@@ -1,15 +0,0 @@
---| Returns the absolute value of an `Integer`, i.e. its non-negative value.
-let abs
- : Integer → Natural
- = λ(n : Integer) →
- if Natural/isZero (Integer/clamp n)
- then Integer/clamp (Integer/negate n)
- else Integer/clamp n
-
-let example0 = assert : abs +7 ≡ 7
-
-let example2 = assert : abs +0 ≡ 0
-
-let example3 = assert : abs -3 ≡ 3
-
-in abs
diff --git a/Integer/add.dhall b/Integer/add.dhall
deleted file mode 100644
index 087f01a..0000000
--- a/Integer/add.dhall
+++ /dev/null
@@ -1,22 +0,0 @@
---| `add m n` computes `m + n`.
-let Integer/subtract = ./subtract.dhall
-
-let add
- : Integer → Integer → Integer
- = λ(m : Integer) → λ(n : Integer) → Integer/subtract (Integer/negate m) n
-
-let example0 = assert : add +3 +5 ≡ +8
-
-let example1 = assert : add -3 -5 ≡ -8
-
-let example2 = assert : add -4 +4 ≡ +0
-
-let example3 = assert : add -3 +5 ≡ +2
-
-let example4 = assert : add +3 -5 ≡ -2
-
-let example5 = assert : add +0 -3 ≡ -3
-
-let example6 = assert : add +0 +3 ≡ +3
-
-in add
diff --git a/Integer/build.dhall b/Integer/build.dhall
index deaa8b3..e6732ea 100644
--- a/Integer/build.dhall
+++ b/Integer/build.dhall
@@ -1,6 +1,6 @@
-let Integer/add = ./add.dhall
+let Integer/add = https://prelude.dhall-lang.org/Integer/add.dhall
-let negate = ./negate.dhall
+let negate = https://prelude.dhall-lang.org/Integer/negate.dhall
let Integer/succ
: Integer → Integer
diff --git a/Integer/clamp.dhall b/Integer/clamp.dhall
deleted file mode 100644
index c55f73d..0000000
--- a/Integer/clamp.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
-{-|
-Convert an `Integer` to a `Natural` number, with negative numbers becoming zero.
--}
-let clamp
- : Integer → Natural
- = Integer/clamp
-
-let example0 = assert : clamp +7 ≡ 7
-
-let example2 = assert : clamp +0 ≡ 0
-
-let example3 = assert : clamp -3 ≡ 0
-
-in clamp
diff --git a/Integer/equal.dhall b/Integer/equal.dhall
deleted file mode 100644
index 5933f29..0000000
--- a/Integer/equal.dhall
+++ /dev/null
@@ -1,21 +0,0 @@
---| `equal` checks if two Integers are equal.
-let Natural/equal = ../Natural/equal.dhall
-
-let equal
- : Integer → Integer → Bool
- = λ(a : Integer) →
- λ(b : Integer) →
- Natural/equal (Integer/clamp a) (Integer/clamp b)
- && Natural/equal
- (Integer/clamp (Integer/negate a))
- (Integer/clamp (Integer/negate b))
-
-let example0 = assert : equal +5 +5 ≡ True
-
-let example1 = assert : equal +5 +6 ≡ False
-
-let example2 = assert : equal +5 -5 ≡ False
-
-let example3 = assert : equal -5 -5 ≡ True
-
-in equal
diff --git a/Integer/fold.dhall b/Integer/fold.dhall
index e40ac2d..f4acbdb 100644
--- a/Integer/fold.dhall
+++ b/Integer/fold.dhall
@@ -1,6 +1,6 @@
-let Integer/negative = ./negative.dhall
+let Integer/negative = https://prelude.dhall-lang.org/Integer/negative.dhall
-let Integer/abs = ./abs.dhall
+let Integer/abs = https://prelude.dhall-lang.org/Integer/abs.dhall
let fold
: Integer →
diff --git a/Integer/greaterThan.dhall b/Integer/greaterThan.dhall
deleted file mode 100644
index 6eb91a9..0000000
--- a/Integer/greaterThan.dhall
+++ /dev/null
@@ -1,24 +0,0 @@
---| `greaterThan` checks if one Integer is greater than another.
-let Bool/not = ../Bool/not.dhall
-
-let lessThanEqual = ./lessThanEqual.dhall
-
-let greaterThan
- : Integer → Integer → Bool
- = λ(x : Integer) → λ(y : Integer) → Bool/not (lessThanEqual x y)
-
-let example0 = assert : greaterThan +5 +6 ≡ False
-
-let example1 = assert : greaterThan +5 +5 ≡ False
-
-let example2 = assert : greaterThan +5 +4 ≡ True
-
-let example3 = assert : greaterThan -5 +8 ≡ False
-
-let example4 = assert : greaterThan -5 -3 ≡ False
-
-let example5 = assert : greaterThan -3 -5 ≡ True
-
-let example6 = assert : greaterThan -3 -3 ≡ False
-
-in greaterThan
diff --git a/Integer/greaterThanEqual.dhall b/Integer/greaterThanEqual.dhall
deleted file mode 100644
index 73be7fd..0000000
--- a/Integer/greaterThanEqual.dhall
+++ /dev/null
@@ -1,24 +0,0 @@
-{-|
-`greaterThanEqual` checks if one Integer is greater than or equal to another.
--}
-let lessThanEqual = ./lessThanEqual.dhall
-
-let greaterThanEqual
- : Integer → Integer → Bool
- = λ(x : Integer) → λ(y : Integer) → lessThanEqual y x
-
-let example0 = assert : greaterThanEqual +5 +6 ≡ False
-
-let example1 = assert : greaterThanEqual +5 +5 ≡ True
-
-let example2 = assert : greaterThanEqual +5 +4 ≡ True
-
-let example3 = assert : greaterThanEqual -5 +8 ≡ False
-
-let example4 = assert : greaterThanEqual -5 -3 ≡ False
-
-let example5 = assert : greaterThanEqual -3 -5 ≡ True
-
-let example6 = assert : greaterThanEqual -3 -3 ≡ True
-
-in greaterThanEqual
diff --git a/Integer/isZero.dhall b/Integer/isZero.dhall
index bb4416a..bbbb944 100644
--- a/Integer/isZero.dhall
+++ b/Integer/isZero.dhall
@@ -1,6 +1,6 @@
-let Integer/nonPositive = ./nonPositive.dhall
+let Integer/nonPositive = https://prelude.dhall-lang.org/Integer/nonPositive.dhall
-let Integer/nonNegative = ./nonNegative.dhall
+let Integer/nonNegative = https://prelude.dhall-lang.org/Integer/nonNegative.dhall
let isZero
: Integer → Bool
diff --git a/Integer/lessThan.dhall b/Integer/lessThan.dhall
deleted file mode 100644
index 9b5cd93..0000000
--- a/Integer/lessThan.dhall
+++ /dev/null
@@ -1,22 +0,0 @@
---| `lessThan` checks if one Integer is less than another.
-let greaterThan = ./greaterThan.dhall
-
-let lessThan
- : Integer → Integer → Bool
- = λ(x : Integer) → λ(y : Integer) → greaterThan y x
-
-let example0 = assert : lessThan +5 +6 ≡ True
-
-let example1 = assert : lessThan +5 +5 ≡ False
-
-let example2 = assert : lessThan +5 +4 ≡ False
-
-let example3 = assert : lessThan -5 +8 ≡ True
-
-let example4 = assert : lessThan -5 -3 ≡ True
-
-let example5 = assert : lessThan -3 -5 ≡ False
-
-let example6 = assert : lessThan -3 -3 ≡ False
-
-in lessThan
diff --git a/Integer/lessThanEqual.dhall b/Integer/lessThanEqual.dhall
deleted file mode 100644
index 6105e39..0000000
--- a/Integer/lessThanEqual.dhall
+++ /dev/null
@@ -1,35 +0,0 @@
---| `lessThanEqual` checks if one Integer is less than or equal to another.
-let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall
-
-let Natural/lessThanEqual = ../Natural/lessThanEqual.dhall
-
-let nonPositive = ./nonPositive.dhall
-
-let nonNegative = ./nonNegative.dhall
-
-let lessThanEqual
- : Integer → Integer → Bool
- = λ(x : Integer) →
- λ(y : Integer) →
- if nonPositive x
- then nonNegative y
- || Natural/greaterThanEqual
- (Integer/clamp (Integer/negate x))
- (Integer/clamp (Integer/negate y))
- else Natural/lessThanEqual (Integer/clamp x) (Integer/clamp y)
-
-let example0 = assert : lessThanEqual +5 +6 ≡ True
-
-let example1 = assert : lessThanEqual +5 +5 ≡ True
-
-let example2 = assert : lessThanEqual +5 +4 ≡ False
-
-let example3 = assert : lessThanEqual -5 +8 ≡ True
-
-let example4 = assert : lessThanEqual -5 -3 ≡ True
-
-let example5 = assert : lessThanEqual -3 -5 ≡ False
-
-let example6 = assert : lessThanEqual -3 -3 ≡ True
-
-in lessThanEqual
diff --git a/Integer/max.dhall b/Integer/max.dhall
index 4d5f7fb..da6be5f 100644
--- a/Integer/max.dhall
+++ b/Integer/max.dhall
@@ -1,5 +1,5 @@
--| `max a b` returns the larger of `a` or `b`
-let lessThanEqual = ./lessThanEqual.dhall
+let lessThanEqual = https://prelude.dhall-lang.org/Integer/lessThanEqual.dhall
let max
: Integer → Integer → Integer
diff --git a/Integer/min.dhall b/Integer/min.dhall
index 246ba56..337b560 100644
--- a/Integer/min.dhall
+++ b/Integer/min.dhall
@@ -1,5 +1,5 @@
--| `min a b` returns the smaller of `a` or `b`
-let lessThanEqual = ./lessThanEqual.dhall
+let lessThanEqual = https://prelude.dhall-lang.org/Integer/lessThanEqual.dhall
let min
: Integer → Integer → Integer
diff --git a/Integer/multiply.dhall b/Integer/multiply.dhall
deleted file mode 100644
index f6a4f78..0000000
--- a/Integer/multiply.dhall
+++ /dev/null
@@ -1,37 +0,0 @@
---| `multiply m n` computes `m * n`.
-let nonPositive = ./nonPositive.dhall
-
-let multiplyNonNegative =
- λ(x : Integer) →
- λ(y : Integer) →
- Natural/toInteger (Integer/clamp x * Integer/clamp y)
-
-let multiply
- : Integer → Integer → Integer
- = λ(m : Integer) →
- λ(n : Integer) →
- if nonPositive m
- then if nonPositive n
- then multiplyNonNegative (Integer/negate m) (Integer/negate n)
- else Integer/negate (multiplyNonNegative (Integer/negate m) n)
- else if nonPositive n
- then Integer/negate (multiplyNonNegative m (Integer/negate n))
- else multiplyNonNegative m n
-
-let example0 = assert : multiply +3 +5 ≡ +15
-
-let example1 = assert : multiply -3 +5 ≡ -15
-
-let example2 = assert : multiply -3 -5 ≡ +15
-
-let example3 = assert : multiply +0 +5 ≡ +0
-
-let example4 = assert : multiply +5 +0 ≡ +0
-
-let example5 = assert : multiply +0 +0 ≡ +0
-
-let example6 = assert : multiply +1 +5 ≡ +5
-
-let example7 = assert : multiply +3 -1 ≡ -3
-
-in multiply
diff --git a/Integer/negate.dhall b/Integer/negate.dhall
deleted file mode 100644
index 03eff72..0000000
--- a/Integer/negate.dhall
+++ /dev/null
@@ -1,12 +0,0 @@
---| Invert the sign of an `Integer`, with zero remaining unchanged.
-let negate
- : Integer → Integer
- = Integer/negate
-
-let example0 = assert : negate -3 ≡ +3
-
-let example2 = assert : negate +7 ≡ -7
-
-let example3 = assert : negate +0 ≡ +0
-
-in negate
diff --git a/Integer/negative.dhall b/Integer/negative.dhall
deleted file mode 100644
index c05bb65..0000000
--- a/Integer/negative.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
-{-|
-Returns `True` for any `Integer` less than `+0`.
-
-`negative` is more efficient than `./lessThan +0` or `./lessThanEqual -1`.
--}
-let positive = ./positive.dhall
-
-let negative
- : Integer → Bool
- = λ(n : Integer) → positive (Integer/negate n)
-
-let example0 = assert : negative +1 ≡ False
-
-let example1 = assert : negative +0 ≡ False
-
-let example2 = assert : negative -1 ≡ True
-
-in negative
diff --git a/Integer/nonNegative.dhall b/Integer/nonNegative.dhall
deleted file mode 100644
index 7f08249..0000000
--- a/Integer/nonNegative.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
-{-|
-Returns `True` for `+0` and any positive `Integer`.
-
-`nonNegative` is more efficient than `./greaterThanEqual +0` or `./greaterThan -1`.
--}
-let nonPositive = ./nonPositive.dhall
-
-let nonNegative
- : Integer → Bool
- = λ(n : Integer) → nonPositive (Integer/negate n)
-
-let example0 = assert : nonNegative +1 ≡ True
-
-let example1 = assert : nonNegative +0 ≡ True
-
-let example2 = assert : nonNegative -1 ≡ False
-
-in nonNegative
diff --git a/Integer/nonPositive.dhall b/Integer/nonPositive.dhall
deleted file mode 100644
index f7d7a49..0000000
--- a/Integer/nonPositive.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
-{-|
-Returns `True` for `+0` and any negative `Integer`.
-
-`nonPositive` is more efficient than `./lessThanEqual +0` or `./lessThan +1`.
--}
-let nonPositive
- : Integer → Bool
- = λ(n : Integer) → Natural/isZero (Integer/clamp n)
-
-let example0 = assert : nonPositive +1 ≡ False
-
-let example1 = assert : nonPositive +0 ≡ True
-
-let example2 = assert : nonPositive -1 ≡ True
-
-in nonPositive
diff --git a/Integer/package.dhall b/Integer/package.dhall
index 7fcbaed..f177f6e 100644
--- a/Integer/package.dhall
+++ b/Integer/package.dhall
@@ -1,33 +1,12 @@
λ(nix : ../NixPrelude.dhall) →
{ Type = Integer
- , abs = ./abs.dhall
- , add = ./add.dhall
, build = ./build.dhall
- , clamp = ./clamp.dhall
, divide = ./divide.dhall nix
- , equal = ./equal.dhall
, fold = ./fold.dhall
, fromAny = ./fromAny.dhall nix
- , greaterThan = ./greaterThan.dhall
- , greaterThanEqual = ./greaterThanEqual.dhall
, isZero = ./isZero.dhall
- , lessThan = ./lessThan.dhall
- , lessThanEqual = ./lessThanEqual.dhall
, listMax = ./listMax.dhall nix
, listMin = ./listMin.dhall nix
- , max = ./max.dhall
- , min = ./min.dhall
- , multiply = ./multiply.dhall
- , negate = ./negate.dhall
- , negative = ./negative.dhall
- , nonNegative = ./nonNegative.dhall
- , nonPositive = ./nonPositive.dhall
- , positive = ./positive.dhall
, product = ./product.dhall
- , show = ./show.dhall
, sort = ./sort.dhall nix
- , subtract = ./subtract.dhall
- , sum = ./sum.dhall
- , toDouble = ./toDouble.dhall
- , toNatural = ./toNatural.dhall
}
diff --git a/Integer/positive.dhall b/Integer/positive.dhall
deleted file mode 100644
index 2f279b9..0000000
--- a/Integer/positive.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-{-|
-Returns `True` for any `Integer` greater than `+0`.
-
-`positive` is more efficient than `./greaterThan +0` or `./greaterThanEqual +1`.
--}
-let not = ../Bool/not.dhall
-
-let nonPositive = ./nonPositive.dhall
-
-let positive
- : Integer → Bool
- = λ(n : Integer) → not (nonPositive n)
-
-let example0 = assert : positive +1 ≡ True
-
-let example1 = assert : positive +0 ≡ False
-
-let example2 = assert : positive -1 ≡ False
-
-in positive
diff --git a/Integer/product.dhall b/Integer/product.dhall
index eaddd19..2c52c38 100644
--- a/Integer/product.dhall
+++ b/Integer/product.dhall
@@ -1,5 +1,5 @@
--| Multiply all the numbers in a `List`
-let Integer/multiply = ./multiply.dhall
+let Integer/multiply = https://prelude.dhall-lang.org/Integer/multiply.dhall
let product
: List Integer → Integer
diff --git a/Integer/show.dhall b/Integer/show.dhall
deleted file mode 100644
index 33e6b5a..0000000
--- a/Integer/show.dhall
+++ /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)
--}
-let show
- : Integer → Text
- = Integer/show
-
-let example0 = assert : show -3 ≡ "-3"
-
-let example1 = assert : show +0 ≡ "+0"
-
-in show
diff --git a/Integer/subtract.dhall b/Integer/subtract.dhall
deleted file mode 100644
index f5768b2..0000000
--- a/Integer/subtract.dhall
+++ /dev/null
@@ -1,51 +0,0 @@
---| `subtract m n` computes `n - m`.
-let nonPositive = ./nonPositive.dhall
-
-let subtractNonNegative =
- λ(xi : Integer) →
- λ(yi : Integer) →
- let xn = Integer/clamp xi
-
- let yn = Integer/clamp yi
-
- let dn = Natural/subtract xn yn
-
- in if Natural/isZero dn
- then Integer/negate (Natural/toInteger (Natural/subtract yn xn))
- else Natural/toInteger dn
-
-let subtract
- : Integer → Integer → Integer
- = λ(m : Integer) →
- λ(n : Integer) →
- if nonPositive m
- then if nonPositive n
- then subtractNonNegative (Integer/negate n) (Integer/negate m)
- else Natural/toInteger
- (Integer/clamp (Integer/negate m) + Integer/clamp n)
- else if nonPositive n
- then Integer/negate
- ( Natural/toInteger
- (Integer/clamp m + Integer/clamp (Integer/negate n))
- )
- else subtractNonNegative m n
-
-let example0 = assert : subtract +3 +5 ≡ +2
-
-let example1 = assert : subtract +4 +4 ≡ +0
-
-let example2 = assert : subtract +5 +3 ≡ -2
-
-let example3 = assert : subtract -3 -5 ≡ -2
-
-let example4 = assert : subtract -4 -4 ≡ +0
-
-let example5 = assert : subtract -5 -3 ≡ +2
-
-let example6 = assert : subtract -3 +5 ≡ +8
-
-let example7 = assert : subtract +3 -5 ≡ -8
-
-let example8 = assert : subtract +0 -3 ≡ -3
-
-in subtract
diff --git a/Integer/toDouble.dhall b/Integer/toDouble.dhall
deleted file mode 100644
index b5d1e61..0000000
--- a/Integer/toDouble.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Convert an `Integer` to the corresponding `Double`
-let toDouble
- : Integer → Double
- = Integer/toDouble
-
-let example0 = assert : toDouble -3 ≡ -3.0
-
-let example1 = assert : toDouble +2 ≡ 2.0
-
-in toDouble
diff --git a/Integer/toNatural.dhall b/Integer/toNatural.dhall
deleted file mode 100644
index fbbd05b..0000000
--- a/Integer/toNatural.dhall
+++ /dev/null
@@ -1,17 +0,0 @@
-{-|
-Convert an `Integer` to an `Optional Natural`, with negative numbers becoming `None Natural`.
--}
-let nonNegative = ./nonNegative.dhall
-
-let toNatural
- : Integer → Optional Natural
- = λ(n : Integer) →
- if nonNegative n then Some (Integer/clamp n) else None Natural
-
-let example0 = assert : toNatural +7 ≡ Some 7
-
-let example2 = assert : toNatural +0 ≡ Some 0
-
-let example3 = assert : toNatural -3 ≡ None Natural
-
-in toNatural
diff --git a/JSON/Format.dhall b/JSON/Format.dhall
deleted file mode 100644
index 649600b..0000000
--- a/JSON/Format.dhall
+++ /dev/null
@@ -1,7 +0,0 @@
-{-|
-An internal type used by `./renderAs` to select the output format.
-
-You should not need to use this type directly, simply use `./render`
-or `./renderYAML` as appropriate.
--}
-< YAML | JSON >
diff --git a/JSON/Nesting.dhall b/JSON/Nesting.dhall
deleted file mode 100644
index b371f73..0000000
--- a/JSON/Nesting.dhall
+++ /dev/null
@@ -1,35 +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 } >
-
-let Nesting = < Inline | Nested : Text >
-
-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/JSON/Tagged.dhall b/JSON/Tagged.dhall
deleted file mode 100644
index 9576d46..0000000
--- a/JSON/Tagged.dhall
+++ /dev/null
@@ -1,67 +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
-
-let Provisioner =
- < shell :
- { inline : List Text }
- | file :
- { source : Text, destination : Text }
- >
-
-let Tagged = ./Tagged
-
-let Nesting = ./Nesting
-
-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.dhall, contents : a }
-
-in Tagged
diff --git a/JSON/Type.dhall b/JSON/Type.dhall
deleted file mode 100644
index 83caf24..0000000
--- a/JSON/Type.dhall
+++ /dev/null
@@ -1,63 +0,0 @@
-{-|
-Dhall encoding of an arbitrary JSON value
-
-For example, the following JSON value:
-
-```
-[ { "foo": null, "bar": [ 1.0, true ] } ]
-```
-
-... corresponds to the following Dhall expression:
-
-```
-λ(JSON : Type) →
-λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , null : JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.object
- [ { mapKey = "foo", mapValue = json.null }
- , { mapKey = "bar"
- , mapValue = json.array [ json.double 1.0, json.bool True ]
- }
- ]
-```
-
- You do not need to create these values directly, though. You can use
- the utilities exported by `./package.dhall` to create values of this type,
- such as:
-
-```
-let JSON = ./package.dhall
-
-in JSON.object
- [ { mapKey = "foo", mapValue = JSON.null }
- , { mapKey = "bar"
- , mapValue = JSON.array [ JSON.double 1.0, JSON.bool True ]
- }
- ]
-```
-
--}
-let JSON/Type
- : Type
- = ∀(JSON : Type) →
- ∀ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- JSON
-
-in JSON/Type
diff --git a/JSON/array.dhall b/JSON/array.dhall
deleted file mode 100644
index 3ad7bc7..0000000
--- a/JSON/array.dhall
+++ /dev/null
@@ -1,35 +0,0 @@
-{-|
-Create a JSON array from a `List` of JSON values
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.array [ JSON.double 1.0, JSON.bool True ])
-= "[ 1.0, true ]"
-
-let JSON/Type = ./Type
-let JSON = ./package.dhall
-in JSON.render (JSON.array ([] : List JSON/Type))
-= "[ ]"
-```
--}
-let JSON = ./Type.dhall
-
-let List/map = ../List/map.dhall
-
-let array
- : List JSON → JSON
- = λ(x : List JSON) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.array (List/map JSON@1 JSON (λ(j : JSON@1) → j JSON json) x)
-
-in array
diff --git a/JSON/bool.dhall b/JSON/bool.dhall
deleted file mode 100644
index de45b0c..0000000
--- a/JSON/bool.dhall
+++ /dev/null
@@ -1,32 +0,0 @@
-{-|
-Create a JSON bool from a Dhall `Bool`
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.bool True)
-= "true"
-
-let JSON = ./package.dhall
-in JSON.render (JSON.bool False)
-= "false"
-```
--}
-let JSON = ./Type.dhall
-
-let bool
- : Bool → JSON
- = λ(x : Bool) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.bool x
-
-in bool
diff --git a/JSON/core.dhall b/JSON/core.dhall
deleted file mode 100644
index 77c1fd8..0000000
--- a/JSON/core.dhall
+++ /dev/null
@@ -1,25 +0,0 @@
-{-|
-A record of functions useful for constructing `JSON` values.
-
-This is only a subset of what `package.dhall` exports. If you are not writing a
-JSON prelude function, you should use the `package.dhall` file instead.
-
-It is used internally by `render`, `renderYAML` and `omitNullFields` instead of
-`package.dhall` to avoid import cycles.
--}
-{ Type = ./Type.dhall
-, Tagged = ./Tagged.dhall
-, Nesting = ./Nesting.dhall
-, keyText = ./keyText.dhall
-, keyValue = ./keyValue.dhall
-, string = ./string.dhall
-, number = ./number.dhall
-, double = ./double.dhall
-, integer = ./integer.dhall
-, natural = ./natural.dhall
-, object = ./object.dhall
-, array = ./array.dhall
-, bool = ./bool.dhall
-, null = ./null.dhall
-, renderInteger = ./renderInteger.dhall
-}
diff --git a/JSON/double.dhall b/JSON/double.dhall
deleted file mode 100644
index 5c0c8f3..0000000
--- a/JSON/double.dhall
+++ /dev/null
@@ -1,32 +0,0 @@
-{-|
-Create a JSON number from a Dhall `Double`
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.double 42.0)
-= "42.0"
-
-let JSON = ./package.dhall
-in JSON.render (JSON.double -1.5e-10)
-= "-1.5e-10"
-```
--}
-let JSON = ./Type.dhall
-
-let double
- : Double → JSON
- = λ(x : Double) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.double x
-
-in double
diff --git a/JSON/integer.dhall b/JSON/integer.dhall
deleted file mode 100644
index 2aaa3bd..0000000
--- a/JSON/integer.dhall
+++ /dev/null
@@ -1,32 +0,0 @@
-{-|
-Create a JSON number from a Dhall `Integer`
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.integer -1)
-= "-1"
-
-let JSON = ./package.dhall
-in JSON.render (JSON.integer +2)
-= "+2"
-```
--}
-let JSON = ./Type.dhall
-
-let integer
- : Integer → JSON
- = λ(x : Integer) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.integer x
-
-in integer
diff --git a/JSON/keyText.dhall b/JSON/keyText.dhall
deleted file mode 100644
index 170a41e..0000000
--- a/JSON/keyText.dhall
+++ /dev/null
@@ -1 +0,0 @@
-../Map/keyText.dhall
diff --git a/JSON/keyValue.dhall b/JSON/keyValue.dhall
deleted file mode 100644
index 81f1a24..0000000
--- a/JSON/keyValue.dhall
+++ /dev/null
@@ -1 +0,0 @@
-../Map/keyValue.dhall
diff --git a/JSON/natural.dhall b/JSON/natural.dhall
deleted file mode 100644
index 18680c8..0000000
--- a/JSON/natural.dhall
+++ /dev/null
@@ -1,28 +0,0 @@
-{-|
-Create a JSON number from a Dhall `Natural`
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.natural 42)
-= "42"
-```
--}
-let JSON = ./Type.dhall
-
-let natural
- : Natural → JSON
- = λ(x : Natural) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.integer (Natural/toInteger x)
-
-in natural
diff --git a/JSON/null.dhall b/JSON/null.dhall
deleted file mode 100644
index d25198c..0000000
--- a/JSON/null.dhall
+++ /dev/null
@@ -1,27 +0,0 @@
-{-|
-Create a JSON null
-
-```
-let JSON = ./package.dhall
-in JSON.render JSON.null
-= "null"
-```
--}
-let JSON = ./Type.dhall
-
-let null
- : JSON
- = λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.null
-
-in null
diff --git a/JSON/number.dhall b/JSON/number.dhall
deleted file mode 100644
index a940106..0000000
--- a/JSON/number.dhall
+++ /dev/null
@@ -1,22 +0,0 @@
-{-|
-Create a JSON number from a Dhall `Double`
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.number 42.0)
-= "42.0"
-
-let JSON = ./package.dhall
-in JSON.render (JSON.number -1.5e-10)
-= "-1.5e-10"
-```
--}
-let JSON = ./Type.dhall
-
-let double = ./double.dhall
-
-let number
- : Double → JSON
- = double
-
-in number
diff --git a/JSON/object.dhall b/JSON/object.dhall
deleted file mode 100644
index d945e96..0000000
--- a/JSON/object.dhall
+++ /dev/null
@@ -1,49 +0,0 @@
-{-|
-Create a JSON object from a Dhall `Map`
-
-```
-let JSON = ./package.dhall
-in JSON.render
- ( JSON.object
- [ { mapKey = "foo", mapValue = JSON.double 1.0 }
- , { mapKey = "bar", mapValue = JSON.bool True }
- ]
- )
-= "{ \"foo\": 1.0, \"bar\": true }"
-
-let JSON/Type = ./Type
-let JSON = ./package.dhall
-in JSON.render
- (JSON.object ([] : List { mapKey : Text, mapValue : JSON/Type }))
-= "{ }"
-```
--}
-let JSON = ./Type.dhall
-
-let List/map = ../List/map.dhall
-
-let object
- : List { mapKey : Text, mapValue : JSON } → JSON
- = λ(x : List { mapKey : Text, mapValue : JSON }) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.object
- ( List/map
- { mapKey : Text, mapValue : JSON@1 }
- { mapKey : Text, mapValue : JSON }
- ( λ(kv : { mapKey : Text, mapValue : JSON@1 }) →
- { mapKey = kv.mapKey, mapValue = kv.mapValue JSON json }
- )
- x
- )
-
-in object
diff --git a/JSON/omitNullFields.dhall b/JSON/omitNullFields.dhall
deleted file mode 100644
index b0be24e..0000000
--- a/JSON/omitNullFields.dhall
+++ /dev/null
@@ -1,136 +0,0 @@
-{-|
-This utility omits all `null` record fields, which is often the idiomatic way
-for a configuration to encode absent fields
--}
-let JSON = ./core.dhall
-
-let List/concatMap = ../List/concatMap.dhall
-
-let List/map = ../List/map.dhall
-
-let omitNullFields
- : JSON.Type → JSON.Type
- = λ(old : JSON.Type) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- let result =
- old
- { value : JSON, isNull : Bool }
- { string =
- λ(x : Text) → { value = json.string x, isNull = False }
- , double =
- λ(x : Double) → { value = json.double x, isNull = False }
- , integer =
- λ(x : Integer) → { value = json.integer x, isNull = False }
- , object =
- λ ( keyValues
- : List
- { mapKey : Text
- , mapValue : { value : JSON, isNull : Bool }
- }
- ) →
- let value =
- json.object
- ( List/concatMap
- { mapKey : Text
- , mapValue : { value : JSON, isNull : Bool }
- }
- { mapKey : Text, mapValue : JSON }
- ( λ ( keyValue
- : { mapKey : Text
- , mapValue :
- { value : JSON, isNull : Bool }
- }
- ) →
- if keyValue.mapValue.isNull
- then [] : List
- { mapKey : Text
- , mapValue : JSON
- }
- else [ keyValue.{ mapKey }
- ∧ { mapValue =
- keyValue.mapValue.value
- }
- ]
- )
- keyValues
- )
-
- in { value, isNull = False }
- , array =
- λ(xs : List { value : JSON, isNull : Bool }) →
- let value =
- json.array
- ( List/map
- { value : JSON, isNull : Bool }
- JSON
- ( λ(x : { value : JSON, isNull : Bool }) →
- x.value
- )
- xs
- )
-
- in { value, isNull = False }
- , bool = λ(x : Bool) → { value = json.bool x, isNull = False }
- , null = { value = json.null, isNull = True }
- }
-
- in result.value
-
-let property =
- λ(a : Text) →
- λ(b : Double) →
- λ(c : Bool) →
- assert
- : omitNullFields
- ( JSON.object
- ( toMap
- { string = JSON.string a
- , double = JSON.double b
- , bool = JSON.bool c
- , null = JSON.null
- }
- )
- )
- ≡ JSON.object
- ( toMap
- { string = JSON.string a
- , double = JSON.double b
- , bool = JSON.bool c
- }
- )
-
-let example =
- assert
- : omitNullFields
- ( JSON.object
- ( toMap
- { array =
- JSON.array [ JSON.object (toMap { null = JSON.null }) ]
- }
- )
- )
- ≡ JSON.object
- ( toMap
- { array =
- JSON.array
- [ JSON.object
- ([] : List { mapKey : Text, mapValue : JSON.Type })
- ]
- }
- )
-
-let example =
- assert
- : omitNullFields (JSON.array [ JSON.null ]) ≡ JSON.array [ JSON.null ]
-
-in omitNullFields
diff --git a/JSON/package.dhall b/JSON/package.dhall
deleted file mode 100644
index d7c3139..0000000
--- a/JSON/package.dhall
+++ /dev/null
@@ -1,9 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- { render = ./render.dhall nix
- , renderCompact = ./renderCompact.dhall
- , renderYAML = ./renderYAML.dhall nix
- , omitNullFields = ./omitNullFields.dhall
- , tagInline = ./tagInline.dhall
- , tagNested = ./tagNested.dhall
- }
- ∧ ./core.dhall
diff --git a/JSON/render.dhall b/JSON/render.dhall
deleted file mode 100644
index de45c78..0000000
--- a/JSON/render.dhall
+++ /dev/null
@@ -1,12 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let JSON = ./core.dhall
-
- let Format = ./Format.dhall
-
- let renderAs = ./renderAs.dhall nix
-
- let render
- : JSON.Type → Text
- = renderAs Format.JSON
-
- in render
diff --git a/JSON/renderAs.dhall b/JSON/renderAs.dhall
deleted file mode 100644
index e71f8be..0000000
--- a/JSON/renderAs.dhall
+++ /dev/null
@@ -1,296 +0,0 @@
---| Render a `JSON` value as `Text` in either JSON or YAML format.
-λ(nix : ../NixPrelude.dhall) →
- let JSON = ./core.dhall
-
- let Function/identity = ../Function/identity.dhall
-
- let Text/concatMap = ../Text/concatMap.dhall
-
- let List/map = ../List/map.dhall
-
- let NonEmpty = ../NonEmpty/Type.dhall
-
- let NonEmpty/toList = ../NonEmpty/toList.dhall
-
- let NonEmpty/concat = ../NonEmpty/concat.dhall
-
- let NonEmpty/map = ../NonEmpty/map.dhall
-
- let NonEmpty/singleton = ../NonEmpty/singleton.dhall
-
- let Optional/fold = ../Optional/fold.dhall nix
-
- let List/uncons
- : ∀(a : Type) → List a → Optional (NonEmpty a)
- = {- This version uses the `ls` argument only once to prevent cache blowups at the price
- of performing two passes over the list:
- A first one to reverse it, a second one with `List/fold` to determine
- the head element.
- See https://github.com/dhall-lang/dhall-lang/pull/1015#issuecomment-633381024
- for some context regarding the caching issue.
- -}
- λ(a : Type) →
- λ(ls : List a) →
- List/fold
- a
- (List/reverse a ls)
- (Optional (NonEmpty a))
- ( λ(x : a) →
- λ(acc : Optional (NonEmpty a)) →
- Optional/fold
- (NonEmpty a)
- acc
- (Optional (NonEmpty a))
- (λ(ne : NonEmpty a) → Some (ne ⫽ { tail = ne.tail # [ x ] }))
- (Some (NonEmpty/singleton a x))
- )
- (None (NonEmpty a))
-
- let NonEmpty/mapHead
- : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
- = λ(a : Type) →
- λ(fn : a → a) →
- λ(ls : NonEmpty a) →
- ls ⫽ { head = fn ls.head }
-
- let NonEmpty/mapTail
- : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
- = λ(a : Type) →
- λ(fn : a → a) →
- λ(ls : NonEmpty a) →
- ls ⫽ { tail = List/map a a fn ls.tail }
-
- let NonEmpty/prepend
- : ∀(a : Type) → a → NonEmpty a → NonEmpty a
- = λ(a : Type) →
- λ(prefix : a) →
- λ(ls : NonEmpty a) →
- { head = prefix, tail = NonEmpty/toList a ls }
-
- let NonYtpme
- : Type → Type
- = λ(a : Type) → { init : List a, last : a }
-
- let List/unsnoc
- : ∀(a : Type) → List a → Optional (NonYtpme a)
- = λ(a : Type) →
- λ(ls : List a) →
- List/fold
- a
- ls
- (Optional (NonYtpme a))
- ( λ(x : a) →
- λ(acc : Optional (NonYtpme a)) →
- Optional/fold
- (NonYtpme a)
- acc
- (Optional (NonYtpme a))
- (λ(ny : NonYtpme a) → Some (ny ⫽ { init = [ x ] # ny.init }))
- (Some { init = [] : List a, last = x })
- )
- (None (NonYtpme a))
-
- let NonEmpty/mapLast
- : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
- = λ(a : Type) →
- λ(fn : a → a) →
- λ(ls : NonEmpty a) →
- Optional/fold
- (NonYtpme a)
- (List/unsnoc a ls.tail)
- (NonEmpty a)
- (λ(x : NonYtpme a) → ls ⫽ { tail = x.init # [ fn x.last ] })
- (NonEmpty/singleton a (fn ls.head))
-
- let NonEmpty/mapLeading
- : ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
- = λ(a : Type) →
- λ(fn : a → a) →
- λ(ls : NonEmpty a) →
- Optional/fold
- (NonYtpme a)
- (List/unsnoc a ls.tail)
- (NonEmpty a)
- ( λ(x : NonYtpme a) →
- { head = fn ls.head
- , tail = List/map a a fn x.init # [ x.last ]
- }
- )
- ls
-
- let Lines
- : Type
- = NonEmpty Text
-
- let Block
- : Type
- = < Simple : Text | Complex : Lines >
-
- let Block/toLines
- : Block → Lines
- = λ(block : Block) →
- merge
- { Simple = NonEmpty/singleton Text
- , Complex = Function/identity Lines
- }
- block
-
- let manyBlocks
- : ∀(a : Type) → Text → (NonEmpty a → Lines) → List a → Block
- = λ(a : Type) →
- λ(ifEmpty : Text) →
- λ(render : NonEmpty a → Lines) →
- λ(inputs : List a) →
- Optional/fold
- (NonEmpty a)
- (List/uncons a inputs)
- Block
- (λ(inputs : NonEmpty a) → Block.Complex (render inputs))
- (Block.Simple ifEmpty)
-
- let blockToText
- : Block → Text
- = λ(block : Block) →
- Text/concatMap
- Text
- (λ(line : Text) → line ++ "\n")
- (NonEmpty/toList Text (Block/toLines block))
-
- let addPrefix = λ(prefix : Text) → λ(line : Text) → prefix ++ line
-
- let addIndent = addPrefix " "
-
- let indentTail = NonEmpty/mapTail Text addIndent
-
- let Format =
- ./Format.dhall
-
- let ObjectField = { mapKey : Text, mapValue : Block }
-
- let -- Essentially the same thing as `Text/show`, except that this does not
- -- escape `$`
- escape =
- List/fold
- (Text → Text)
- [ Text/replace "\"" "\\\""
- , Text/replace "\b" "\\b"
- , Text/replace "\f" "\\f"
- , Text/replace "\n" "\\n"
- , Text/replace "\r" "\\r"
- , Text/replace "\t" "\\t"
- , Text/replace "\\" "\\\\"
- ]
- Text
- (λ(replace : Text → Text) → λ(text : Text) → replace text)
-
- let renderJSONStruct =
- λ(prefix : Text) →
- λ(suffix : Text) →
- λ(blocks : NonEmpty Lines) →
- let indent = List/map Text Text addIndent
-
- let appendComma
- : Lines → Lines
- = NonEmpty/mapLast Text (λ(line : Text) → line ++ ",")
-
- let blocks = NonEmpty/mapLeading Lines appendComma blocks
-
- let block = NonEmpty/concat Text blocks
-
- in Optional/fold
- (NonYtpme Text)
- (List/unsnoc Text block.tail)
- (NonEmpty Text)
- ( λ(ny : NonYtpme Text) →
- { head = prefix
- , tail =
- indent ([ block.head ] # ny.init # [ ny.last ])
- # [ suffix ]
- }
- )
- (NonEmpty/singleton Text "${prefix} ${block.head} ${suffix}")
-
- let renderObject =
- λ(format : Format) →
- λ(fields : NonEmpty ObjectField) →
- let keystr = λ(field : ObjectField) → "\"${escape field.mapKey}\":"
-
- let prefixKeyOnFirst =
- λ(field : ObjectField) →
- NonEmpty/mapHead
- Text
- (addPrefix "${keystr field} ")
- (Block/toLines field.mapValue)
-
- let prependKeyLine =
- λ(field : ObjectField) →
- NonEmpty/prepend
- Text
- (keystr field)
- (Block/toLines field.mapValue)
-
- let renderYAMLField =
- λ(field : ObjectField) →
- merge
- { Simple =
- λ(line : Text) →
- NonEmpty/singleton Text "${keystr field} ${line}"
- , Complex = λ(_ : Lines) → indentTail (prependKeyLine field)
- }
- field.mapValue
-
- in merge
- { JSON =
- renderJSONStruct
- "{"
- "}"
- (NonEmpty/map ObjectField Lines prefixKeyOnFirst fields)
- , YAML =
- NonEmpty/concat
- Text
- (NonEmpty/map ObjectField Lines renderYAMLField fields)
- }
- format
-
- let renderYAMLArrayField =
- λ(block : Block) →
- NonEmpty/mapHead
- Text
- (addPrefix "- ")
- (indentTail (Block/toLines block))
-
- let renderArray =
- λ(format : Format) →
- λ(fields : NonEmpty Block) →
- merge
- { JSON =
- renderJSONStruct
- "["
- "]"
- (NonEmpty/map Block Lines Block/toLines fields)
- , YAML =
- NonEmpty/concat
- Text
- (NonEmpty/map Block Lines renderYAMLArrayField fields)
- }
- format
-
- let renderAs
- : Format → JSON.Type → Text
- = λ(format : Format) →
- λ(json : JSON.Type) →
- blockToText
- ( json
- Block
- { string = λ(x : Text) → Block.Simple "\"${escape x}\""
- , double = λ(x : Double) → Block.Simple (Double/show x)
- , integer = λ(x : Integer) → Block.Simple (JSON.renderInteger x)
- , object = manyBlocks ObjectField "{}" (renderObject format)
- , array = manyBlocks Block "[]" (renderArray format)
- , bool =
- λ(x : Bool) → Block.Simple (if x then "true" else "false")
- , null = Block.Simple "null"
- }
- )
-
- in renderAs
diff --git a/JSON/renderCompact.dhall b/JSON/renderCompact.dhall
deleted file mode 100644
index 6a4e8e2..0000000
--- a/JSON/renderCompact.dhall
+++ /dev/null
@@ -1,52 +0,0 @@
---| This renders JSON on a single line
-let JSON = ./core.dhall
-
-let Text/concatMapSep = ../Text/concatMapSep.dhall
-
-let renderInteger = ./renderInteger.dhall
-
-let renderCompact
- : JSON.Type → Text
- = λ(j : JSON.Type) →
- j
- Text
- { string = Text/show
- , double = Double/show
- , integer = renderInteger
- , object =
- λ(x : List { mapKey : Text, mapValue : Text }) →
- let body =
- Text/concatMapSep
- ","
- { mapKey : Text, mapValue : Text }
- ( λ(e : { mapKey : Text, mapValue : Text }) →
- " ${Text/show e.mapKey}: ${e.mapValue}"
- )
- x
-
- in "{${body} }"
- , array =
- λ(x : List Text) →
- let body = Text/concatMapSep "," Text (λ(y : Text) → " ${y}") x
-
- in "[${body} ]"
- , bool = λ(x : Bool) → if x then "true" else "false"
- , null = "null"
- }
-
-let example =
- assert
- : renderCompact
- ( JSON.array
- [ JSON.bool True
- , JSON.string "Hello"
- , JSON.object
- [ { mapKey = "foo", mapValue = JSON.null }
- , { mapKey = "bar", mapValue = JSON.double 1.1 }
- , { mapKey = "baz", mapValue = JSON.integer +2 }
- ]
- ]
- )
- ≡ "[ true, \"Hello\", { \"foo\": null, \"bar\": 1.1, \"baz\": 2 } ]"
-
-in renderCompact
diff --git a/JSON/renderInteger.dhall b/JSON/renderInteger.dhall
deleted file mode 100644
index 67b17de..0000000
--- a/JSON/renderInteger.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-{-|
-Render an `Integer` value as a `JSON number`, according to the JSON standard, in
-which a number may not start with a plus sign (`+`).
--}
-let Integer/nonNegative = ../Integer/nonNegative.dhall
-
-let renderInteger
- : Integer → Text
- = λ(integer : Integer) →
- if Integer/nonNegative integer
- then Natural/show (Integer/clamp integer)
- else Integer/show integer
-
-let positive = assert : renderInteger +1 ≡ "1"
-
-let zero = assert : renderInteger +0 ≡ "0"
-
-let negative = assert : renderInteger -1 ≡ "-1"
-
-in renderInteger
diff --git a/JSON/renderYAML.dhall b/JSON/renderYAML.dhall
deleted file mode 100644
index a755beb..0000000
--- a/JSON/renderYAML.dhall
+++ /dev/null
@@ -1,12 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let JSON = ./core.dhall
-
- let Format = ./Format.dhall
-
- let renderAs = ./renderAs.dhall nix
-
- let renderYAML
- : JSON.Type → Text
- = renderAs Format.YAML
-
- in renderYAML
diff --git a/JSON/string.dhall b/JSON/string.dhall
deleted file mode 100644
index 872cacc..0000000
--- a/JSON/string.dhall
+++ /dev/null
@@ -1,32 +0,0 @@
-{-|
-Create a JSON string from Dhall `Text`
-
-```
-let JSON = ./package.dhall
-in JSON.render (JSON.string "ABC $ \" 🙂")
-= "\"ABC \\u0024 \\\" 🙂\""
-
-let JSON = ./package.dhall
-in JSON.render (JSON.string "")
-= "\"\""
-```
--}
-let JSON = ./Type.dhall
-
-let string
- : Text → JSON
- = λ(x : Text) →
- λ(JSON : Type) →
- λ ( json
- : { array : List JSON → JSON
- , bool : Bool → JSON
- , double : Double → JSON
- , integer : Integer → JSON
- , null : JSON
- , object : List { mapKey : Text, mapValue : JSON } → JSON
- , string : Text → JSON
- }
- ) →
- json.string x
-
-in string
diff --git a/JSON/tagInline.dhall b/JSON/tagInline.dhall
deleted file mode 100644
index 842cb04..0000000
--- a/JSON/tagInline.dhall
+++ /dev/null
@@ -1,23 +0,0 @@
---| Prepare a union value for JSON- or YAML-encoding with the inline layout
-let Nesting = ./Nesting.dhall
-
-let Tagged = ./Tagged.dhall
-
-let tagInline
- : Text → ∀(a : Type) → a → Tagged a
- = λ(tagFieldName : Text) →
- λ(a : Type) →
- λ(contents : a) →
- { nesting = Nesting.Inline, field = tagFieldName, contents }
-
-let example0 =
- let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
-
- in assert
- : tagInline "name" Example (Example.Left { foo = 2 })
- ≡ { field = "name"
- , nesting = Nesting.Inline
- , contents = Example.Left { foo = 2 }
- }
-
-in tagInline
diff --git a/JSON/tagNested.dhall b/JSON/tagNested.dhall
deleted file mode 100644
index b32ed2d..0000000
--- a/JSON/tagNested.dhall
+++ /dev/null
@@ -1,27 +0,0 @@
---| Prepare a union value for JSON- or YAML-encoding with the nested layout
-let Nesting = ./Nesting.dhall
-
-let Tagged = ./Tagged.dhall
-
-let tagNested
- : Text → Text → ∀(a : Type) → a → Tagged a
- = λ(contentsFieldName : Text) →
- λ(tagFieldName : Text) →
- λ(a : Type) →
- λ(contents : a) →
- { nesting = Nesting.Nested contentsFieldName
- , field = tagFieldName
- , contents
- }
-
-let example0 =
- let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
-
- in assert
- : tagNested "value" "name" Example (Example.Left { foo = 2 })
- ≡ { field = "name"
- , nesting = Nesting.Nested "value"
- , contents = Example.Left { foo = 2 }
- }
-
-in tagNested
diff --git a/List/all.dhall b/List/all.dhall
deleted file mode 100644
index 11b1613..0000000
--- a/List/all.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
-{-|
-Returns `True` if the supplied function returns `True` for all elements in the
-`List`
--}
-let all
- : ∀(a : Type) → (a → Bool) → List a → Bool
- = λ(a : Type) →
- λ(f : a → Bool) →
- λ(xs : List a) →
- List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True
-
-let example0 = assert : all Natural Natural/even [ 2, 3, 5 ] ≡ False
-
-let example1 = assert : all Natural Natural/even ([] : List Natural) ≡ True
-
-in all
diff --git a/List/any.dhall b/List/any.dhall
deleted file mode 100644
index 130bf0b..0000000
--- a/List/any.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
-{-|
-Returns `True` if the supplied function returns `True` for any element in the
-`List`
--}
-let any
- : ∀(a : Type) → (a → Bool) → List a → Bool
- = λ(a : Type) →
- λ(f : a → Bool) →
- λ(xs : List a) →
- List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
-
-let example0 = assert : any Natural Natural/even [ 2, 3, 5 ] ≡ True
-
-let example1 = assert : any Natural Natural/even ([] : List Natural) ≡ False
-
-in any
diff --git a/List/build.dhall b/List/build.dhall
deleted file mode 100644
index c59c3c5..0000000
--- a/List/build.dhall
+++ /dev/null
@@ -1,30 +0,0 @@
---| `build` is the inverse of `fold`
-let build
- : ∀(a : Type) →
- (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) →
- List a
- = List/build
-
-let example0 =
- assert
- : build
- Text
- ( λ(list : Type) →
- λ(cons : Text → list → list) →
- λ(nil : list) →
- cons "ABC" (cons "DEF" nil)
- )
- ≡ [ "ABC", "DEF" ]
-
-let example1 =
- assert
- : build
- Text
- ( λ(list : Type) →
- λ(cons : Text → list → list) →
- λ(nil : list) →
- nil
- )
- ≡ ([] : List Text)
-
-in build
diff --git a/List/concat.dhall b/List/concat.dhall
deleted file mode 100644
index ee17d84..0000000
--- a/List/concat.dhall
+++ /dev/null
@@ -1,34 +0,0 @@
---| Concatenate a `List` of `List`s into a single `List`
-let concat
- : ∀(a : Type) → List (List a) → List a
- = λ(a : Type) →
- λ(xss : List (List a)) →
- List/build
- a
- ( λ(list : Type) →
- λ(cons : a → list → list) →
- λ(nil : list) →
- List/fold
- (List a)
- xss
- list
- (λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys)
- nil
- )
-
-let example0 =
- assert
- : concat Natural [ [ 0, 1, 2 ], [ 3, 4 ], [ 5, 6, 7, 8 ] ]
- ≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
-
-let example1 =
- assert
- : concat
- Natural
- [ [] : List Natural, [] : List Natural, [] : List Natural ]
- ≡ ([] : List Natural)
-
-let example2 =
- assert : concat Natural ([] : List (List Natural)) ≡ ([] : List Natural)
-
-in concat
diff --git a/List/concatMap.dhall b/List/concatMap.dhall
deleted file mode 100644
index 4cc2e77..0000000
--- a/List/concatMap.dhall
+++ /dev/null
@@ -1,32 +0,0 @@
-{-|
-Transform a list by applying a function to each element and flattening the
-results
--}
-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)
- )
-
-let example0 =
- assert
- : concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ]
- ≡ [ 2, 2, 3, 3, 5, 5 ]
-
-let example1 =
- assert
- : concatMap
- Natural
- Natural
- (λ(n : Natural) → [ n, n ])
- ([] : List Natural)
- ≡ ([] : List Natural)
-
-in concatMap
diff --git a/List/default.dhall b/List/default.dhall
deleted file mode 100644
index 0d9bf6d..0000000
--- a/List/default.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let Optional/default = ../Optional/default.dhall nix
-
- let default
- : ∀(a : Type) → Optional (List a) → List a
- = λ(a : Type) →
- λ(o : Optional (List a)) →
- Optional/default (List a) ([] : List a) o
-
- in default
diff --git a/List/drop.dhall b/List/drop.dhall
deleted file mode 100644
index 329c752..0000000
--- a/List/drop.dhall
+++ /dev/null
@@ -1,25 +0,0 @@
---| Remove first `n` elements of a list
-let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall
-
-let drop
- : ∀(n : Natural) → ∀(a : Type) → List a → List a
- = λ(n : Natural) →
- λ(a : Type) →
- λ(xs : List a) →
- List/fold
- { index : Natural, value : a }
- (List/indexed a xs)
- (List a)
- ( λ(x : { index : Natural, value : a }) →
- λ(xs : List a) →
- if Natural/greaterThanEqual x.index n
- then [ x.value ] # xs
- else xs
- )
- ([] : List a)
-
-let example = assert : drop 2 Natural [ 2, 3, 5 ] ≡ [ 5 ]
-
-let example = assert : drop 5 Natural [ 2, 3, 5 ] ≡ ([] : List Natural)
-
-in drop
diff --git a/List/empty.dhall b/List/empty.dhall
deleted file mode 100644
index fe66a71..0000000
--- a/List/empty.dhall
+++ /dev/null
@@ -1,8 +0,0 @@
---| An empty list of the given type
-let empty
- : ∀(a : Type) → List a
- = λ(a : Type) → [] : List a
-
-let example0 = assert : empty Bool ≡ ([] : List Bool)
-
-in empty
diff --git a/List/filter.dhall b/List/filter.dhall
deleted file mode 100644
index 6b2a63f..0000000
--- a/List/filter.dhall
+++ /dev/null
@@ -1,22 +0,0 @@
---| Only keep elements of the list where the supplied function returns `True`
-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)
- )
-
-let example0 = assert : filter Natural Natural/even [ 2, 3, 5 ] ≡ [ 2 ]
-
-let example1 = assert : filter Natural Natural/odd [ 2, 3, 5 ] ≡ [ 3, 5 ]
-
-in filter
diff --git a/List/filterMap.dhall b/List/filterMap.dhall
index 5a4e722..fdad7ed 100644
--- a/List/filterMap.dhall
+++ b/List/filterMap.dhall
@@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) →
- let List/concatMap = ./concatMap.dhall
+ let List/concatMap = https://prelude.dhall-lang.org/List/concatMap.dhall
- let Optional/toList = ../Optional/toList.dhall nix
+ let Optional/toList = https://prelude.dhall-lang.org/Optional/toList.dhall
let filterMap
: ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b
diff --git a/List/fold.dhall b/List/fold.dhall
deleted file mode 100644
index ee8b8e9..0000000
--- a/List/fold.dhall
+++ /dev/null
@@ -1,43 +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
--}
-let fold
- : ∀(a : Type) →
- List a →
- ∀(list : Type) →
- ∀(cons : a → list → list) →
- ∀(nil : list) →
- list
- = List/fold
-
-let example0 =
- assert
- : fold
- Natural
- [ 2, 3, 5 ]
- Text
- (λ(x : Natural) → λ(y : Text) → Natural/show x ++ y)
- "0"
- ≡ "2350"
-
-let example1 =
- λ(nil : Text) →
- assert
- : fold
- Natural
- [ 2, 3, 5 ]
- Text
- (λ(x : Natural) → λ(y : Text) → Natural/show x ++ y)
- nil
- ≡ "2" ++ ("3" ++ ("5" ++ nil))
-
-let example2 =
- λ(cons : Natural → Text → Text) →
- λ(nil : Text) →
- assert
- : fold Natural [ 2, 3, 5 ] Text cons nil ≡ cons 2 (cons 3 (cons 5 nil))
-
-in fold
diff --git a/List/foldLeft.dhall b/List/foldLeft.dhall
deleted file mode 100644
index c943877..0000000
--- a/List/foldLeft.dhall
+++ /dev/null
@@ -1,60 +0,0 @@
-{-|
-`foldLeft` is like `List/fold` except that the accumulation starts from the left
-
-If you treat the list `[ x, y, z ]` as `cons (cons (cons nil x) y) z`, then
-`foldLeft` just replaces each `cons` and `nil` with something else
--}
-let foldLeft
- : ∀(a : Type) →
- List a →
- ∀(list : Type) →
- ∀(cons : list → a → list) →
- ∀(nil : list) →
- list
- = λ(a : Type) →
- λ(xs : List a) →
- λ(list : Type) →
- λ(cons : list → a → list) →
- λ(nil : list) →
- List/fold
- a
- xs
- (list → list)
- (λ(x : a) → λ(f : list → list) → λ(l : list) → f (cons l x))
- (λ(l : list) → l)
- nil
-
-let example0 =
- assert
- : foldLeft
- Natural
- [ 2, 3, 5 ]
- Text
- (λ(x : Text) → λ(y : Natural) → x ++ Natural/show y)
- "0"
- ≡ "0235"
-
-let example1 =
- assert
- : ( λ(nil : Text) →
- foldLeft
- Natural
- [ 2, 3, 5 ]
- Text
- (λ(x : Text) → λ(y : Natural) → x ++ Natural/show y)
- nil
- )
- ≡ (λ(nil : Text) → nil ++ "2" ++ "3" ++ "5")
-
-let example2 =
- assert
- : ( λ(cons : Text → Natural → Text) →
- λ(nil : Text) →
- foldLeft Natural [ 2, 3, 5 ] Text cons nil
- )
- ≡ ( λ(cons : Text → Natural → Text) →
- λ(nil : Text) →
- cons (cons (cons nil 2) 3) 5
- )
-
-in foldLeft
diff --git a/List/generate.dhall b/List/generate.dhall
deleted file mode 100644
index 2afdeb7..0000000
--- a/List/generate.dhall
+++ /dev/null
@@ -1,35 +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
--}
-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))
- )
-
-let example0 =
- assert : generate 5 Bool Natural/even ≡ [ True, False, True, False, True ]
-
-let example1 = assert : generate 0 Bool Natural/even ≡ ([] : List Bool)
-
-in generate
diff --git a/List/head.dhall b/List/head.dhall
deleted file mode 100644
index a50f692..0000000
--- a/List/head.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Retrieve the first element of the list
-let head
- : ∀(a : Type) → List a → Optional a
- = List/head
-
-let example0 = assert : head Natural [ 0, 1, 2 ] ≡ Some 0
-
-let example1 = assert : head Natural ([] : List Natural) ≡ None Natural
-
-in head
diff --git a/List/index.dhall b/List/index.dhall
deleted file mode 100644
index 6e19329..0000000
--- a/List/index.dhall
+++ /dev/null
@@ -1,15 +0,0 @@
---| Retrieve an element from a `List` using its 0-based index
-let drop = ./drop.dhall
-
-let index
- : Natural → ∀(a : Type) → List a → Optional a
- = λ(n : Natural) → λ(a : Type) → λ(xs : List a) → List/head a (drop n a xs)
-
-let property =
- λ(n : Natural) → λ(a : Type) → assert : index n a ([] : List a) ≡ None a
-
-let example0 = assert : index 1 Natural [ 2, 3, 5 ] ≡ Some 3
-
-let example1 = assert : index 1 Natural ([] : List Natural) ≡ None Natural
-
-in index
diff --git a/List/indexed.dhall b/List/indexed.dhall
deleted file mode 100644
index 20500e1..0000000
--- a/List/indexed.dhall
+++ /dev/null
@@ -1,19 +0,0 @@
---| Tag each element of the list with its index
-let indexed
- : ∀(a : Type) → List a → List { index : Natural, value : a }
- = List/indexed
-
-let example0 =
- assert
- : indexed Bool [ True, False, True ]
- ≡ [ { index = 0, value = True }
- , { index = 1, value = False }
- , { index = 2, value = True }
- ]
-
-let example1 =
- assert
- : indexed Bool ([] : List Bool)
- ≡ ([] : List { index : Natural, value : Bool })
-
-in indexed
diff --git a/List/iterate.dhall b/List/iterate.dhall
deleted file mode 100644
index 02fed82..0000000
--- a/List/iterate.dhall
+++ /dev/null
@@ -1,42 +0,0 @@
-{-|
-Generate a list of the specified length given a seed value and transition
-function
--}
-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)
- )
- )
-
-let example0 =
- assert
- : iterate 10 Natural (λ(x : Natural) → x * 2) 1
- ≡ [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
-
-let example1 =
- assert
- : iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)
-
-in iterate
diff --git a/List/last.dhall b/List/last.dhall
deleted file mode 100644
index 2e695fb..0000000
--- a/List/last.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Retrieve the last element of the list
-let last
- : ∀(a : Type) → List a → Optional a
- = List/last
-
-let example0 = assert : last Natural [ 0, 1, 2 ] ≡ Some 2
-
-let example1 = assert : last Natural ([] : List Natural) ≡ None Natural
-
-in last
diff --git a/List/length.dhall b/List/length.dhall
deleted file mode 100644
index 1238fd5..0000000
--- a/List/length.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Returns the number of elements in a list
-let length
- : ∀(a : Type) → List a → Natural
- = List/length
-
-let example0 = assert : length Natural [ 0, 1, 2 ] ≡ 3
-
-let example1 = assert : length Natural ([] : List Natural) ≡ 0
-
-in length
diff --git a/List/map.dhall b/List/map.dhall
deleted file mode 100644
index 70fc570..0000000
--- a/List/map.dhall
+++ /dev/null
@@ -1,23 +0,0 @@
---| Transform a list by applying a function to each element
-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))
- )
-
-let example0 =
- assert
- : map Natural Bool Natural/even [ 2, 3, 5 ] ≡ [ True, False, False ]
-
-let example1 =
- assert
- : map Natural Bool Natural/even ([] : List Natural) ≡ ([] : List Bool)
-
-in map
diff --git a/List/null.dhall b/List/null.dhall
deleted file mode 100644
index fd11976..0000000
--- a/List/null.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Returns `True` if the `List` is empty and `False` otherwise
-let null
- : ∀(a : Type) → List a → Bool
- = λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs)
-
-let example0 = assert : null Natural [ 0, 1, 2 ] ≡ False
-
-let example1 = assert : null Natural ([] : List Natural) ≡ True
-
-in null
diff --git a/List/package.dhall b/List/package.dhall
index f845798..3795e0b 100644
--- a/List/package.dhall
+++ b/List/package.dhall
@@ -1,31 +1,4 @@
λ(nix : ../NixPrelude.dhall) →
- { all = ./all.dhall
- , any = ./any.dhall
- , build = ./build.dhall
- , concat = ./concat.dhall
- , concatMap = ./concatMap.dhall
- , default = ./default.dhall nix
- , drop = ./drop.dhall
- , empty = ./empty.dhall
- , filter = ./filter.dhall
- , filterMap = ./filterMap.dhall nix
- , fold = ./fold.dhall
- , foldLeft = ./foldLeft.dhall
- , generate = ./generate.dhall
- , head = ./head.dhall
- , index = ./index.dhall
- , indexed = ./indexed.dhall
- , iterate = ./iterate.dhall
- , last = ./last.dhall
- , length = ./length.dhall
- , map = ./map.dhall
- , null = ./null.dhall
- , partition = ./partition.dhall
- , replicate = ./replicate.dhall
- , reverse = ./reverse.dhall
- , shifted = ./shifted.dhall
- , take = ./take.dhall
- , unpackOptionals = ./unpackOptionals.dhall nix
- , unzip = ./unzip.dhall
- , zip = ./zip.dhall nix
+ {
+ , filterMap = ./filterMap.dhall
}
diff --git a/List/partition.dhall b/List/partition.dhall
deleted file mode 100644
index d38ebae..0000000
--- a/List/partition.dhall
+++ /dev/null
@@ -1,31 +0,0 @@
-{-|
-`partition` divides a `List` of elements into those that satisfy a predicate
-and those that do not
--}
-let Partition
- : Type → Type
- = λ(a : Type) → { true : List a, false : List a }
-
-let partition
- : ∀(a : Type) → (a → Bool) → List a → Partition a
- = λ(a : Type) →
- λ(f : a → Bool) →
- λ(xs : List a) →
- List/fold
- a
- xs
- (Partition a)
- ( λ(x : a) →
- λ(p : Partition a) →
- if f x
- then { true = [ x ] # p.true, false = p.false }
- else { true = p.true, false = [ x ] # p.false }
- )
- { true = [] : List a, false = [] : List a }
-
-let example0 =
- assert
- : partition Natural Natural/even [ 0, 1, 2, 3 ]
- ≡ { true = [ 0, 2 ], false = [ 1, 3 ] }
-
-in partition
diff --git a/List/replicate.dhall b/List/replicate.dhall
deleted file mode 100644
index 90bfbd0..0000000
--- a/List/replicate.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
---| Build a list by copying the given element the specified number of times
-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)
- )
-
-let example0 = assert : replicate 9 Natural 1 ≡ [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
-
-let example1 = assert : replicate 0 Natural 1 ≡ ([] : List Natural)
-
-in replicate
diff --git a/List/reverse.dhall b/List/reverse.dhall
deleted file mode 100644
index d958987..0000000
--- a/List/reverse.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
---| Reverse a list
-let reverse
- : ∀(a : Type) → List a → List a
- = List/reverse
-
-let example0 = assert : reverse Natural [ 0, 1, 2 ] ≡ [ 2, 1, 0 ]
-
-let example1 =
- assert : reverse Natural ([] : List Natural) ≡ ([] : List Natural)
-
-in reverse
diff --git a/List/shifted.dhall b/List/shifted.dhall
deleted file mode 100644
index 0db406d..0000000
--- a/List/shifted.dhall
+++ /dev/null
@@ -1,83 +0,0 @@
-{-|
-Combine a `List` of `List`s, offsetting the `index` of each element by the
-number of elements in preceding lists
--}
-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
- )
-
-let example0 =
- assert
- : 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 }
- ]
-
-let example1 =
- assert
- : shifted Bool ([] : List (List { index : Natural, value : Bool }))
- ≡ ([] : List { index : Natural, value : Bool })
-
-in shifted
diff --git a/List/take.dhall b/List/take.dhall
deleted file mode 100644
index da66287..0000000
--- a/List/take.dhall
+++ /dev/null
@@ -1,23 +0,0 @@
---| Truncate a list to the first `n` elements
-let Natural/lessThan = ../Natural/lessThan.dhall
-
-let take
- : ∀(n : Natural) → ∀(a : Type) → List a → List a
- = λ(n : Natural) →
- λ(a : Type) →
- λ(xs : List a) →
- List/fold
- { index : Natural, value : a }
- (List/indexed a xs)
- (List a)
- ( λ(x : { index : Natural, value : a }) →
- λ(xs : List a) →
- if Natural/lessThan x.index n then [ x.value ] # xs else xs
- )
- ([] : List a)
-
-let example = assert : take 2 Natural [ 2, 3, 5 ] ≡ [ 2, 3 ]
-
-let example = assert : take 5 Natural [ 2, 3, 5 ] ≡ [ 2, 3, 5 ]
-
-in take
diff --git a/List/unpackOptionals.dhall b/List/unpackOptionals.dhall
deleted file mode 100644
index 665a189..0000000
--- a/List/unpackOptionals.dhall
+++ /dev/null
@@ -1,8 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let List/filterMap = ./filterMap.dhall nix
-
- let unpackOptionals
- : ∀(a : Type) → ∀(l : List (Optional a)) → List a
- = λ(a : Type) → List/filterMap (Optional a) a (λ(x : Optional a) → x)
-
- in unpackOptionals
diff --git a/List/unzip.dhall b/List/unzip.dhall
deleted file mode 100644
index 3ce4f76..0000000
--- a/List/unzip.dhall
+++ /dev/null
@@ -1,50 +0,0 @@
---| Unzip a `List` into two separate `List`s
-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)
- )
- }
-
-let example0 =
- assert
- : unzip
- Text
- Bool
- [ { _1 = "ABC", _2 = True }
- , { _1 = "DEF", _2 = False }
- , { _1 = "GHI", _2 = True }
- ]
- ≡ { _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }
-
-let example1 =
- assert
- : unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
- ≡ { _1 = [] : List Text, _2 = [] : List Bool }
-
-in unzip
diff --git a/List/zip.dhall b/List/zip.dhall
deleted file mode 100644
index 8bc25b4..0000000
--- a/List/zip.dhall
+++ /dev/null
@@ -1,36 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let List/index = ./index.dhall
-
- let List/map = ./map.dhall
-
- let Natural/min = ../Natural/min.dhall
-
- let Natural/enumerate = ../Natural/enumerate.dhall
-
- let Optional/unwrap = ../Optional/unwrap.dhall nix
-
- let zip
- : ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b }
- = λ(a : Type) →
- λ(xs : List a) →
- λ(b : Type) →
- λ(ys : List b) →
- let xsLen = List/length a xs
-
- let ysLen = List/length b ys
-
- let resLen = Natural/min xsLen ysLen
-
- let indexes = Natural/enumerate resLen
-
- in List/map
- Natural
- { _1 : a, _2 : b }
- ( λ(i : Natural) →
- { _1 = Optional/unwrap a (List/index i a xs)
- , _2 = Optional/unwrap b (List/index i b ys)
- }
- )
- indexes
-
- in zip
diff --git a/Location/Type.dhall b/Location/Type.dhall
deleted file mode 100644
index f0a057e..0000000
--- a/Location/Type.dhall
+++ /dev/null
@@ -1,15 +0,0 @@
---| This is the union type returned when you import something `as Location`
-let Location
- : Type
- = < Environment : Text | Local : Text | Missing | Remote : Text >
-
-let example0 =
- assert
- : missing as Location
- ≡ < Environment : Text
- | Local : Text
- | Missing
- | Remote : Text
- >.Missing
-
-in Location
diff --git a/Location/package.dhall b/Location/package.dhall
deleted file mode 100644
index ac35283..0000000
--- a/Location/package.dhall
+++ /dev/null
@@ -1 +0,0 @@
-{ Type = ./Type.dhall }
diff --git a/Map/Entry.dhall b/Map/Entry.dhall
deleted file mode 100644
index 16d02f9..0000000
--- a/Map/Entry.dhall
+++ /dev/null
@@ -1,6 +0,0 @@
---| The type of each key-value pair in a `Map`
-let Entry
- : Type → Type → Type
- = λ(k : Type) → λ(v : Type) → { mapKey : k, mapValue : v }
-
-in Entry
diff --git a/Map/Type.dhall b/Map/Type.dhall
deleted file mode 100644
index 7118c3b..0000000
--- a/Map/Type.dhall
+++ /dev/null
@@ -1,25 +0,0 @@
-{-|
-This is the canonical way to encode a dynamic list of key-value pairs.
-
-Tools (such as `dhall-to-json`/`dhall-to-yaml` will recognize values of this
-type and convert them to maps/dictionaries/hashes in the target language
-
-For example, `dhall-to-json` converts a Dhall value like this:
-
-```
-[ { mapKey = "foo", mapValue = 1 }
-, { mapKey = "bar", mapValue = 2 }
-] : ./Map Text Natural
-```
-
-... to a JSON value like this:
-
-```
-{ "foo": 1, "bar", 2 }
-```
--}
-let Map
- : Type → Type → Type
- = λ(k : Type) → λ(v : Type) → List { mapKey : k, mapValue : v }
-
-in Map
diff --git a/Map/empty.dhall b/Map/empty.dhall
deleted file mode 100644
index 508947d..0000000
--- a/Map/empty.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
---| An empty `Map` of the given key and value types
-let Map = ./Type.dhall
-
-let empty
- : ∀(k : Type) → ∀(v : Type) → Map k v
- = λ(k : Type) → λ(v : Type) → [] : Map k v
-
-let example0 =
- assert : empty Text Bool ≡ ([] : List { mapKey : Text, mapValue : Bool })
-
-in empty
diff --git a/Map/keyText.dhall b/Map/keyText.dhall
deleted file mode 100644
index 0e9a223..0000000
--- a/Map/keyText.dhall
+++ /dev/null
@@ -1,15 +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 `./keyValue` for a polymorphic version.
--}
-let keyText =
- λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
-
-let example0 =
- assert : keyText "foo" "bar" ≡ { mapKey = "foo", mapValue = "bar" }
-
-in keyText
diff --git a/Map/keyValue.dhall b/Map/keyValue.dhall
deleted file mode 100644
index b7d60cb..0000000
--- a/Map/keyValue.dhall
+++ /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.
--}
-let keyValue =
- λ(v : Type) →
- λ(key : Text) →
- λ(value : v) →
- { mapKey = key, mapValue = value }
-
-let example0 =
- assert : keyValue Natural "foo" 2 ≡ { mapKey = "foo", mapValue = 2 }
-
-let example1 =
- assert : keyValue Text "bar" "baz" ≡ { mapKey = "bar", mapValue = "baz" }
-
-in keyValue
diff --git a/Map/keys.dhall b/Map/keys.dhall
deleted file mode 100644
index eeafc0d..0000000
--- a/Map/keys.dhall
+++ /dev/null
@@ -1,30 +0,0 @@
---| Get all of the keys of a `Map` as a `List`
-let Map = ./Type.dhall
-
-let Entry = ./Entry.dhall
-
-let List/map = ../List/map.dhall
-
-let keys
- : ∀(k : Type) → ∀(v : Type) → Map k v → List k
- = λ(k : Type) →
- λ(v : Type) →
- List/map (Entry k v) k (λ(x : Entry k v) → x.mapKey)
-
-let example0 =
- assert
- : keys
- Text
- Natural
- [ { mapKey = "A", mapValue = 2 }
- , { mapKey = "B", mapValue = 3 }
- , { mapKey = "C", mapValue = 5 }
- ]
- ≡ [ "A", "B", "C" ]
-
-let example1 =
- assert
- : keys Text Natural ([] : List { mapKey : Text, mapValue : Natural })
- ≡ ([] : List Text)
-
-in keys
diff --git a/Map/map.dhall b/Map/map.dhall
deleted file mode 100644
index 5c1b2e4..0000000
--- a/Map/map.dhall
+++ /dev/null
@@ -1,49 +0,0 @@
---| Transform a `Map` by applying a function to each value
-let Map = ./Type.dhall
-
-let Entry = ./Entry.dhall
-
-let List/map = ../List/map.dhall
-
-let map
- : ∀(k : Type) → ∀(a : Type) → ∀(b : Type) → (a → b) → Map k a → Map k b
- = λ(k : Type) →
- λ(a : Type) →
- λ(b : Type) →
- λ(f : a → b) →
- λ(m : Map k a) →
- List/map
- (Entry k a)
- (Entry k b)
- ( λ(before : Entry k a) →
- { mapKey = before.mapKey, mapValue = f before.mapValue }
- )
- m
-
-let example0 =
- assert
- : map
- Text
- Natural
- Bool
- Natural/even
- [ { mapKey = "A", mapValue = 2 }
- , { mapKey = "B", mapValue = 3 }
- , { mapKey = "C", mapValue = 5 }
- ]
- ≡ [ { mapKey = "A", mapValue = True }
- , { mapKey = "B", mapValue = False }
- , { mapKey = "C", mapValue = False }
- ]
-
-let example1 =
- assert
- : map
- Text
- Natural
- Bool
- Natural/even
- ([] : List { mapKey : Text, mapValue : Natural })
- ≡ ([] : List { mapKey : Text, mapValue : Bool })
-
-in map
diff --git a/Map/package.dhall b/Map/package.dhall
deleted file mode 100644
index c6c505c..0000000
--- a/Map/package.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- { Type = ./Type.dhall
- , Entry = ./Entry.dhall
- , empty = ./empty.dhall
- , keyText = ./keyText.dhall
- , keyValue = ./keyValue.dhall
- , keys = ./keys.dhall
- , map = ./map.dhall
- , unpackOptionals = ./unpackOptionals.dhall nix
- , values = ./values.dhall
- }
diff --git a/Map/unpackOptionals.dhall b/Map/unpackOptionals.dhall
deleted file mode 100644
index 00f22cc..0000000
--- a/Map/unpackOptionals.dhall
+++ /dev/null
@@ -1,26 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let List/concatMap = ../List/concatMap.dhall
-
- let Map/Entry = ./Entry.dhall
-
- let Map/Type = ./Type.dhall
-
- let Optional/fold = ../Optional/fold.dhall nix
-
- let unpackOptionals
- : ∀(k : Type) → ∀(v : Type) → Map/Type k (Optional v) → Map/Type k v
- = λ(k : Type) →
- λ(v : Type) →
- List/concatMap
- (Map/Entry k (Optional v))
- (Map/Entry k v)
- ( λ(e : Map/Entry k (Optional v)) →
- Optional/fold
- v
- e.mapValue
- (Map/Type k v)
- (λ(v : v) → [ { mapKey = e.mapKey, mapValue = v } ])
- ([] : Map/Type k v)
- )
-
- in unpackOptionals
diff --git a/Map/values.dhall b/Map/values.dhall
deleted file mode 100644
index a60af6e..0000000
--- a/Map/values.dhall
+++ /dev/null
@@ -1,30 +0,0 @@
---| Get all of the values of a `Map` as a `List`
-let Map = ./Type.dhall
-
-let Entry = ./Entry.dhall
-
-let List/map = ../List/map.dhall
-
-let values
- : ∀(k : Type) → ∀(v : Type) → Map k v → List v
- = λ(k : Type) →
- λ(v : Type) →
- List/map (Entry k v) v (λ(x : Entry k v) → x.mapValue)
-
-let example0 =
- assert
- : values
- Text
- Natural
- [ { mapKey = "A", mapValue = 2 }
- , { mapKey = "B", mapValue = 3 }
- , { mapKey = "C", mapValue = 5 }
- ]
- ≡ [ 2, 3, 5 ]
-
-let example1 =
- assert
- : values Text Natural ([] : List { mapKey : Text, mapValue : Natural })
- ≡ ([] : List Natural)
-
-in values
diff --git a/Monoid.dhall b/Monoid.dhall
deleted file mode 100644
index e52d8f1..0000000
--- a/Monoid.dhall
+++ /dev/null
@@ -1,43 +0,0 @@
-{-|
-Any function `f` that is a `Monoid` must satisfy the following law:
-
-```
-t : Type
-f : ./Monoid t
-xs : List (List t)
-
-f (./List/concat t xs) = f (./map (List t) t f xs)
-```
-
-Examples:
-
-```
-./Bool/and
- : ./Monoid Bool
-./Bool/or
- : ./Monoid Bool
-./Bool/even
- : ./Monoid Bool
-./Bool/odd
- : ./Monoid Bool
-./List/concat
- : ∀(a : Type) → ./Monoid (List a)
-./List/shifted
- : ∀(a : Type) → ./Monoid (List { index : Natural, value : a })
-./Natural/sum
- : ./Monoid Natural
-./Natural/product
- : ./Monoid Natural
-./Optional/head
- : ∀(a : Type) → ./Monoid (Optional a)
-./Optional/last
- : ∀(a : Type) → ./Monoid (Optional a)
-./Text/concat
- : ./Monoid Text
-```
--}
-let Monoid
- : ∀(m : Type) → Type
- = λ(m : Type) → List m → m
-
-in Monoid
diff --git a/Natural/build.dhall b/Natural/build.dhall
deleted file mode 100644
index f09ac2c..0000000
--- a/Natural/build.dhall
+++ /dev/null
@@ -1,31 +0,0 @@
---| `build` is the inverse of `fold`
-let build
- : ( ∀(natural : Type) →
- ∀(succ : natural → natural) →
- ∀(zero : natural) →
- natural
- ) →
- Natural
- = Natural/build
-
-let example0 =
- assert
- : build
- ( λ(natural : Type) →
- λ(succ : natural → natural) →
- λ(zero : natural) →
- succ (succ (succ zero))
- )
- ≡ 3
-
-let example1 =
- assert
- : build
- ( λ(natural : Type) →
- λ(succ : natural → natural) →
- λ(zero : natural) →
- zero
- )
- ≡ 0
-
-in build
diff --git a/Natural/enumerate.dhall b/Natural/enumerate.dhall
deleted file mode 100644
index de86110..0000000
--- a/Natural/enumerate.dhall
+++ /dev/null
@@ -1,32 +0,0 @@
-{-|
-Generate a list of numbers from `0` up to but not including the specified
-number
--}
-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)
- )
-
-let example0 = assert : enumerate 10 ≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ]
-
-let example1 = assert : enumerate 0 ≡ ([] : List Natural)
-
-in enumerate
diff --git a/Natural/equal.dhall b/Natural/equal.dhall
deleted file mode 100644
index 558a001..0000000
--- a/Natural/equal.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
---| `equal` checks if two Naturals are equal.
-let lessThanEqual = ./lessThanEqual.dhall
-
-let equal
- : Natural → Natural → Bool
- = λ(a : Natural) → λ(b : Natural) → lessThanEqual a b && lessThanEqual b a
-
-let example0 = assert : equal 5 5 ≡ True
-
-let example1 = assert : equal 5 6 ≡ False
-
-let property0 = λ(n : Natural) → assert : equal n n ≡ True
-
-in equal
diff --git a/Natural/even.dhall b/Natural/even.dhall
deleted file mode 100644
index d65cad1..0000000
--- a/Natural/even.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Returns `True` if a number if even and returns `False` otherwise
-let even
- : Natural → Bool
- = Natural/even
-
-let example0 = assert : even 3 ≡ False
-
-let example1 = assert : even 0 ≡ True
-
-in even
diff --git a/Natural/fold.dhall b/Natural/fold.dhall
deleted file mode 100644
index 4f6dd03..0000000
--- a/Natural/fold.dhall
+++ /dev/null
@@ -1,28 +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
--}
-let fold
- : Natural →
- ∀(natural : Type) →
- ∀(succ : natural → natural) →
- ∀(zero : natural) →
- natural
- = Natural/fold
-
-let example0 = assert : fold 3 Text (λ(x : Text) → "A" ++ x) "B" ≡ "AAAB"
-
-let example1 =
- λ(zero : Text) →
- assert
- : fold 3 Text (λ(x : Text) → "A" ++ x) zero
- ≡ "A" ++ ("A" ++ ("A" ++ zero))
-
-let example2 =
- λ(succ : Text → Text) →
- λ(zero : Text) →
- assert : fold 3 Text succ zero ≡ succ (succ (succ zero))
-
-in fold
diff --git a/Natural/fromAny.dhall b/Natural/fromAny.dhall
index e9a6578..92a0e8b 100644
--- a/Natural/fromAny.dhall
+++ b/Natural/fromAny.dhall
@@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) →
let Any = ../Any/Type.dhall
- let Integer/nonNegative = ../Integer/nonNegative.dhall
+ let Integer/nonNegative = https://prelude.dhall-lang.org/Integer/nonNegative.dhall
let Misc/throw = ../Misc/throw.dhall nix
diff --git a/Natural/greaterThan.dhall b/Natural/greaterThan.dhall
deleted file mode 100644
index ebf83fa..0000000
--- a/Natural/greaterThan.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
---| `greaterThan` checks if one Natural is strictly greater than another.
-let lessThan = ./lessThan.dhall
-
-let greaterThan
- : Natural → Natural → Bool
- = λ(x : Natural) → λ(y : Natural) → lessThan y x
-
-let example0 = assert : greaterThan 5 6 ≡ False
-
-let example1 = assert : greaterThan 5 5 ≡ False
-
-let example2 = assert : greaterThan 5 4 ≡ True
-
-let property0 = λ(n : Natural) → assert : greaterThan 0 n ≡ False
-
-let property1 = λ(n : Natural) → assert : greaterThan n n ≡ False
-
-in greaterThan
diff --git a/Natural/greaterThanEqual.dhall b/Natural/greaterThanEqual.dhall
deleted file mode 100644
index faec49c..0000000
--- a/Natural/greaterThanEqual.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-{-|
-`greaterThanEqual` checks if one Natural is greater than or equal to another.
--}
-let lessThanEqual = ./lessThanEqual.dhall
-
-let greaterThanEqual
- : Natural → Natural → Bool
- = λ(x : Natural) → λ(y : Natural) → lessThanEqual y x
-
-let example0 = assert : greaterThanEqual 5 6 ≡ False
-
-let example1 = assert : greaterThanEqual 5 5 ≡ True
-
-let example2 = assert : greaterThanEqual 5 4 ≡ True
-
-let property0 = λ(n : Natural) → assert : greaterThanEqual n 0 ≡ True
-
-let property1 = λ(n : Natural) → assert : greaterThanEqual n n ≡ True
-
-in greaterThanEqual
diff --git a/Natural/isZero.dhall b/Natural/isZero.dhall
deleted file mode 100644
index 16d5109..0000000
--- a/Natural/isZero.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Returns `True` if a number is `0` and returns `False` otherwise
-let isZero
- : Natural → Bool
- = Natural/isZero
-
-let example0 = assert : isZero 2 ≡ False
-
-let example1 = assert : isZero 0 ≡ True
-
-in isZero
diff --git a/Natural/lessThan.dhall b/Natural/lessThan.dhall
deleted file mode 100644
index 6a0f874..0000000
--- a/Natural/lessThan.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
---| `lessThan` checks if one Natural is strictly less than another.
-let greaterThanEqual = ./greaterThanEqual.dhall
-
-let Bool/not = ../Bool/not.dhall
-
-let lessThan
- : Natural → Natural → Bool
- = λ(x : Natural) → λ(y : Natural) → Bool/not (greaterThanEqual x y)
-
-let example0 = assert : lessThan 5 6 ≡ True
-
-let example1 = assert : lessThan 5 5 ≡ False
-
-let example2 = assert : lessThan 5 4 ≡ False
-
-let property0 = λ(n : Natural) → assert : lessThan n 0 ≡ False
-
-let property1 = λ(n : Natural) → assert : lessThan n n ≡ False
-
-in lessThan
diff --git a/Natural/lessThanEqual.dhall b/Natural/lessThanEqual.dhall
deleted file mode 100644
index 822d271..0000000
--- a/Natural/lessThanEqual.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
---| `lessThanEqual` checks if one Natural is less than or equal to another.
-let lessThanEqual
- : Natural → Natural → Bool
- = λ(x : Natural) → λ(y : Natural) → Natural/isZero (Natural/subtract y x)
-
-let example0 = assert : lessThanEqual 5 6 ≡ True
-
-let example1 = assert : lessThanEqual 5 5 ≡ True
-
-let example2 = assert : lessThanEqual 5 4 ≡ False
-
-let property0 = λ(n : Natural) → assert : lessThanEqual 0 n ≡ True
-
-let property1 = λ(n : Natural) → assert : lessThanEqual n n ≡ True
-
-in lessThanEqual
diff --git a/Natural/listMax.dhall b/Natural/listMax.dhall
deleted file mode 100644
index 9fd1c39..0000000
--- a/Natural/listMax.dhall
+++ /dev/null
@@ -1,15 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let max = ./max.dhall
-
- let Optional/map = ../Optional/map.dhall nix
-
- let listMax
- : List Natural → Optional Natural
- = λ(xs : List Natural) →
- Optional/map
- Natural
- Natural
- (λ(n : Natural) → List/fold Natural xs Natural max n)
- (List/head Natural xs)
-
- in listMax
diff --git a/Natural/listMin.dhall b/Natural/listMin.dhall
deleted file mode 100644
index 8de0d9d..0000000
--- a/Natural/listMin.dhall
+++ /dev/null
@@ -1,19 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let min = ./min.dhall
-
- let Optional/map = ../Optional/map.dhall nix
-
- let listMin
- : List Natural → Optional Natural
- = λ(xs : List Natural) →
- Optional/map
- Natural
- Natural
- ( λ(n : Natural) →
- if Natural/isZero n
- then n
- else List/fold Natural xs Natural min n
- )
- (List/head Natural xs)
-
- in listMin
diff --git a/Natural/max.dhall b/Natural/max.dhall
deleted file mode 100644
index 41da61e..0000000
--- a/Natural/max.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
---| `max a b` returns the larger of `a` or `b`
-let lessThanEqual = ./lessThanEqual.dhall
-
-let max
- : Natural → Natural → Natural
- = λ(a : Natural) → λ(b : Natural) → if lessThanEqual a b then b else a
-
-let example0 = assert : max 1 2 ≡ 2
-
-let example1 = assert : max 2 1 ≡ 2
-
-let property0 = λ(n : Natural) → assert : max n n ≡ n
-
-let property1 = λ(n : Natural) → assert : max 0 n ≡ n
-
-in max
diff --git a/Natural/min.dhall b/Natural/min.dhall
deleted file mode 100644
index bb0ff40..0000000
--- a/Natural/min.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
---| `min a b` returns the smaller of `a` or `b`
-let lessThanEqual = ./lessThanEqual.dhall
-
-let min
- : Natural → Natural → Natural
- = λ(a : Natural) → λ(b : Natural) → if lessThanEqual a b then a else b
-
-let example0 = assert : min 1 2 ≡ 1
-
-let example1 = assert : min 2 1 ≡ 1
-
-let property0 = λ(n : Natural) → assert : min n n ≡ n
-
-in min
diff --git a/Natural/odd.dhall b/Natural/odd.dhall
deleted file mode 100644
index 801471f..0000000
--- a/Natural/odd.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Returns `True` if a number is odd and returns `False` otherwise
-let odd
- : Natural → Bool
- = Natural/odd
-
-let example0 = assert : odd 3 ≡ True
-
-let example1 = assert : odd 0 ≡ False
-
-in odd
diff --git a/Natural/package.dhall b/Natural/package.dhall
index 2f2a8e7..206ae9b 100644
--- a/Natural/package.dhall
+++ b/Natural/package.dhall
@@ -1,27 +1,5 @@
λ(nix : ../NixPrelude.dhall) →
{ Type = Natural
- , build = ./build.dhall
, divide = ./divide.dhall nix
- , enumerate = ./enumerate.dhall
- , even = ./even.dhall
- , fold = ./fold.dhall
- , isZero = ./isZero.dhall
- , odd = ./odd.dhall
- , product = ./product.dhall
- , sum = ./sum.dhall
- , show = ./show.dhall
- , toDouble = ./toDouble.dhall
- , toInteger = ./toInteger.dhall
- , lessThan = ./lessThan.dhall
- , lessThanEqual = ./lessThanEqual.dhall
- , equal = ./equal.dhall
- , greaterThanEqual = ./greaterThanEqual.dhall
- , greaterThan = ./greaterThan.dhall
- , min = ./min.dhall
- , max = ./max.dhall
- , listMin = ./listMin.dhall nix
- , listMax = ./listMax.dhall nix
- , sort = ./sort.dhall nix
- , subtract = ./subtract.dhall
, fromAny = ./fromAny.dhall nix
}
diff --git a/Natural/product.dhall b/Natural/product.dhall
deleted file mode 100644
index 803f67c..0000000
--- a/Natural/product.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
---| Multiply all the numbers in a `List`
-let product
- : List Natural → Natural
- = λ(xs : List Natural) →
- List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l * r) 1
-
-let example0 = assert : product [ 2, 3, 5 ] ≡ 30
-
-let example1 = assert : product ([] : List Natural) ≡ 1
-
-in product
diff --git a/Natural/show.dhall b/Natural/show.dhall
deleted file mode 100644
index 8547c15..0000000
--- a/Natural/show.dhall
+++ /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)
--}
-let show
- : Natural → Text
- = Natural/show
-
-let example0 = assert : show 3 ≡ "3"
-
-let example1 = assert : show 0 ≡ "0"
-
-in show
diff --git a/Natural/sort.dhall b/Natural/sort.dhall
deleted file mode 100644
index 6c321f3..0000000
--- a/Natural/sort.dhall
+++ /dev/null
@@ -1,21 +0,0 @@
---| `sort` sorts a `List` of `Natural`s in ascending order
-λ(nix : ../NixPrelude.dhall) →
- let Any = ../Any/Type.dhall
-
- let Any/toAny = ../Any/toAny.dhall nix
-
- let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
-
- let Any/lessThan = ../Any/lessThan.dhall nix
-
- let coerceList =
- λ(from : Type) →
- λ(to : Type) →
- λ(list : List from) →
- Any/toTypeUnchecked (List to) (Any/toAny (List from) list)
-
- in λ(xs : List Natural) →
- coerceList
- Any
- Natural
- (nix.builtins.sort Any/lessThan (coerceList Natural Any xs))
diff --git a/Natural/subtract.dhall b/Natural/subtract.dhall
deleted file mode 100644
index 47352b5..0000000
--- a/Natural/subtract.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
---| `subtract m n` computes `n - m`, truncating to `0` if `m > n`
-let subtract
- : Natural → Natural → Natural
- = Natural/subtract
-
-let example0 = assert : subtract 1 2 ≡ 1
-
-let example1 = assert : subtract 1 1 ≡ 0
-
-let example2 = assert : subtract 2 1 ≡ 0
-
-let property0 = λ(n : Natural) → assert : subtract 0 n ≡ n
-
-let property1 = λ(n : Natural) → assert : subtract n 0 ≡ 0
-
-let property2 = λ(n : Natural) → assert : subtract n n ≡ 0
-
-in subtract
diff --git a/Natural/sum.dhall b/Natural/sum.dhall
deleted file mode 100644
index 40b6920..0000000
--- a/Natural/sum.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
---| Add all the numbers in a `List`
-let sum
- : List Natural → Natural
- = λ(xs : List Natural) →
- List/fold Natural xs Natural (λ(l : Natural) → λ(r : Natural) → l + r) 0
-
-let example = assert : sum [ 2, 3, 5 ] ≡ 10
-
-let example = assert : sum ([] : List Natural) ≡ 0
-
-in sum
diff --git a/Natural/toDouble.dhall b/Natural/toDouble.dhall
deleted file mode 100644
index ecd6cd0..0000000
--- a/Natural/toDouble.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Convert a `Natural` number to the corresponding `Double`
-let toDouble
- : Natural → Double
- = λ(n : Natural) → Integer/toDouble (Natural/toInteger n)
-
-let example0 = assert : toDouble 3 ≡ 3.0
-
-let example1 = assert : toDouble 0 ≡ 0.0
-
-in toDouble
diff --git a/Natural/toInteger.dhall b/Natural/toInteger.dhall
deleted file mode 100644
index 05b4a2d..0000000
--- a/Natural/toInteger.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Convert a `Natural` number to the corresponding `Integer`
-let toInteger
- : Natural → Integer
- = Natural/toInteger
-
-let example0 = assert : toInteger 3 ≡ +3
-
-let example1 = assert : toInteger 0 ≡ +0
-
-in toInteger
diff --git a/NonEmpty/Type.dhall b/NonEmpty/Type.dhall
deleted file mode 100644
index 300bb67..0000000
--- a/NonEmpty/Type.dhall
+++ /dev/null
@@ -1,9 +0,0 @@
-{-|
-A `NonEmpty` list has at least one element and supports many of the same
-operations as `List`s
--}
-let NonEmpty
- : Type → Type
- = λ(a : Type) → { head : a, tail : List a }
-
-in NonEmpty
diff --git a/NonEmpty/all.dhall b/NonEmpty/all.dhall
deleted file mode 100644
index 9398e95..0000000
--- a/NonEmpty/all.dhall
+++ /dev/null
@@ -1,28 +0,0 @@
-{-|
-Returns `True` if the supplied function returns `True` for all elements in the
-`NonEmpty` list
--}
-let NonEmpty = ./Type.dhall
-
-let NonEmpty/toList = ./toList.dhall
-
-let all
- : ∀(a : Type) → (a → Bool) → NonEmpty a → Bool
- = λ(a : Type) →
- λ(f : a → Bool) →
- λ(xs : NonEmpty a) →
- List/fold
- a
- (NonEmpty/toList a xs)
- Bool
- (λ(x : a) → λ(r : Bool) → f x && r)
- True
-
-let example0 =
- assert : all Natural Natural/even { head = 2, tail = [ 3, 5 ] } ≡ False
-
-let example1 =
- assert
- : all Natural Natural/even { head = 2, tail = [] : List Natural } ≡ True
-
-in all
diff --git a/NonEmpty/any.dhall b/NonEmpty/any.dhall
deleted file mode 100644
index 8245ee2..0000000
--- a/NonEmpty/any.dhall
+++ /dev/null
@@ -1,28 +0,0 @@
-{-|
-Returns `True` if the supplied function returns `True` for any element in the
-`NonEmpty` list
--}
-let NonEmpty = ./Type.dhall
-
-let NonEmpty/toList = ./toList.dhall
-
-let any
- : ∀(a : Type) → (a → Bool) → NonEmpty a → Bool
- = λ(a : Type) →
- λ(f : a → Bool) →
- λ(xs : NonEmpty a) →
- List/fold
- a
- (NonEmpty/toList a xs)
- Bool
- (λ(x : a) → λ(r : Bool) → f x || r)
- False
-
-let example0 =
- assert : any Natural Natural/even { head = 2, tail = [ 3, 5 ] } ≡ True
-
-let example1 =
- assert
- : any Natural Natural/even { head = 3, tail = [] : List Natural } ≡ False
-
-in any
diff --git a/NonEmpty/concat.dhall b/NonEmpty/concat.dhall
deleted file mode 100644
index d696302..0000000
--- a/NonEmpty/concat.dhall
+++ /dev/null
@@ -1,52 +0,0 @@
-{-|
-Concatenate a `NonEmpty` list of `NonEmpty` lists into a single `NonEmpty`
-list
--}
-let NonEmpty = ./Type.dhall
-
-let NonEmpty/toList = ./toList.dhall
-
-let List/concatMap = ../List/concatMap.dhall
-
-let concat
- : ∀(a : Type) → NonEmpty (NonEmpty a) → NonEmpty a
- = λ(a : Type) →
- λ(xss : NonEmpty (NonEmpty a)) →
- { head = xss.head.head
- , tail =
- xss.head.tail
- # List/concatMap (NonEmpty a) a (NonEmpty/toList a) xss.tail
- }
-
-let example0 =
- assert
- : concat
- Natural
- { head = { head = 0, tail = [ 1, 2 ] }
- , tail =
- [ { head = 3, tail = [ 4 ] }, { head = 5, tail = [ 6, 7, 8 ] } ]
- }
- ≡ { head = 0, tail = [ 1, 2, 3, 4, 5, 6, 7, 8 ] }
-
-let example1 =
- assert
- : concat
- Natural
- { head = { head = 0, tail = [] : List Natural }
- , tail =
- [ { head = 1, tail = [] : List Natural }
- , { head = 2, tail = [] : List Natural }
- ]
- }
- ≡ { head = 0, tail = [ 1, 2 ] : List Natural }
-
-let example2 =
- assert
- : concat
- Natural
- { head = { head = 0, tail = [] : List Natural }
- , tail = [] : List (NonEmpty Natural)
- }
- ≡ { head = 0, tail = [] : List Natural }
-
-in concat
diff --git a/NonEmpty/concatMap.dhall b/NonEmpty/concatMap.dhall
deleted file mode 100644
index acf0eba..0000000
--- a/NonEmpty/concatMap.dhall
+++ /dev/null
@@ -1,47 +0,0 @@
-{-|
-Transform a `NonEmpty` list by applying a function to each element and
-flattening the results
--}
-let NonEmpty = ./Type.dhall
-
-let NonEmpty/toList = ./toList.dhall
-
-let List/concatMap = ../List/concatMap.dhall
-
-let concatMap
- : ∀(a : Type) → ∀(b : Type) → (a → NonEmpty b) → NonEmpty a → NonEmpty b
- = λ(a : Type) →
- λ(b : Type) →
- λ(f : a → NonEmpty b) →
- λ(xs : NonEmpty a) →
- let ys = f xs.head
-
- in { head = ys.head
- , tail =
- ys.tail
- # List/concatMap
- a
- b
- (λ(x : a) → NonEmpty/toList b (f x))
- xs.tail
- }
-
-let example0 =
- assert
- : concatMap
- Natural
- Natural
- (λ(n : Natural) → { head = n, tail = [ n ] })
- { head = 2, tail = [ 3, 5 ] }
- ≡ { head = 2, tail = [ 2, 3, 3, 5, 5 ] }
-
-let example1 =
- assert
- : concatMap
- Natural
- Natural
- (λ(n : Natural) → { head = n, tail = [ n ] })
- { head = 2, tail = [] : List Natural }
- ≡ { head = 2, tail = [ 2 ] }
-
-in concatMap
diff --git a/NonEmpty/head.dhall b/NonEmpty/head.dhall
deleted file mode 100644
index ee3dac4..0000000
--- a/NonEmpty/head.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
---| Retrieve the first element of the `NonEmpty` list
-let NonEmpty = ./Type.dhall
-
-let head
- : ∀(a : Type) → NonEmpty a → a
- = λ(a : Type) → λ(xs : NonEmpty a) → xs.head
-
-let example = assert : head Natural { head = 0, tail = [ 1, 2 ] } ≡ 0
-
-in head
diff --git a/NonEmpty/index.dhall b/NonEmpty/index.dhall
deleted file mode 100644
index dd05b72..0000000
--- a/NonEmpty/index.dhall
+++ /dev/null
@@ -1,27 +0,0 @@
---| Retrieve an element from a `NonEmpty` list using its 0-based index
-let NonEmpty = ./Type.dhall
-
-let List/index = ../List/index.dhall
-
-let index
- : Natural → ∀(a : Type) → NonEmpty a → Optional a
- = λ(n : Natural) →
- λ(a : Type) →
- λ(xs : NonEmpty a) →
- if Natural/isZero n
- then Some xs.head
- else List/index (Natural/subtract 1 n) a xs.tail
-
-let property =
- λ(n : Natural) →
- λ(a : Type) →
- λ(xs : NonEmpty a) →
- assert : index 0 a xs ≡ Some xs.head
-
-let example0 = assert : index 1 Natural { head = 2, tail = [ 3, 5 ] } ≡ Some 3
-
-let example1 =
- assert
- : index 1 Natural { head = 2, tail = [] : List Natural } ≡ None Natural
-
-in index
diff --git a/NonEmpty/indexed.dhall b/NonEmpty/indexed.dhall
deleted file mode 100644
index c91351f..0000000
--- a/NonEmpty/indexed.dhall
+++ /dev/null
@@ -1,35 +0,0 @@
---| Tag each element of the `NonEmpty` list with its index
-let NonEmpty = ./Type.dhall
-
-let List/map = ../List/map.dhall
-
-let indexed
- : ∀(a : Type) → NonEmpty a → NonEmpty { index : Natural, value : a }
- = λ(a : Type) →
- λ(xs : NonEmpty a) →
- { head = { index = 0, value = xs.head }
- , tail =
- List/map
- { index : Natural, value : a }
- { index : Natural, value : a }
- ( λ(ix : { index : Natural, value : a }) →
- { index = ix.index + 1, value = ix.value }
- )
- (List/indexed a xs.tail)
- }
-
-let example0 =
- assert
- : indexed Bool { head = True, tail = [ False, True ] }
- ≡ { head = { index = 0, value = True }
- , tail = [ { index = 1, value = False }, { index = 2, value = True } ]
- }
-
-let example1 =
- assert
- : indexed Bool { head = True, tail = [] : List Bool }
- ≡ { head = { index = 0, value = True }
- , tail = [] : List { index : Natural, value : Bool }
- }
-
-in indexed
diff --git a/NonEmpty/last.dhall b/NonEmpty/last.dhall
deleted file mode 100644
index 496e272..0000000
--- a/NonEmpty/last.dhall
+++ /dev/null
@@ -1,12 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let NonEmpty = ./Type.dhall
-
- let Optional/default = ../Optional/default.dhall nix
-
- let last
- : ∀(a : Type) → NonEmpty a → a
- = λ(a : Type) →
- λ(xs : NonEmpty a) →
- Optional/default a xs.head (List/last a xs.tail)
-
- in last
diff --git a/NonEmpty/length.dhall b/NonEmpty/length.dhall
deleted file mode 100644
index d7132ff..0000000
--- a/NonEmpty/length.dhall
+++ /dev/null
@@ -1,13 +0,0 @@
---| Returns the number of elements in a `NonEmpty` list
-let NonEmpty = ./Type.dhall
-
-let length
- : ∀(a : Type) → NonEmpty a → Natural
- = λ(a : Type) → λ(xs : NonEmpty a) → List/length a xs.tail + 1
-
-let example0 = assert : length Natural { head = 0, tail = [ 1, 2 ] } ≡ 3
-
-let example1 =
- assert : length Natural { head = 0, tail = [] : List Natural } ≡ 1
-
-in length
diff --git a/NonEmpty/make.dhall b/NonEmpty/make.dhall
deleted file mode 100644
index 685726d..0000000
--- a/NonEmpty/make.dhall
+++ /dev/null
@@ -1,15 +0,0 @@
-{-|
-Create a `NonEmpty` list using a function instead of a record
-
-This might come in handy if you want to decouple the `NonEmpty` list
-construction from the specific names of the fields.
--}
-let NonEmpty = ./Type.dhall
-
-let make
- : ∀(a : Type) → ∀(head : a) → ∀(tail : List a) → NonEmpty a
- = λ(a : Type) → λ(head : a) → λ(tail : List a) → { head, tail }
-
-let example = assert : make Natural 1 [ 2, 3 ] ≡ { head = 1, tail = [ 2, 3 ] }
-
-in make
diff --git a/NonEmpty/map.dhall b/NonEmpty/map.dhall
deleted file mode 100644
index bf72019..0000000
--- a/NonEmpty/map.dhall
+++ /dev/null
@@ -1,24 +0,0 @@
---| Transform a `NonEmpty` list by applying a function to each element
-let NonEmpty = ./Type.dhall
-
-let List/map = ../List/map.dhall
-
-let map
- : ∀(a : Type) → ∀(b : Type) → (a → b) → NonEmpty a → NonEmpty b
- = λ(a : Type) →
- λ(b : Type) →
- λ(f : a → b) →
- λ(xs : NonEmpty a) →
- { head = f xs.head, tail = List/map a b f xs.tail }
-
-let example0 =
- assert
- : map Natural Bool Natural/even { head = 2, tail = [ 3, 5 ] }
- ≡ { head = True, tail = [ False, False ] }
-
-let example1 =
- assert
- : map Natural Bool Natural/even { head = 2, tail = [] : List Natural }
- ≡ { head = True, tail = [] : List Bool }
-
-in map
diff --git a/NonEmpty/package.dhall b/NonEmpty/package.dhall
deleted file mode 100644
index 74cc6bb..0000000
--- a/NonEmpty/package.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- { Type = ./Type.dhall
- , all = ./all.dhall
- , any = ./any.dhall
- , concat = ./concat.dhall
- , concatMap = ./concatMap.dhall
- , head = ./head.dhall
- , index = ./index.dhall
- , indexed = ./indexed.dhall
- , last = ./last.dhall nix
- , length = ./length.dhall
- , make = ./make.dhall
- , map = ./map.dhall
- , reverse = ./reverse.dhall nix
- , shifted = ./shifted.dhall
- , singleton = ./singleton.dhall
- , toList = ./toList.dhall
- , unzip = ./unzip.dhall
- , zip = ./zip.dhall nix
- }
diff --git a/NonEmpty/reverse.dhall b/NonEmpty/reverse.dhall
deleted file mode 100644
index 474778b..0000000
--- a/NonEmpty/reverse.dhall
+++ /dev/null
@@ -1,21 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let NonEmpty = ./Type.dhall
-
- let List/drop = ../List/drop.dhall
-
- let Optional/fold = ../Optional/fold.dhall nix
-
- let reverse
- : ∀(a : Type) → NonEmpty a → NonEmpty a
- = λ(a : Type) →
- λ(xs : NonEmpty a) →
- let ys = List/reverse a xs.tail
-
- in Optional/fold
- a
- (List/head a ys)
- (NonEmpty a)
- (λ(y : a) → { head = y, tail = List/drop 1 a ys # [ xs.head ] })
- { head = xs.head, tail = [] : List a }
-
- in reverse
diff --git a/NonEmpty/shifted.dhall b/NonEmpty/shifted.dhall
deleted file mode 100644
index 2fbf0f6..0000000
--- a/NonEmpty/shifted.dhall
+++ /dev/null
@@ -1,89 +0,0 @@
-{-|
-Combine a `NonEmpty` list of `NonEmpty` lists, offsetting the `index` of each
-element by the number of elements in preceding lists
--}
-let NonEmpty = ./Type.dhall
-
-let NonEmpty/toList = ./toList.dhall
-
-let List/map = ../List/map.dhall
-
-let List/shifted = ../List/shifted.dhall
-
-let shifted
- : ∀(a : Type) →
- NonEmpty (NonEmpty { index : Natural, value : a }) →
- NonEmpty { index : Natural, value : a }
- = λ(a : Type) →
- λ(kvss : NonEmpty (NonEmpty { index : Natural, value : a })) →
- { head = kvss.head.head
- , tail =
- List/shifted
- a
- ( [ kvss.head.tail ]
- # List/map
- (NonEmpty { index : Natural, value : a })
- (List { index : Natural, value : a })
- ( λ(kvs : NonEmpty { index : Natural, value : a }) →
- List/map
- { index : Natural, value : a }
- { index : Natural, value : a }
- ( λ(kv : { index : Natural, value : a }) →
- { index = kv.index + 1, value = kv.value }
- )
- (NonEmpty/toList { index : Natural, value : a } kvs)
- )
- kvss.tail
- )
- }
-
-let example0 =
- assert
- : shifted
- Bool
- { head =
- { head = { index = 0, value = True }
- , tail =
- [ { index = 1, value = True }, { index = 2, value = True } ]
- }
- , tail =
- [ { head = { index = 0, value = False }
- , tail = [ { index = 1, value = False } ]
- }
- , { head = { index = 0, value = True }
- , tail =
- [ { index = 1, value = True }
- , { index = 2, value = True }
- , { index = 3, value = True }
- ]
- }
- ]
- }
- ≡ { head = { index = 0, value = True }
- , tail =
- [ { 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 }
- ]
- }
-
-let example1 =
- assert
- : shifted
- Bool
- { head =
- { head = { index = 0, value = True }
- , tail = [] : List { index : Natural, value : Bool }
- }
- , tail = [] : List (NonEmpty { index : Natural, value : Bool })
- }
- ≡ { head = { index = 0, value = True }
- , tail = [] : List { index : Natural, value : Bool }
- }
-
-in shifted
diff --git a/NonEmpty/singleton.dhall b/NonEmpty/singleton.dhall
deleted file mode 100644
index 24a4360..0000000
--- a/NonEmpty/singleton.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
---| Create a `NonEmpty` list with just one element
-let NonEmpty = ./Type.dhall
-
-let singleton
- : ∀(a : Type) → a → NonEmpty a
- = λ(a : Type) → λ(x : a) → { head = x, tail = [] : List a }
-
-let example =
- assert : singleton Natural 2 ≡ { head = 2, tail = [] : List Natural }
-
-in singleton
diff --git a/NonEmpty/toList.dhall b/NonEmpty/toList.dhall
deleted file mode 100644
index 2add232..0000000
--- a/NonEmpty/toList.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
---| Convert a `NonEmpty` list into the equivalent `List`
-let NonEmpty = ./Type.dhall
-
-let toList
- : ∀(a : Type) → NonEmpty a → List a
- = λ(a : Type) → λ(xs : NonEmpty a) → [ xs.head ] # xs.tail
-
-let example0 =
- assert : toList Natural { head = 2, tail = [ 3, 5 ] } ≡ [ 2, 3, 5 ]
-
-let example1 =
- assert : toList Natural { head = 2, tail = [] : List Natural } ≡ [ 2 ]
-
-in toList
diff --git a/NonEmpty/unzip.dhall b/NonEmpty/unzip.dhall
deleted file mode 100644
index f48bd28..0000000
--- a/NonEmpty/unzip.dhall
+++ /dev/null
@@ -1,52 +0,0 @@
---| Unzip a `NonEmpty` list into two separate `NonEmpty` lists
-let NonEmpty = ./Type.dhall
-
-let NonEmpty/map = ./map.dhall
-
-let unzip
- : ∀(a : Type) →
- ∀(b : Type) →
- NonEmpty { _1 : a, _2 : b } →
- { _1 : NonEmpty a, _2 : NonEmpty b }
- = λ(a : Type) →
- λ(b : Type) →
- λ(xs : NonEmpty { _1 : a, _2 : b }) →
- { _1 =
- NonEmpty/map
- { _1 : a, _2 : b }
- a
- (λ(x : { _1 : a, _2 : b }) → x._1)
- xs
- , _2 =
- NonEmpty/map
- { _1 : a, _2 : b }
- b
- (λ(x : { _1 : a, _2 : b }) → x._2)
- xs
- }
-
-let example0 =
- assert
- : unzip
- Text
- Bool
- { head = { _1 = "ABC", _2 = True }
- , tail = [ { _1 = "DEF", _2 = False }, { _1 = "GHI", _2 = True } ]
- }
- ≡ { _1 = { head = "ABC", tail = [ "DEF", "GHI" ] }
- , _2 = { head = True, tail = [ False, True ] }
- }
-
-let example1 =
- assert
- : unzip
- Text
- Bool
- { head = { _1 = "ABC", _2 = True }
- , tail = [] : List { _1 : Text, _2 : Bool }
- }
- ≡ { _1 = { head = "ABC", tail = [] : List Text }
- , _2 = { head = True, tail = [] : List Bool }
- }
-
-in unzip
diff --git a/NonEmpty/zip.dhall b/NonEmpty/zip.dhall
deleted file mode 100644
index e8c587d..0000000
--- a/NonEmpty/zip.dhall
+++ /dev/null
@@ -1,20 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let NonEmpty = ./Type.dhall
-
- let List/zip = ../List/zip.dhall nix
-
- let zip
- : ∀(a : Type) →
- NonEmpty a →
- ∀(b : Type) →
- NonEmpty b →
- NonEmpty { _1 : a, _2 : b }
- = λ(a : Type) →
- λ(xs : NonEmpty a) →
- λ(b : Type) →
- λ(ys : NonEmpty b) →
- { head = { _1 = xs.head, _2 = ys.head }
- , tail = List/zip a xs.tail b ys.tail
- }
-
- in zip
diff --git a/Number/greaterThan.dhall b/Number/greaterThan.dhall
index 5b54dd3..cdef166 100644
--- a/Number/greaterThan.dhall
+++ b/Number/greaterThan.dhall
@@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
- let Bool/not = ../Bool/not.dhall
+ let Bool/not = https://prelude.dhall-lang.org/Bool/not.dhall
let Number/lessThanEqual = ./lessThanEqual.dhall nix
diff --git a/Number/greaterThanEqual.dhall b/Number/greaterThanEqual.dhall
index a1601c6..e9bdd8a 100644
--- a/Number/greaterThanEqual.dhall
+++ b/Number/greaterThanEqual.dhall
@@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
- let Bool/not = ../Bool/not.dhall
+ let Bool/not = https://prelude.dhall-lang.org/Bool/not.dhall
let Number/lessThan = ./lessThan.dhall nix
diff --git a/Number/positive.dhall b/Number/positive.dhall
index 2018008..87280bd 100644
--- a/Number/positive.dhall
+++ b/Number/positive.dhall
@@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
- let Bool/not = ../Bool/not.dhall
+ let Bool/not = https://prelude.dhall-lang.org/Bool/not.dhall
let Number/nonPositive = ./nonPositive.dhall nix
diff --git a/Number/toNatural.dhall b/Number/toNatural.dhall
index 7847028..6d9c566 100644
--- a/Number/toNatural.dhall
+++ b/Number/toNatural.dhall
@@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
- let Integer/toNatural = ../Integer/toNatural.dhall
+ let Integer/toNatural = https://prelude.dhall-lang.org/Integer/toNatural.dhall
let Number/toInteger = ./toInteger.dhall nix
diff --git a/Optional/all.dhall b/Optional/all.dhall
deleted file mode 100644
index ad943b9..0000000
--- a/Optional/all.dhall
+++ /dev/null
@@ -1,5 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
-λ(a : Type) →
-λ(f : a → Bool) →
-λ(xs : Optional a) →
- let fold = ./fold.dhall nix in fold a xs Bool f True
diff --git a/Optional/any.dhall b/Optional/any.dhall
deleted file mode 100644
index 3ff0bb5..0000000
--- a/Optional/any.dhall
+++ /dev/null
@@ -1,5 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
-λ(a : Type) →
-λ(f : a → Bool) →
-λ(xs : Optional a) →
- let fold = ./fold.dhall nix in fold a xs Bool f False
diff --git a/Optional/build.dhall b/Optional/build.dhall
deleted file mode 100644
index b26d2d1..0000000
--- a/Optional/build.dhall
+++ /dev/null
@@ -1,41 +0,0 @@
---| `build` is the inverse of `fold`
-let build
- : ∀(a : Type) →
- ( ∀(optional : Type) →
- ∀(some : a → optional) →
- ∀(none : optional) →
- optional
- ) →
- Optional a
- = λ(a : Type) →
- λ ( build
- : ∀(optional : Type) →
- ∀(some : a → optional) →
- ∀(none : optional) →
- optional
- ) →
- build (Optional a) (λ(x : a) → Some x) (None a)
-
-let example0 =
- assert
- : build
- Natural
- ( λ(optional : Type) →
- λ(some : Natural → optional) →
- λ(none : optional) →
- some 1
- )
- ≡ Some 1
-
-let example1 =
- assert
- : build
- Natural
- ( λ(optional : Type) →
- λ(some : Natural → optional) →
- λ(none : optional) →
- none
- )
- ≡ None Natural
-
-in build
diff --git a/Optional/concat.dhall b/Optional/concat.dhall
deleted file mode 100644
index 541a166..0000000
--- a/Optional/concat.dhall
+++ /dev/null
@@ -1,8 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
-λ(a : Type) →
-λ(x : Optional (Optional a)) →
- let identity = ../Function/identity.dhall
-
- let fold = ./fold.dhall nix
-
- in fold (Optional a) x (Optional a) (identity (Optional a)) (None a)
diff --git a/Optional/concatMap.dhall b/Optional/concatMap.dhall
deleted file mode 100644
index a75b4e8..0000000
--- a/Optional/concatMap.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
-λ(a : Type) →
-λ(b : Type) →
-λ(f : a → Optional b) →
-λ(o : Optional a) →
- let map = ./map.dhall nix
-
- let concat = ./concat.dhall nix
-
- in concat b (map a (Optional b) f o)
diff --git a/Optional/default.dhall b/Optional/default.dhall
deleted file mode 100644
index cfd37d0..0000000
--- a/Optional/default.dhall
+++ /dev/null
@@ -1,13 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let identity = ../Function/identity.dhall
-
- let fold = ./fold.dhall nix
-
- let default
- : ∀(a : Type) → a → Optional a → a
- = λ(a : Type) →
- λ(default : a) →
- λ(o : Optional a) →
- fold a o a (identity a) default
-
- in default
diff --git a/Optional/filter.dhall b/Optional/filter.dhall
deleted file mode 100644
index 28d1e66..0000000
--- a/Optional/filter.dhall
+++ /dev/null
@@ -1,7 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
-λ(a : Type) →
-λ(f : a → Bool) →
-λ(xs : Optional a) →
- let concatMap = ./concatMap.dhall nix
-
- in concatMap a a (λ(v : a) → if f v then Some v else None a) xs
diff --git a/Optional/fold.dhall b/Optional/fold.dhall
deleted file mode 100644
index f2900cc..0000000
--- a/Optional/fold.dhall
+++ /dev/null
@@ -1,36 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let Any = ../Any/Type.dhall
-
- let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
-
- let Any/equal = ../Any/equal.dhall nix
-
- let Any/toAny = ../Any/toAny.dhall nix
-
- let null = Any/toAny (Optional Any) (None Any)
-
- let isNone =
- λ(t : Type) →
- λ(o : Optional t) →
- Any/equal (Any/toAny (Optional t) o) null
-
- let unwrapUnsafe =
- λ(t : Type) →
- λ(o : Optional t) →
- Any/toTypeUnchecked t (Any/toAny (Optional t) o)
-
- let fold
- : ∀(a : Type) →
- Optional a →
- ∀(optional : Type) →
- ∀(some : a → optional) →
- ∀(none : optional) →
- optional
- = λ(a : Type) →
- λ(o : Optional a) →
- λ(optional : Type) →
- λ(some : a → optional) →
- λ(none : optional) →
- if isNone a o then none else some (unwrapUnsafe a o)
-
- in fold
diff --git a/Optional/head.dhall b/Optional/head.dhall
deleted file mode 100644
index df14931..0000000
--- a/Optional/head.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- 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) →
- fold a l (Optional a) (λ(v : a) → Some v) r
- )
- (None a)
-
- in head
diff --git a/Optional/last.dhall b/Optional/last.dhall
deleted file mode 100644
index a602c48..0000000
--- a/Optional/last.dhall
+++ /dev/null
@@ -1,18 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- 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) →
- fold a r (Optional a) (λ(v : a) → Some v) l
- )
- (None a)
-
- in head
diff --git a/Optional/length.dhall b/Optional/length.dhall
deleted file mode 100644
index 5182999..0000000
--- a/Optional/length.dhall
+++ /dev/null
@@ -1,8 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- let length
- : ∀(a : Type) → Optional a → Natural
- = λ(a : Type) → λ(xs : Optional a) → fold a xs Natural (λ(_ : a) → 1) 0
-
- in length
diff --git a/Optional/map.dhall b/Optional/map.dhall
deleted file mode 100644
index 7ee91e1..0000000
--- a/Optional/map.dhall
+++ /dev/null
@@ -1,12 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- let map
- : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b
- = λ(a : Type) →
- λ(b : Type) →
- λ(f : a → b) →
- λ(o : Optional a) →
- fold a o (Optional b) (λ(v : a) → Some (f v)) (None b)
-
- in map
diff --git a/Optional/null.dhall b/Optional/null.dhall
deleted file mode 100644
index 8343f90..0000000
--- a/Optional/null.dhall
+++ /dev/null
@@ -1,10 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- let null
- : ∀(a : Type) → Optional a → Bool
- = λ(a : Type) →
- λ(xs : Optional a) →
- fold a xs Bool (λ(_ : a) → True) False
-
- in null
diff --git a/Optional/package.dhall b/Optional/package.dhall
deleted file mode 100644
index 3efb34b..0000000
--- a/Optional/package.dhall
+++ /dev/null
@@ -1,17 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- { all = ./all.dhall nix
- , any = ./any.dhall nix
- , build = ./build.dhall
- , concat = ./concat.dhall nix
- , concatMap = ./concatMap.dhall nix
- , default = ./default.dhall nix
- , filter = ./filter.dhall nix
- , fold = ./fold.dhall nix
- , head = ./head.dhall nix
- , last = ./last.dhall nix
- , length = ./length.dhall nix
- , map = ./map.dhall nix
- , null = ./null.dhall nix
- , toList = ./toList.dhall nix
- , unzip = ./unzip.dhall nix
- }
diff --git a/Optional/toList.dhall b/Optional/toList.dhall
deleted file mode 100644
index 4ded163..0000000
--- a/Optional/toList.dhall
+++ /dev/null
@@ -1,6 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- in λ(a : Type) →
- λ(o : Optional a) →
- fold a o (List a) (λ(v : a) → [ v ]) ([] : List a)
diff --git a/Optional/unwrap.dhall b/Optional/unwrap.dhall
deleted file mode 100644
index 1c6523f..0000000
--- a/Optional/unwrap.dhall
+++ /dev/null
@@ -1,8 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let default = ./default.dhall nix
-
- let Misc/throw = ../Misc/throw.dhall nix
-
- in λ(t : Type) →
- λ(o : Optional t) →
- default t (Misc/throw t "Tried to unwrap None") o
diff --git a/Optional/unzip.dhall b/Optional/unzip.dhall
deleted file mode 100644
index 49274d1..0000000
--- a/Optional/unzip.dhall
+++ /dev/null
@@ -1,12 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- let fold = ./fold.dhall nix
-
- in λ(a : Type) →
- λ(b : Type) →
- λ(xs : Optional { _1 : a, _2 : b }) →
- fold
- { _1 : a, _2 : b }
- xs
- { _1 : Optional a, _2 : Optional b }
- (λ(v : { _1 : a, _2 : b }) → { _1 = Some v._1, _2 = Some v._2 })
- { _1 = None a, _2 = None b }
diff --git a/Text/concat.dhall b/Text/concat.dhall
deleted file mode 100644
index 6acc016..0000000
--- a/Text/concat.dhall
+++ /dev/null
@@ -1,11 +0,0 @@
---| Concatenate all the `Text` values in a `List`
-let concat
- : List Text → Text
- = λ(xs : List Text) →
- List/fold Text xs Text (λ(x : Text) → λ(y : Text) → x ++ y) ""
-
-let example0 = assert : concat [ "ABC", "DEF", "GHI" ] ≡ "ABCDEFGHI"
-
-let example1 = assert : concat ([] : List Text) ≡ ""
-
-in concat
diff --git a/Text/concatMap.dhall b/Text/concatMap.dhall
deleted file mode 100644
index 2defcfa..0000000
--- a/Text/concatMap.dhall
+++ /dev/null
@@ -1,22 +0,0 @@
---| Transform each value in a `List` into `Text` and concatenate the result
-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) ""
-
-let example0 =
- assert
- : concatMap Natural (λ(n : Natural) → "${Natural/show n} ") [ 0, 1, 2 ]
- ≡ "0 1 2 "
-
-let example1 =
- assert
- : concatMap
- Natural
- (λ(n : Natural) → "${Natural/show n} ")
- ([] : List Natural)
- ≡ ""
-
-in concatMap
diff --git a/Text/concatMapSep.dhall b/Text/concatMapSep.dhall
deleted file mode 100644
index 8e23b70..0000000
--- a/Text/concatMapSep.dhall
+++ /dev/null
@@ -1,38 +0,0 @@
-{-|
-Transform each value in a `List` to `Text` and then concatenate them with a
-separator in between each value
--}
-let Status = < Empty | NonEmpty : Text >
-
-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
- Status
- ( λ(x : a) →
- λ(status : Status) →
- merge
- { Empty = Status.NonEmpty (f x)
- , NonEmpty =
- λ(result : Text) →
- Status.NonEmpty (f x ++ separator ++ result)
- }
- status
- )
- Status.Empty
-
- in merge { Empty = "", NonEmpty = λ(result : Text) → result } status
-
-let example0 =
- assert : concatMapSep ", " Natural Natural/show [ 0, 1, 2 ] ≡ "0, 1, 2"
-
-let example1 =
- assert : concatMapSep ", " Natural Natural/show ([] : List Natural) ≡ ""
-
-in concatMapSep
diff --git a/Text/concatSep.dhall b/Text/concatSep.dhall
deleted file mode 100644
index 9e2959e..0000000
--- a/Text/concatSep.dhall
+++ /dev/null
@@ -1,31 +0,0 @@
---| Concatenate a `List` of `Text` values with a separator in between each value
-let Status = < Empty | NonEmpty : Text >
-
-let concatSep
- : ∀(separator : Text) → ∀(elements : List Text) → Text
- = λ(separator : Text) →
- λ(elements : List Text) →
- let status =
- List/fold
- Text
- elements
- Status
- ( λ(element : Text) →
- λ(status : Status) →
- merge
- { Empty = Status.NonEmpty element
- , NonEmpty =
- λ(result : Text) →
- Status.NonEmpty (element ++ separator ++ result)
- }
- status
- )
- Status.Empty
-
- in merge { Empty = "", NonEmpty = λ(result : Text) → result } status
-
-let example0 = assert : concatSep ", " [ "ABC", "DEF", "GHI" ] ≡ "ABC, DEF, GHI"
-
-let example1 = assert : concatSep ", " ([] : List Text) ≡ ""
-
-in concatSep
diff --git a/Text/default.dhall b/Text/default.dhall
deleted file mode 100644
index 110c3e2..0000000
--- a/Text/default.dhall
+++ /dev/null
@@ -1,9 +0,0 @@
---| Unwrap an `Optional` `Text` value, defaulting `None` to `""`
-λ(nix : ../NixPrelude.dhall) →
- let Optional/default = ../Optional/default.dhall nix
-
- let default
- : Optional Text → Text
- = λ(o : Optional Text) → Optional/default Text "" o
-
- in default
diff --git a/Text/defaultMap.dhall b/Text/defaultMap.dhall
deleted file mode 100644
index fb02441..0000000
--- a/Text/defaultMap.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
---| Transform the value in an `Optional` into `Text`, defaulting `None` to `""`
-λ(nix : ../NixPrelude.dhall) →
- let Optional/map = ../Optional/map.dhall nix
-
- let default = ./default.dhall nix
-
- let defaultMap
- : ∀(a : Type) → (a → Text) → Optional a → Text
- = λ(a : Type) →
- λ(f : a → Text) →
- λ(o : Optional a) →
- default (Optional/map a Text f o)
-
- in defaultMap
diff --git a/Text/lowerASCII.dhall b/Text/lowerASCII.dhall
deleted file mode 100644
index a96ae8e..0000000
--- a/Text/lowerASCII.dhall
+++ /dev/null
@@ -1,56 +0,0 @@
-{-|
-Lowercase all ASCII characters
-
-Note that this will also lowercase decomposed Unicode characters that contain
-codepoints in the ASCII range
--}
-let lowerASCII
- : Text → Text
- = List/fold
- (Text → Text)
- [ Text/replace "A" "a"
- , Text/replace "B" "b"
- , Text/replace "C" "c"
- , Text/replace "D" "d"
- , Text/replace "E" "e"
- , Text/replace "F" "f"
- , Text/replace "G" "g"
- , Text/replace "H" "h"
- , Text/replace "I" "i"
- , Text/replace "J" "j"
- , Text/replace "K" "k"
- , Text/replace "L" "l"
- , Text/replace "M" "m"
- , Text/replace "N" "n"
- , Text/replace "O" "o"
- , Text/replace "P" "p"
- , Text/replace "Q" "q"
- , Text/replace "R" "r"
- , Text/replace "S" "s"
- , Text/replace "T" "t"
- , Text/replace "U" "u"
- , Text/replace "V" "v"
- , Text/replace "W" "w"
- , Text/replace "X" "x"
- , Text/replace "Y" "y"
- , Text/replace "Z" "z"
- ]
- Text
- (λ(replacement : Text → Text) → replacement)
-
-let example0 = assert : lowerASCII "ABCdef" ≡ "abcdef"
-
-let -- This does not lowercase precomposed Unicode characters
- --
- -- • The `Á` in the following example is U+00C1
- example1 =
- assert : lowerASCII "Á" ≡ "Á"
-
-let -- … but this does lowercase decomposed Unicode characters
- --
- -- • The `Á` in the following example is U+0041 U+0301
- -- • The `á` in the following example is U+0061 U+0301
- example1 =
- assert : lowerASCII "Á" ≡ "á"
-
-in lowerASCII
diff --git a/Text/package.dhall b/Text/package.dhall
deleted file mode 100644
index 3704252..0000000
--- a/Text/package.dhall
+++ /dev/null
@@ -1,15 +0,0 @@
-λ(nix : ../NixPrelude.dhall) →
- { concat = ./concat.dhall
- , concatMap = ./concatMap.dhall
- , concatMapSep = ./concatMapSep.dhall
- , concatSep = ./concatSep.dhall
- , default = ./default.dhall nix
- , defaultMap = ./defaultMap.dhall nix
- , lowerASCII = ./lowerASCII.dhall
- , replace = ./replace.dhall
- , replicate = ./replicate.dhall
- , shell-escape = ./shell-escape.dhall
- , show = ./show.dhall
- , spaces = ./spaces.dhall
- , upperASCII = ./upperASCII.dhall
- }
diff --git a/Text/replace.dhall b/Text/replace.dhall
deleted file mode 100644
index ba01e91..0000000
--- a/Text/replace.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
-{-
-Replace a section of `Text` with another inside a `Text` literal.
--}
-let replace
- : ∀(needle : Text) → ∀(replacement : Text) → ∀(haystack : Text) → Text
- = Text/replace
-
-let example0 = assert : replace "-" "_" "foo-bar" ≡ "foo_bar"
-
-let example1 = assert : replace "💣" "💥" "💣💣💣" ≡ "💥💥💥"
-
-let example2 = assert : replace "👨" "👩" "👨👩👧👦" ≡ "👩👩👧👦"
-
-in replace
diff --git a/Text/replicate.dhall b/Text/replicate.dhall
deleted file mode 100644
index 388712e..0000000
--- a/Text/replicate.dhall
+++ /dev/null
@@ -1,14 +0,0 @@
---| Build a Text by copying the given Text the specified number of times
-let concat = ./concat.dhall
-
-let List/replicate = ../List/replicate.dhall
-
-let replicate
- : Natural → Text → Text
- = λ(num : Natural) → λ(text : Text) → concat (List/replicate num Text text)
-
-let example0 = assert : replicate 3 "foo" ≡ "foofoofoo"
-
-let property = λ(text : Text) → assert : replicate 0 text ≡ ""
-
-in replicate
diff --git a/Text/shell-escape.dhall b/Text/shell-escape.dhall
deleted file mode 100644
index ecabd14..0000000
--- a/Text/shell-escape.dhall
+++ /dev/null
@@ -1,16 +0,0 @@
-{-|
-Escape a Text value such that it can be used safely in shells.
-The escaping is done by replacing all `'` with `'"'"'` and wraps that string in
-single quotes.
-
-This works for all POSIX-compliant shells and some other shells like csh.
--}
-let shell-escape
- : Text -> Text
- = \(xs : Text) -> "'${Text/replace "'" "'\"'\"'" xs}'"
-
-let example0 = assert : shell-escape "foo" === "'foo'"
-
-let example1 = assert : shell-escape "foo'bar" === "'foo'\"'\"'bar'"
-
-in shell-escape
diff --git a/Text/show.dhall b/Text/show.dhall
deleted file mode 100644
index 93858d9..0000000
--- a/Text/show.dhall
+++ /dev/null
@@ -1,19 +0,0 @@
-{-
-Render a `Text` literal as its own representation as Dhall source code (i.e. a
-double-quoted string literal)
--}
-let show
- : Text → Text
- = Text/show
-
-let example0 = assert : show "ABC" ≡ "\"ABC\""
-
-let example1 =
- assert
- : show
- ''
- ${"\u0000"} $ \
- ${" "}☺''
- ≡ "\"\\u0000 \\u0024 \\\\ \\n ☺\""
-
-in show
diff --git a/Text/spaces.dhall b/Text/spaces.dhall
deleted file mode 100644
index 30693c2..0000000
--- a/Text/spaces.dhall
+++ /dev/null
@@ -1,17 +0,0 @@
-{-|
-Return a Text with the number of spaces specified.
-
-This function is particularly helpful when trying to generate Text where
-whitespace is significant, i.e. with nested indentation.
--}
-let replicate = ./replicate.dhall
-
-let spaces
- : Natural → Text
- = λ(a : Natural) → replicate a " "
-
-let example0 = assert : spaces 1 ≡ " "
-
-let example1 = assert : spaces 0 ≡ ""
-
-in spaces
diff --git a/Text/upperASCII.dhall b/Text/upperASCII.dhall
deleted file mode 100644
index 4f17f1d..0000000
--- a/Text/upperASCII.dhall
+++ /dev/null
@@ -1,56 +0,0 @@
-{-|
-Uppercase all ASCII characters
-
-Note that this will also uppercase decomposed Unicode characters that contain
-codepoints in the ASCII range
--}
-let upperASCII
- : Text → Text
- = List/fold
- (Text → Text)
- [ Text/replace "a" "A"
- , Text/replace "b" "B"
- , Text/replace "c" "C"
- , Text/replace "d" "D"
- , Text/replace "e" "E"
- , Text/replace "f" "F"
- , Text/replace "g" "G"
- , Text/replace "h" "H"
- , Text/replace "i" "I"
- , Text/replace "j" "J"
- , Text/replace "k" "K"
- , Text/replace "l" "L"
- , Text/replace "m" "M"
- , Text/replace "n" "N"
- , Text/replace "o" "O"
- , Text/replace "p" "P"
- , Text/replace "q" "Q"
- , Text/replace "r" "R"
- , Text/replace "s" "S"
- , Text/replace "t" "T"
- , Text/replace "u" "U"
- , Text/replace "v" "V"
- , Text/replace "w" "W"
- , Text/replace "x" "X"
- , Text/replace "y" "Y"
- , Text/replace "z" "Z"
- ]
- Text
- (λ(replacement : Text → Text) → replacement)
-
-let example0 = assert : upperASCII "ABCdef" ≡ "ABCDEF"
-
-let -- This does not uppercase precomposed Unicode characters
- --
- -- • The `á` in the following example is U+00E1
- example1 =
- assert : upperASCII "á" ≡ "á"
-
-let -- … but this does uppercase decomposed Unicode characters
- --
- -- • The `Á` in the following example is U+0041 U+0301
- -- • The `á` in the following example is U+0061 U+0301
- example1 =
- assert : upperASCII "á" ≡ "Á"
-
-in upperASCII
diff --git a/XML/Type.dhall b/XML/Type.dhall
deleted file mode 100644
index d891680..0000000
--- a/XML/Type.dhall
+++ /dev/null
@@ -1,65 +0,0 @@
-{-|
-Dhall encoding of an arbitrary XML element
-
-For example, the following XML element:
-
-```
-baz
-```
-
-... corresponds to the following Dhall expression:
-
-
-```
-λ(XML : Type)
- → λ ( xml
- : { text :
- Text → XML
- , rawText :
- Text → XML
- , element :
- { attributes :
- List { mapKey : Text, mapValue : Text }
- , content :
- List XML
- , name :
- Text
- }
- → XML
- }
- )
- → xml.element
- { attributes =
- [ { mapKey = "n", mapValue = "1" } ]
- , content =
- [ xml.element
- { attributes =
- [] : List { mapKey : Text, mapValue : Text }
- , content =
- [ xml.text "baz" ]
- , name =
- "bar"
- }
- ]
- , name =
- "foo"
- }
-```
--}
-let XML/Type
- : Type
- = ∀(XML : Type) →
- ∀ ( xml
- : { text : Text → XML
- , rawText : Text → XML
- , element :
- { attributes : List { mapKey : Text, mapValue : Text }
- , content : List XML
- , name : Text
- } →
- XML
- }
- ) →
- XML
-
-in XML/Type
diff --git a/XML/attribute.dhall b/XML/attribute.dhall
deleted file mode 100644
index 94bd4c4..0000000
--- a/XML/attribute.dhall
+++ /dev/null
@@ -1,6 +0,0 @@
---| Builds a key-value record with a Text key and value.
-let attribute
- : Text → Text → { mapKey : Text, mapValue : Text }
- = λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
-
-in attribute
diff --git a/XML/element.dhall b/XML/element.dhall
deleted file mode 100644
index 079c08a..0000000
--- a/XML/element.dhall
+++ /dev/null
@@ -1,55 +0,0 @@
-{-|
-Create an XML element value.
-
-```
-let XML = ./package.dhall
-
-in XML.render
- ( XML.element
- { name = "foo"
- , attributes = XML.emptyAttributes
- , content =
- [ XML.leaf { name = "bar", attributes = [ XML.attribute "n" "1" ] }
- , XML.leaf { name = "baz", attributes = [ XML.attribute "n" "2" ] }
- ]
- }
- )
-
-= ""
-```
--}
-let XML =
- ./Type.dhall
-
-let List/map =
- ../List/map.dhall
-
-let Args =
- { attributes : List { mapKey : Text, mapValue : Text }
- , name : Text
- , content : List XML
- }
- : Type
-
-let element
- : Args → XML
- = λ(elem : Args) →
- λ(XML : Type) →
- λ ( xml
- : { text : Text → XML
- , rawText : Text → XML
- , element :
- { attributes : List { mapKey : Text, mapValue : Text }
- , content : List XML
- , name : Text
- } →
- XML
- }
- ) →
- xml.element
- { attributes = elem.attributes
- , name = elem.name
- , content = List/map XML@1 XML (λ(x : XML@1) → x XML xml) elem.content
- }
-
-in element
diff --git a/XML/emptyAttributes.dhall b/XML/emptyAttributes.dhall
deleted file mode 100644
index 3a449ba..0000000
--- a/XML/emptyAttributes.dhall
+++ /dev/null
@@ -1,2 +0,0 @@
---| Create an empty XML attribute List.
-[] : List { mapKey : Text, mapValue : Text }
diff --git a/XML/leaf.dhall b/XML/leaf.dhall
deleted file mode 100644
index 0f921b8..0000000
--- a/XML/leaf.dhall
+++ /dev/null
@@ -1,26 +0,0 @@
-{-|
-Create an XML element value without child elements.
-
-```
-let XML = ./package.dhall
-
-in XML.render (XML.leaf { name = "foobar", attributes = XML.emptyAttributes })
-
-= ""
-```
--}
-let XML =
- ./Type.dhall
-
-let element =
- ./element.dhall
-
-let leaf
- : { attributes : List { mapKey : Text, mapValue : Text }, name : Text } →
- XML
- = λ ( elem
- : { attributes : List { mapKey : Text, mapValue : Text }, name : Text }
- ) →
- element (elem ⫽ { content = [] : List XML })
-
-in leaf
diff --git a/XML/package.dhall b/XML/package.dhall
deleted file mode 100644
index d48591e..0000000
--- a/XML/package.dhall
+++ /dev/null
@@ -1,17 +0,0 @@
-{ Type =
- ./Type.dhall
-, attribute =
- ./attribute.dhall
-, render =
- ./render.dhall
-, element =
- ./element.dhall
-, leaf =
- ./leaf.dhall
-, text =
- ./text.dhall
-, rawText =
- ./rawText.dhall
-, emptyAttributes =
- ./emptyAttributes.dhall
-}
diff --git a/XML/rawText.dhall b/XML/rawText.dhall
deleted file mode 100644
index d3f22a1..0000000
--- a/XML/rawText.dhall
+++ /dev/null
@@ -1,38 +0,0 @@
-{-|
-Create a Text value to be inserted into an XML element as content with no
-character escaping.
-
-```
-let XML = ./package.dhall
-
-in XML.render
- ( XML.element
- { name = "location"
- , attributes = XML.emptyAttributes
- , content = [ XML.rawText "" ]
- }
- )
-= ""
-```
--}
-let XML =
- ./Type.dhall
-
-let rawText
- : Text → XML
- = λ(d : Text) →
- λ(XML : Type) →
- λ ( xml
- : { text : Text → XML
- , rawText : Text → XML
- , element :
- { attributes : List { mapKey : Text, mapValue : Text }
- , content : List XML
- , name : Text
- } →
- XML
- }
- ) →
- xml.rawText d
-
-in rawText
diff --git a/XML/render.dhall b/XML/render.dhall
deleted file mode 100644
index 333e149..0000000
--- a/XML/render.dhall
+++ /dev/null
@@ -1,128 +0,0 @@
-{-|
-Render an `XML` value as `Text`
-
-For indentation and schema validation, see the `xmllint` utility
-bundled with libxml2.
-
-```
-let XML = ./package.dhall
-
-in XML.render
- ( XML.element
- { name = "foo"
- , attributes = [ XML.attribute "a" "x", XML.attribute "b" (Natural/show 2) ]
- , content = [ XML.leaf { name = "bar", attributes = XML.emptyAttributes } ]
- }
- )
-= ""
-```
-
--}
-let XML =
- ./Type.dhall
-
-let Text/concatMap =
- ../Text/concatMap.dhall
-
-let Text/concat =
- ../Text/concat.dhall
-
-let element =
- ./element.dhall
-
-let text =
- ./text.dhall
-
-let emptyAttributes =
- ./emptyAttributes.dhall
-
-let Attr = { mapKey : Text, mapValue : Text }
-
-let esc = λ(x : Text) → λ(y : Text) → Text/replace x "&${y};"
-
-let `escape&` = esc "&" "amp"
-
-let `escape<` = esc "<" "lt"
-
-let `escape>` = esc ">" "gt"
-
-let `escape'` = esc "'" "apos"
-
-let `escape"` = esc "\"" "quot"
-
-let escapeCommon = λ(text : Text) → `escape<` (`escape&` text)
-
-let escapeAttr = λ(text : Text) → `escape"` (`escape'` (escapeCommon text))
-
-let escapeText = λ(text : Text) → `escape>` (escapeCommon text)
-
-let renderAttr = λ(x : Attr) → " ${x.mapKey}=\"${escapeAttr x.mapValue}\""
-
-let render
- : XML → Text
- = λ(x : XML) →
- x
- Text
- { text = escapeText
- , rawText = λ(t : Text) → t
- , element =
- λ ( elem
- : { attributes : List { mapKey : Text, mapValue : Text }
- , content : List Text
- , name : Text
- }
- ) →
- let attribs = Text/concatMap Attr renderAttr elem.attributes
-
- in "<${elem.name}${attribs}"
- ++ ( if Natural/isZero (List/length Text elem.content)
- then "/>"
- else ">${Text/concat elem.content}"
- )
- }
-
-let simple =
- λ(name : Text) →
- λ(content : List XML) →
- element { name, attributes = emptyAttributes, content }
-
-let example0 =
- assert
- : render
- ( simple
- "note"
- [ simple "to" [ text "Tove" ]
- , simple "from" [ text "Jani" ]
- , simple "heading" [ text "Reminder" ]
- , simple "body" [ text "Don't forget me this weekend!" ]
- ]
- )
- ≡ Text/replace
- "\n"
- ""
- ''
-
- Tove
- Jani
- Reminder
- Don't forget me this weekend!
-
- ''
-
-let example1 =
- assert
- : render
- ( element
- { name = "escape"
- , attributes = toMap { attribute = "<>'\"&" }
- , content = [ text "<>'\"&" ]
- }
- )
- ≡ Text/replace
- "\n"
- ""
- ''
- <>'"&
- ''
-
-in render
diff --git a/XML/text.dhall b/XML/text.dhall
deleted file mode 100644
index c3145e4..0000000
--- a/XML/text.dhall
+++ /dev/null
@@ -1,37 +0,0 @@
-{-|
-Create a Text value to be inserted into an XML element as content.
-
-```
-let XML = ./package.dhall
-
-in XML.render
- ( XML.element
- { name = "location"
- , attributes = XML.emptyAttributes
- , content = [ XML.text "/foo/bar" ]
- }
- )
-= "/foo/bar"
-```
--}
-let XML =
- ./Type.dhall
-
-let text
- : Text → XML
- = λ(d : Text) →
- λ(XML : Type) →
- λ ( xml
- : { text : Text → XML
- , rawText : Text → XML
- , element :
- { attributes : List { mapKey : Text, mapValue : Text }
- , content : List XML
- , name : Text
- } →
- XML
- }
- ) →
- xml.text d
-
-in text
diff --git a/package.dhall b/package.dhall
index b728108..d2e73db 100644
--- a/package.dhall
+++ b/package.dhall
@@ -1,21 +1,10 @@
λ(nix : ./NixPrelude.dhall) →
+ https://prelude.dhall-lang.org/package.dhall ∧
{ Any = ./Any/package.dhall nix
, Bool = ./Bool/package.dhall nix
, Double = ./Double/package.dhall nix
- , Function = ./Function/package.dhall
, Integer = ./Integer/package.dhall nix
- , JSON = ./JSON/package.dhall nix
, List = ./List/package.dhall nix
- , Location = ./Location/package.dhall
- , Map = ./Map/package.dhall nix
, Misc = ./Misc/package.dhall nix
- , Monoid = ./Monoid.dhall
- , NonNull = ./NonEmpty/package.dhall nix
, Natural = ./Natural/package.dhall nix
- , Number = ./Number/package.dhall nix
- , Optional = ./Optional/package.dhall nix
- , Path = ./Path/package.dhall nix
- , Set = ./Set/package.dhall nix
- , Text = ./Text/package.dhall nix
- , XML = ./XML/package.dhall
- }
+ , Number = ./Number/package.dhall nix}