
   0 | module Text.WebIDL.Types.Definition
   1 | 
   2 | import Data.List.Elem
   3 | import Data.SOP
   4 | import Derive.Prelude
   5 | import Text.WebIDL.Types.Attribute
   6 | import Text.WebIDL.Types.Argument
   7 | import Text.WebIDL.Types.Identifier
   8 | import Text.WebIDL.Types.Member
   9 | import Text.WebIDL.Types.StringLit
  10 | import Text.WebIDL.Types.Type
  11 | 
  12 | %hide Language.Reflection.TT.Namespace
  13 | %language ElabReflection
  14 | 
  15 | ||| CallbackRest ::
  16 | |||     identifier = Type ( ArgumentList ) ;
  17 | public export
  18 | record Callback where
  19 |   constructor MkCallback
  20 |   attributes : ExtAttributeList
  21 |   name       : Identifier
  22 |   type       : IdlType
  23 |   args       : ArgumentList
  24 | 
  25 | %runElab derive "Callback" [Eq,Show,HasAttributes]
  26 | 
  27 | ||| CallbackRestOrInterface ::
  28 | |||     CallbackRest
  29 | |||     interface identifier { CallbackInterfaceMembers } ;
  30 | public export
  31 | record CallbackInterface where
  32 |   constructor MkCallbackInterface
  33 |   attributes : ExtAttributeList
  34 |   name       : Identifier
  35 |   members    : CallbackInterfaceMembers
  36 | 
  37 | %runElab derive "CallbackInterface" [Eq,Show,HasAttributes]
  38 | 
  39 | ||| Dictionary ::
  40 | |||     dictionary identifier Inheritance { DictionaryMembers } ;
  41 | public export
  42 | record Dictionary where
  43 |   constructor MkDictionary
  44 |   attributes : ExtAttributeList
  45 |   name       : Identifier
  46 |   inherits   : Inheritance
  47 |   members    : DictionaryMembers
  48 | 
  49 | %runElab derive "Dictionary" [Eq,Show,HasAttributes]
  50 | 
  51 | ||| Enum ::
  52 | |||     enum identifier { EnumValueList } ;
  53 | |||
  54 | ||| EnumValueList ::
  55 | |||     string EnumValueListComma
  56 | |||
  57 | ||| EnumValueListComma ::
  58 | |||     , EnumValueListString
  59 | |||     ε
  60 | |||
  61 | ||| EnumValueListString ::
  62 | |||     string EnumValueListComma
  63 | |||     ε
  64 | public export
  65 | record Enum where
  66 |   constructor MkEnum
  67 |   attributes : ExtAttributeList
  68 |   name       : Identifier
  69 |   values     : List1 StringLit
  70 | 
  71 | %runElab derive "Enum" [Eq,Show,HasAttributes]
  72 | 
  73 | ||| IncludesStatement ::
  74 | |||     identifier includes identifier ;
  75 | public export
  76 | record Includes where
  77 |   constructor MkIncludes
  78 |   attributes : ExtAttributeList
  79 |   name       : Identifier
  80 |   includes   : Identifier
  81 | 
  82 | %runElab derive "Includes" [Eq,Show,HasAttributes]
  83 | 
  84 | ||| InterfaceRest ::
  85 | |||     identifier Inheritance { InterfaceMembers } ;
  86 | public export
  87 | record Interface where
  88 |   constructor MkInterface
  89 |   attributes : ExtAttributeList
  90 |   name       : Identifier
  91 |   inherits   : Inheritance
  92 |   members    : InterfaceMembers
  93 | 
  94 | %runElab derive "Interface" [Eq,Show,HasAttributes]
  95 | 
  96 | ||| MixinRest ::
  97 | |||     mixin identifier { MixinMembers } ;
  98 | public export
  99 | record Mixin where
 100 |   constructor MkMixin
 101 |   attributes : ExtAttributeList
 102 |   name       : Identifier
 103 |   members    : MixinMembers
 104 | 
 105 | %runElab derive "Mixin" [Eq,Show,HasAttributes]
 106 | 
 107 | ||| Namespace ::
 108 | |||     namespace identifier { NamespaceMembers } ;
 109 | public export
 110 | record Namespace where
 111 |   constructor MkNamespace
 112 |   attributes : ExtAttributeList
 113 |   name       : Identifier
 114 |   members    : NamespaceMembers
 115 | 
 116 | %runElab derive "Namespace" [Eq,Show,HasAttributes]
 117 | 
 118 | ||| Typedef ::
 119 | |||     typedef TypeWithExtendedAttributes identifier ;
 120 | public export
 121 | record Typedef where
 122 |   constructor MkTypedef
 123 |   attributes     : ExtAttributeList
 124 |   typeAttributes : ExtAttributeList
 125 |   type           : IdlType
 126 |   name           : Identifier
 127 | 
 128 | %runElab derive "Typedef" [Eq,Show,HasAttributes]
 129 | 
 130 | ||| PartialDictionary ::
 131 | |||     dictionary identifier { DictionaryMembers } ;
 132 | public export
 133 | record PDictionary where
 134 |   constructor MkPDictionary
 135 |   attributes : ExtAttributeList
 136 |   name       : Identifier
 137 |   members    : DictionaryMembers
 138 | 
 139 | %runElab derive "PDictionary" [Eq,Show,HasAttributes]
 140 | 
 141 | ||| PartialInterfaceRest ::
 142 | |||     identifier { PartialInterfaceMembers } ;
 143 | public export
 144 | record PInterface where
 145 |   constructor MkPInterface
 146 |   attributes : ExtAttributeList
 147 |   name       : Identifier
 148 |   members    : PartialInterfaceMembers
 149 | 
 150 | %runElab derive "PInterface" [Eq,Show,HasAttributes]
 151 | 
 152 | ||| MixinRest ::
 153 | |||     mixin identifier { MixinMembers } ;
 154 | public export
 155 | record PMixin where
 156 |   constructor MkPMixin
 157 |   attributes : ExtAttributeList
 158 |   name       : Identifier
 159 |   members    : MixinMembers
 160 | 
 161 | %runElab derive "PMixin" [Eq,Show,HasAttributes]
 162 | 
 163 | ||| Namespace ::
 164 | |||     namespace identifier { NamespaceMembers } ;
 165 | public export
 166 | record PNamespace where
 167 |   constructor MkPNamespace
 168 |   attributes : ExtAttributeList
 169 |   name       : Identifier
 170 |   members    : NamespaceMembers
 171 | 
 172 | %runElab derive "PNamespace" [Eq,Show,HasAttributes]
 173 | 
 174 | public export
 175 | DefTypes : List Type
 176 | DefTypes =
 177 |   [ Callback
 178 |   , CallbackInterface
 179 |   , Dictionary
 180 |   , Enum
 181 |   , Includes
 182 |   , Interface
 183 |   , Mixin
 184 |   , Namespace
 185 |   , Typedef
 186 |   ]
 187 | 
 188 | public export
 189 | PartTypes : List Type
 190 | PartTypes = [PDictionary, PInterface, PMixin, PNamespace]
 191 | 
 192 | ||| Definition ::
 193 | |||     CallbackOrInterfaceOrMixin
 194 | |||     Namespace
 195 | |||     Partial
 196 | |||     Dictionary
 197 | |||     Enum
 198 | |||     Typedef
 199 | |||     IncludesStatement
 200 | ||| CallbackOrInterfaceOrMixin ::
 201 | |||     callback CallbackRestOrInterface
 202 | |||     interface InterfaceOrMixin
 203 | |||
 204 | ||| InterfaceOrMixin ::
 205 | |||     InterfaceRest
 206 | |||     MixinRest
 207 | public export
 208 | Definition : Type
 209 | Definition = NS I DefTypes
 210 | 
 211 | public export
 212 | 0 Definitions : Type
 213 | Definitions = NP List DefTypes
 214 | 
 215 | ||| PartialDefinition ::
 216 | |||     interface PartialInterfaceOrPartialMixin
 217 | |||     PartialDictionary
 218 | |||     Namespace
 219 | |||
 220 | ||| PartialInterfaceOrPartialMixin ::
 221 | |||     PartialInterfaceRest
 222 | |||     MixinRest
 223 | public export
 224 | Part : Type
 225 | Part = NS I PartTypes
 226 | 
 227 | public export
 228 | accumNs : {ts : _} -> List (NS I ts) -> NP List ts
 229 | accumNs = foldl (\np,ns => hliftA2 (++) (toNP ns) np) hempty
 230 | 
 231 | public export
 232 | 0 PartOrDef : Type
 233 | PartOrDef = NS I [Part,Definition]
 234 | 
 235 | public export
 236 | 0 PartsAndDefs : Type
 237 | PartsAndDefs = NP List [Part,Definition]
 238 | 
 239 | public export
 240 | defs : PartsAndDefs -> Definitions
 241 | defs [_,d] = accumNs d
 242 | 
 243 | --------------------------------------------------------------------------------
 244 | --          Domain
 245 | --------------------------------------------------------------------------------
 246 | 
 247 | update : Eq k => (b -> b) -> k -> (b -> k) -> List b -> List b
 248 | update f k bk = map (\b => if bk b == k then f b else b)
 249 | 
 250 | mergeDict : PDictionary -> Dictionary -> Dictionary
 251 | mergeDict d = { members $= (++ d.members) }
 252 | 
 253 | mergeIface : PInterface -> Interface -> Interface
 254 | mergeIface i = { members $= (++ map to i.members) }
 255 | 
 256 |   where
 257 |     to : (a,b) -> (a, NS I [c,b])
 258 |     to (x, y) = (x, inject y)
 259 | 
 260 | mergeMixin : PMixin -> Mixin -> Mixin
 261 | mergeMixin m = { members $= (++ m.members) }
 262 | 
 263 | mergeNamespace : PNamespace -> Namespace -> Namespace
 264 | mergeNamespace n = { members $= (++ n.members) }
 265 | 
 266 | public export
 267 | record Domain where
 268 |   constructor MkDomain
 269 |   domain              : String
 270 |   callbacks           : List Callback
 271 |   callbackInterfaces  : List CallbackInterface
 272 |   dictionaries        : List Dictionary
 273 |   enums               : List Enum
 274 |   includeStatements   : List Includes
 275 |   interfaces          : List Interface
 276 |   mixins              : List Mixin
 277 |   namespaces          : List Namespace
 278 |   typedefs            : List Typedef
 279 | 
 280 | %runElab derive "Domain" [Eq,Show,HasAttributes]
 281 | 
 282 | applyPart : Domain -> Part -> Domain
 283 | applyPart d (Z v) =
 284 |   { dictionaries $= update (mergeDict v) v.name name } d
 285 | applyPart d (S $ Z v) =
 286 |   { interfaces $= update (mergeIface v) v.name name } d
 287 | applyPart d (S $ S $ Z v) =
 288 |   { mixins $= update (mergeMixin v) v.name name } d
 289 | applyPart d (S $ S $ S $ Z v) =
 290 |   { namespaces $= update (mergeNamespace v) v.name name } d
 291 | 
 292 | export
 293 | toDomains : List (String,PartsAndDefs) -> List Domain
 294 | toDomains ps =
 295 |   let defs = map (\(s,pad) => fromNP s (defs pad)) ps
 296 |       prts = concatMap (\(_,pad) => get Part pad) ps
 297 |    in map (\d => foldl applyPart d prts) defs
 298 | 
 299 |   where
 300 |     fromNP : String -> Definitions -> Domain
 301 |     fromNP s [c,ci,d,e,ic,it,m,n,t] = MkDomain s c ci d e ic it m n t
 302 |