std.cli

A command line, described once: what each command takes is a term of Args, and the words given are read by it, the usage and each command’s help written from it, and what the word being written completes to said by it (the shells’ scripts ask the program).

The words are read as getopt_long reads them: flags anywhere among the positionals; --long V, --long=V, -s V, -sV, switches side by side (-abc); a long name by any start of it that is no other’s; an option’s value the next word, whatever it is; given twice, the last; -- ends the flags, and so does the start of a rest; - alone is a positional; --help and -h ask for the command’s help.

They are read in two stages — split by the shape (which flags take a value), then the values taken — so the shape is known before a word is read: Args is applicative, not a monad. A program’s commands are ordinary functions given the values; the library has no effect, and says what the program is to do (Outcome).

Complete

data Complete = None | Files String | Dirs | Among (List String)

what a word completes to

Flag

type Flag =
  { long : String
  , short : String
  , meta : String
  , doc : String
  , values : List String
  , repeated : Bool
  , required : Bool
  , complete : Complete
  }

a flag: --long, -s (short: "" for none), the value it takes (meta: "" for a switch), the values it may have (Nil: any), whether it may be given more than once, and must be given

Arity

data Arity = One | Optional | Many | Some | Rest

how many words a positional takes: one, one or none, any number, at least one, or the rest (verbatim: flags are not read in them)

Pos

type Pos = { meta : String, arity : Arity, complete : Complete }

Shape

type Shape = { flags : List Flag, pos : List Pos }

Problem

data Problem
  = Unknown String (Maybe String)
  | NoValue String
  | SwitchValue String
  | Ambiguous String (List String)
  | MissingFlag String
  | NotIn String String (List String)
  | Missing String
  | Extra String
  | Help
  | BadShape String

what is wrong with the words given

Args

theory Args where
  A : Type -> Type
  give : {a : Type} -> a -> A a
  ap : {a b : Type} -> A (a -> b) -> A a -> A b
  flag : Flag -> A (List String)
  pos : Pos -> A (List String)

Term

type Term a = (s : Args) -> s.A a

a term: what a command takes, read as an a

Reader

type Reader a =
  { shape : Shape
  , take : List (List String) -> List (String, List String) -> a
  }

readerOf

readerOf : {a : Type} -> Term a -> Reader a

shapeOf

shapeOf : {a : Type} -> Term a -> Shape

switch

switch : (s : Args) -> String -> String -> String -> s.A Bool

--long, -s: given or not

option

option : (s : Args)
       -> String
       -> String
       -> String
       -> String
       -> s.A (Maybe String)

--long V, --long=V, -s V, -sV: the last one given

choose

choose : (s : Args)
       -> String
       -> String
       -> String
       -> String
       -> List String
       -> s.A String

… given, one of values

arg

arg : (s : Args) -> String -> Complete -> s.A String

optional

optional : (s : Args) -> String -> Complete -> s.A (Maybe String)

some

some : (s : Args) -> String -> Complete -> s.A (List String)

many

many : (s : Args) -> String -> Complete -> s.A (List String)

rest

rest : (s : Args) -> String -> s.A (List String)

with1

with1 : (s : Args) -> {a r : Type} -> (a -> r) -> s.A a -> s.A r

f given what each of the terms read

with2

with2 : (s : Args) -> {a b r : Type} -> (a -> b -> r) -> s.A a -> s.A b -> s.A r

with3

with3 : (s : Args)
      -> {a b c r : Type}
      -> (a -> b -> c -> r)
      -> s.A a
      -> s.A b
      -> s.A c
      -> s.A r

with4

with4 : (s : Args)
      -> {a b c d r : Type}
      -> (a -> b -> c -> d -> r)
      -> s.A a
      -> s.A b
      -> s.A c
      -> s.A d
      -> s.A r

shapeProblem

shapeProblem : Shape -> Maybe String

what is wrong with a shape: a name twice, a short name that is not one letter, help/h taken, a positional of many words before the last, a switch with values, flags where every word is the rest

