Port trivial.nix
This commit is contained in:
parent
c5e01bdce3
commit
f3b636b485
48 changed files with 683 additions and 24 deletions
38
Any/isFunction.dhall
Normal file
38
Any/isFunction.dhall
Normal file
|
@ -0,0 +1,38 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Optional/fold =
|
||||
https://prelude.dhall-lang.org/Optional/fold.dhall
|
||||
sha256:c5b9d72f6f62bdaa0e196ac1c742cc175cd67a717b880fb8aec1333a5a4132cf
|
||||
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let Any/selectOptional = ../Any/selectOptional.dhall nix
|
||||
|
||||
let FunctionType = λ(x : Type) → x → Any → Bool
|
||||
|
||||
let function =
|
||||
λ(function : FunctionType Any) →
|
||||
let functionArgs =
|
||||
Any/toTypeUnchecked
|
||||
(FunctionType (FunctionType Any))
|
||||
(Any/toAny (FunctionType Any) function)
|
||||
function
|
||||
|
||||
in λ(v : Any) →
|
||||
nix.builtins.isFunction v
|
||||
|| Optional/fold
|
||||
Any
|
||||
(Any/selectOptional v "__functor")
|
||||
Bool
|
||||
(λ(v : Any) → functionArgs v)
|
||||
False
|
||||
|
||||
let functionErased =
|
||||
Any/toTypeUnchecked
|
||||
(FunctionType Any)
|
||||
(Any/toAny (FunctionType (FunctionType Any)) function)
|
||||
|
||||
in function functionErased
|
|
@ -7,6 +7,7 @@
|
|||
, apply = ./apply.dhall nix
|
||||
, negate = ./negate.dhall nix
|
||||
, hasAttr = ./hasAttr.dhall nix
|
||||
, isFunction = ./isFunction.dhall nix
|
||||
, listConcat = ./listConcat.dhall nix
|
||||
, multiply = ./multiply.dhall nix
|
||||
, divide = ./divide.dhall nix
|
||||
|
@ -24,4 +25,5 @@
|
|||
, land = ./land.dhall nix
|
||||
, lor = ./lor.dhall nix
|
||||
, impl = ./impl.dhall nix
|
||||
, toFunction = ./toFunction.dhall nix
|
||||
}
|
||||
|
|
17
Any/toFunction.dhall
Normal file
17
Any/toFunction.dhall
Normal file
|
@ -0,0 +1,17 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ./Type.dhall
|
||||
|
||||
let Function/const = ../Function/const.dhall
|
||||
|
||||
let isFunction = ./isFunction.dhall nix
|
||||
|
||||
let toTypeUnchecked = ./toTypeUnchecked.dhall nix
|
||||
|
||||
let toFunction
|
||||
: Any → Any → Any
|
||||
= λ(v : Any) →
|
||||
if isFunction v
|
||||
then toTypeUnchecked (Any → Any) v
|
||||
else Function/const Any v Any
|
||||
|
||||
in toFunction
|
12
Double/compare.dhall
Normal file
12
Double/compare.dhall
Normal file
|
@ -0,0 +1,12 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let lessThan = ./lessThan.dhall nix
|
||||
|
||||
let greaterThan = ./greaterThan.dhall nix
|
||||
|
||||
let compare
|
||||
: Double → Double → Integer
|
||||
= λ(a : Double) →
|
||||
λ(b : Double) →
|
||||
if lessThan a b then -1 else if greaterThan a b then +1 else +0
|
||||
|
||||
in compare
|
|
@ -4,6 +4,7 @@
|
|||
, add = ./add.dhall nix
|
||||
, build = ./build.dhall nix
|
||||
, clamp = ./clamp.dhall nix
|
||||
, compare = ./compare.dhall nix
|
||||
, divide = ./divide.dhall nix
|
||||
, equal = ./equal.dhall nix
|
||||
, fromAny = ./fromAny.dhall nix
|
||||
|
|
7
Function/const.dhall
Normal file
7
Function/const.dhall
Normal file
|
@ -0,0 +1,7 @@
|
|||
let const
|
||||
: ∀(A : Type) → A → ∀(B : Type) → B → A
|
||||
= λ(A : Type) → λ(a : A) → λ(B : Type) → λ(_ : B) → a
|
||||
|
||||
let example1 = assert : const Natural 5 Natural 10 ≡ 5
|
||||
|
||||
in const
|
7
Function/deepSeq.dhall
Normal file
7
Function/deepSeq.dhall
Normal file
|
@ -0,0 +1,7 @@
|
|||
λ(nix: ../NixPrelude.dhall) →
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
let seq : ∀(A: Type) → ∀(B: Type) → A → B → B
|
||||
= λ(A: Type) → λ(B: Type) → λ(a: A) → λ(b: B) → Any/toTypeUnchecked B (nix.builtins.deepSeq (Any/toAny A a) (Any/toAny B b))
|
||||
in seq
|
||||
|
15
Function/flip.dhall
Normal file
15
Function/flip.dhall
Normal file
|
@ -0,0 +1,15 @@
|
|||
let flip
|
||||
: ∀(A : Type) → ∀(B : Type) → ∀(C : Type) → (B → A → C) → A → B → C
|
||||
= λ(A : Type) →
|
||||
λ(B : Type) →
|
||||
λ(C : Type) →
|
||||
λ(f : B → A → C) →
|
||||
λ(a : A) →
|
||||
λ(b : B) →
|
||||
f b a
|
||||
|
||||
let example1 =
|
||||
assert
|
||||
: flip Text Text Text (λ(a : Text) → λ(b : Text) → a ++ b) "a" "b" ≡ "ba"
|
||||
|
||||
in flip
|
55
Function/functionArgs.dhall
Normal file
55
Function/functionArgs.dhall
Normal file
|
@ -0,0 +1,55 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Set = ../Set/Type.dhall
|
||||
|
||||
let Optional/fold =
|
||||
https://prelude.dhall-lang.org/Optional/fold.dhall
|
||||
sha256:c5b9d72f6f62bdaa0e196ac1c742cc175cd67a717b880fb8aec1333a5a4132cf
|
||||
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/hasAttr = ../Any/hasAttr.dhall nix
|
||||
|
||||
let Any/select = ../Any/select.dhall nix
|
||||
|
||||
let Any/selectOptional = ../Any/selectOptional.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let FunctionType = λ(x : Type) → x → ∀(a : Type) → ∀(b : Type) → (a → b) → Set
|
||||
|
||||
let function =
|
||||
λ(function : FunctionType Any) →
|
||||
let functionArgs =
|
||||
Any/toTypeUnchecked
|
||||
(FunctionType (FunctionType Any))
|
||||
(Any/toAny (FunctionType Any) function)
|
||||
function
|
||||
|
||||
in λ(a : Type) →
|
||||
λ(b : Type) →
|
||||
λ(f : a → b) →
|
||||
let fAny = Any/toAny (a → b) f
|
||||
|
||||
let functor =
|
||||
Any/toTypeUnchecked (a → b) (Any/select fAny "__functor")
|
||||
|
||||
let functorArg =
|
||||
Optional/fold
|
||||
Any
|
||||
(Any/selectOptional fAny "__functionArgs")
|
||||
Set
|
||||
(Any/toTypeUnchecked Set)
|
||||
(functionArgs a b functor)
|
||||
|
||||
in if Any/hasAttr fAny "__functor"
|
||||
then functorArg
|
||||
else nix.builtins.functionArgs (Any/toAny (a → b) f)
|
||||
|
||||
let functionErased =
|
||||
Any/toTypeUnchecked
|
||||
(FunctionType Any)
|
||||
(Any/toAny (FunctionType (FunctionType Any)) function)
|
||||
|
||||
in function functionErased
|
10
Function/package.dhall
Normal file
10
Function/package.dhall
Normal file
|
@ -0,0 +1,10 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ const = ./const.dhall
|
||||
, deepSeq = ./seq.dhall nix
|
||||
, flip = ./flip.dhall
|
||||
, functionArgs = ./functionArgs.dhall nix
|
||||
, pipe = ./pipe.dhall
|
||||
, setFunctionArgs = ./setFunctionArgs.dhall nix
|
||||
, seq = ./seq.dhall nix
|
||||
, splitAndCompare = ./splitAndCompare.dhall
|
||||
}
|
16
Function/pipe.dhall
Normal file
16
Function/pipe.dhall
Normal file
|
@ -0,0 +1,16 @@
|
|||
let List/foldLeft =
|
||||
https://prelude.dhall-lang.org/List/foldLeft.dhall
|
||||
sha256:3c6ab57950fe644906b7bbdef0b9523440b6ee17773ebb8cbd41ffacb8bfab61
|
||||
|
||||
let pipe
|
||||
: ∀(a : Type) → a → List (a → a) → a
|
||||
= λ(a : Type) →
|
||||
λ(v : a) →
|
||||
λ(fns : List (a → a)) →
|
||||
List/foldLeft (a → a) fns a (λ(v : a) → λ(f : a → a) → f v) v
|
||||
|
||||
let example =
|
||||
assert
|
||||
: pipe Natural 2 [ λ(x : Natural) → x + 2, λ(x : Natural) → x * 2 ] ≡ 8
|
||||
|
||||
in pipe
|
16
Function/seq.dhall
Normal file
16
Function/seq.dhall
Normal file
|
@ -0,0 +1,16 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let seq
|
||||
: ∀(A : Type) → ∀(B : Type) → A → B → B
|
||||
= λ(A : Type) →
|
||||
λ(B : Type) →
|
||||
λ(a : A) →
|
||||
λ(b : B) →
|
||||
Any/toTypeUnchecked
|
||||
B
|
||||
(nix.builtins.seq (Any/toAny A a) (Any/toAny B b))
|
||||
|
||||
in seq
|
31
Function/setFunctionArgs.dhall
Normal file
31
Function/setFunctionArgs.dhall
Normal file
|
@ -0,0 +1,31 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Map =
|
||||
https://prelude.dhall-lang.org/Map/Type.dhall
|
||||
sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed
|
||||
|
||||
let Set = ../Set/Type.dhall
|
||||
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let Set/toSet = ../Set/toSet.dhall nix
|
||||
|
||||
let setFunctionArgs
|
||||
: ∀(A : Type) → ∀(B : Type) → (A → B) → Map Text Bool → A → B
|
||||
= λ(A : Type) →
|
||||
λ(B : Type) →
|
||||
λ(f : A → B) →
|
||||
λ(args : Map Text Bool) →
|
||||
Any/toTypeUnchecked
|
||||
(A → B)
|
||||
( Any/toAny
|
||||
{ __functor : Any → A → B, __functionArgs : Set }
|
||||
{ __functor = λ(_ : Any) → f
|
||||
, __functionArgs = Set/toSet Bool args
|
||||
}
|
||||
)
|
||||
|
||||
in setFunctionArgs
|
17
Function/splitAndCompare.dhall
Normal file
17
Function/splitAndCompare.dhall
Normal file
|
@ -0,0 +1,17 @@
|
|||
let splitAndCompare
|
||||
: ∀(a : Type) →
|
||||
(a → Bool) →
|
||||
(a → a → Integer) →
|
||||
(a → a → Integer) →
|
||||
a →
|
||||
a →
|
||||
Integer
|
||||
= λ(t : Type) →
|
||||
λ(p : t → Bool) →
|
||||
λ(yes : t → t → Integer) →
|
||||
λ(no : t → t → Integer) →
|
||||
λ(a : t) →
|
||||
λ(b : t) →
|
||||
if p a then if p b then yes a b else -1 else if p b then +1 else no a b
|
||||
|
||||
in splitAndCompare
|
15
Integer/compare.dhall
Normal file
15
Integer/compare.dhall
Normal file
|
@ -0,0 +1,15 @@
|
|||
let lessThan =
|
||||
https://prelude.dhall-lang.org/Integer/lessThan.dhall
|
||||
sha256:eeaa0081d10c6c97464ef193c40f1aa5cbb12f0202972ab42f3d310c2fd6a3f0
|
||||
|
||||
let greaterThan =
|
||||
https://prelude.dhall-lang.org/Integer/greaterThan.dhall
|
||||
sha256:d23affd73029fc9aaf867c2c7b86510ca2802d3f0d1f3e1d1a93ffd87b7cb64b
|
||||
|
||||
let compare
|
||||
: Integer → Integer → Integer
|
||||
= λ(a : Integer) →
|
||||
λ(b : Integer) →
|
||||
if lessThan a b then -1 else if greaterThan a b then +1 else +0
|
||||
|
||||
in compare
|
|
@ -1,6 +1,7 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ Type = Integer
|
||||
, build = ./build.dhall
|
||||
, compare = ./compare.dhall
|
||||
, divide = ./divide.dhall nix
|
||||
, fold = ./fold.dhall
|
||||
, fromAny = ./fromAny.dhall nix
|
||||
|
|
|
@ -1,17 +1,16 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let List/concatMap =
|
||||
let List/concatMap =
|
||||
https://prelude.dhall-lang.org/List/concatMap.dhall
|
||||
sha256:3b2167061d11fda1e4f6de0522cbe83e0d5ac4ef5ddf6bb0b2064470c5d3fb64
|
||||
|
||||
let Optional/toList =
|
||||
let Optional/toList =
|
||||
https://prelude.dhall-lang.org/Optional/toList.dhall
|
||||
sha256:d78f160c619119ef12389e48a629ce293d69f7624c8d016b7a4767ab400344c4
|
||||
|
||||
let filterMap
|
||||
let filterMap
|
||||
: ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b
|
||||
= λ(a : Type) →
|
||||
λ(b : Type) →
|
||||
λ(f : a → Optional b) →
|
||||
List/concatMap a b (λ(x : a) → Optional/toList b (f x))
|
||||
|
||||
in filterMap
|
||||
in filterMap
|
||||
|
|
|
@ -1 +1,4 @@
|
|||
λ(nix : ../NixPrelude.dhall) → { filterMap = ./filterMap.dhall }
|
||||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ -- TODO: checkListOfEnum
|
||||
filterMap = ./filterMap.dhall
|
||||
}
|
||||
|
|
18
Misc/info.dhall
Normal file
18
Misc/info.dhall
Normal file
|
@ -0,0 +1,18 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let info
|
||||
: Text → ∀(a : Type) → a → a
|
||||
= λ(text : Text) →
|
||||
λ(a : Type) →
|
||||
λ(v : a) →
|
||||
Any/toTypeUnchecked
|
||||
a
|
||||
( nix.builtins.trace
|
||||
(Any/toAny Text "INFO: ${text}")
|
||||
(Any/toAny a v)
|
||||
)
|
||||
|
||||
in info
|
|
@ -1 +1,10 @@
|
|||
λ(nix : ../NixPrelude.dhall) → { throw = ./throw.dhall nix }
|
||||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ info = ./info.dhall nix
|
||||
, showWarnings = ./showWarnings.dhall nix
|
||||
, throw = ./throw.dhall nix
|
||||
, throwIf = ./throwIf.dhall nix
|
||||
, throwIfNot = ./throwIfNot.dhall nix
|
||||
, warn = ./warn.dhall nix
|
||||
, warnIf = ./warnIf.dhall nix
|
||||
, warnIfNot = ./warnIfNot.dhall nix
|
||||
}
|
||||
|
|
10
Misc/showWarnings.dhall
Normal file
10
Misc/showWarnings.dhall
Normal file
|
@ -0,0 +1,10 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let warn = ./warn.dhall nix
|
||||
|
||||
let showWarnings
|
||||
: List Text → ∀(a : Type) → a → a
|
||||
= λ(warnings : List Text) →
|
||||
λ(a : Type) →
|
||||
List/fold Text warnings a (λ(text : Text) → λ(v : a) → warn text a v)
|
||||
|
||||
in showWarnings
|
15
Misc/throwIf.dhall
Normal file
15
Misc/throwIf.dhall
Normal file
|
@ -0,0 +1,15 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Function/identity =
|
||||
https://prelude.dhall-lang.org/Function/identity.dhall
|
||||
sha256:f78b96792b459cb664f41c6119bd8897dd04353a3343521d436cd82ad71cb4d4
|
||||
|
||||
let throw = ./throw.dhall nix
|
||||
|
||||
let throwIf
|
||||
: Bool → Text → ∀(a : Type) → a → a
|
||||
= λ(cond : Bool) →
|
||||
if cond
|
||||
then λ(message : Text) → λ(a : Type) → λ(_ : a) → throw a message
|
||||
else λ(msg : Text) → Function/identity
|
||||
|
||||
in throwIf
|
12
Misc/throwIfNot.dhall
Normal file
12
Misc/throwIfNot.dhall
Normal file
|
@ -0,0 +1,12 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Bool/not =
|
||||
https://prelude.dhall-lang.org/Bool/not.dhall
|
||||
sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
|
||||
|
||||
let throwIf = ./throwIf.dhall nix
|
||||
|
||||
let throwIfNot
|
||||
: Bool → Text → ∀(a : Type) → a → a
|
||||
= λ(cond : Bool) → throwIf (Bool/not cond)
|
||||
|
||||
in throwIfNot
|
18
Misc/warn.dhall
Normal file
18
Misc/warn.dhall
Normal file
|
@ -0,0 +1,18 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let warn
|
||||
: Text → ∀(a : Type) → a → a
|
||||
= λ(text : Text) →
|
||||
λ(a : Type) →
|
||||
λ(v : a) →
|
||||
Any/toTypeUnchecked
|
||||
a
|
||||
( nix.builtins.trace
|
||||
(Any/toAny Text "\u001B[1;31mwarning: ${text}\u001B[0m")
|
||||
(Any/toAny a v)
|
||||
)
|
||||
|
||||
in warn
|
13
Misc/warnIf.dhall
Normal file
13
Misc/warnIf.dhall
Normal file
|
@ -0,0 +1,13 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Function/identity =
|
||||
https://prelude.dhall-lang.org/Function/identity.dhall
|
||||
sha256:f78b96792b459cb664f41c6119bd8897dd04353a3343521d436cd82ad71cb4d4
|
||||
|
||||
let warn = ./warn.dhall nix
|
||||
|
||||
let warnIf
|
||||
: Bool → Text → ∀(a : Type) → a → a
|
||||
= λ(cond : Bool) →
|
||||
if cond then warn else λ(msg : Text) → Function/identity
|
||||
|
||||
in warnIf
|
12
Misc/warnIfNot.dhall
Normal file
12
Misc/warnIfNot.dhall
Normal file
|
@ -0,0 +1,12 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Bool/not =
|
||||
https://prelude.dhall-lang.org/Bool/not.dhall
|
||||
sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
|
||||
|
||||
let warnIf = ./warnIf.dhall nix
|
||||
|
||||
let warnIfNot
|
||||
: Bool → Text → ∀(a : Type) → a → a
|
||||
= λ(cond : Bool) → warnIf (Bool/not cond)
|
||||
|
||||
in warnIfNot
|
6
Natural/bitAnd.dhall
Normal file
6
Natural/bitAnd.dhall
Normal file
|
@ -0,0 +1,6 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let bitAnd
|
||||
: Natural → Natural → Natural
|
||||
= nix.builtins.bitAnd
|
||||
|
||||
in bitAnd
|
6
Natural/bitOr.dhall
Normal file
6
Natural/bitOr.dhall
Normal file
|
@ -0,0 +1,6 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let bitOr
|
||||
: Natural → Natural → Natural
|
||||
= nix.builtins.bitOr
|
||||
|
||||
in bitOr
|
6
Natural/bitXor.dhall
Normal file
6
Natural/bitXor.dhall
Normal file
|
@ -0,0 +1,6 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let bitXor
|
||||
: Natural → Natural → Natural
|
||||
= nix.builtins.bitXor
|
||||
|
||||
in bitXor
|
15
Natural/compare.dhall
Normal file
15
Natural/compare.dhall
Normal file
|
@ -0,0 +1,15 @@
|
|||
let lessThan =
|
||||
https://prelude.dhall-lang.org/Natural/lessThan.dhall
|
||||
sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c
|
||||
|
||||
let greaterThan =
|
||||
https://prelude.dhall-lang.org/Natural/greaterThan.dhall
|
||||
sha256:f702abcdfcd7ad73619b9285d7e41c3a1d017fb6b8d037cf40bd93bf30c09b2c
|
||||
|
||||
let compare
|
||||
: Natural → Natural → Integer
|
||||
= λ(a : Natural) →
|
||||
λ(b : Natural) →
|
||||
if lessThan a b then -1 else if greaterThan a b then +1 else +0
|
||||
|
||||
in compare
|
10
Natural/mod.dhall
Normal file
10
Natural/mod.dhall
Normal file
|
@ -0,0 +1,10 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Natural/divide = ./divide.dhall nix
|
||||
|
||||
let mod
|
||||
: Natural → Natural → Natural
|
||||
= λ(base : Natural) →
|
||||
λ(int : Natural) →
|
||||
Natural/subtract base (int * Natural/divide base int)
|
||||
|
||||
in mod
|
|
@ -1,2 +1,12 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ Type = Natural, divide = ./divide.dhall nix, fromAny = ./fromAny.dhall nix }
|
||||
{ Type = Natural
|
||||
, bitAnd = ./bitAnd.dhall nix
|
||||
, bitOr = ./bitOr.dhall nix
|
||||
, bitXor = ./bitXor.dhall nix
|
||||
, compare = ./compare.dhall
|
||||
, divide = ./divide.dhall nix
|
||||
, fromAny = ./fromAny.dhall nix
|
||||
, mod = ./mod.dhall nix
|
||||
, toBaseDigits = ./toBaseDigits.dhall nix
|
||||
, toHexString = ./toHexString.dhall nix
|
||||
}
|
||||
|
|
60
Natural/toBaseDigits.dhall
Normal file
60
Natural/toBaseDigits.dhall
Normal file
|
@ -0,0 +1,60 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let lessThan =
|
||||
https://prelude.dhall-lang.org/Natural/lessThan.dhall
|
||||
sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c
|
||||
|
||||
let greaterThanEqual =
|
||||
https://prelude.dhall-lang.org/Natural/greaterThanEqual.dhall
|
||||
sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4
|
||||
|
||||
let subtract =
|
||||
https://prelude.dhall-lang.org/Natural/subtract.dhall
|
||||
sha256:b9277ac637d09142a3a3ac79137ef5955c42f8b33b6746d59db2c9d75ccdd745
|
||||
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let divide = ./divide.dhall nix
|
||||
|
||||
let throwIfNot = ../Misc/throwIfNot.dhall nix
|
||||
|
||||
let toBaseDigits
|
||||
: Natural → Natural → List Natural
|
||||
= λ(base : Natural) →
|
||||
λ(i : Natural) →
|
||||
let FunctionType = λ(x : Type) → x → Natural → List Natural
|
||||
|
||||
let function =
|
||||
λ(function : FunctionType Any) →
|
||||
let functionArgs =
|
||||
Any/toTypeUnchecked
|
||||
(FunctionType (FunctionType Any))
|
||||
(Any/toAny (FunctionType Any) function)
|
||||
function
|
||||
|
||||
in λ(i : Natural) →
|
||||
if lessThan i base
|
||||
then [ i ]
|
||||
else let r = subtract i (divide i base * base)
|
||||
|
||||
let q = divide (subtract i r) base
|
||||
|
||||
in [ r ] # functionArgs q
|
||||
|
||||
let functionErased =
|
||||
Any/toTypeUnchecked
|
||||
(FunctionType Any)
|
||||
(Any/toAny (FunctionType (FunctionType Any)) function)
|
||||
|
||||
let go = function functionErased
|
||||
|
||||
in throwIfNot
|
||||
(greaterThanEqual base 2)
|
||||
"Base must be 2 or greater"
|
||||
(List Natural)
|
||||
(List/reverse Natural (go i))
|
||||
|
||||
in toBaseDigits
|
44
Natural/toHexString.dhall
Normal file
44
Natural/toHexString.dhall
Normal file
|
@ -0,0 +1,44 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let List/index =
|
||||
https://prelude.dhall-lang.org/List/index.dhall
|
||||
sha256:e657b55ecae4d899465c3032cb1a64c6aa6dc2aa3034204f3c15ce5c96c03e63
|
||||
|
||||
let Optional/default =
|
||||
https://prelude.dhall-lang.org/Optional/default.dhall
|
||||
sha256:5bd665b0d6605c374b3c4a7e2e2bd3b9c1e39323d41441149ed5e30d86e889ad
|
||||
|
||||
let toBaseDigits = ./toBaseDigits.dhall nix
|
||||
|
||||
let hexDigits =
|
||||
[ "0"
|
||||
, "1"
|
||||
, "2"
|
||||
, "3"
|
||||
, "4"
|
||||
, "5"
|
||||
, "6"
|
||||
, "7"
|
||||
, "8"
|
||||
, "9"
|
||||
, "A"
|
||||
, "B"
|
||||
, "C"
|
||||
, "D"
|
||||
, "E"
|
||||
, "F"
|
||||
]
|
||||
|
||||
let getHexDigit =
|
||||
λ(n : Natural) → Optional/default Text "" (List/index n Text hexDigits)
|
||||
|
||||
let toHexString
|
||||
: Natural → Text
|
||||
= λ(v : Natural) →
|
||||
List/fold
|
||||
Natural
|
||||
(toBaseDigits 16 v)
|
||||
Text
|
||||
(λ(v : Natural) → λ(s : Text) → getHexDigit v ++ s)
|
||||
""
|
||||
|
||||
in toHexString
|
14
Number/compare.dhall
Normal file
14
Number/compare.dhall
Normal file
|
@ -0,0 +1,14 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Number = ./Type.dhall
|
||||
|
||||
let lessThan = ./lessThan.dhall nix
|
||||
|
||||
let greaterThan = ./greaterThan.dhall nix
|
||||
|
||||
let compare
|
||||
: Number → Number → Integer
|
||||
= λ(a : Number) →
|
||||
λ(b : Number) →
|
||||
if lessThan a b then -1 else if greaterThan a b then +1 else +0
|
||||
|
||||
in compare
|
|
@ -4,6 +4,7 @@
|
|||
, add = ./add.dhall nix
|
||||
, build = ./build.dhall nix
|
||||
, clamp = ./clamp.dhall nix
|
||||
, compare = ./compare.dhall nix
|
||||
, divide = ./divide.dhall nix
|
||||
, equal = ./equal.dhall nix
|
||||
, fromAny = ./fromAny.dhall nix
|
||||
|
|
|
@ -1,10 +1,6 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Number = ./Type.dhall
|
||||
|
||||
let Integer/toNatural =
|
||||
https://prelude.dhall-lang.org/Integer/toNatural.dhall
|
||||
sha256:4d128730d74e7f832e53873cb5204aa91b79758be5ce4e1aa991fe1951304a0e
|
||||
|
||||
let Number/toInteger = ./toInteger.dhall nix
|
||||
|
||||
in λ(a : Number) → Integer/toNatural (Number/toInteger a)
|
||||
in λ(a : Number) → Integer/clamp (Number/toInteger a)
|
||||
|
|
12
Path/importJSON.dhall
Normal file
12
Path/importJSON.dhall
Normal file
|
@ -0,0 +1,12 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Path = ./Type.dhall
|
||||
|
||||
let readFile = ./readFile.dhall nix
|
||||
|
||||
let importJSON
|
||||
: Path → Any
|
||||
= λ(p : Path) → nix.builtins.fromJSON (readFile p)
|
||||
|
||||
in importJSON
|
12
Path/importTOML.dhall
Normal file
12
Path/importTOML.dhall
Normal file
|
@ -0,0 +1,12 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Path = ./Type.dhall
|
||||
|
||||
let readFile = ./readFile.dhall nix
|
||||
|
||||
let importTOML
|
||||
: Path → Any
|
||||
= λ(p : Path) → nix.builtins.fromTOML (readFile p)
|
||||
|
||||
in importTOML
|
|
@ -1 +1,7 @@
|
|||
λ(nix : ../NixPrelude.dhall) → { Type = ./Type.dhall }
|
||||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ Type = ./Type.dhall
|
||||
, importJSON = ./importJSON.dhall nix
|
||||
, importTOML = ./importTOML.dhall nix
|
||||
, pathExists = ./pathExists.dhall nix
|
||||
, readFile = ./readFile.dhall nix
|
||||
}
|
||||
|
|
1
Path/pathExists.dhall
Normal file
1
Path/pathExists.dhall
Normal file
|
@ -0,0 +1 @@
|
|||
λ(nix : ../NixPrelude.dhall) → nix.builtins.pathExists
|
1
Path/readFile.dhall
Normal file
1
Path/readFile.dhall
Normal file
|
@ -0,0 +1 @@
|
|||
λ(nix : ../NixPrelude.dhall) → nix.builtins.readFile
|
16
Set/mergeAttrs.dhall
Normal file
16
Set/mergeAttrs.dhall
Normal file
|
@ -0,0 +1,16 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Set = ./Type.dhall
|
||||
|
||||
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
|
||||
|
||||
let mergeAttrFile = "a: b: a // b"
|
||||
|
||||
let mergeAttrs =
|
||||
Any/toTypeUnchecked
|
||||
(Set → Set → Set)
|
||||
( nix.builtins.import
|
||||
(nix.builtins.toFile "mergeAttrs.nix" mergeAttrFile)
|
||||
)
|
||||
: Set → Set → Set
|
||||
|
||||
in mergeAttrs
|
|
@ -1 +1,6 @@
|
|||
λ(nix : ../NixPrelude.dhall) → { Type = ./Type.dhall }
|
||||
λ(nix : ../NixPrelude.dhall) →
|
||||
{ Type = ./Type.dhall
|
||||
, setToMap = ./toMap.dhall nix
|
||||
, toSet = ./toSet.dhall nix
|
||||
, mergeAttrs = ./mergeAttrs.dhall nix
|
||||
}
|
||||
|
|
31
Set/toMap.dhall
Normal file
31
Set/toMap.dhall
Normal file
|
@ -0,0 +1,31 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Set = ./Type.dhall
|
||||
|
||||
let Map =
|
||||
https://prelude.dhall-lang.org/Map/Type.dhall
|
||||
sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed
|
||||
|
||||
let Entry =
|
||||
https://prelude.dhall-lang.org/Map/Entry.dhall
|
||||
sha256:f334283bdd9cd88e6ea510ca914bc221fc2dab5fb424d24514b2e0df600d5346
|
||||
|
||||
let List/map =
|
||||
https://prelude.dhall-lang.org/List/map.dhall
|
||||
sha256:dd845ffb4568d40327f2a817eb42d1c6138b929ca758d50bc33112ef3c885680
|
||||
|
||||
let setToMap
|
||||
: Set → Map Text Any
|
||||
= λ(set : Set) →
|
||||
let attrs = nix.builtins.attrNames set
|
||||
|
||||
in List/map
|
||||
Text
|
||||
(Entry Text Any)
|
||||
( λ(k : Text) →
|
||||
{ mapKey = k, mapValue = nix.builtins.getAttr k set }
|
||||
)
|
||||
attrs
|
||||
|
||||
in setToMap
|
34
Set/toSet.dhall
Normal file
34
Set/toSet.dhall
Normal file
|
@ -0,0 +1,34 @@
|
|||
λ(nix : ../NixPrelude.dhall) →
|
||||
let Any = ../Any/Type.dhall
|
||||
|
||||
let Set = ./Type.dhall
|
||||
|
||||
let Map =
|
||||
https://prelude.dhall-lang.org/Map/Type.dhall
|
||||
sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed
|
||||
|
||||
let Entry =
|
||||
https://prelude.dhall-lang.org/Map/Entry.dhall
|
||||
sha256:f334283bdd9cd88e6ea510ca914bc221fc2dab5fb424d24514b2e0df600d5346
|
||||
|
||||
let List/map =
|
||||
https://prelude.dhall-lang.org/List/map.dhall
|
||||
sha256:dd845ffb4568d40327f2a817eb42d1c6138b929ca758d50bc33112ef3c885680
|
||||
|
||||
let Any/toAny = ../Any/toAny.dhall nix
|
||||
|
||||
let toSet
|
||||
: ∀(a : Type) → Map Text a → Set
|
||||
= λ(a : Type) →
|
||||
λ(map : Map Text a) →
|
||||
nix.builtins.listToAttrs
|
||||
( List/map
|
||||
(Entry Text a)
|
||||
{ name : Text, value : Any }
|
||||
( λ(entry : Entry Text a) →
|
||||
{ name = entry.mapKey, value = Any/toAny a entry.mapValue }
|
||||
)
|
||||
map
|
||||
)
|
||||
|
||||
in toSet
|
|
@ -44,6 +44,7 @@ in { derivation : ∀(attrs : Set) → Path
|
|||
∀(list : List Any) →
|
||||
Any
|
||||
, fromJSON : ∀(e : Text) → Any
|
||||
, fromTOML : Text → Any
|
||||
, functionArgs : ∀(e : Any) → Set
|
||||
, genList :
|
||||
∀(generator : ∀(e : Natural) → Any) → ∀(length : Natural) → List Any
|
||||
|
|
|
@ -4,9 +4,12 @@
|
|||
∧ { Any = ./Any/package.dhall nix
|
||||
, Bool = ./Bool/package.dhall nix
|
||||
, Double = ./Double/package.dhall nix
|
||||
, Function = ./Function/package.dhall nix
|
||||
, Integer = ./Integer/package.dhall nix
|
||||
, List = ./List/package.dhall nix
|
||||
, Misc = ./Misc/package.dhall nix
|
||||
, Natural = ./Natural/package.dhall nix
|
||||
, Number = ./Number/package.dhall nix
|
||||
, Path = ./Path/package.dhall nix
|
||||
, Set = ./Set/package.dhall nix
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue