0 | module Collie.Modifiers
  1 |
  2 | import Data.Magma
  3 | import public Data.Record
  4 | import public Collie.Options.Domain
  5 | import public Collie.Error
  6 | import Data.Maybe
  7 |
  8 | %default total
  9 |
 10 | export infix 4 ::=
 11 | public export
 12 | (::=) : {0 a : String -> Type} -> (nm : String) -> a nm -> (nm : String ** a nm)
 13 | (::=) = MkDPair
 14 |
 15 | public export
 16 | Flag : Fields (const Type)
 17 | Flag = [ "description" ::=  String
 18 |        , "default"     ::=  Bool]
 19 |
 20 | public export
 21 | Option : Fields (const Type)
 22 | Option = [ "description" ::= String
 23 |          , "arguments"   ::= Arguments]
 24 |
 25 | public export
 26 | data Modifier : (nm : String) -> Type where
 27 |   MkFlag   : Record DPair.snd Flag   -> Modifier nm
 28 |   MkOption : Record DPair.snd Option -> Modifier nm
 29 |
 30 | public export
 31 | flag : {0 nm : String} ->
 32 |        (description : String) ->
 33 |        {default False defaultVal : Bool} ->
 34 |        Modifier nm
 35 | flag desc = MkFlag $ MkRecord [desc, defaultVal]
 36 |
 37 | public export
 38 | option : {0 nm : String} ->
 39 |          (description : String) ->
 40 |          (arguments : Arguments) ->
 41 |          Modifier nm
 42 | option desc ducer = MkOption $ MkRecord [desc, ducer]
 43 |
 44 | public export
 45 | ParsedModifierT : (f, g : Type -> Type) -> Modifier nm -> Type
 46 | ParsedModifierT f g (MkFlag   flg) = f Bool
 47 | ParsedModifierT f g (MkOption opt) = ParsedArgumentsT g (opt.project "arguments")
 48 |
 49 | public export
 50 | ParsedModifier : Modifier nm -> Type
 51 | ParsedModifier (MkFlag   flg) = Bool
 52 | ParsedModifier (MkOption opt) = ParsedArguments (opt.project "arguments")
 53 |
 54 | public export
 55 | ParsedModifiersT : (f, g : Type -> Type) -> (mods : Fields Modifier) -> Type
 56 | ParsedModifiersT f g mods = Record (\ fld => ParsedModifierT f g (snd fld)) mods
 57 |
 58 | public export
 59 | ParsedModifiers : (mods : Fields Modifier) -> Type
 60 | ParsedModifiers mods = Record (\ fld => ParsedModifier (snd fld)) mods
 61 |
 62 | public export
 63 | updateModifier :
 64 |   {name : String} ->
 65 |   {mod : Modifier name} ->
 66 |   (new : ParsedModifierT Prelude.id Prelude.id mod) ->
 67 |   (old : ParsedModifierT Maybe Maybe mod) ->
 68 |   Error (ParsedModifierT Maybe Maybe mod)
 69 | updateModifier   {mod = MkFlag   flg} new Nothing    = pure $ Just new
 70 | updateModifier   {mod = MkOption opt} new Nothing    = pure $ Just new
 71 | {- TODO: currently, overwrite previous flag, but we can do something
 72 | better here: customise the behaviour, or parameterise by a partial
 73 | monoid -}
 74 | updateModifier   {mod = MkFlag   flg} new (Just old) = pure $ Just new
 75 | updateModifier   {mod = MkOption opt} new (Just old)
 76 |   with ((opt.project "arguments").domain)
 77 |   updateModifier {mod = MkOption opt} new (Just old) | Some d
 78 |     = throwE $ OptionSetTwice name
 79 |   updateModifier {mod = MkOption opt} new (Just old) | ALot ds
 80 |     = let _ = openMagma ds in
 81 |       pure $ Just $ old <+> new
 82 |
 83 | public export
 84 | -- TODO: can we generalise this beyond `Maybe`?
 85 | (.update) : {mods : Fields Modifier} ->
 86 |   (ps : ParsedModifiersT Maybe Maybe mods) ->
 87 |   (pos : Any p mods) ->
 88 |   (p : ParsedModifierT Prelude.id Prelude.id (snd (field pos))) ->
 89 |   Error (ParsedModifiersT Maybe Maybe mods)
 90 | ps.update pos p = MkRecord <$> ps.content.update pos (updateModifier p)
 91 |
 92 | ||| All the flags have a default value. If no value has been set then use
 93 | ||| that default instead.
 94 | public export
 95 | defaulting : {mods : Fields Modifier} ->
 96 |   ParsedModifiersT Maybe f mods -> ParsedModifiersT Prelude.id f mods
 97 | defaulting = map $ \ (str ** mod), val => case mod of
 98 |   MkFlag   flg => fromMaybe (flg.project "default") val
 99 |   MkOption opt => val
100 |
101 | namespace Arguments
102 |
103 |   public export
104 |   finalising :
105 |     Lazy ErrorMsg ->
106 |     (args : Arguments) ->
107 |     ParsedArgumentsT Maybe args ->
108 |     Error (ParsedArguments args)
109 |   finalising err args val with (args.required)
110 |     finalising err args val | True  = case val of
111 |       Nothing => throwE err
112 |       Just val => pure val
113 |     finalising err args val | False = pure val
114 |
115 | namespace Modifier
116 |
117 |   public export
118 |   finalising :
119 |     {nm : String} ->
120 |     (mod : Modifier nm) ->
121 |     ParsedModifierT Maybe Maybe mod ->
122 |     Error (ParsedModifier mod)
123 |   finalising (MkFlag   flg) val = pure $ fromMaybe (flg.project "default") val
124 |   finalising (MkOption opt) val
125 |     = finalising
126 |       (MissingOption nm)
127 |       (opt.project "arguments")
128 |       val
129 |
130 | ||| Setting the flags to their default value and ensuring that the required
131 | ||| options are passed.
132 | public export
133 | finalising :
134 |   {mods : Fields Modifier} ->
135 |   ParsedModifiersT Maybe Maybe mods ->
136 |   Error (ParsedModifiers mods)
137 | finalising = traverse $ \ (str ** mod) => finalising mod
138 |
139 | public export
140 | initNothing : {flds : Fields Modifier} -> ParsedModifiersT Maybe Maybe flds
141 | initNothing = MkRecord $ tabulate $ \ (str ** mod) => case mod of
142 |   MkFlag   flg => Nothing
143 |   MkOption opt => Nothing
144 |