add missing methods from Integer, Double and Number

This commit is contained in:
Charlotte 🦝 Delenk 2022-09-01 15:41:13 +01:00
parent be8a2426b2
commit cb33a0d06f
Signed by: darkkirb
GPG key ID: AB2BD8DAF2E37122
36 changed files with 505 additions and 1 deletions

12
Double/abs.dhall Normal file
View file

@ -0,0 +1,12 @@
λ(nix : ../NixPrelude.dhall) →
let isZero = ./isZero.dhall nix
let clamp = ./clamp.dhall nix
let negate = ./negate.dhall nix
let abs
: Double → Double
= λ(n : Double) → if isZero (clamp n) then clamp (negate n) else clamp n
in abs

21
Double/build.dhall Normal file
View file

@ -0,0 +1,21 @@
λ(nix : ../NixPrelude.dhall) →
let add = ./add.dhall nix
let negate = ./negate.dhall nix
let divide = ./divide.dhall nix
let succ = λ(n : Double) → add n 1.0
let build =
λ ( builder
: ∀(double : Type) →
(double → double) →
(double → double) →
(double → double → double) →
double →
double
) →
builder Double succ negate divide 0.0
in build

10
Double/isZero.dhall Normal file
View file

@ -0,0 +1,10 @@
λ(nix : ../NixPrelude.dhall) →
let nonPositive = ./nonPositive.dhall nix
let nonNegative = ./nonNegative.dhall nix
let isZero
: Double → Bool
= λ(v : Double) → nonPositive v && nonNegative v
in isZero

15
Double/listMax.dhall Normal file
View file

@ -0,0 +1,15 @@
λ(nix : ../NixPrelude.dhall) →
let max = ./max.dhall nix
let Optional/map = ../Optional/map.dhall nix
let listMax
: List Double → Optional Double
= λ(xs : List Double) →
Optional/map
Double
Double
(λ(n : Double) → List/fold Double xs Double max n)
(List/head Double xs)
in listMax

19
Double/listMin.dhall Normal file
View file

@ -0,0 +1,19 @@
λ(nix : ../NixPrelude.dhall) →
let min = ./min.dhall nix
let Double/isZero = ./isZero.dhall nix
let Optional/map = ../Optional/map.dhall nix
let listMin
: List Double → Optional Double
= λ(xs : List Double) →
Optional/map
Double
Double
( λ(n : Double) →
if Double/isZero n then n else List/fold Double xs Double min n
)
(List/head Double xs)
in listMin

8
Double/max.dhall Normal file
View file

@ -0,0 +1,8 @@
λ(nix : ../NixPrelude.dhall) →
let lessThanEqual = ./lessThanEqual.dhall nix
let max
: Double → Double → Double
= λ(a : Double) → λ(b : Double) → if lessThanEqual a b then b else a
in max

8
Double/min.dhall Normal file
View file

@ -0,0 +1,8 @@
λ(nix : ../NixPrelude.dhall) →
let lessThanEqual = ./lessThanEqual.dhall nix
let min
: Double → Double → Double
= λ(a : Double) → λ(b : Double) → if lessThanEqual a b then a else b
in min

View file

