From 3c3713c69f9a7fb0c14ef463ab520de7f601e1e9 Mon Sep 17 00:00:00 2001
From: Profpatsch <mail@profpatsch.de>
Date: Sun, 19 Jun 2022 15:07:14 +0200
Subject: 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
---
 users/Profpatsch/dhall/lib.dhall | 84 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 users/Profpatsch/dhall/lib.dhall

(limited to 'users/Profpatsch/dhall')

diff --git a/users/Profpatsch/dhall/lib.dhall b/users/Profpatsch/dhall/lib.dhall
new file mode 100644
index 000000000000..fb97ba6070ef
--- /dev/null
+++ b/users/Profpatsch/dhall/lib.dhall
@@ -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 }
-- 
cgit 1.4.1