0 | module Stellar.CLI

  2 | import public Stellar.API

  3 | import public Stellar.API.Morphism

  4 | import public Stellar.API.Maybe

  5 | import public Stellar.API.Maybe

  6 | import Data.List.Quantifiers

  7 | import Data.List1.Quantifiers

  8 | import Data.List1

  9 | import public Data.String

 10 | import Data.DPair

 11 | import Data.String.Parser

 13 | import System

 14 | import System.File

 15 | import Data.Either

 16 | import Control.Monad.Error.Either

 17 | import Control.Monad.Maybe

 19 | import Debug.Trace

 21 | %hide Data.List.Alternating.infixl.(+>)

 22 | %hide Data.String.Extra.infixl.(+>)

 23 | %hide Data.List.Alternating.infixr.(<+)

 24 | %hide Data.String.Extra.infixr.(<+)

 27 | public export

 28 | CLI : API

 29 | CLI = List String :- String

 33 | cli : HasIO io => (List String -> io String) -> io ()

 34 | cli f = getArgs >>= f >>= putStrLn

 38 | cli' : HasIO io => Costate (Lift io CLI) -> io ()

 39 | cli' = cli . extract

 41 | covering export %hint

 42 | parseString : Parser String

 43 | parseString = takeWhile (not . isSpace)

 45 | indexAny : {0 p : a -> Type} ->

 46 |            (xs : List a) -> Any p xs -> a

 47 | indexAny (x :: xs) (Here y) = x

 48 | indexAny (x :: xs) (There ys) = indexAny xs ys

 50 | indexAny1 : {0 p : a -> Type} ->

 51 |            (xs : List1 a) -> Any p xs -> a

 52 | indexAny1 (x ::: _) (Here y) = x

 53 | indexAny1 (_ ::: xs) (There ys) = indexAny xs ys

 55 | public export

 56 | checkNonEmpty : String -> Type

 57 | checkNonEmpty str with (strM str)

 58 |   checkNonEmpty "" | StrNil = Void

 59 |   checkNonEmpty (strCons x xs) | (StrCons x xs) = Unit

 61 | Uninhabited (Z === S n) where

 62 |   uninhabited _ impossible

 64 | headNonEmpty : (str : String) -> (prf : checkNonEmpty str) => Char

 65 | headNonEmpty str {prf} with (strM str)

 66 |   headNonEmpty "" {prf} | StrNil = absurd prf

 67 |   headNonEmpty (strCons x xs) {prf} | (StrCons x xs) = x

 70 | namespace CLI

 71 |   public export

 72 |   record Flag where

 73 |     constructor MkFlag

 74 |     {default Nothing prefix_ : Maybe String}

 75 |     fullFlag : String

 76 |     {auto check : checkNonEmpty fullFlag}

 78 |   export

 79 |   fromString : (str : String) -> {auto check : checkNonEmpty str} -> Flag

 80 |   fromString str = MkFlag str

 82 |   parserFromAbirvFlag : (str : String) -> (prf : checkNonEmpty str) => Parser ()

 83 |   parserFromAbirvFlag str =

 84 |     ignore (string "--\{str}"  <|> string "-\{toLower $ String.singleton (headNonEmpty str)}")

 86 |   public export

 87 |   record GenericCommand where

 88 |     constructor MkGenericCommand

 89 |     input : Type

 90 |     parseInput : Parser input

 91 |     output : Type

 92 |     printOutput : Show output

 93 |     -- a string that identifies the command when debugging incorrect parsing

 94 |     debug : String

 95 |     doc : String

 97 |   public export

 98 |   record FlagCommand where

 99 |     constructor MkFlagCommand

100 |     input : Type

101 |     {auto parser : Parser input}

102 |     output : Type

103 |     {auto show : Show output}

104 |     flag : Flag

105 |     doc : String

107 |   public export

108 |   interface ToCommand t where

109 |     toCmd : t -> GenericCommand

111 |   parserFromFullFlag : Flag -> Parser ()

112 |   parserFromFullFlag (MkFlag {prefix_ = Nothing} fullFlag) = parserFromAbirvFlag fullFlag

113 |   parserFromFullFlag (MkFlag {prefix_ = Just x} fullFlag) = string x *> space *> parserFromAbirvFlag fullFlag

115 |   public export

116 |   flagToGeneric : FlagCommand -> GenericCommand

117 |   flagToGeneric (MkFlagCommand i {parser} o {show = ishow} f d)

118 |     = MkGenericCommand

119 |       { input = i

120 |       , parseInput = (parserFromFullFlag f *> space *> parser)

121 |       , output = o

122 |       , printOutput = ishow

123 |       , debug = f.fullFlag

124 |       , doc = show d

125 |       }

127 |   public export

128 |   ToCommand GenericCommand where

129 |     toCmd = id

131 |   public export

132 |   ToCommand FlagCommand where

133 |     toCmd = flagToGeneric

135 |   public export

136 |   (.toAPI) : GenericCommand -> API

137 |   (.toAPI) cmd = input cmd :- output cmd

139 |   public export

140 |   Commands : Type

141 |   Commands = List1 GenericCommand

143 |   public export

144 |   mapList1 : (a -> b) -> List1 a -> List1 b

145 |   mapList1 f ls = f ls.head ::: map f ls.tail

147 |   public export

148 |   fromGeneric : {0 xs : List1 Type} -> All (\x => x) xs -> (cmds : All ToCommand xs) => List1 GenericCommand

149 |   fromGeneric (x ::: []) {cmds = c ::: cds} = toCmd x ::: []

150 |   fromGeneric (x ::: y :: xs) {cmds = c ::: cdz :: cds}

