Idris ArgParse

A simple argument parser written in Idris.

What

I was stuck on a train with no internet for several hours and decided to create a naive argument parser in Idris. It is naive in the sense that I have not written combinators before (see optparse-applicative) nor could think of a CmdOptions style for implementation.

Library consumers must declare their options data type and a means to convert an Arg to an instance of their options data type. The library takes care of parsing the args string to args and application of the conversion.

This code is cheap and dirty, and could do with some improvement. Explore other implementation styles is something for the future. Having used both optparse-applicative and CmdOptions I am, personally, not completely swayed to either style. If you can convince me great, if not try harder.

Example

For a more in-depth example see ArgParse/Test.idr

||| Options Data Type
record MyFirstOpts where
  constructor MkOpts
  from    : Maybe String
  verbose : Bool
  help    : Bool
  version : Bool
  files   : List String

||| Default settings
defOpts : Opts
defOpts = MkOpts Nothing False False False Nil

||| Convert Arguments into Options
convOpts : Arg -> Opts -> Maybe Opts
convOpts (File f)     o = Just $ record {args = f :: args } o

convOpts (KeyValue k v) o =
  case k of
    "from"    => Just $ record {from = Just v} o
    otherwise => Nothing

convOpts (Flag x) = case x of
    "verbose" => Just $ record {verbose = True} o
    "help"    => Just $ record {help    = True} o
    "version" => Just $ record {version = True} o
    otherwise => Nothing


main : IO ()
main = do
  (a::args) <- getArgs
  let os = parseArgs defOpts (convOpts) args
  print os