
  0 | module Collie.Options.Usual
  1 | 
  2 | import Collie.Options.Domain
  3 | import Data.Magma
  4 | import Data.String
  5 | 
  6 | %default total
  7 | 
  8 | public export
  9 | none : Arguments
 10 | none = MkArguments
 11 |      False
 12 |      (Some Void)
 13 |      (const $ Left "Argument provided when none expected")
 14 | 
 15 | public export
 16 | lotsOf : Arguments -> Arguments
 17 | lotsOf args@(MkArguments {}) = MkArguments
 18 |   False
 19 |   (ALot (List.rawMagma (Carrier args.domain)))
 20 |   (((:: []) <$>) . args.rawParser)
 21 | 
 22 | public export
 23 | Regex : Type
 24 | Regex = String
 25 | 
 26 | public export
 27 | regex : Arguments
 28 | regex = MkArguments False (Some Regex) pure
 29 | 
 30 | public export
 31 | FilePath : Type
 32 | FilePath = String
 33 | 
 34 | public export
 35 | filePath : Arguments
 36 | filePath = MkArguments False (Some FilePath) pure
 37 | 
 38 | public export
 39 | Regexp : Type
 40 | Regexp = String
 41 | 
 42 | public export
 43 | regexp : Arguments
 44 | regexp = MkArguments False (Some Regexp) pure
 45 | 
 46 | public export
 47 | Url : Type
 48 | Url = String
 49 | 
 50 | public export
 51 | url : Arguments
 52 | url = MkArguments False (Some Url) pure
 53 | 
 54 | public export
 55 | nat : Arguments
 56 | -- TODO: Parse naturals properly
 57 | nat = MkArguments False (Some Nat) $ \ str =>
 58 |   case parsePositive str of
 59 |     Nothing => Left $ "Expect a natural number, got: " ++ str
 60 |     Just n => pure n
 61 | 
 62 | public export
 63 | integer : Arguments
 64 | integer = MkArguments False (Some Integer) $ \ str =>
 65 |   case parseInteger str of
 66 |     Nothing => Left $ "Expect an integer, got: " ++ str
 67 |     Just n => pure n
 68 |