0 | module Collie.Core
  1 |
  2 | import public Collie.Options.Domain
  3 | import public Collie.Options.Usual
  4 | import public Collie.Modifiers
  5 | import public Data.Record
  6 | import public Data.Record.SmartConstructors
  7 |
  8 | import public Data.Vect
  9 | import public Data.DPair
 10 | import public Data.Magma
 11 |
 12 | import public Syntax.WithProof
 13 |
 14 | import public Decidable.Decidable
 15 | import public Decidable.Decidable.Extra1
 16 |
 17 | %default total
 18 |
 19 | public export
 20 | record Command (name : String) where
 21 |   constructor MkCommand
 22 |   description : String
 23 |   subcommands : Fields Command
 24 |   modifiers : Fields Modifier
 25 |   arguments : Arguments
 26 |
 27 | public export
 28 | basic : {cmdName : String} ->
 29 |         (description : String) -> Arguments -> Command cmdName
 30 | basic desc args = MkCommand
 31 |   { description = desc
 32 |   , subcommands = []
 33 |   , modifiers   = []
 34 |   , arguments   = args
 35 |   }
 36 |
 37 | public export
 38 | data Any : (p : (0 nm : String) -> Command nm -> Type) ->
 39 |            {0 nm : String} -> (cmd : Command nm) -> Type where
 40 |   Here : {0 p : (0 nm : String) -> Command nm -> Type} ->
 41 |          p nm cmd -> Any p cmd
 42 |   There :
 43 |     {c : String} ->
 44 |     (pos : c `IsField` cmd.subcommands) ->
 45 |     (parsedSub : Any p (snd $ field pos)) ->
 46 |     Any p cmd
 47 |
 48 | namespace Any
 49 |
 50 |   public export
 51 |   map : {0 p, q : (0 nm : String) -> Command nm -> Type} ->
 52 |         {cmd : Command nm} ->
 53 |         ({0 nm : String} -> (cmd : Command nm) -> p nm cmd -> q nm cmd) ->
 54 |         Any p cmd -> Any q cmd
 55 |   map f (Here pcmd) = Here (f _ pcmd)
 56 |   map f (There pos p) = There pos (map f p)
 57 |
 58 |   public export
 59 |   traverse : Applicative m =>
 60 |       {0 p, q : (0 nm : String) -> Command nm -> Type} ->
 61 |       {cmd : Command nm} ->
 62 |       ({0 nm : String} -> (cmd : Command nm) -> p nm cmd -> m (q nm cmd)) ->
 63 |       Any p cmd -> m (Any q cmd)
 64 |   traverse f (Here pcmd)   = Here <$> f _ pcmd
 65 |   traverse f (There pos p) = There pos <$> traverse f p
 66 |
 67 | public export
 68 | record ParsedCommandT
 69 |        (f, g : Type -> Type)
 70 |        (0 nm : String) (cmd : Command nm) where
 71 |   constructor MkParsedCommandT
 72 |   modifiers : ParsedModifiersT f g cmd.modifiers
 73 |   arguments : ParsedArgumentsT g cmd.arguments
 74 |
 75 | public export
 76 | record ParsedCommand
 77 |        (0 nm : String) (cmd : Command nm) where
 78 |   constructor MkParsedCommand
 79 |   modifiers : ParsedModifiers cmd.modifiers
 80 |   arguments : ParsedArguments cmd.arguments
 81 |
 82 | namespace ParsedCommand
 83 |
 84 |   public export
 85 |   defaulting : {cmd : Command nm} ->
 86 |     ParsedCommandT Maybe f nm cmd -> ParsedCommandT Prelude.id f nm cmd
 87 |   defaulting (MkParsedCommandT mods args)
 88 |     = MkParsedCommandT (defaulting mods) args
 89 |
 90 |   public export
 91 |   finalising : {cmd : Command nm} ->
 92 |     ParsedCommandT Maybe Maybe nm cmd -> Error (ParsedCommand nm cmd)
 93 |   finalising (MkParsedCommandT mods args)
 94 |     = MkParsedCommand
 95 |     <$> finalising mods
 96 |     <*> finalising MissingArgument _ args
 97 |
 98 | public export
 99 | ParseTreeT : (f, g : Type -> Type) -> (cmd : Command nm) -> Type
100 | ParseTreeT f g = Any (ParsedCommandT f g)
101 |
102 | public export
103 | ParseTree : (cmd : Command nm) -> Type
104 | ParseTree = Any ParsedCommand
105 |
106 | namespace ParsedTree
107 |
108 |   public export
109 |   defaulting : {cmd : Command nm} ->
110 |     ParseTreeT Maybe f cmd -> ParseTreeT Prelude.id f cmd
111 |   defaulting = map (\ _ => defaulting)
112 |
113 |   public export
114 |   finalising : {cmd : Command nm} ->
115 |     ParseTreeT Maybe Maybe cmd -> Error (ParseTree cmd)
116 |   finalising = traverse (\ _ => finalising)
117 |
118 | public export
119 | lookup : {nm : String} -> {c : Command nm} -> Any p c -> (nm ** Command nm)
120 | lookup (Here {}) = (_ ** c)
121 | lookup (There {parsedSub, _}) = lookup parsedSub
122 |
123 | {-
124 |   Some agda syntax magic goes here, so that:
125 |
126 |     [ descr ::= mods & args ]
127 |   desugars into
128 |     TheCommand {descr} mods args
129 |   and
130 |     descr [ pos ] sub
131 |   desugars into
132 |     SubCommand {sub = desc} pos sub
133 |
134 |   These can't be just smart constructors though, since they're meant
135 |   to appear in patterns, I think.
136 | -}
137 |
138 | public export
139 | (.update) : {arg : Arguments} -> (ps : ParsedArgumentsT Maybe arg) ->
140 |   String -> Error $ ParsedArgumentsT Maybe arg
141 | (.update) {arg = MkArguments _ (Some d ) parser} (Just _) _
142 |   = throwE TooManyArguments
143 | (.update) {arg = MkArguments _ (Some d ) parser} Nothing x
144 |   = fromEither $ bimap CouldNotParse Just (parser x)
145 | (.update) {arg = MkArguments _ (ALot ds) parser} old     x
146 |   = let _ = openMagma $ Maybe.rawMagma ds
147 |   in do
148 |     p <- fromEither $ bimap CouldNotParse Just $ parser x
149 |     pure (old <+> p)
150 |
151 | public export
152 | (.parse) : (args : Arguments) ->
153 |   (old : ParsedArgumentsT Maybe args) ->
154 |   List String ->
155 |   Error $ ParsedArgumentsT Maybe args
156 | args.parse old = foldl (\u,s => do {acc <- u; acc.update s}) (pure old)
157 |
158 | public export
159 | initParsedCommand : {cmd : Command nm} -> ParsedCommandT Maybe Maybe nm cmd
160 | initParsedCommand = MkParsedCommandT initNothing Nothing
161 |