0 | module Collie.Options.Domain
 1 |
 2 | import Data.Magma
 3 | import Collie.Error
 4 |
 5 | %default total
 6 |
 7 | public export
 8 | data Domain : Type where
 9 |   Some : (d  : Type    ) -> Domain
10 |   ALot : (ds : RawMagma) -> Domain
11 |
12 | public export
13 | elimDomain : {p : Domain -> Type} ->
14 |   (dSome : (d  : Type    ) -> p (Some d )) ->
15 |   (dALot : (ds : RawMagma) -> p (ALot ds)) ->
16 |   (d : Domain) -> p d
17 | elimDomain dSome dALot (Some d ) = dSome d
18 | elimDomain dSome dALot (ALot ds) = dALot ds
19 |
20 | public export
21 | Carrier : Domain -> Type
22 | Carrier = elimDomain id (\ds => ds.Carrier)
23 |
24 | public export
25 | Parser : Domain -> Type
26 | Parser d = String -> Either String $ Carrier d
27 |
28 | public export
29 | record Arguments where
30 |   constructor MkArguments
31 |   required  : Bool
32 |   domain    : Domain
33 |   rawParser : Parser domain
34 |
35 | public export
36 | (.parser) : (arg : Arguments) -> String -> Error (Carrier arg.domain)
37 | arg .parser x = fromEither $ mapFst CouldNotParse (arg.rawParser x)
38 |
39 | public export
40 | ParsedArgumentsT : (f : Type -> Type) -> Arguments -> Type
41 | ParsedArgumentsT f ducer = f $ Carrier ducer.domain
42 |
43 | public export
44 | ParsedArguments : Arguments -> Type
45 | ParsedArguments ducer
46 |   = ParsedArgumentsT
47 |     (if ducer.required then id else Maybe)
48 |     ducer
49 |