0 | ||| Collie: Command line interface for Idris2 applications
 1 | |||
 2 | ||| Based on Guillaume Allais's agdARGS library:
 3 | |||
 4 | ||| https://github.com/gallais/agdargs/
 5 | module Collie
 6 |
 7 | import public Collie.Core
 8 | import public Collie.Parser
 9 | import public Collie.Usage
10 |
11 | import public Collie.Options.Domain
12 | import public Collie.Options.Usual
13 | import public Collie.Modifiers
14 | import public Data.Record
15 | import public Data.Record.SmartConstructors
16 |
17 | import public Data.DPair
18 | import public Data.Magma
19 |
20 | import public Data.SnocList
21 |
22 | import public System
23 |
24 | %default total
25 |
26 | public export
27 | (.parseArgs) : (cmd : Command nm) -> HasIO io =>
28 |   io (String `Either` ParseTreeT Maybe Maybe cmd)
29 | cmd.parseArgs = do
30 |   args <- getArgs
31 |   let args' =
32 |         case args of
33 |           [] => []
34 |           _ :: xs => xs
35 |   -- putStrLn "parsing arguments: \{show $ cmd.name :: args'}"
36 |   let Pure res = parse cmd args'
37 |        | err => pure $ Left (show (() <$ err))
38 |   pure $ Right res
39 |
40 |
41 | public export
42 | record Handlers (a : Type) (cmd : Field Command) where
43 |   constructor MkHandlers
44 |   here  : ParsedCommand (cmd .fst) (cmd .snd) -> a
45 |   there : Checkable (Handlers a) cmd.snd.subcommands
46 |
47 | ||| Givent that we already have list syntax to build records, this gives us the
48 | ||| ability to use list syntax to build `Handlers`: the head will be the handler
49 | ||| for the toplevel command and the tail will go towards building the record of
50 | ||| handlers for the subcommands.
51 | public export
52 | (::) : (ParsedCommand (cmd .fst) (cmd .snd) -> a) ->
53 |        Checkable (Handlers a) cmd.snd.subcommands ->
54 |        Handlers a cmd
55 | (::) = MkHandlers
56 |
57 | export infixr 4 ~~>
58 |
59 | ||| A nicer notation for handlers
60 | public export
61 | 0 (~~>) : (Command arg) -> Type -> Type
62 | (~~>) cmd a = Handlers a (_ ** cmd)
63 |
64 | ||| Handling a parsetree is pretty simple: use `there` together with `(!!)` to
65 | ||| select the appropriate subhandler while you're encountering  the `There`
66 | ||| constructor and finish up with `here`.
67 | public export
68 | handle : {0 cmd : Field Command} ->
69 |          ParseTree cmd.snd -> Handlers a cmd -> a
70 | handle (Here res)    h = h.here res
71 | handle (There pos p) h = handle p $ content h.there.mkCheckable !! pos
72 |
73 | ||| Finally we can put the various pieces together to get a toplevel command
74 | ||| parsing the arguments and handling the resulting command using the
75 | ||| user-provided handlers
76 | public export
77 | (.handleWith) : {nm : String} -> (cmd : Command nm) -> (cmd ~~> IO a) -> IO a
78 | cmd .handleWith h
79 |   = do Right args <- cmd.parseArgs
80 |          | _ => do putStrLn (cmd .usage)
81 |                    exitFailure
82 |        let Pure args = ParsedTree.finalising args
83 |          | Fail err => exitWith err
84 |        handle args h
85 |