refactor(users/Profpatsch/aerc): move ini stuff out r/4247

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

5 files changed, 256 insertions, 145 deletions

diff --git a/users/Profpatsch/aerc.dhall b/users/Profpatsch/aerc.dhall
index fb63f7044b..2a02b418dd 100644
--- a/users/Profpatsch/aerc.dhall
+++ b/users/Profpatsch/aerc.dhall
@@ -1,157 +1,139 @@
-let NameVal = λ(T : Type) → { name : Text, value : T }
+let Lib = ./dhall/lib.dhall
+
+let List/map = Lib.List/map
+
+let Ini = ./ini/ini.dhall
 
 in  λ ( imports
       : { -- Take an aerc filter from the aerc distribution /share directory
           aercFilter : Text → Text
-        , -- given a dsl of functions to create an Ini, render the ini file
-          toIni :
-            { globalSection : List (NameVal Text)
-            , sections : List (NameVal (List (NameVal Text)))
-            } →
-              Text
+        , Ini/externs : Ini.Externs
         }
       ) →
-      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))
-                )
-
-      in  { accounts =
-              imports.toIni
-                { globalSection = [] : List (NameVal Text)
-                , sections =
-                  [ { name = "mail"
-                    , value =
-                      [ { name = "archive", value = "Archive" }
-                      , { name = "copy-to", value = "Sent" }
-                      , { name = "default", value = "INBOX" }
-                      , { name = "from"
-                        , value = "Profpatsch <mail@profpatsch.de>"
-                        }
-                      , { name = "source", value = "maildir://~/.Mail/mail" }
-                      , { name = "postpone", value = "Drafts" }
-                      ]
-                    }
+      { accounts =
+          imports.Ini/externs.renderIni
+            { globalSection = [] : Ini.Section
+            , sections =
+              [ { name = "mail"
+                , value =
+                  [ { name = "archive", value = "Archive" }
+                  , { name = "copy-to", value = "Sent" }
+                  , { name = "default", value = "INBOX" }
+                  , { name = "from", value = "Profpatsch <mail@profpatsch.de>" }
+                  , { name = "source", value = "maildir://~/.Mail/mail" }
+                  , { name = "postpone", value = "Drafts" }
                   ]
                 }
-          , aerc =
-              imports.toIni
-                { globalSection = [] : List (NameVal Text)
-                , sections =
-                  [ { name = "filters"
-                    , value =
-                      [ { name = "text/html"
-                        , value = imports.aercFilter "html"
+              ]
+            }
+      , aerc =
+          imports.Ini/externs.renderIni
+            { globalSection = [] : Ini.Section
+            , sections =
+              [ { name = "filters"
+                , value =
+                  [ { name = "text/html", value = imports.aercFilter "html" }
+                  , let _ = "-- TODO: this awk should be taken from nix!"
+
+                    in  { name = "text/*"
+                        , value = "awk -f ${imports.aercFilter "plaintext"}"
                         }
-                      , let _ = "-- TODO: this awk should be taken from nix!"
-
-                        in  { name = "text/*"
-                            , value = "awk -f ${imports.aercFilter "plaintext"}"
-                            }
-                      ]
-                    }
                   ]
                 }
-          , binds =
+              ]
+            }
+      , binds =
+          let
+              -- keybinding and command to run
+              Key =
+                { ctrl : Bool, key : Text, cmd : Text }
+
+          in  let
+                  -- render a key to config format
+                  renderKey =
+                    λ(k : Key) →
+                      if    k.ctrl
+                      then  { name = "<C-${k.key}>", value = k.cmd }
+                      else  { name = k.key, value = k.cmd }
+
+              let
+
+                  -- render a list of keys to config format
+                  renderKeys =
+                    λ(keys : List Key) →
+                      List/map Key (Ini.NameVal Text) renderKey keys
+
               let
-                  -- keybinding and command to run
-                  Key =
-                    { ctrl : Bool, key : Text, cmd : Text }
-
-              in  let
-                      -- render a key to config format
-                      renderKey =
-                        λ(k : Key) →
-                          if    k.ctrl
-                          then  { name = "<C-${k.key}>", value = k.cmd }
-                          else  { name = k.key, value = k.cmd }
-
-                  let
-
-                      -- render a list of keys to config format
-                      renderKeys =
-                        λ(keys : List Key) →
-                          List/map Key (NameVal Text) renderKey keys
-
-                  let
-                      -- create a section whith a name and a list of keys
-                      sect =
-                        λ(section : Text) →
-                        λ(keys : List Key) →
-                          { name = section, value = renderKeys keys }
-
-                  let
-
-                      -- set key without modifiers
-                      key =
-                        λ(key : Text) → { key }
-
-                  let
-                      -- set special key without modifiers
-                      special =
-                        λ(key : Text) → { key = "<${key}>" }
-
-                  let
-                      -- no modifier
-                      none =
-                        { ctrl = False }
-
-                  let
-                      -- set control key
-                      ctrl =
-                        { ctrl = True }
-
-                  let
-                      -- set a command to execute
-                      cmd =
-                        λ(cmd : Text) → { cmd = ":${cmd}<Enter>" }
-
-                  let
-                      -- set a command, but stay on the prompt
-                      prompt =
-                        λ(cmd : Text) → { cmd = ":${cmd}<Space>" }
-
-                  let config =
-                        { globalSection =
-                            renderKeys
-                              [ ctrl ∧ key "p" ∧ cmd "prev-tab"
-                              , ctrl ∧ key "n" ∧ cmd "next-tab"
-                              , ctrl ∧ key "t" ∧ cmd "term"
-                              ]
-                        , sections =
-                          [ sect
-                              "messages"
-                              [ ctrl ∧ key "q" ∧ cmd "quit"
-                              , none ∧ special "Up" ∧ cmd "prev"
-                              , none ∧ special "Down" ∧ cmd "next"
-                              , none ∧ special "PgUp" ∧ cmd "prev 100%"
-                              , none ∧ special "PgDn" ∧ cmd "next 100%"
-                              , none ∧ key "g" ∧ cmd "select 0"
-                              , none ∧ key "G" ∧ cmd "select -1"
-                              , ctrl ∧ key "Up" ∧ cmd "prev-folder"
-                              , ctrl ∧ key "Down" ∧ cmd "next-folder"
-                              , none ∧ key "v" ∧ cmd "mark -t"
-                              , none ∧ key "V" ∧ cmd "mark -v"
-                              , none ∧ special "Enter" ∧ cmd "view"
-                              , none ∧ key "c" ∧ cmd "compose"
-                              , none ∧ key "|" ∧ prompt "pipe"
-                              , none ∧ key "t" ∧ prompt "term"
-                              , none ∧ key "/" ∧ prompt "search"
-                              , none ∧ key "n" ∧ cmd "next-result"
-                              , none ∧ key "N" ∧ cmd "prev-result"
-                              , none ∧ special "Esc" ∧ cmd "clear"
-                              ]
-                          , sect "view" [ none ∧ key "q" ∧ cmd "close" ]
+                  -- create a section whith a name and a list of keys
+                  sect =
+                    λ(section : Text) →
+                    λ(keys : List Key) →
+                      { name = section, value = renderKeys keys }
+
+              let
+
+                  -- set key without modifiers
+                  key =
+                    λ(key : Text) → { key }
+
+              let
+                  -- set special key without modifiers
+                  special =
+                    λ(key : Text) → { key = "<${key}>" }
+
+              let
+                  -- no modifier
+                  none =
+                    { ctrl = False }
+
+              let
+                  -- set control key
+                  ctrl =
+                    { ctrl = True }
+
+              let
+                  -- set a command to execute
+                  cmd =
+                    λ(cmd : Text) → { cmd = ":${cmd}<Enter>" }
+
+              let
+                  -- set a command, but stay on the prompt
+                  prompt =
+                    λ(cmd : Text) → { cmd = ":${cmd}<Space>" }
+
+              let config =
+                    { globalSection =
+                        renderKeys
+                          [ ctrl ∧ key "p" ∧ cmd "prev-tab"
+                          , ctrl ∧ key "n" ∧ cmd "next-tab"
+                          , ctrl ∧ key "t" ∧ cmd "term"
                           ]
-                        }
+                    , sections =
+                      [ sect
+                          "messages"
+                          [ ctrl ∧ key "q" ∧ cmd "quit"
+                          , none ∧ special "Up" ∧ cmd "prev"
+                          , none ∧ special "Down" ∧ cmd "next"
+                          , none ∧ special "PgUp" ∧ cmd "prev 100%"
+                          , none ∧ special "PgDn" ∧ cmd "next 100%"
+                          , none ∧ key "g" ∧ cmd "select 0"
+                          , none ∧ key "G" ∧ cmd "select -1"
+                          , ctrl ∧ key "Up" ∧ cmd "prev-folder"
+                          , ctrl ∧ key "Down" ∧ cmd "next-folder"
+                          , none ∧ key "v" ∧ cmd "mark -t"
+                          , none ∧ key "V" ∧ cmd "mark -v"
+                          , none ∧ special "Enter" ∧ cmd "view"
+                          , none ∧ key "c" ∧ cmd "compose"
+                          , none ∧ key "|" ∧ prompt "pipe"
+                          , none ∧ key "t" ∧ prompt "term"
+                          , none ∧ key "/" ∧ prompt "search"
+                          , none ∧ key "n" ∧ cmd "next-result"
+                          , none ∧ key "N" ∧ cmd "prev-result"
+                          , none ∧ special "Esc" ∧ cmd "clear"
+                          ]
+                      , sect "view" [ none ∧ key "q" ∧ cmd "close" ]
+                      ]
+                    }
 
-                  in  imports.toIni config
-          }
+              in  imports.Ini/externs.renderIni config
+      }
diff --git a/users/Profpatsch/aerc.nix b/users/Profpatsch/aerc.nix
index 569f045a00..407f224e58 100644
--- a/users/Profpatsch/aerc.nix
+++ b/users/Profpatsch/aerc.nix
@@ -15,13 +15,16 @@ let
         root = ./.;
         files = [
           "aerc.dhall"
+          "dhall/lib.dhall"
+          "ini/ini.dhall"
         ];
         main = "aerc.dhall";
-        deps = [ ];
+        deps = [
+        ];
       }
       {
         aercFilter = name: "${aerc-patched}/share/aerc/filters/${name}";
-        toIni = depot.users.Profpatsch.toINI { };
+        "Ini/externs" = depot.users.Profpatsch.ini.externs;
       };
 
   aerc-config = pkgs.linkFarm "alacritty-config" [
diff --git a/users/Profpatsch/dhall/lib.dhall b/users/Profpatsch/dhall/lib.dhall
new file mode 100644
index 0000000000..fb97ba6070
--- /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 }
diff --git a/users/Profpatsch/ini/default.nix b/users/Profpatsch/ini/default.nix
new file mode 100644
index 0000000000..e1a7a1a7b6
--- /dev/null
+++ b/users/Profpatsch/ini/default.nix
@@ -0,0 +1,6 @@
+{ depot, ... }:
+{
+  externs = {
+    renderIni = depot.users.Profpatsch.toINI { };
+  };
+}
diff --git a/users/Profpatsch/ini/ini.dhall b/users/Profpatsch/ini/ini.dhall
new file mode 100644
index 0000000000..f2efbc0af4
--- /dev/null
+++ b/users/Profpatsch/ini/ini.dhall
@@ -0,0 +1,36 @@
+let lib = ../dhall/lib.dhall
+
+let NameVal = λ(T : Type) → { name : Text, value : T }
+
+let ValueList = λ(T : Type) → List (NameVal T)
+
+let Section = ValueList Text
+
+let Sections = ValueList Section
+
+let Ini = { globalSection : Section, sections : Sections }
+
+let
+    -- Takes to INI files and merges their global sections and their section lists,
+    -- without duplicating by section name.
+    appendInis =
+      λ(inis : List Ini) →
+          { globalSection =
+              lib.List/concat
+                (NameVal Text)
+                (lib.List/map Ini Section (λ(i : Ini) → i.globalSection) inis)
+          , sections =
+              lib.List/concat
+                (NameVal Section)
+                (lib.List/map Ini Sections (λ(i : Ini) → i.sections) inis)
+          }
+        : Ini
+
+let
+    -- Signatures of functions that are input via FFI.
+    Externs =
+      { -- given a dsl of functions to create an Ini, render the ini file
+        renderIni : Ini → Text
+      }
+
+in  { NameVal, ValueList, Section, Sections, Ini, appendInis, Externs }