3c3713c69f
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
84 lines
2.4 KiB
Text
84 lines
2.4 KiB
Text
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 }
|