let
-- DSL for building INI files
ToIniFns =
λ ( Ini
: { -- A Section in the ini
Section : Type
, -- A couple of sections
SectionList : Type
}
) →
{ -- Create a new section
newSection : Ini.Section
, -- Add a key/value pair to the section
add : Text → Text → Ini.Section → Ini.Section
, -- Add all these key/value pairs to the section
addAll :
List { name : Text, value : Text } → Ini.Section → Ini.Section
, -- Create a new SectionList
newSectionList : Ini.SectionList
, -- Add a section to the list of sections
addSection : Text → Ini.Section → Ini.SectionList → Ini.SectionList
}
in λ ( imports
: { -- concatenate a list with newlines
concatNewline : List Text → Text
, -- 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 :
( ∀(Ini : { Section : Type, SectionList : Type }) →
ToIniFns Ini →
{ globalSection : Ini.Section, sections : Ini.SectionList }
) →
Text
}
) →
let List/foldLeft
: ∀(a : Type) →
List a →
∀(list : Type) →
∀(cons : list → a → list) →
∀(nil : list) →
list
= λ(a : Type) →
λ(xs : List a) →
λ(list : Type) →
λ(cons : list → a → list) →
λ(nil : list) →
List/fold
a
xs
(list → list)
(λ(x : a) → λ(f : list → list) → λ(l : list) → f (cons l x))
(λ(l : list) → l)
nil
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
-- A builder is a list of “build methods” that go from (a -> a) and change the a step by step.
Builder/build =
λ(a : Type) →
λ(init : a) →
λ(builders : List (a → a)) →
List/foldLeft
(a → a)
builders
a
(λ(acc : a) → λ(f : a → a) → f acc)
init
in { accounts =
imports.toIni
( λ(Ini : { Section : Type, SectionList : Type }) →
λ(ini : ToIniFns Ini) →
{ globalSection = ini.newSection
, sections =
ini.addSection
"mail"
( ini.addAll
[ { 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" }
]
ini.newSection
)
ini.newSectionList
}
)
, aerc =
imports.toIni
( λ(Ini : { Section : Type, SectionList : Type }) →
λ(ini : ToIniFns Ini) →
{ globalSection = ini.newSection
, sections =
ini.addSection
"filters"
( Builder/build
Ini.Section
ini.newSection
[ ini.add "text/html" (imports.aercFilter "html")
, let _ =
"-- TODO: this awk should be taken from nix!"
in ini.add
"text/*"
"awk -f ${imports.aercFilter "plaintext"}"
]
)
ini.newSectionList
}
)
, 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 "<C-${k.key}> = ${k.cmd}"
else "${k.key} = ${k.cmd}"
let
-- render a list of keys to config format
renderKeys =
λ(keys : List Key) → List/map Key Text renderKey keys
let
-- create a section whith a name and a list of keys
sect =
λ(section : Text) →
λ(keys : List Key) →
{ section, keys = 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" ]
]
}
let Section = { section : Text, keys : List Text }
let iniToJson =
λ ( ini
: { globalSection : List Text
, sections : List Section
}
) →
let mkKeys = imports.concatNewline
let
-- TODO: escaping section header?
mkSection =
λ(section : Section) →
''
[${section.section}]
''
++ mkKeys section.keys
in mkKeys ini.globalSection
++ mkKeys
( List/map
Section
Text
mkSection
ini.sections
)
in iniToJson config
}