longNamed

longNamed : Shape -> String -> Either (List String) Flag

a long name as written: the flag it names, or the one it is the start of (getopt_long’s abbreviation); Left: the flags it could be (none, or more than one)

longMaybe

longMaybe : Shape -> String -> Maybe Flag

… if it names one

flagLike

flagLike : Shape -> String -> Bool

a word is a flag’s: --x..., -x... — not - alone (getopt’s)

distance

distance : String -> String -> Int

Split

type Split = { pos : List String, flags : List (String, String) }

the words split: the positionals, and each flag given (its long name, its value), in order

At

type At =
  { sh : Shape
  , ra : Int
  , on : Bool
  , ps : List String
  , fs : List (String, String)
  }

Splitter

type Splitter = { words : At -> List String -> Either Problem Split }

splitWords

splitWords : Shape -> List String -> Either Problem Split

the words, split by the shape

groupsGo

groupsGo : List Pos -> List String -> Either Problem (List (List String))

the words each positional takes, in order

parse

parse : {a : Type} -> Term a -> List String -> Either Problem a

the words read as the term says, or what is wrong with them

problemOf

problemOf : Shape -> List String -> Maybe Problem

What is wrong with the words, read by the shape, if anything: what parse would say, the words not read as anything.

Candidates

data Candidates = Words (List String) | FilesBy String | DirsOnly | Nothing

what the word being written completes to

Where

type Where =
  { on : Bool, waiting : Maybe Flag, count : Int, given : List String }

where the words before the one being written leave the reading: flags read or not, a flag waiting for its value, how many positionals

complete

complete : Shape -> List String -> String -> Candidates

what cur completes to, after the words before

Command

type Command r = { name : String, doc : String, shown : Bool, args : Term r }

a command: its name, what it does, whether the usage shows it, and what it takes, read as an r

command

command : {r : Type} -> String -> String -> Term r -> Command r

hidden

hidden : {r : Type} -> String -> Term r -> Command r

a command not in the usage, nor completed

parseCommand

parseCommand : {r : Type} -> Command r -> List String -> Either Problem r

shapeOfCommand

shapeOfCommand : {r : Type} -> Command r -> Shape

posWord

posWord : Pos -> String

flagWord

flagWord : Flag -> String

synopsis

synopsis : Shape -> String

how a command is called: its positionals, then its flags

headOf

headOf : {r : Type} -> Command r -> String

a command’s name and how it is called

usage

usage : {r : Type} -> String -> List (Command r) -> String

the program’s usage: its commands, and the library’s

flagLine

flagLine : Flag -> String

helpOf

helpOf : {r : Type} -> String -> Command r -> String

a command’s help: how it is called, what it does, its flags

problemSaid

problemSaid : Problem -> String

what is wrong, said

findCommand

findCommand : {r : Type} -> List (Command r) -> String -> Maybe (Command r)

completeLine

completeLine : {r : Type} -> List (Command r) -> List String -> String

the answer to PROG complete WORD...

chosenVariable

chosenVariable : String -> String

The environment variable in which the shell’s function names the file the command line chosen in the program’s app is written to.

>>> chosenVariable "fs-tree"
"FS_TREE_CHOSEN"

fishScript

fishScript : String -> String

fish’s script: it asks PROG complete for the words before the cursor and the one at it

bashScript

bashScript : String -> String

bash’s script (bash 3.2 and on): the words are the line up to the cursor, split at blanks; bash splits a word at = too, so what follows a = is what replaces the word being written

zshScript

zshScript : String -> String

zsh’s script

Outcome

data Outcome r = Run r | Out String | Fail String

what the program is to do: run what the words were read as, or write a text on its output (and end well), or on its error stream (and end badly)

readLine

readLine : {r : Type} -> String -> List (Command r) -> List String -> Outcome r