151 |   = let (y ::: ys) = assert_total $ fromGeneric (y ::: xs) @{cdz ::: cds}

152 |     in toCmd x ::: y :: ys

154 |   public export

155 |   GetAPI : Commands -> API

156 |   GetAPI (cmd ::: []) = cmd.toAPI

157 |   GetAPI cmds@(_ ::: _::_) = (i : Any input cmds) !> output (indexAny1 cmds i)

159 |   public export

160 |   GetAPI' : {0 xs : List1 Type} -> All (\x => x) xs -> (cmds : All ToCommand xs) => API

161 |   GetAPI' xs = GetAPI $ fromGeneric xs

163 |   public export

164 |   InOut : List1 API -> API

165 |   InOut (head ::: []) = head

166 |   InOut (head ::: (x :: xs)) = head + assert_total (InOut (x ::: xs))

168 |   anyToAny1 : Any p (x :: xs) -> Any p (x ::: xs)

169 |   anyToAny1 (Here y) = Here y

170 |   anyToAny1 (There y) = There y

172 |   toIndexAny : {0 a : Type} -> {0 p, q : a -> Type} ->

173 |                {0 x : a} -> {0 xs : List a} -> {ys : Any p (x :: xs)} ->

174 |                q (indexAny1 (x ::: xs) (anyToAny1 ys)) -> q (indexAny (x :: xs) ys)

175 |   toIndexAny {ys = (Here z)} y = y

176 |   toIndexAny {ys = (There z)} y = y

178 |   AnyToChoice : {0 a : Type} -> {0 p, q : a -> Type} -> {xs : List1 a} ->

179 |                 ((i : Any p xs) !> q (indexAny1 xs i)) =&> InOut (map (\x => p x :- q x) xs)

180 |   AnyToChoice {xs = (v ::: [])} = !! \(Here x) => x ## id

181 |   AnyToChoice {xs = (v ::: (x :: xs))} =

182 |     let rec = (assert_total $ AnyToChoice {p, q, xs = (x ::: xs)}).continuation

183 |     in !! \case (Here y) => <+ y ## id

184 |                 (There y) => let r1 ## r2 = rec (anyToAny1 y) in +> r1 ## toIndexAny {p, q} . r2

186 |   export

187 |   toChoice : (cmds : Commands) -> GetAPI cmds =&> InOut (CLI.mapList1 (.toAPI) cmds)

188 |   toChoice (cmd ::: []) = identity

189 |   toChoice (c1 ::: c2 :: c3) = AnyToChoice {p = input, q = output, xs = c1 ::: c2 :: c3}

192 |   export

193 |   (.parseCommand) : (cmd : GenericCommand) -> List String -> Maybe cmd.input

194 |   (.parseCommand) cmd strs =

195 |     let input = concat (intersperse " " $ drop 1 strs) -- combine the list of args into one string

196 |         parser = parse cmd.parseInput input -- run the parser from the command

197 |     in trace "parsing: \{input}" $ eitherToMaybe (map fst parser) -- drop the Int counting how deep we are in the string

199 | %unbound_implicits off

201 | extend : {0 a : Type} -> {0 p : a -> Type} -> {0 x, y : a} -> {0 xs : List a} ->

202 |          Any p (x ::: xs) -> Any p (y ::: x :: xs)

203 | extend (Here z) = There (Here z)

204 | extend (There z) = There (There z)

207 | parse1Any : (cmd : GenericCommand) -> CLI =&> Any.Maybe cmd.toAPI

208 | parse1Any cmd =

209 |   !! \input => case cmd.parseCommand input of

210 |                     Nothing => Nothing ## absurd

211 |                     Just x => Just x ## show @{cmd.printOutput} . extract

214 | parse1All : (cmd : GenericCommand) -> CLI =&> All.Maybe cmd.toAPI

215 | parse1All cmd =

216 |   !! \input => let

217 |       result = cmd.parseCommand input

218 |    in result ## \case [] => "could not parse command \{show $ cmd.debug}"

219 |                       (Value x) => show @{cmd.printOutput} x

222 | genCLI : (cmds : Commands) -> CLI =&> All.Maybe (GetAPI cmds)

223 | genCLI (cmd ::: []) =

224 |   !! \input => let result = cmd.parseCommand input

225 |                 in result ## \case [] => "Command not found"

226 |                                    (Value x) => show @{cmd.printOutput} x

227 | genCLI cmds@(_:::_::_) =

228 |   !! \input => let result = parseInput cmds input

229 |                 in result ## buildOutput cmds result

230 |   where

231 |     parseInput : (cmds : Commands) -> List String -> Maybe (Any (.input) cmds)

232 |     parseInput (cmd ::: []) strs = map Here (cmd.parseCommand strs)

233 |     parseInput (cmd ::: c :: cmds) strs =

234 |       case cmd.parseCommand strs of

235 |         Just x => Just (Here x)

236 |         Nothing => let xx = assert_total (parseInput (c ::: cmds) strs)

237 |                     in map extend xx

239 |     buildOutput : (cmds : Commands) -> (result : Maybe (Any input cmds)) ->

240 |                   All (\i => (indexAny1 cmds i) .output) result -> String

241 |     buildOutput cmds Nothing x = "Command not found"

242 |     buildOutput cmds (Just y) (Value x) with (indexAny1 cmds y)

243 |       buildOutput cmds (Just y) (Value x) | cmd = show @{cmd.printOutput} x

246 | genCLI' : (cmds : Commands) -> CLI =&> All.Maybe (InOut (CLI.mapList1 (.toAPI) cmds))

247 | genCLI' cmds = genCLI cmds |&> All.map_Maybe (toChoice cmds)