0 | module Text.WebIDL.Parser.Type

  2 | import Text.WebIDL.Parser.Attributes

  3 | import Text.WebIDL.Parser.Util

  5 | %default total

  7 | data UnionTree : Bool -> Type where

  8 |   Leaf   : UnionMemberType -> UnionTree False

  9 |   Branch : UnionTree b -> UnionTree c -> UnionTree d

 11 | weaken : UnionTree x -> UnionTree False

 12 | weaken (Leaf m)     = Leaf m

 13 | weaken (Branch l r) = Branch l r

 15 | flat : UnionTree b -> List1 UnionMemberType

 16 | flat (Leaf x)     = singleton x

 17 | flat (Branch x y) = flat x ++ flat y

 19 | flatten : Nullable (UnionTree True) -> IdlType

 20 | flatten x =

 21 |   let Branch l r  := val x

 22 |       (hl ::: tl) := flat l

 23 |       (hr ::: tr) := flat r

 24 |    in case tl of

 25 |         []     => U $ x $> UT hl hr tr

 26 |         (h::t) => U $ x $> UT hl h  (t ++ hr :: tr)

 28 | int : Rule True IntType

 29 | int (B "long" _ :: B "long" _ :: xs) = Succ0 LongLong xs

 30 | int (B "long" _ :: xs)               = Succ0 Long xs

 31 | int (B "short" _ :: xs)              = Succ0 Short xs

 32 | int xs                               = fail xs

 34 | float : Rule True FloatType

 35 | float (B "double" _ :: xs) = Succ0 Dbl xs

 36 | float (B "float" _ :: xs)  = Succ0 Float xs

 37 | float xs                   = fail xs

 40 | primitive : Rule True PrimitiveType

 41 | primitive (B "boolean" _ :: xs)      = Succ0 Boolean xs

 42 | primitive (B "byte" _ :: xs)         = Succ0 Byte xs

 43 | primitive (B "octet" _ :: xs)        = Succ0 Octet xs

 44 | primitive (B "bigint" _ :: xs)       = Succ0 BigInt xs

 45 | primitive (B "undefined" _ :: xs)    = Succ0 Undefined xs

 46 | primitive (B "unsigned" _ :: xs)     = succT $ Unsigned <$> int xs

 47 | primitive (B "unrestricted" _ :: xs) = succT $ Unrestricted <$> float xs

 48 | primitive xs = map Signed (int xs) <|> map Restricted (float xs)

 50 | simple : Rule True Distinguishable

 51 | simple (B "ArrayBuffer" _ :: xs)       = Succ0 (B ArrayBuffer) xs

 52 | simple (B "DataView"  _ :: xs)         = Succ0 (B DataView) xs

 53 | simple (B "Int8Array" _ :: xs)         = Succ0 (B Int8Array) xs

 54 | simple (B "Int16Array" _ :: xs)        = Succ0 (B Int16Array) xs

 55 | simple (B "Int32Array" _ :: xs)        = Succ0 (B Int32Array) xs

 56 | simple (B "Uint8Array" _ :: xs)        = Succ0 (B Uint8Array) xs

 57 | simple (B "Uint16Array" _ :: xs)       = Succ0 (B Uint16Array) xs

 58 | simple (B "Uint32Array" _ :: xs)       = Succ0 (B Uint32Array) xs

 59 | simple (B "Uint8ClampedArray" _ :: xs) = Succ0 (B Uint8ClampedArray) xs

 60 | simple (B "Float32Array" _ :: xs)      = Succ0 (B Float32Array) xs

 61 | simple (B "Float64Array" _ :: xs)      = Succ0 (B Float64Array) xs

 62 | simple (B "ByteString" _ :: xs)        = Succ0 (S ByteString) xs

 63 | simple (B "DOMString" _ :: xs)         = Succ0 (S DOMString) xs

 64 | simple (B "USVString" _ :: xs)         = Succ0 (S USVString) xs

 65 | simple xs                              = P <$> primitive xs

 68 | constType : Rule True ConstType

 69 | constType (B (Ident i) _ :: xs) = Succ0 (CI i) xs

 70 | constType xs                    = CP <$> primitive xs

 72 | idlAttr : (ExtAttributeList -> IdlType -> a) -> AccRule True a

 74 | idlAttrAngle : (ExtAttributeList -> IdlType -> a) -> AccRule True a

 76 | idlTpe : AccRule True IdlType

 78 | unionMember : AccRule True (Nullable $ UnionTree False)

 80 | unionRest : Bounds -> AccRule True (Nullable $ UnionTree False)

 82 | union : Bounds -> AccRule True (Nullable $ UnionTree True)

 86 | recrd : Bounds -> StringType -> AccRule True Distinguishable

 87 | recrd b s (B ',' _ :: xs) (SA r) = case succT (idlAttr (Record s) xs r) of

 88 |   Succ0 t (B '>' _ :: ys) => Succ0 t ys

 89 |   res                     => failInParen b '<' res

 90 | recrd b s (x :: xs) _ = expected x.bounds "," "\{x.val}"

 91 | recrd b s []        _ = eoi

 93 |   -- DistinguishableType ::

 94 |   --     PrimitiveType Null

 95 |   --     StringType Null

 96 |   --     identifier Null

 97 |   --     sequence < TypeWithExtendedAttributes > Null

 98 |   --     object Null

 99 |   --     symbol Null