the words given the program prog (not its own name), read by its commands; help [COMMAND], completions SHELL and complete WORD... (what the scripts ask) are the library’s

compileArgs

compileArgs : Term String

>>> parse compileArgs ["a.hf", "a.mjs", "--backend=page"]
Right "a.hf a.mjs - page"
>>> parse compileArgs ["--back", "page", "a.hf", "-nmain", "a.mjs"]
Right "a.hf a.mjs main page"
>>> parse compileArgs ["a.hf", "a.mjs", "-b", "esm", "--backend=page"]
Right "a.hf a.mjs - page"
>>> parse compileArgs ["--backend=esm", "--", "-a.hf", "a.mjs"]
Right "-a.hf a.mjs - esm"
>>> parse compileArgs ["a.hf", "a.mjs"]
Left (MissingFlag "--backend=MODE")
>>> parse compileArgs ["a.hf", "a.mjs", "--backend=wasm"]
Left (NotIn "--backend" "wasm" ["esm", "page", "c"])
>>> parse compileArgs ["a.hf", "a.mjs", "--bakend=c"]
Left (Unknown "--bakend" (Just "backend"))
>>> parse compileArgs ["a.hf", "--name", "--help", "a.mjs", "-b", "esm"]
Right "a.hf a.mjs --help esm"
>>> parse compileArgs ["a.hf", "-h"]
Left Help
>>> parse compileArgs ["a.hf", "a.mjs", "b.mjs", "-b", "esm"]
Left (Extra "b.mjs")
>>> synopsis (shapeOf compileArgs)
"FILE OUT [--name NAME] --backend=MODE"
>>> complete (shapeOf compileArgs) ["a.hf", "a.mjs", "--backend"] ""
Words ["esm", "page", "c"]
>>> complete (shapeOf compileArgs) ["a.hf", "-b"] "p"
Words ["page"]
>>> complete (shapeOf compileArgs) ["a.hf", "--name", "x"] "--"
Words ["--help", "--backend"]
>>> complete (shapeOf compileArgs) Nil ""
FilesBy ".hf"
>>> complete (shapeOf compileArgs) ["a.hf"] "--backend=c"
Words ["--backend=c"]
>>> problemOf (shapeOf compileArgs) ["a.hf", "-bc"]
Just (Missing "OUT")
>>> problemOf (shapeOf compileArgs) ["a.hf", "a.c", "-bc"]
Nothing

listArgs

listArgs : Term String

>>> parse listArgs ["-aAl3"]
Right "all almost 3"
>>> parse listArgs ["--al"]
Left (Ambiguous "--al" ["all", "almost"])
>>> parse listArgs ["--all=1"]
Left (SwitchValue "--all")
>>> parse listArgs ["-l"]
Left (NoValue "-l")
>>> shapeProblem { flags = (shapeOf listArgs).flags, pos = [{ meta = "ARGS", arity = Rest, complete = None }] }
Just "ARGS is every word, so no flag could be given"

runArgs

runArgs : Term String

>>> parse runArgs ["main.hf", "--verbose", "--", "-h"]
Right "main.hf --verbose,--,-h"
>>> shapeProblem { flags = (shapeOf listArgs).flags, pos = (shapeOf runArgs).pos }
Nothing

commandsEx

commandsEx : List (Command String)

>>> readLine "heff" commandsEx ["compile", "a.hf", "a.mjs", "-bc"]
Run "a.hf a.mjs - c"
>>> readLine "heff" commandsEx ["compile", "a.hf", "-b", "esm"]
Fail "heff compile: expected OUT\nusage: heff compile FILE OUT [--name NAME] --backend=MODE\n"
>>> completeLine commandsEx ["c"]
"compile\tFILE as JavaScript\ncompletions\ta completion script for SHELL\n"
>>> completeLine commandsEx ["compile", "a.hf", "--"]
"--help\n--name\tthe computation run\n--backend\thow it runs\n"
>>> completeLine commandsEx ["help", ""]
"compile\nrun\n"