From 3c3713c69f9a7fb0c14ef463ab520de7f601e1e9 Mon Sep 17 00:00:00 2001 From: Profpatsch 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 Tested-by: BuildkiteCI --- users/Profpatsch/aerc.dhall | 268 ++++++++++++++++++--------------------- users/Profpatsch/aerc.nix | 7 +- users/Profpatsch/dhall/lib.dhall | 84 ++++++++++++ users/Profpatsch/ini/default.nix | 6 + users/Profpatsch/ini/ini.dhall | 36 ++++++ 5 files changed, 256 insertions(+), 145 deletions(-) create mode 100644 users/Profpatsch/dhall/lib.dhall create mode 100644 users/Profpatsch/ini/default.nix create mode 100644 users/Profpatsch/ini/ini.dhall 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 " - } - , { 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 " } + , { 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 = "", 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 = "", 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}" } - - let - -- set a command, but stay on the prompt - prompt = - λ(cmd : Text) → { cmd = ":${cmd}" } - - 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}" } + + let + -- set a command, but stay on the prompt + prompt = + λ(cmd : Text) → { cmd = ":${cmd}" } + + 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 } -- cgit 1.4.1