
   0 | module Text.WebIDL.Types.Identifier
   1 | 
   2 | import Data.List1
   3 | import Data.Refined
   4 | import Derive.Prelude
   5 | import Derive.Refined
   6 | 
   7 | %default total
   8 | %language ElabReflection
   9 | 
  10 | %default total
  11 | 
  12 | %language ElabReflection
  13 | 
  14 | --------------------------------------------------------------------------------
  15 | --          Keyword Predicates
  16 | --------------------------------------------------------------------------------
  17 | 
  18 | ||| Checks, whether a given string corresponds to a WebIDL
  19 | ||| argument name keyword.
  20 | public export
  21 | IsArgumentNameKeyword : String -> Bool
  22 | IsArgumentNameKeyword "async"        = True
  23 | IsArgumentNameKeyword "attribute"    = True
  24 | IsArgumentNameKeyword "callback"     = True
  25 | IsArgumentNameKeyword "const"        = True
  26 | IsArgumentNameKeyword "constructor"  = True
  27 | IsArgumentNameKeyword "deleter"      = True
  28 | IsArgumentNameKeyword "dictionary"   = True
  29 | IsArgumentNameKeyword "enum"         = True
  30 | IsArgumentNameKeyword "getter"       = True
  31 | IsArgumentNameKeyword "includes"     = True
  32 | IsArgumentNameKeyword "inherit"      = True
  33 | IsArgumentNameKeyword "interface"    = True
  34 | IsArgumentNameKeyword "iterable"     = True
  35 | IsArgumentNameKeyword "maplike"      = True
  36 | IsArgumentNameKeyword "mixin"        = True
  37 | IsArgumentNameKeyword "namespace"    = True
  38 | IsArgumentNameKeyword "partial"      = True
  39 | IsArgumentNameKeyword "readonly"     = True
  40 | IsArgumentNameKeyword "required"     = True
  41 | IsArgumentNameKeyword "setlike"      = True
  42 | IsArgumentNameKeyword "setter"       = True
  43 | IsArgumentNameKeyword "static"       = True
  44 | IsArgumentNameKeyword "stringifier"  = True
  45 | IsArgumentNameKeyword "typedef"      = True
  46 | IsArgumentNameKeyword "unrestricted" = True
  47 | IsArgumentNameKeyword _              = False
  48 | 
  49 | IsAttributeNameKeyword : String -> Bool
  50 | IsAttributeNameKeyword "async"    = True
  51 | IsAttributeNameKeyword "required" = True
  52 | IsAttributeNameKeyword _          = False
  53 | 
  54 | ||| Checks, whether a given string corresponds to one
  55 | ||| of the floating point constants "NaN", "Infinity", or
  56 | ||| "-Infinity".
  57 | public export
  58 | IsFloatKeyword : String -> Bool
  59 | IsFloatKeyword "NaN"       = True
  60 | IsFloatKeyword "Infinity"  = True
  61 | IsFloatKeyword "-Infinity" = True
  62 | IsFloatKeyword _           = False
  63 | 
  64 | ||| Checks, whether a given string corresponds to any WebIDL keyword.
  65 | public export
  66 | IsKeyword : String -> Bool
  67 | IsKeyword "ArrayBuffer"       = True
  68 | IsKeyword "ByteString"        = True
  69 | IsKeyword "DOMString"         = True
  70 | IsKeyword "DataView"          = True
  71 | IsKeyword "Float32Array"      = True
  72 | IsKeyword "Float64Array"      = True
  73 | IsKeyword "FrozenArray"       = True
  74 | IsKeyword "Int16Array"        = True
  75 | IsKeyword "Int32Array"        = True
  76 | IsKeyword "Int8Array"         = True
  77 | IsKeyword "ObservableArray"   = True
  78 | IsKeyword "Promise"           = True
  79 | IsKeyword "USVString"         = True
  80 | IsKeyword "Uint16Array"       = True
  81 | IsKeyword "Uint32Array"       = True
  82 | IsKeyword "Uint8Array"        = True
  83 | IsKeyword "Uint8ClampedArray" = True
  84 | IsKeyword "any"               = True
  85 | IsKeyword "bigint"            = True
  86 | IsKeyword "boolean"           = True
  87 | IsKeyword "byte"              = True
  88 | IsKeyword "double"            = True
  89 | IsKeyword "false"             = True
  90 | IsKeyword "float"             = True
  91 | IsKeyword "long"              = True
  92 | IsKeyword "null"              = True
  93 | IsKeyword "object"            = True
  94 | IsKeyword "octet"             = True
  95 | IsKeyword "optional"          = True
  96 | IsKeyword "or"                = True
  97 | IsKeyword "record"            = True
  98 | IsKeyword "sequence"          = True
  99 | IsKeyword "short"             = True
 100 | IsKeyword "symbol"            = True
 101 | IsKeyword "true"              = True
 102 | IsKeyword "undefined"         = True
 103 | IsKeyword "unsigned"          = True
 104 | IsKeyword s = IsArgumentNameKeyword s || IsFloatKeyword s
 105 | 
 106 | --------------------------------------------------------------------------------
 107 | --          Keyword
 108 | --------------------------------------------------------------------------------
 109 | 
 110 | public export
 111 | record Keyword where
 112 |   constructor MkKeyword
 113 |   value : String
 114 |   0 isValid : Holds IsKeyword value
 115 | 
 116 | export %inline
 117 | Interpolation Keyword where interpolate = value
 118 | 
 119 | namespace Keyword
 120 |   %runElab derive "Keyword" [Show,Eq,Ord,RefinedString]
 121 | 
 122 | --------------------------------------------------------------------------------
 123 | --          ArgumentNameKeyword
 124 | --------------------------------------------------------------------------------
 125 | 
 126 | public export
 127 | record ArgumentNameKeyword where
 128 |   constructor MkArgumentNameKeyword
 129 |   value : String
 130 |   0 isValid : Holds IsArgumentNameKeyword value
 131 | 
 132 | export %inline
 133 | Interpolation ArgumentNameKeyword where interpolate = value
 134 | 
 135 | namespace ArgumentNameKeyword
 136 |   %runElab derive "ArgumentNameKeyword" [Show,Eq,Ord,RefinedString]
 137 | 
 138 | --------------------------------------------------------------------------------
 139 | --          AttributeNameKeyword
 140 | --------------------------------------------------------------------------------
 141 | 
 142 | ||| Wrapper for one of the attribute name keywords
 143 | public export
 144 | record AttributeNameKeyword where
 145 |   constructor MkAttributeNameKeyword
 146 |   value : String
 147 |   0 isValid : Holds IsAttributeNameKeyword value
 148 | 
 149 | export %inline
 150 | Interpolation AttributeNameKeyword where interpolate = value
 151 | 
 152 | namespace AttributeNameKeyword
 153 |   %runElab derive "AttributeNameKeyword" [Show,Eq,Ord,RefinedString]
 154 | 
 155 | --------------------------------------------------------------------------------
 156 | --          Identifier
 157 | --------------------------------------------------------------------------------
 158 | 
 159 | ||| Identifier
 160 | public export
 161 | record Identifier where
 162 |   constructor MkIdent
 163 |   value : String
 164 | 
 165 | export %inline
 166 | Interpolation Identifier where interpolate = value
 167 | 
 168 | %runElab derive "Identifier" [Eq,Ord,Show,FromString]
 169 | 
 170 | ||| IdentifierList :: identifier Identifiers
 171 | ||| Identifiers :: "," identifier Identifiers | ε
 172 | public export
 173 | 0 IdentifierList : Type
 174 | IdentifierList = List1 Identifier
 175 | 
 176 | --------------------------------------------------------------------------------
 177 | --          Idris Identifier
 178 | --------------------------------------------------------------------------------
 179 | 
 180 | ||| Checks, if a String corresponds to an Idris2 keyword.
 181 | public export
 182 | IsIdrisKeyword : String -> Bool
 183 | IsIdrisKeyword "covering"       = True
 184 | IsIdrisKeyword "data"           = True
 185 | IsIdrisKeyword "do"             = True
 186 | IsIdrisKeyword "default"        = True
 187 | IsIdrisKeyword "else"           = True
 188 | IsIdrisKeyword "export"         = True
 189 | IsIdrisKeyword "if"             = True
 190 | IsIdrisKeyword "implementation" = True
 191 | IsIdrisKeyword "interface"      = True
 192 | IsIdrisKeyword "module"         = True
 193 | IsIdrisKeyword "mutual"         = True
 194 | IsIdrisKeyword "namespace"      = True
 195 | IsIdrisKeyword "open"           = True
 196 | IsIdrisKeyword "parameters"     = True
 197 | IsIdrisKeyword "partial"        = True
 198 | IsIdrisKeyword "private"        = True
 199 | IsIdrisKeyword "prefix"         = True
 200 | IsIdrisKeyword "public"         = True
 201 | IsIdrisKeyword "record"         = True
 202 | IsIdrisKeyword "then"           = True
 203 | IsIdrisKeyword "total"          = True
 204 | IsIdrisKeyword "using"          = True
 205 | IsIdrisKeyword "where"          = True
 206 | IsIdrisKeyword _                = False
 207 | 
 208 | ||| Wrapper type making sure that no Idris2 keyword
 209 | ||| is used as a function's name
 210 | public export
 211 | data IdrisIdent : Type where
 212 |   ||| A string that was successfully checked to be not
 213 |   ||| an Idris2 keyword. This can be used without further
 214 |   ||| adjustments as an Idris2 identifier.
 215 |   II :
 216 |        (v : String)
 217 |     -> {auto 0 _ : Holds (Prelude.not . IsIdrisKeyword) v}
 218 |     -> IdrisIdent
 219 | 
 220 |   ||| Primitive function name. This will be prefixed by
 221 |   ||| "prim__" during code generation. As such, the resulting
 222 |   ||| identifier always valid in idris.
 223 |   Prim : (v : String) -> IdrisIdent
 224 | 
 225 |   ||| Fallback constructor for Idris2 keywords. An underscore
 226 |   ||| will be appended to the wrapped string during code generation.
 227 |   Underscore : (v : String) -> IdrisIdent
 228 | 
 229 | %runElab derive "IdrisIdent" [Eq,Show]
 230 | 
 231 | public export
 232 | Interpolation IdrisIdent where
 233 |   interpolate (II v) =  case strM  v of
 234 |     StrCons '_' xs => xs
 235 |     _              => v
 236 |   interpolate (Prim v) = "prim__\{v}"
 237 |   interpolate (Underscore v) = "\{v}_"
 238 | 
 239 | public export
 240 | FromString IdrisIdent where
 241 |   fromString s = case hdec0 {p = Holds (not . IsIdrisKeyword)} s of
 242 |     Nothing0 => Underscore s
 243 |     Just0 _  => II s
 244 | 
 245 | export %inline
 246 | fromIdent : Identifier -> IdrisIdent
 247 | fromIdent = fromString . value
 248 |