
   0 | module Text.WebIDL.Types.Argument
   1 | 
   2 | import Data.Bitraversable
   3 | import Data.Traversable
   4 | import Derive.Prelude
   5 | import Text.WebIDL.Types.Attribute
   6 | import Text.WebIDL.Types.Identifier
   7 | import Text.WebIDL.Types.Numbers
   8 | import Text.WebIDL.Types.StringLit
   9 | import Text.WebIDL.Types.Type
  10 | 
  11 | %language ElabReflection
  12 | 
  13 | ||| ConstValue ::
  14 | |||     BooleanLiteral
  15 | |||     FloatLiteral
  16 | |||     integer
  17 | |||
  18 | ||| BooleanLiteral ::
  19 | |||     true
  20 | |||     false
  21 | public export
  22 | data ConstValue = B Bool | F FloatLit | I IntLit
  23 | 
  24 | %runElab derive "ConstValue" [Eq,Show,HasAttributes]
  25 | 
  26 | ||| Default ::
  27 | |||     = DefaultValue
  28 | |||     ε
  29 | |||
  30 | ||| (part of Default)] DefaultValue ::
  31 | |||     ConstValue
  32 | |||     string
  33 | |||     [ ]
  34 | |||     { }
  35 | |||     null
  36 | public export
  37 | data Default =
  38 |     None
  39 |   | EmptyList
  40 |   | EmptySet
  41 |   | Null
  42 |   | S StringLit
  43 |   | C ConstValue
  44 | 
  45 | %runElab derive "Default" [Eq,Show,HasAttributes]
  46 | 
  47 | ||| ArgumentName ::
  48 | |||     ArgumentNameKeyword
  49 | |||     identifier
  50 | public export
  51 | record ArgumentName where
  52 |   constructor MkArgName
  53 |   value : String
  54 | 
  55 | %runElab derive "ArgumentName" [Eq,Show,HasAttributes]
  56 | 
  57 | public export
  58 | record ArgF (a : Type) (b : Type) where
  59 |   constructor MkArg
  60 |   attrs    : a
  61 |   type     : IdlTypeF a b
  62 |   name     : ArgumentName
  63 | 
  64 | %runElab derive "ArgF" [Eq,Show]
  65 | 
  66 | public export
  67 | Arg : Type
  68 | Arg = ArgF ExtAttributeList Identifier
  69 | 
  70 | public export
  71 | record OptArgF (a : Type) (b : Type) where
  72 |   constructor MkOptArg
  73 |   attrs     : a
  74 |   typeAttrs : a
  75 |   type      : IdlTypeF a b
  76 |   name      : ArgumentName
  77 |   def       : Default
  78 | 
  79 | %runElab derive "OptArgF" [Eq,Show]
  80 | 
  81 | public export
  82 | OptArg : Type
  83 | OptArg = OptArgF ExtAttributeList Identifier
  84 | 
  85 | ||| ArgumentList ::
  86 | |||     Argument Arguments
  87 | |||     ε
  88 | |||
  89 | ||| Arguments ::
  90 | |||     , Argument Arguments
  91 | |||     ε
  92 | |||
  93 | ||| Argument ::
  94 | |||     ExtendedAttributeList ArgumentRest
  95 | |||
  96 | ||| Ellipsis ::
  97 | |||     ...
  98 | |||     ε
  99 | ||| ArgumentRest ::
 100 | |||     optional TypeWithExtendedAttributes ArgumentName Default
 101 | |||     Type Ellipsis ArgumentName
 102 | public export
 103 | data ArgumentListF : (a : Type) -> (b : Type) -> Type where
 104 |   VarArg :  (args : List $ ArgF a b)
 105 |          -> (vararg : ArgF a b)
 106 |          -> ArgumentListF a b
 107 | 
 108 |   NoVarArg :  (args : List $ ArgF a b)
 109 |            -> (optArgs : List $ OptArgF a b)
 110 |            -> ArgumentListF a b
 111 | 
 112 | %runElab derive "ArgumentListF" [Eq,Show]
 113 | 
 114 | public export
 115 | ArgumentList : Type
 116 | ArgumentList = ArgumentListF ExtAttributeList Identifier
 117 | 
 118 | --------------------------------------------------------------------------------
 119 | --          Implementations
 120 | --------------------------------------------------------------------------------
 121 | 
 122 | mutual
 123 |   export
 124 |   Bifunctor ArgF where bimap = assert_total bimapDefault
 125 | 
 126 |   export
 127 |   Bifoldable ArgF where bifoldr = bifoldrDefault
 128 | 
 129 |   export
 130 |   Bitraversable ArgF where
 131 |     bitraverse f g (MkArg a t n) =
 132 |       [| MkArg (f a) (bitraverse f g t) (pure n) |]
 133 | 
 134 |   export
 135 |   Functor (ArgF a) where map = bimap id
 136 | 
 137 |   export
 138 |   Foldable (ArgF a) where foldr = bifoldr (const id)
 139 | 
 140 |   export
 141 |   Traversable (ArgF a) where traverse = bitraverse pure
 142 | 
 143 | mutual
 144 |   export
 145 |   Bifunctor OptArgF where bimap = assert_total bimapDefault
 146 | 
 147 |   export
 148 |   Bifoldable OptArgF where bifoldr = bifoldrDefault
 149 | 
 150 |   export
 151 |   Bitraversable OptArgF where
 152 |     bitraverse f g (MkOptArg a1 a2 t n d) =
 153 |       [| MkOptArg (f a1) (f a2) (bitraverse f g t) (pure n) (pure d) |]
 154 | 
 155 |   export
 156 |   Functor (OptArgF a) where map = bimap id
 157 | 
 158 |   export
 159 |   Foldable (OptArgF a) where foldr = bifoldr (const id)
 160 | 
 161 |   export
 162 |   Traversable (OptArgF a) where traverse = bitraverse pure
 163 | 
 164 | mutual
 165 |   export
 166 |   Bifunctor ArgumentListF where bimap = assert_total bimapDefault
 167 | 
 168 |   export
 169 |   Bifoldable ArgumentListF where bifoldr = bifoldrDefault
 170 | 
 171 |   export
 172 |   Bitraversable ArgumentListF where
 173 |     bitraverse f g (VarArg as a) =
 174 |       [| VarArg (traverse (bitraverse f g) as) (bitraverse f g a) |]
 175 |     bitraverse f g (NoVarArg as os) =
 176 |       [| NoVarArg
 177 |           (traverse (bitraverse f g) as)
 178 |           (traverse (bitraverse f g) os)
 179 |       |]
 180 | 
 181 |   export
 182 |   Functor (ArgumentListF a) where map = bimap id
 183 | 
 184 |   export
 185 |   Foldable (ArgumentListF a) where foldr = bifoldr (const id)
 186 | 
 187 |   export
 188 |   Traversable (ArgumentListF a) where traverse = bitraverse pure
 189 | 
 190 |   export
 191 |   HasAttributes a => HasAttributes (ArgumentListF a b) where
 192 |     attributes = bifoldMap attributes (const Nil)
 193 |