System.Console.GetOpt


   0 | ||| This library provides facilities for parsing the command-line options
   1 | ||| in a standalone program. It is essentially an Idris port of the GNU getopt library.
   2 | ||| (Actually, it is an Idris port of the [corresponding Haskell module]
   3 | ||| (http://hackage.haskell.org/package/base-4.14.1.0/docs/System-Console-GetOpt.html)).
   4 | module System.Console.GetOpt
   5 | 
   6 | import Data.List
   7 | import Data.List1
   8 | import Data.String
   9 | import Data.These
  10 | 
  11 | %default total
  12 | 
  13 | ||| What to do with options following non-options
  14 | public export
  15 | data ArgOrder a =
  16 |   ||| no option processing after first non-option
  17 |   RequireOrder                |
  18 |   ||| freely intersperse options and non-options
  19 |   Permute                     |
  20 |   ||| wrap non-options into options
  21 |   ReturnInOrder (String -> a) |
  22 |   ||| wrap non-options into options (or fail, if can't)
  23 |   ReturnInOrder' (String -> Either String a)
  24 | 
  25 | export
  26 | Functor ArgOrder where
  27 |   map _ RequireOrder       = RequireOrder
  28 |   map _ Permute            = Permute
  29 |   map f (ReturnInOrder g)  = ReturnInOrder (f . g)
  30 |   map f (ReturnInOrder' g) = ReturnInOrder' (map f . g)
  31 | 
  32 | ||| Describes whether an option takes an argument or not, and if so
  33 | ||| how the argument is injected into a value of type `a`.
  34 | public export
  35 | data ArgDescr a =
  36 |    ||| no argument expected
  37 |    NoArg                    a                       |
  38 |    ||| option requires argument
  39 |    ReqArg  (String       -> a) String               |
  40 |    ||| option requires argument and may fail during parsing
  41 |    ReqArg' (String       -> Either String a) String |
  42 |    ||| optional argument
  43 |    OptArg  (Maybe String -> a) String               |
  44 |    ||| optional argument and may fail during parsing
  45 |    OptArg' (Maybe String -> Either String a) String
  46 | 
  47 | export
  48 | Functor ArgDescr where
  49 |   map f (NoArg x)     = NoArg (f x)
  50 |   map f (ReqArg g x)  = ReqArg (f . g) x
  51 |   map f (ReqArg' g x) = ReqArg' (map f . g) x
  52 |   map f (OptArg g x)  = OptArg (f . g) x
  53 |   map f (OptArg' g x) = OptArg' (map f . g) x
  54 | 
  55 | ||| Each `OptDescr` describes a single option.
  56 | |||
  57 | ||| The arguments to 'Option' are:
  58 | |||
  59 | ||| * list of short option characters
  60 | ||| * list of long option strings (without \"--\")
  61 | ||| * argument descriptor
  62 | ||| * explanation of option for user
  63 | public export
  64 | record OptDescr a where
  65 |   constructor MkOpt
  66 |   ||| list of short option characters
  67 |   shortNames  : List Char
  68 |   ||| list of long option strings (without "--")
  69 |   longNames   : List String
  70 |   ||| argument descriptor
  71 |   argDescr    : ArgDescr a
  72 |   ||| explanation of option for user
  73 |   description : String
  74 | 
  75 | export
  76 | Functor OptDescr where
  77 |   map f = { argDescr $= map f }
  78 | 
  79 | -- kind of cmd line arg (internal use only):
  80 | data OptKind a
  81 |    = Opt       a                --    an option
  82 |    | UnreqOpt  String           --    an un-recognized option
  83 |    | NonOpt    String           --    a non-option
  84 |    | EndOfOpts                  --    end-of-options marker (i.e. "--")
  85 |    | OptErr    String           --    something went wrong...
  86 | 
  87 | optOrErr : Either String a -> OptKind a
  88 | optOrErr = either OptErr Opt
  89 | 
  90 | --------------------------------------------------------------------------------
  91 | --          Printing Usage Info
  92 | --------------------------------------------------------------------------------
  93 | 
  94 | fmtShort : ArgDescr a -> Char -> String
  95 | fmtShort (NoArg   _   ) so = "-" ++ singleton so
  96 | fmtShort (ReqArg  _ ad) so = "-" ++ singleton so ++ " " ++ ad
  97 | fmtShort (ReqArg' _ ad) so = "-" ++ singleton so ++ " " ++ ad
  98 | fmtShort (OptArg  _ ad) so = "-" ++ singleton so ++ "[" ++ ad ++ "]"
  99 | fmtShort (OptArg' _ ad) so = "-" ++ singleton so ++ "[" ++ ad ++ "]"
 100 | 
 101 | fmtLong : ArgDescr a -> String -> String
 102 | fmtLong (NoArg   _   ) lo = "--" ++ lo
 103 | fmtLong (ReqArg  _ ad) lo = "--" ++ lo ++ "=" ++ ad
 104 | fmtLong (ReqArg' _ ad) lo = "--" ++ lo ++ "=" ++ ad
 105 | fmtLong (OptArg  _ ad) lo = "--" ++ lo ++ "[=" ++ ad ++ "]"
 106 | fmtLong (OptArg' _ ad) lo = "--" ++ lo ++ "[=" ++ ad ++ "]"
 107 | 
 108 | fmtOpt : OptDescr a -> List (String,String,String)
 109 | fmtOpt (MkOpt sos los ad descr) =
 110 |   let sosFmt = concat $ intersperse ", " (map (fmtShort ad) sos)
 111 |       losFmt = concat $ intersperse ", " (map (fmtLong ad) los)
 112 |       (h ::: t) = lines1 descr in
 113 |       (sosFmt,losFmt,h) :: map (\s => ("","",s)) t
 114 |   where lines1 : String -> List1 String
 115 |         lines1 s = case lines s of
 116 |                         [] => "" ::: []
 117 |                         (x :: xs) => x ::: xs
 118 | 
 119 | ||| Return a string describing the usage of a command, derived from
 120 | ||| the header (first argument) and the options described by the
 121 | ||| second argument.
 122 | public export
 123 | usageInfo : (header : String) -> List (OptDescr a) -> String
 124 | usageInfo header optDescr =
 125 |   let (ss,ls,ds)   = (unzip3 . concatMap fmtOpt) optDescr
 126 |       paste        = \x,y,z => "  " ++ x ++ "  " ++ y ++ "  " ++ z
 127 |       table        = zipWith3 paste (sameLen ss) (sameLen ls) ds
 128 |    in unlines $ header :: table
 129 | 
 130 |   where flushLeft : Nat -> String -> String
 131 |         flushLeft n s = s ++ pack (replicate (n `minus` length s) ' ')
 132 | 
 133 |         sameLen : List String -> List String
 134 |         sameLen ss = let len = foldl (\n => max n . length) 0 ss
 135 |                       in map (flushLeft len) ss
 136 | 
 137 | --------------------------------------------------------------------------------
 138 | --          Error Formatting
 139 | --------------------------------------------------------------------------------
 140 | 
 141 | errAmbig : List (OptDescr a) -> (optStr : String) -> OptKind a
 142 | errAmbig ods s = let h = "option `" ++ s ++ "' is ambiguous; could be one of:"
 143 |                   in OptErr (usageInfo h ods)
 144 | 
 145 | errReq : String -> (optStr : String) -> OptKind a
 146 | errReq d s = OptErr ("option `" ++ s ++ "' requires an argument " ++ d ++ "\n")
 147 | 
 148 | errNoArg : (optStr : String) -> OptKind a
 149 | errNoArg s = OptErr ("option `" ++ s ++ "' doesn't allow an argument\n")
 150 | 
 151 | --------------------------------------------------------------------------------
 152 | --          Parsing Options
 153 | --------------------------------------------------------------------------------
 154 | 
 155 | ||| Result of parsing the command line arguments according to a list
 156 | ||| of `OptDescr`s. (see also function `getOpt`).
 157 | public export
 158 | record Result a where
 159 |   constructor MkResult
 160 |   ||| List of successfully parsed options
 161 |   options      : List a
 162 | 
 163 |   ||| List of non-options (other command line arguments)
 164 |   nonOptions   : List String
 165 | 
 166 |   ||| List of unrecognized options.
 167 |   unrecognized : List String
 168 | 
 169 |   ||| Errors during option parsing. These occur, for instance, when
 170 |   ||| an option requires an additional argument but none was given.
 171 |   errors       : List String
 172 | 
 173 | public export
 174 | emptyRes : Result a
 175 | emptyRes = MkResult [] [] [] []
 176 | 
 177 | export
 178 | Functor Result where
 179 |   map f = { options $= map f }
 180 | 
 181 | OptFun : Type -> Type
 182 | OptFun a = List String -> List (OptDescr a) -> (OptKind a,List String)
 183 | 
 184 | longOpt : String -> OptFun a
 185 | longOpt ls rs descs =
 186 |   let (opt,arg) = break ('=' ==) ls
 187 |       getWith   = \p => filter (any (p opt) . longNames) descs
 188 |       exact     = getWith (==)
 189 |       options   = if null exact then getWith isPrefixOf else exact
 190 |       ads       = map argDescr options
 191 |       os        = "--" ++ opt
 192 |    in case (ads, unpack arg, rs) of
 193 |            (_ :: _ :: _ , _      ,  r        ) => (errAmbig options os, r)
 194 |            ([NoArg  a  ], []     ,  r        ) => (Opt a, r)
 195 |            ([NoArg  a  ], c :: _ ,  r        ) => (errNoArg os,r)
 196 | --                        ^ this is known (but not proven) to be '='
 197 | 
 198 |            ([ReqArg _ d], []     ,  []       ) => (errReq d os,[])
 199 |            ([ReqArg f _], []     ,  (r::rest)) => (Opt $ f r,rest)
 200 |            ([ReqArg f _], c :: xs,  r        ) => (Opt $ f (pack xs),r)
 201 | --                        ^ this is known (but not proven) to be '='
 202 | 
 203 |            ([ReqArg' _ d], []     ,  []       ) => (errReq d os,[])
 204 |            ([ReqArg' f _], []     ,  (r::rest)) => (optOrErr $ f r, rest)
 205 |            ([ReqArg' f _], c :: xs,  r        ) => (optOrErr $ f (pack xs) ,r)
 206 | --                         ^ this is known (but not proven) to be '='
 207 | 
 208 |            ([OptArg f _], []     ,  r        ) => (Opt $ f Nothing,r)
 209 |            ([OptArg f _], c :: xs,  r        ) => (Opt . f . Just $ pack xs,r)
 210 | --                        ^ this is known (but not proven) to be '='
 211 | 
 212 |            ([OptArg' f _], []     ,  r        ) => (optOrErr $ f Nothing, r)
 213 |            ([OptArg' f _], c :: xs,  r        ) => (optOrErr . f . Just $ pack xs, r)
 214 | --                         ^ this is known (but not proven) to be '='
 215 | 
 216 |            ([]          , _      ,  r        ) => (UnreqOpt $ "--" ++ ls,r)
 217 | 
 218 | shortOpt : Char -> String -> OptFun a
 219 | shortOpt y ys rs descs =
 220 |   let options = filter (elem y . shortNames) descs
 221 |       ads     = map argDescr options
 222 |       mkOs    = strCons '-'
 223 |       os      = mkOs (singleton y)
 224 |    in case (ads,ys,rs) of
 225 |            (_ :: _ :: _  , _ ,  r        ) => (errAmbig options os, r)
 226 |            ([NoArg   a  ], "",  r        ) => (Opt a,r)
 227 |            ([NoArg   a  ], s ,  r        ) => (Opt a, mkOs s :: r)
 228 |            ([ReqArg  _ d], "",  []       ) => (errReq d os, [])
 229 |            ([ReqArg  f _], "",  (r::rest)) => (Opt $ f r, rest)
 230 |            ([ReqArg  f _], s ,  r        ) => (Opt $ f s, r)
 231 |            ([ReqArg' _ d], "",  []       ) => (errReq d os, [])
 232 |            ([ReqArg' f _], "",  (r::rest)) => (optOrErr $ f r, rest)
 233 |            ([ReqArg' f _], s ,  r        ) => (optOrErr $ f s, r)
 234 |            ([OptArg  f _], "",  r        ) => (Opt $ f Nothing, r)
 235 |            ([OptArg  f _], s ,  r        ) => (Opt . f $ Just s, r)
 236 |            ([OptArg' f _], "",  r        ) => (optOrErr $ f Nothing, r)
 237 |            ([OptArg' f _], s ,  r        ) => (optOrErr . f $ Just s, r)
 238 |            ([]           , "",  r        ) => (UnreqOpt os, r)
 239 |            ([]           , s ,  r        ) => (UnreqOpt os, mkOs s :: r)
 240 | 
 241 | 
 242 | -- take a look at the next cmd line arg and decide what to do with it
 243 | getNext : List Char -> OptFun a
 244 | getNext ('-'::'-'::[]) r _        = (EndOfOpts,r)
 245 | getNext ('-'::'-'::xs) r descs    = longOpt (pack xs) r descs
 246 | getNext ('-':: x ::xs) r descs    = shortOpt x (pack xs) r descs
 247 | getNext a              r _        = (NonOpt $ pack a,r)
 248 | 
 249 | ||| Process the command-line, and return the list of values that matched
 250 | ||| (and those that didn't). The arguments are:
 251 | |||
 252 | ||| * The order requirements (see `ArgOrder`)
 253 | |||
 254 | ||| * The option descriptions (see `OptDescr`)
 255 | |||
 256 | ||| * The actual command line arguments (presumably got from
 257 | |||   `System.getArgs`).
 258 | export
 259 | getOpt :  ArgOrder a                         -- non-option handling
 260 |        -> List (OptDescr a)                  -- option descriptors
 261 |        -> (args : List String)               -- the command-line arguments
 262 |        -> Result a
 263 | getOpt _        _        []         =  emptyRes
 264 | getOpt ordering descs (arg::args)   =
 265 |   let (opt,rest) = getNext (unpack arg) args descs
 266 |       res        = getOpt ordering descs (assert_smaller args rest)
 267 |    in case (opt,ordering) of
 268 |            (Opt x, _)                    => {options $= (x::)} res
 269 |            (UnreqOpt x, _)               => {unrecognized $= (x::)} res
 270 |            (NonOpt x, RequireOrder)      => MkResult [] (x::rest) [] []
 271 |            (NonOpt x, Permute)           => {nonOptions $= (x::)} res
 272 |            (NonOpt x, ReturnInOrder f)   => {options $= (f x::)} res
 273 |            (NonOpt x, ReturnInOrder' f)  => updOptOrErr (f x) res
 274 |            (EndOfOpts, RequireOrder)     => MkResult [] rest [] []
 275 |            (EndOfOpts, Permute)          => MkResult [] rest [] []
 276 |            (EndOfOpts, ReturnInOrder f)  => MkResult (map f rest) [] [] []
 277 |            (EndOfOpts, ReturnInOrder' f) => parseRest f rest
 278 |            (OptErr e, _)                 => {errors $= (e::)} res
 279 |   where
 280 |     updOptOrErr : Either String a -> Result a -> Result a
 281 |     updOptOrErr (Left e)  = {errors $= (e::)}
 282 |     updOptOrErr (Right o) = {options $= (o::)}
 283 | 
 284 |     parseRest : (String -> Either String a) -> (rest : List String) -> Result a
 285 |     parseRest f rest =
 286 |       these' [] [] (\es, os => MkResult os [] [] es) $
 287 |         for rest $ fromEither . mapFst pure . f
 288 | 
 289 | ||| Parse the command-line like `getOpt`, but allow each option parser to do
 290 | ||| additional work in some `Applicative`.
 291 | |||
 292 | ||| Place, notice that options parsing is done first, i.e. if you use
 293 | ||| applicatives that can have a failure semantics, you will lose all errors
 294 | ||| reported inside the `Result` type in case of any option parsing fails.
 295 | export
 296 | getOpt' :  Applicative f
 297 |         => ArgOrder (f a)
 298 |         -> List (OptDescr $ f a)
 299 |         -> (args : List String)
 300 |         -> f $ Result a
 301 | getOpt' ao os args = do
 302 |   let MkResult opts nonOpts unrec errs = getOpt ao os args
 303 |   sequence opts <&> \opts' => MkResult opts' nonOpts unrec errs
 304 |