@ -1,22 +1,32 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) →
{ Type = Double { Type = Double
, abs = ./abs.dhall nix
, add = ./add.dhall nix , add = ./add.dhall nix
, build = ./build.dhall nix
, clamp = ./clamp.dhall nix , clamp = ./clamp.dhall nix
, divide = ./divide.dhall nix , divide = ./divide.dhall nix
, equal = ./equal.dhall nix , equal = ./equal.dhall nix
, fromAny = ./fromAny.dhall nix , fromAny = ./fromAny.dhall nix
, greaterThan = ./greaterThan.dhall nix , greaterThan = ./greaterThan.dhall nix
, greaterThanEqual = ./greaterThanEqual.dhall nix , greaterThanEqual = ./greaterThanEqual.dhall nix
, isZero = ./isZero.dhall nix
, lessThan = ./lessThan.dhall nix , lessThan = ./lessThan.dhall nix
, lessThanEqual = ./lessThanEqual.dhall nix , lessThanEqual = ./lessThanEqual.dhall nix
, listMax = ./listMax.dhall nix
, listMin = ./listMin.dhall nix
, max = ./max.dhall nix
, min = ./min.dhall nix
, multiply = ./multiply.dhall nix , multiply = ./multiply.dhall nix
, negate = ./negate.dhall nix , negate = ./negate.dhall nix
, negative = ./negative.dhall nix , negative = ./negative.dhall nix
, nonNegative = ./nonNegative.dhall nix , nonNegative = ./nonNegative.dhall nix
, nonPositive = ./nonPositive.dhall nix , nonPositive = ./nonPositive.dhall nix
, positive = ./positive.dhall nix , positive = ./positive.dhall nix
, product = ./product.dhall nix
, show = ./show.dhall , show = ./show.dhall
, sort = ./sort.dhall nix
, subtract = ./subtract.dhall nix , subtract = ./subtract.dhall nix
, sum = ./sum.dhall nix
, toInteger = ./toInteger.dhall nix , toInteger = ./toInteger.dhall nix
, toNatural = ./toNatural.dhall nix , toNatural = ./toNatural.dhall nix
} }

8
Double/product.dhall Normal file
View file

@ -0,0 +1,8 @@
λ(nix : ../NixPrelude.dhall) →
let Double/multiply = ./multiply.dhall nix
let product
: List Double → Double
= λ(xs : List Double) → List/fold Double xs Double Double/multiply 1.0
in product

21
Double/sort.dhall Normal file
View file

@ -0,0 +1,21 @@
--| `sort` sorts a `List` of `Double`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 Double) →
coerceList
Any
Double
(nix.builtins.sort Any/lessThan (coerceList Double Any xs))

8
Double/sum.dhall Normal file
View file

@ -0,0 +1,8 @@
λ(nix : ../NixPrelude.dhall) →
let Double/add = ./add.dhall nix
let sum
: List Double → Double
= λ(xs : List Double) → List/fold Double xs Double Double/add 0.0
in sum

26
Integer/build.dhall Normal file
View file

@ -0,0 +1,26 @@
let Integer/add = ./add.dhall
let negate = ./negate.dhall
let Integer/succ
: Integer → Integer
= λ(n : Integer) → Integer/add n +1
let build
: ( ∀(integer : Type) →
∀(succ : integer → integer) →
∀(negate : integer → integer) →
∀(zero : integer) →
integer
) →
Integer
= λ ( builder
: ∀(integer : Type) →
∀(succ : integer → integer) →
∀(negate : integer → integer) →
∀(zero : integer) →
integer
) →
builder Integer Integer/succ negate +0
in build

21
Integer/fold.dhall Normal file
View file

@ -0,0 +1,21 @@
let Integer/negative = ./negative.dhall
let Integer/abs = ./abs.dhall
let fold
: Integer →
∀(integer : Type) →
∀(succ : integer → integer) →
∀(negate : integer → integer) →
∀(zero : integer) →
integer
= λ(e : Integer) →
λ(integer : Type) →
λ(succ : integer → integer) →
λ(negate : integer → integer) →
λ(zero : integer) →
let folded = Natural/fold (Integer/abs e) integer succ zero
in if Integer/negative e then negate folded else folded
in fold

View file

@ -8,4 +8,4 @@
in λ(v : Any) → in λ(v : Any) →
if nix.builtins.isInt v if nix.builtins.isInt v
then Any/toTypeUnchecked Integer v then Any/toTypeUnchecked Integer v
else Misc/throw Integer "Failed to coerce object into Double" else Misc/throw Integer "Failed to coerce object into Integer"

13
Integer/isZero.dhall Normal file
View file