100 |   --     BufferRelatedType Null

101 |   --     FrozenArray < TypeWithExtendedAttributes > Null

102 |   --     ObservableArray < TypeWithExtendedAttributes > Null

103 |   --     RecordType Null

104 | distinguishable : AccRule True Distinguishable

105 | distinguishable [] _           = eoi

106 | distinguishable (x::xs) (SA r) = case x.val of

107 |   "object"          => Succ0 Object xs

108 |   "symbol"          => Succ0 Symbol xs

109 |   "sequence"        => succT (idlAttrAngle Sequence xs r)

110 |   "FrozenArray"     => succT (idlAttrAngle FrozenArray xs r)

111 |   "ObservableArray" => succT (idlAttrAngle ObservableArray xs r)

112 |   "record"          => case xs of

113 |     B '<' b :: B "DOMString"  _ :: ys => succT (recrd b DOMString ys r)

114 |     B '<' b :: B "ByteString" _ :: ys => succT (recrd b ByteString ys r)

115 |     B '<' b :: B "USVString"  _ :: ys => succT (recrd b USVString ys r)

116 |     B '<' b :: y :: ys  => unexpected y

117 |     B '<' b :: []       => unclosed b '<'

118 |     x :: xs             => expected x.bounds "<" "\{x.val}"

119 |     []                  => eoi

120 |   Ident i           => Succ0 (I i) xs

121 |   _                 => simple (x::xs)

123 | distinguishableType : AccRule True (Nullable Distinguishable)

124 | distinguishableType ts acc = case distinguishable ts acc of

125 |   Succ0 d (B '?' _ :: xs) => Succ0 (MaybeNull d) xs

126 |   Succ0 d xs              => Succ0 (NotNull d) xs

127 |   Fail0 err               => Fail0 err

129 | unionMember (B '(' b :: xs) (SA r) = succT (map weaken <$> union b xs r)

130 | unionMember (B '[' b :: xs) (SA r) =

131 |   let Succ0 as r1 := succT $ eas [<] b xs r | Fail0 err => Fail0 err

132 |    in map (Leaf . MkUnionMember as) <$> succT (distinguishableType r1 r)

133 | unionMember xs a = map (Leaf . MkUnionMember []) <$> distinguishableType xs a

135 | union b xs acc@(SA r) = case unionMember xs acc of

136 |   Succ0 u1 (B "or" _ :: ys) => succT (zipWith Branch u1 <$> unionRest b ys r)

137 |   Succ0 _  (x :: _)         => expected x.bounds "or" "\{x.val}"

138 |   res                       => failInParen b '(' res

140 | unionRest b xs acc@(SA r) = case unionMember xs acc of

141 |   Succ0 u1 (B "or" _ :: ys) => succT (zipWith Branch u1 <$> unionRest b ys r)

142 |   Succ0 u1 (B ')' _  :: B '?' _ :: ys) => Succ0 (MaybeNull $ val u1) ys

143 |   Succ0 u1 (B ')' _  :: ys) => Succ0 u1 ys

144 |   res                       => failInParen b '(' res

156 | idlTpe (B "any" _ :: xs) _ = Succ0 Any xs

157 | idlTpe (B "Promise" _ :: B '<' b :: xs) (SA r) = case succT $ idlTpe xs r of

158 |   Succ0 t (B '>' _ :: ys) => Succ0 (Promise t) ys

159 |   xs                      => failInParen b '<' xs

160 | idlTpe (B '(' b :: xs) (SA r)  = flatten <$> succT (union b xs r)

161 | idlTpe xs acc = D <$> distinguishableType xs acc

163 | idlAttr f (B '[' b :: xs) (SA r) = case succT (eas [<] b xs r) of

164 |   Succ0 as ys => f as <$> succT (idlTpe ys r)

165 |   Fail0 err   => Fail0 err

166 | idlAttr f xs acc = f [] <$> idlTpe xs acc

168 | idlAttrAngle f (B '<' b :: xs) (SA r) = case succT (idlAttr f xs r) of

169 |   Succ0 v (B '>' _ :: ys) => Succ0 v ys

170 |   res                     => failInParen b '<' res

171 | idlAttrAngle f (x::xs) _ = expected x.bounds "<" "\{x.val}"

172 | idlAttrAngle f []      _ = eoi

174 | export %inline

175 | idlType : Rule True IdlType

176 | idlType = acc idlTpe

178 | export %inline

179 | optionalType : Rule False OptionalType

180 | optionalType (B ',' _ :: xs) = succF $ Just <$> attributed idlType xs

181 | optionalType xs              = Succ0 Nothing xs