refactor(users/Profpatsch/aerc): move ini stuff out
First shot at generating a dhall FFI standard. Change-Id: I1cdf7eeaa6b2668a49282315f308a8e51abd0cf6 Reviewed-on: https://cl.tvl.fyi/c/depot/+/5887 Reviewed-by: Profpatsch <mail@profpatsch.de> Tested-by: BuildkiteCI
This commit is contained in:
parent
2cf67e113e
commit
3c3713c69f
5 changed files with 246 additions and 135 deletions
84
users/Profpatsch/dhall/lib.dhall
Normal file
84
users/Profpatsch/dhall/lib.dhall
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
let List/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
|
||||
|
||||
--| Concatenate a `List` of `List`s into a single `List`
|
||||
List/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
|
||||
|
||||
|
||||
-- Transform a list by applying a function to each element and flattening the results
|
||||
List/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 Status = < Empty | NonEmpty : Text >
|
||||
|
||||
let
|
||||
|
||||
{-|
|
||||
Transform each value in a `List` to `Text` and then concatenate them with a
|
||||
separator in between each value
|
||||
-}
|
||||
Text/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
|
||||
|
||||
in { List/map, List/concat, List/concatMap, Text/concatMapSep }
|
||||
Loading…
Add table
Add a link
Reference in a new issue