@ -0,0 +1,13 @@
let Integer/nonPositive = ./nonPositive.dhall
let Integer/nonNegative = ./nonNegative.dhall
let isZero
: Integer → Bool
= λ(v : Integer) → Integer/nonPositive v && Integer/nonNegative v
let example0 = assert : isZero +2 ≡ False
let example1 = assert : isZero +0 ≡ True
in isZero

15
Integer/listMax.dhall Normal file
View file

@ -0,0 +1,15 @@
λ(nix : ../NixPrelude.dhall) →
let max = ./max.dhall
let Optional/map = ../Optional/map.dhall nix
let listMax
: List Integer → Optional Integer
= λ(xs : List Integer) →
Optional/map
Integer
Integer
(λ(n : Integer) → List/fold Integer xs Integer max n)
(List/head Integer xs)
in listMax

21
Integer/listMin.dhall Normal file
View file

@ -0,0 +1,21 @@
λ(nix : ../NixPrelude.dhall) →
let min = ./min.dhall
let Integer/isZero = ./isZero.dhall
let Optional/map = ../Optional/map.dhall nix
let listMin
: List Integer → Optional Integer
= λ(xs : List Integer) →
Optional/map
Integer
Integer
( λ(n : Integer) →
if Integer/isZero n
then n
else List/fold Integer xs Integer min n
)
(List/head Integer xs)
in listMin

14
Integer/max.dhall Normal file
View file

@ -0,0 +1,14 @@
--| `max a b` returns the larger of `a` or `b`
let lessThanEqual = ./lessThanEqual.dhall
let max
: Integer → Integer → Integer
= λ(a : Integer) → λ(b : Integer) → 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 : Integer) → assert : max n n ≡ n
in max

14
Integer/min.dhall Normal file
View file

@ -0,0 +1,14 @@
--| `min a b` returns the smaller of `a` or `b`
let lessThanEqual = ./lessThanEqual.dhall
let min
: Integer → Integer → Integer
= λ(a : Integer) → λ(b : Integer) → 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 : Integer) → assert : min n n ≡ n
in min

View file

@ -2,22 +2,32 @@
{ Type = Integer { Type = Integer
, abs = ./abs.dhall , abs = ./abs.dhall
, add = ./add.dhall , add = ./add.dhall
, build = ./build.dhall
, clamp = ./clamp.dhall , clamp = ./clamp.dhall
, divide = ./divide.dhall nix , divide = ./divide.dhall nix
, equal = ./equal.dhall , equal = ./equal.dhall
, fold = ./fold.dhall
, fromAny = ./fromAny.dhall nix , fromAny = ./fromAny.dhall nix
, greaterThan = ./greaterThan.dhall , greaterThan = ./greaterThan.dhall
, greaterThanEqual = ./greaterThanEqual.dhall , greaterThanEqual = ./greaterThanEqual.dhall
, isZero = ./isZero.dhall
, lessThan = ./lessThan.dhall , lessThan = ./lessThan.dhall
, lessThanEqual = ./lessThanEqual.dhall , lessThanEqual = ./lessThanEqual.dhall
, listMax = ./listMax.dhall nix
, listMin = ./listMin.dhall nix
, max = ./max.dhall
, min = ./min.dhall
, multiply = ./multiply.dhall , multiply = ./multiply.dhall
, negate = ./negate.dhall , negate = ./negate.dhall
, negative = ./negative.dhall , negative = ./negative.dhall
, nonNegative = ./nonNegative.dhall , nonNegative = ./nonNegative.dhall
, nonPositive = ./nonPositive.dhall , nonPositive = ./nonPositive.dhall
, positive = ./positive.dhall , positive = ./positive.dhall
, product = ./product.dhall
, show = ./show.dhall , show = ./show.dhall
, sort = ./sort.dhall
, subtract = ./subtract.dhall , subtract = ./subtract.dhall
, sum = ./sum.dhall
, toDouble = ./toDouble.dhall , toDouble = ./toDouble.dhall
, toNatural = ./toNatural.dhall , toNatural = ./toNatural.dhall
} }

14
Integer/product.dhall Normal file
View file

@ -0,0 +1,14 @@
--| Multiply all the numbers in a `List`
let Integer/multiply = ./multiply.dhall
let product
: List Integer → Integer
= λ(xs : List Integer) → List/fold Integer xs Integer Integer/multiply +1
let example0 = assert : product [ +2, +3, +5 ] ≡ +30
let example1 = assert : product ([] : List Integer) ≡ +1
let example2 = assert : product [ -2, +3, +5 ] ≡ -30
in product

21
Integer/sort.dhall Normal file
View file

@ -0,0 +1,21 @@
--| `sort` sorts a `List` of `Integer`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 Integer) →
coerceList
Any
Integer
(nix.builtins.sort Any/lessThan (coerceList Integer Any xs))

11
Integer/sum.dhall Normal file
View file

@ -0,0 +1,11 @@
let Integer/add = ./add.dhall
let sum
: List Integer → Integer
= λ(xs : List Integer) → List/fold Integer xs Integer Integer/add +0
let example = assert : sum [ +2, +3, +5 ] ≡ +10
let example = assert : sum ([] : List Integer) ≡ +0
in sum

15
Natural/fromAny.dhall Normal file
View file

@ -0,0 +1,15 @@
λ(nix : ../NixPrelude.dhall) →
let Any = ../Any/Type.dhall
let Integer/nonNegative = ../Integer/nonNegative.dhall
let Misc/throw = ../Misc/throw.dhall nix
let Integer/fromAny = ../Integer/fromAny.dhall nix
in λ(v : Any) →
let int = Integer/fromAny v
in if Integer/nonNegative int
then Integer/clamp int
else Misc/throw Natural "Failed to coerce object into Natural"

View file

@ -23,4 +23,5 @@
, listMax = ./listMax.dhall nix , listMax = ./listMax.dhall nix
, sort = ./sort.dhall nix , sort = ./sort.dhall nix
, subtract = ./subtract.dhall , subtract = ./subtract.dhall
, fromAny = ./fromAny.dhall nix
} }

14
Number/abs.dhall Normal file
View file

@ -0,0 +1,14 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let isZero = ./isZero.dhall nix
let clamp = ./clamp.dhall nix
let negate = ./negate.dhall nix
let abs
: Number → Number
= λ(n : Number) → if isZero (clamp n) then clamp (negate n) else clamp n
in abs

25
Number/build.dhall Normal file
View file

@ -0,0 +1,25 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let add = ./add.dhall nix
let negate = ./negate.dhall nix
let divide = ./divide.dhall nix
let fromNatural = ./fromNatural.dhall nix
let succ = λ(n : Number) → add n (fromNatural 1)
let build =
λ ( builder
: ∀(number : Type) →
(number → number) →
(number → number) →
(number → number → number) →
number →
number
) →
builder Number succ negate divide (fromNatural 0)
in build

12
Number/isZero.dhall Normal file
View file

@ -0,0 +1,12 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let nonPositive = ./nonPositive.dhall nix
let nonNegative = ./nonNegative.dhall nix
let isZero
: Number → Bool
= λ(v : Number) → nonPositive v && nonNegative v
in isZero

17
Number/listMax.dhall Normal file
View file

@ -0,0 +1,17 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let max = ./max.dhall nix
let Optional/map = ../Optional/map.dhall nix
let listMax
: List Number → Optional Number
= λ(xs : List Number) →
Optional/map
Number
Number
(λ(n : Number) → List/fold Number xs Number max n)
(List/head Number xs)
in listMax

21
Number/listMin.dhall Normal file
View file

@ -0,0 +1,21 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let min = ./min.dhall nix
let Number/isZero = ./isZero.dhall nix
let Optional/map = ../Optional/map.dhall nix
let listMin
: List Number → Optional Number
= λ(xs : List Number) →
Optional/map
Number
Number
( λ(n : Number) →
if Number/isZero n then n else List/fold Number xs Number min n
)
(List/head Number xs)
in listMin

