
   0 | module Text.WebIDL.Types.Attribute
   1 | 
   2 | import Data.List1
   3 | import Derive.Prelude
   4 | import Language.Reflection.Util
   5 | import Data.SOP
   6 | import Text.WebIDL.Types.Numbers
   7 | import Text.WebIDL.Types.StringLit
   8 | import Text.WebIDL.Types.Identifier
   9 | import Text.WebIDL.Types.Symbol
  10 | 
  11 | %default total
  12 | %language ElabReflection
  13 | 
  14 | public export
  15 | isParenOrQuote : Char -> Bool
  16 | isParenOrQuote '(' = True
  17 | isParenOrQuote ')' = True
  18 | isParenOrQuote '[' = True
  19 | isParenOrQuote ']' = True
  20 | isParenOrQuote '{' = True
  21 | isParenOrQuote '}' = True
  22 | isParenOrQuote '"' = True
  23 | isParenOrQuote _   = False
  24 | 
  25 | public export
  26 | isCommaOrParenOrQuote : Char -> Bool
  27 | isCommaOrParenOrQuote ',' = True
  28 | isCommaOrParenOrQuote c   = isParenOrQuote c
  29 | 
  30 | public export
  31 | 0 Other : Type
  32 | Other = NS I [IntLit,FloatLit,StringLit,Identifier,Keyword,Symbol]
  33 | 
  34 | ||| ExtendedAttributeInner ::
  35 | public export
  36 | data EAInner : Type where
  37 |   |||   ε
  38 |   Nil : EAInner
  39 |   
  40 |   |||   ( ExtendedAttributeInner ) ExtendedAttributeInner
  41 |   |||   [ ExtendedAttributeInner ] ExtendedAttributeInner
  42 |   |||   { ExtendedAttributeInner } ExtendedAttributeInner
  43 |   (::) : (head : Either EAInner Other) -> (eai : EAInner) -> EAInner
  44 | 
  45 | %runElab derive "EAInner" [Eq,Show]
  46 | 
  47 | public export
  48 | 0 InnerOrOther : Type
  49 | InnerOrOther = Either EAInner Other
  50 | 
  51 | public export
  52 | innerAttribute : SnocList InnerOrOther -> EAInner -> EAInner
  53 | innerAttribute [<]       x = x
  54 | innerAttribute (sx :< y) x = innerAttribute sx $ y :: x
  55 | 
  56 | namespace EAInner
  57 | 
  58 |   ||| Number of `Other`s.
  59 |   public export
  60 |   size : EAInner -> Nat
  61 |   size (Left eai :: t) = size eai + size t
  62 |   size (Right _ :: t)  = 1 + size t
  63 |   size []              = 0
  64 | 
  65 |   ||| Number of `Other`s.
  66 |   public export
  67 |   leaves : EAInner -> Nat
  68 |   leaves (Left eai :: t) = leaves eai + leaves t
  69 |   leaves (Right _ :: t)  = 1 + leaves t
  70 |   leaves []              = 1
  71 | 
  72 |   ||| Number of `Other`s.
  73 |   public export
  74 |   depth : EAInner -> Nat
  75 |   depth (Left eai :: t) = 1 + (depth eai `max` depth t)
  76 |   depth (Right _ :: t)  = 1 + depth t
  77 |   depth []              = 0
  78 | 
  79 | ||| ExtendedAttributeRest ::
  80 | |||   ExtendedAttribute
  81 | |||   ε
  82 | |||
  83 | ||| ExtendedAttribute ::
  84 | public export
  85 | data ExtAttribute : Type where
  86 |   ||| ( ExtendedAttributeInner ) ExtendedAttributeRest
  87 |   ||| [ ExtendedAttributeInner ] ExtendedAttributeRest
  88 |   ||| { ExtendedAttributeInner } ExtendedAttributeRest
  89 |   ||| Other ExtendedAttributeRest
  90 |   Last : InnerOrOther -> ExtAttribute
  91 |   Cons : InnerOrOther -> ExtAttribute -> ExtAttribute
  92 | 
  93 | %runElab derive "ExtAttribute" [Eq,Show]
  94 | 
  95 | public export
  96 | extAttribute : SnocList InnerOrOther -> ExtAttribute -> ExtAttribute
  97 | extAttribute [<]       x = x
  98 | extAttribute (sx :< y) x = extAttribute sx $ Cons y x
  99 | 
 100 | namespace ExtAttribute
 101 | 
 102 |   ||| Number of `Other`s.
 103 |   public export
 104 |   size : ExtAttribute -> Nat
 105 |   size (Cons (Left i) r)  = size i + size r
 106 |   size (Cons (Right _) r) = 1 + size r
 107 |   size (Last (Left i))    = size i
 108 |   size (Last (Right _))   = 1
 109 | 
 110 |   ||| Number of leaves (unlike `size`, this includes empty leaves)
 111 |   public export
 112 |   leaves : ExtAttribute -> Nat
 113 |   leaves (Cons (Left i) r)  = leaves i + leaves r
 114 |   leaves (Cons (Right _) r) = 1 + leaves r
 115 |   leaves (Last (Left i))    = leaves i + 1
 116 |   leaves (Last (Right _))   = 2
 117 | 
 118 |   ||| Number of `Other`s.
 119 |   public export
 120 |   depth : ExtAttribute -> Nat
 121 |   depth (Cons (Left i) r)  = 1 + (depth i `max` depth r)
 122 |   depth (Cons (Right _) r) = 1 + depth r
 123 |   depth (Last (Left i))    = 1 + depth i
 124 |   depth (Last (Right _))   = 1
 125 | 
 126 | 
 127 | ||| ExtendedAttributeList ::
 128 | |||   [ ExtendedAttribute ExtendedAttributes ]
 129 | |||   ε
 130 | |||
 131 | ||| ExtendedAttributes ::
 132 | |||   , ExtendedAttribute ExtendedAttributes
 133 | |||   ε
 134 | public export
 135 | ExtAttributeList : Type
 136 | ExtAttributeList = List ExtAttribute
 137 | 
 138 | ||| TypeWithExtendedAttributes ::
 139 | |||     ExtendedAttributeList Type
 140 | public export
 141 | Attributed : Type -> Type
 142 | Attributed a = (ExtAttributeList, a)
 143 | 
 144 | public export
 145 | interface HasAttributes a where
 146 |   constructor MkHasAttributes
 147 |   attributes : a -> ExtAttributeList
 148 | 
 149 | public export
 150 | HasAttributes () where
 151 |   attributes = const Nil
 152 | 
 153 | public export
 154 | HasAttributes String where
 155 |   attributes = const Nil
 156 | 
 157 | public export %inline
 158 | HasAttributes Identifier where
 159 |   attributes = const Nil
 160 | 
 161 | public export %inline
 162 | HasAttributes Bool where
 163 |   attributes = const Nil
 164 | 
 165 | public export %inline
 166 | HasAttributes FloatLit where
 167 |   attributes = const Nil
 168 | 
 169 | public export %inline
 170 | HasAttributes IntLit where
 171 |   attributes = const Nil
 172 | 
 173 | public export %inline
 174 | HasAttributes StringLit where
 175 |   attributes = const Nil
 176 | 
 177 | public export %inline
 178 | (HasAttributes a, HasAttributes b) => HasAttributes (a,b) where
 179 |   attributes (x,y) = attributes x ++ attributes y
 180 | 
 181 | public export %inline
 182 | HasAttributes ExtAttribute where
 183 |   attributes = pure
 184 | 
 185 | public export %inline
 186 | HasAttributes a => HasAttributes (Maybe a) where
 187 |   attributes = maybe Nil attributes
 188 | 
 189 | public export %inline
 190 | HasAttributes a => HasAttributes (List a) where
 191 |   attributes x = x >>= attributes
 192 | 
 193 | public export %inline
 194 | HasAttributes a => HasAttributes (List1 a) where
 195 |   attributes = attributes . forget
 196 | 
 197 | --------------------------------------------------------------------------------
 198 | --          Deriving HasAttributes
 199 | --------------------------------------------------------------------------------
 200 | 
 201 | public export
 202 | (all : NP HasAttributes ts) => HasAttributes (NP I ts) where
 203 |   attributes = hcconcatMap HasAttributes attributes
 204 | 
 205 | public export
 206 | (all : NP HasAttributes ts) => HasAttributes (NS I ts) where
 207 |   attributes = hcconcatMap HasAttributes attributes
 208 | 
 209 | public export
 210 | (all : POP HasAttributes ts) => HasAttributes (SOP I ts) where
 211 |   attributes = hcconcatMap HasAttributes attributes
 212 | 
 213 | --------------------------------------------------------------------------------
 214 | --          Claims
 215 | --------------------------------------------------------------------------------
 216 | 
 217 | ||| General type of a `attributes` function with the given list
 218 | ||| of implicit and auto-implicit arguments, plus the given argument type
 219 | ||| to be displayed.
 220 | export
 221 | generalAttrType : (implicits : List Arg) -> (arg : TTImp) -> TTImp
 222 | generalAttrType is arg = piAll `(~(arg) -> ExtAttributeList) is
 223 | 
 224 | ||| Top-level function declaration implementing the `attrbutes` function for
 225 | ||| the given data type.
 226 | export
 227 | attrClaim : (fun : Name) -> (p : ParamTypeInfo) -> Decl
 228 | attrClaim fun p =
 229 |   let arg := p.applied
 230 |       tpe := generalAttrType (allImplicits p "HasAttributes") arg
 231 |    in public' fun tpe
 232 | 
 233 | ||| Top-level declaration of the `HasAttributes`
 234 | ||| implementation for the given data type.
 235 | export
 236 | attrImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
 237 | attrImplClaim impl p = implClaim impl (implType "HasAttributes" p)
 238 | 
 239 | --------------------------------------------------------------------------------
 240 | --          Definitions
 241 | --------------------------------------------------------------------------------
 242 | 
 243 | ||| Top-level definition of the `Show` implementation for the given data type.
 244 | export
 245 | attrImplDef : (fun, impl : Name) -> Decl
 246 | attrImplDef f i =
 247 |   def i [patClause (var i) (var "MkHasAttributes" `app` var f)]
 248 | 
 249 | parameters (nms : List Name)
 250 |   ttimp : BoundArg 1 Regular -> TTImp
 251 |   ttimp (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(attributes ~(var x))
 252 | 
 253 |   rsh : SnocList TTImp -> TTImp
 254 |   rsh [<] = `(Nil)
 255 |   rsh st  = `(listBind ~(listOf st) id)
 256 | 
 257 |   export
 258 |   attrClauses : (fun : Name) -> TypeInfo -> List Clause
 259 |   attrClauses fun ti = map clause ti.cons
 260 | 
 261 |     where
 262 |       clause : Con ti.arty ti.args -> Clause
 263 |       clause c =
 264 |         let ns  := freshNames "x" c.arty
 265 |             bc  := bindCon c ns
 266 |             lhs := var fun `app` bc
 267 |             st  := ttimp <$> boundArgs regular c.args [ns]
 268 |          in patClause lhs (rsh st)
 269 | 
 270 |   export
 271 |   attrDef : Name -> TypeInfo -> Decl
 272 |   attrDef fun ti = def fun (attrClauses fun ti)
 273 | 
 274 | --------------------------------------------------------------------------------
 275 | --          Deriving
 276 | --------------------------------------------------------------------------------
 277 | 
 278 | namespace Derive
 279 | 
 280 |   ||| Generate declarations and implementations for `HasAttributes`
 281 |   ||| for a given data type.
 282 |   export
 283 |   HasAttributes : List Name -> ParamTypeInfo -> Res (List TopLevel)
 284 |   HasAttributes nms p =
 285 |     let fun  := funName p "attributes"
 286 |         impl := implName p "HasAttributes"
 287 |      in Right
 288 |           [ TL (attrClaim fun p) (attrDef nms fun p.info)
 289 |           , TL (attrImplClaim impl p) (attrImplDef fun impl)
 290 |           ]
 291 | 
 292 | --------------------------------------------------------------------------------
 293 | --          Tests and Proofs
 294 | -----------------------------------------------------------------------------
 295 | 
 296 | isParenTrue : all Attribute.isParenOrQuote (unpack "(){}[]\"") = True
 297 | isParenTrue = Refl
 298 | 
 299 | isParenFalse : any Attribute.isParenOrQuote (unpack "=!?><:;,.-_") = False
 300 | isParenFalse = Refl
 301 | 
 302 | isCommaOrParenTrue : all Attribute.isCommaOrParenOrQuote (unpack ",(){}[]\"") = True
 303 | isCommaOrParenTrue = Refl
 304 | 
 305 | isCommaOrParenFalse : any Attribute.isCommaOrParenOrQuote (unpack "=!?><:;.-_") = False
 306 | isCommaOrParenFalse = Refl
 307 |