10
Number/max.dhall Normal file
View file

@ -0,0 +1,10 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let lessThanEqual = ./lessThanEqual.dhall nix
let max
: Number → Number → Number
= λ(a : Number) → λ(b : Number) → if lessThanEqual a b then b else a
in max

10
Number/min.dhall Normal file
View file

@ -0,0 +1,10 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let lessThanEqual = ./lessThanEqual.dhall nix
let min
: Number → Number → Number
= λ(a : Number) → λ(b : Number) → if lessThanEqual a b then a else b
in min

View file

@ -1,6 +1,8 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) →
{ Type = ./Type.dhall { Type = ./Type.dhall
, abs = ./abs.dhall nix
, add = ./add.dhall nix , add = ./add.dhall nix
, build = ./build.dhall
, clamp = ./clamp.dhall nix , clamp = ./clamp.dhall nix
, divide = ./divide.dhall nix , divide = ./divide.dhall nix
, equal = ./equal.dhall nix , equal = ./equal.dhall nix
@ -10,16 +12,24 @@
, fromNatural = ./fromNatural.dhall nix , fromNatural = ./fromNatural.dhall nix
, greaterThan = ./greaterThan.dhall nix , greaterThan = ./greaterThan.dhall nix
, greaterThanEqual = ./greaterThanEqual.dhall nix , greaterThanEqual = ./greaterThanEqual.dhall nix
, isZero = ./isZero.dhall nix
, lessThan = ./lessThan.dhall nix , lessThan = ./lessThan.dhall nix
, lessThanEqual = ./lessThanEqual.dhall nix , lessThanEqual = ./lessThanEqual.dhall nix
, listMax = ./listMax.dhall nix
, listMin = ./listMin.dhall nix
, max = ./max.dhall nix
, min = ./min.dhall nix
, multiply = ./multiply.dhall nix , multiply = ./multiply.dhall nix
, negate = ./negate.dhall nix , negate = ./negate.dhall nix
, negative = ./negative.dhall nix , negative = ./negative.dhall nix
, nonNegative = ./nonNegative.dhall nix , nonNegative = ./nonNegative.dhall nix
, nonPositive = ./nonPositive.dhall nix , nonPositive = ./nonPositive.dhall nix
, positive = ./positive.dhall nix , positive = ./positive.dhall nix
, product = ./product.dhall nix
, show = ./show.dhall nix , show = ./show.dhall nix
, sort = ./sort.dhall nix
, subtract = ./subtract.dhall nix , subtract = ./subtract.dhall nix
, sum = ./sum.dhall nix
, toDouble = ./toDouble.dhall nix , toDouble = ./toDouble.dhall nix
, toInteger = ./toInteger.dhall nix , toInteger = ./toInteger.dhall nix
, toNatural = ./toNatural.dhall nix , toNatural = ./toNatural.dhall nix

13
Number/product.dhall Normal file
View file

@ -0,0 +1,13 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let Number/multiply = ./multiply.dhall nix
let fromNatural = ./fromNatural.dhall nix
let product
: List Number → Number
= λ(xs : List Number) →
List/fold Number xs Number Number/multiply (fromNatural 1)
in product

23
Number/sort.dhall Normal file
View file

@ -0,0 +1,23 @@
--| `sort` sorts a `List` of `Number`s in ascending order
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.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 Number) →
coerceList
Any
Number
(nix.builtins.sort Any/lessThan (coerceList Number Any xs))

13
Number/sum.dhall Normal file
View file

@ -0,0 +1,13 @@
λ(nix : ../NixPrelude.dhall) →
let Number = ./Type.dhall
let Number/add = ./add.dhall nix
let fromNatural = ./fromNatural.dhall nix
let sum
: List Number → Number
= λ(xs : List Number) →
List/fold Number xs Number Number/add (fromNatural 0)
in sum