9 | module Text.WebIDL.Codegen.Args

 11 | import Data.List

 12 | import Data.List1

 13 | import Text.WebIDL.Codegen.Util

 14 | import Text.WebIDL.Encoder as E

 16 | %default total

 18 | public export

 19 | record PrettyArg (opts : LayoutOpts) where

 20 |   constructor MkPrettyArg

 21 |   name  : ArgumentName

 22 |   doc   : Doc opts

 25 | argIdent : PrettyArg opts -> IdrisIdent

 26 | argIdent = fromString . value . name

 28 | public export

 29 | 0 PrettyArgs : (opts : LayoutOpts) -> Type

 30 | PrettyArgs = List . PrettyArg

 36 | parameters {opts : LayoutOpts}

 38 |   nullableSimpleFFI :  Prec -> Nullable SimpleType -> Doc opts

 40 |   nullableUnionFFI :  Prec -> Nullable (List1 SimpleType) -> Doc opts

 42 |   simpleFFI : Prec -> SimpleType -> Doc opts

 44 |   simpleFFIs : Prec -> List SimpleType -> List (Doc opts)

 46 |   unionFFI : Prec -> List1 SimpleType -> Doc opts

 48 |   export

 49 |   ffi : Prec -> CGType -> Doc opts

 52 |   simpleFFI p Undef            = line "Undefined"

 53 |   simpleFFI p Boolean          = line "Boolean"

 54 |   simpleFFI p (Interface _ x)  = line x.value

 55 |   simpleFFI p (Dictionary x)   = line x.value

 56 |   simpleFFI p (Mixin x)        = line x.value

 57 |   simpleFFI p (Primitive x)    = line x

 58 |   simpleFFI p (Unchangeable x) = line x

 59 |   simpleFFI p (Enum x)         = line "String"

 60 |   simpleFFI p (Array x)        = prettyCon p "Array" [ffi App x]

 61 |   simpleFFI p (Record x y)     = prettyCon p "Record" [line x, ffi App y]

 63 |   simpleFFIs p []     = []

 64 |   simpleFFIs p (h::t) = simpleFFI p h :: simpleFFIs p t

 66 |   unionFFI p (h:::t) =

 67 |     prettyCon p "Union\{show . S $ length t}"

 68 |       (simpleFFI App h :: simpleFFIs App t)

 70 |   ffi p Any         = "AnyPtr"

 71 |   ffi p (Promise x) = prettyCon p "Promise" [ffi App x]

 72 |   ffi p (Simple x)  = nullableSimpleFFI p x

 73 |   ffi p (Union x)   = nullableUnionFFI p x

 75 |   nullableSimpleFFI p (MaybeNull x) = prettyCon p "Nullable" [simpleFFI App x]

 76 |   nullableSimpleFFI p (NotNull x) = simpleFFI p x

 78 |   nullableUnionFFI p (MaybeNull x) = prettyCon p "Nullable" [unionFFI App x]

 79 |   nullableUnionFFI p (NotNull x)   = unionFFI p x

 86 |   simpleAPI : Maybe Nat -> Prec -> SimpleType -> Doc opts

 87 |   simpleAPI (Just k) _ (Dictionary _)     = line "t\{show k}"

 88 |   simpleAPI (Just k) _ (Mixin _)          = line "t\{show k}"

 89 |   simpleAPI (Just k) _ (Interface True _) = line "t\{show k}"

 90 |   simpleAPI Nothing _ (Dictionary x)      = line x.value

 91 |   simpleAPI Nothing _ (Mixin x)           = line x.value

 92 |   simpleAPI _ _        (Interface _ x)    = line x.value

 93 |   simpleAPI _ _ Undef                     = line "Undefined"

 94 |   simpleAPI _ _ Boolean                   = line "Bool"

 95 |   simpleAPI _ _ (Primitive x)             = line x

 96 |   simpleAPI _ _ (Unchangeable x)          = line x

 97 |   simpleAPI _ _ (Enum x)                  = line x.value

 98 |   simpleAPI _ p (Array x)                 = prettyCon p "Array" [ffi App x]

 99 |   simpleAPI _ p (Record x y)              = prettyCon p "Record" [line x, ffi App y]

101 |   unionAPI : Prec -> List1 SimpleType -> Doc opts

102 |   unionAPI p (h ::: t) =

103 |     prettyCon p "HSum" [list $ map (simpleAPI Nothing Open) (h::t)]

105 |   nullableAPI :  (Prec -> a -> Doc opts) -> Prec -> Nullable a -> Doc opts

106 |   nullableAPI f p (MaybeNull x) = prettyCon p "Maybe" [f App x]

107 |   nullableAPI f p (NotNull x)   = f p x

109 |   api : Maybe Nat -> Prec -> CGType -> Doc opts

110 |   api _ p Any         = "Any"

111 |   api _ p (Promise x) = prettyCon p "Promise" [ffi App x]

112 |   api k p (Simple x)  = nullableAPI (simpleAPI k) p x

113 |   api _ p (Union x)   = nullableAPI unionAPI p x

119 |   export

120 |   ret : Prec -> CGType -> Doc opts

121 |   ret p (Union $ MaybeNull xs) =

122 |     let u :=

123 |       if all SimpleType.safeCast xs

124 |          then unionAPI App xs

125 |          else unionFFI App xs

127 |      in prettyCon p "Maybe" [u]

129 |   ret p t@(Union $ NotNull xs) =

130 |     if all SimpleType.safeCast xs then api Nothing p t else ffi p t

132 |   ret p t             = api Nothing p t

134 |   returnTypeFFI' : (io : String) -> ReturnType -> Doc opts

135 |   returnTypeFFI' io Undefined     = line "\{io} ()"

136 |   returnTypeFFI' io (Def t)       = prettyCon Open io [ffi App t]

137 |   returnTypeFFI' io (UndefOr t _) =

138 |     prettyCon Open io [prettyCon App "UndefOr" [ffi App t]]

140 |   returnTypeFFI : ReturnType -> Doc opts

141 |   returnTypeFFI = returnTypeFFI' "PrimIO"

143 |   returnTypeAPI : ReturnType -> Doc opts

144 |   returnTypeAPI Undefined     = line "JSIO ()"

145 |   returnTypeAPI (Def t)       = prettyCon Open "JSIO" [ret App t]

146 |   returnTypeAPI (UndefOr t _) =

147 |     prettyCon Open "JSIO" [prettyCon App "Optional" [ret App t]]

149 |   export

150 |   constTpe : CGConstType -> Doc opts

151 |   constTpe = line . primitive

157 |   export

158 |   prettyConst : ConstValue -> Doc opts

159 |   prettyConst (B x) = pretty x

160 |   prettyConst (F x) = line "\{x}"

161 |   prettyConst (I x) = line "\{x}"

163 |   defltS : SimpleType -> Default -> Maybe (Doc opts)

164 |   defltS Boolean (C $ B x)   = Just $ pretty x

165 |   defltS (Primitive _) (S x) = Just . line $ interpolate x

166 |   defltS (Primitive _) (C x) = Just $ prettyConst x

167 |   defltS _ _                 = Nothing

169 |   unionD : Prec -> List1 SimpleType -> Default -> Maybe (Doc opts)

170 |   unionD p ts d =

171 |     let m = choiceMap (`defltS` d) ts

172 |      in map (\x => prettyCon p "inject" [x]) m

174 |   export

175 |   deflt : Bool -> Prec -> CGType -> Default -> Maybe (Doc opts)

176 |   deflt _ p Any Null  = Just $ prettyCon p "MkAny" [line "$ null {a = ()}"]

177 |   deflt _ p Any (S x) = Just $ prettyCon p "MkAny" [line "\{x}"]

178 |   deflt _ p Any (C x) = Just $ prettyCon p "MkAny" [prettyConst x]

179 |   deflt _ _ (Simple $ MaybeNull x) Null = Just "Nothing"

181 |   deflt _ p (Simple $ MaybeNull x) d =

182 |     map (\v => prettyCon p "Just" [v]) (defltS x d)

184 |   deflt _ _ (Simple $ NotNull x) d = defltS x d

186 |   deflt _ p (Union $ MaybeNull x) Null = Just "Nothing"

188 |   deflt True p (Union $ MaybeNull x) d =

189 |     map (\v => prettyCon p "Just" [v]) (unionD App x d)

191 |   deflt True p (Union $ NotNull x) d = unionD p x d

192 |   deflt _ _ _ _ = Nothing

198 |   argTypeFFI : Prec -> CGArg -> Doc opts

199 |   argTypeFFI p (Mandatory _ t)  = ffi p t

200 |   argTypeFFI p (VarArg _ t)     =

201 |     prettyCon p "IO" [prettyCon App "Array" [ffi App t]]

202 |   argTypeFFI p (Optional _ t _) = prettyCon p "UndefOr" [ffi App t]

204 |   argTypeAPI : Nat -> Prec -> CGArg -> Doc opts

205 |   argTypeAPI k p (Mandatory _ t)  = api (Just k) p t

206 |   argTypeAPI _ p (VarArg _ t)     = prettyCon p "List" [api Nothing App t]

207 |   argTypeAPI k p (Optional _ t _) = prettyCon p "Optional" [api (Just k) App t]

209 |   arg : PrettyArg opts -> Doc opts

210 |   arg a = parens $ hsep [line "\{argIdent a}", ":", a.doc]

212 |   prettyArgFFI : CGArg -> Doc opts

213 |   prettyArgFFI = argTypeFFI Open

215 |   prettyArgAPI : Nat -> CGArg -> PrettyArg opts

216 |   prettyArgAPI k a =

217 |     let doc := argTypeAPI k Open a

218 |      in MkPrettyArg (argName a) doc

224 |   funTypeFFI : (name : IdrisIdent) -> ReturnType -> Args -> Doc opts

225 |   funTypeFFI n t as = typeDecl n (returnTypeFFI t) (map prettyArgFFI as)

227 |   funType : (name : IdrisIdent) -> ReturnType -> Args -> Doc opts

228 |   funType n t as =

229 |      typeDecl n (returnTypeAPI t) (run 0 as [<] [<] [<])

231 |     where

232 |       run : Nat -> Args -> (imp,aut,expl : SnocList $ Doc opts) -> List (Doc opts)

233 |       run _ []      is aus es = is <>> aus <>> es <>> []

234 |       run k (a::as) is aus es = case CGArg.inheritance a of

235 |         Just (n,_) =>

236 |           let k2   := S k

237 |               pk2  := "t\{show k2}"

238 |               impl := line "{auto 0 _ : JSType \{pk2}}"

239 |               aut  := line "{auto 0 _ : Elem \{n} (Types \{pk2})}"

240 |               expl = arg (prettyArgAPI k2 a)

241 |            in run k2 as (is :< impl) (aus :< aut) (es :< expl)

242 |         Nothing =>

243 |           let expl := arg (prettyArgAPI k a)

244 |            in run (S k) as is aus (es :< expl)

247 | callbackFFI :

248 |      (obj  : Identifier)

249 |   -> (name : IdrisIdent)

250 |   -> (impl : String)

251 |   -> (args : Args)

252 |   -> (tpe  : ReturnType)

253 |   -> String

254 | callbackFFI o n impl as t =

255 |   let cbTpe  := functionTypeOnly (returnTypeFFI' "IO" t) (map prettyArgFFI as)

256 |       retTpe := line "PrimIO \{o}"

257 |    in render80 . indent 2 $

258 |         vsep

259 |           [ line ""

260 |           , line "export"

261 |           , line "\{impl}"

262 |           , typeDecl n retTpe [cbTpe]

263 |           ]

266 | callbackAPI :

267 |      (obj  : Identifier)

268 |   -> (name : IdrisIdent)

269 |   -> (prim : IdrisIdent)

270 |   -> (args : Args)

271 |   -> (tpe  : ReturnType)

272 |   -> String

273 | callbackAPI o n prim as t =

274 |   let cbTpe  :=

275 |         functionTypeOnly

276 |           (returnTypeFFI' "IO" t)

277 |           (map prettyArgFFI as)

279 |       retTpe := line "JSIO \{o}"

280 |       impl   := line "\{n} cb = primJS $ \{prim} cb"

282 |    in render80 . indent 2 $

283 |         vsep

284 |           [ line ""

285 |           , line "export"

286 |           , typeDecl n retTpe [cbTpe]

287 |           , impl

288 |           ]

291 | funFFI :

292 |      (name : IdrisIdent)

293 |   -> (impl : String)

294 |   -> (args : Args)

295 |   -> (tpe  : ReturnType)

296 |   -> String

297 | funFFI n impl as t = render80 . indent 2 $

298 |   vsep [line "", line "export", line impl, funTypeFFI n t as ]

301 | namespacedIdent : (ns : Kind) -> (name : IdrisIdent) -> String

302 | namespacedIdent ns n = #""\#{kindToString ns}.\#{n}""#

304 | fun' :

305 |      {opts       : _}

306 |   -> (ns         : Kind)

307 |   -> (name       : IdrisIdent)

308 |   -> (prim       : IdrisIdent)

309 |   -> (args       : Args)

310 |   -> (undefs     : List String)

311 |   -> (returnType : ReturnType)

312 |   -> List (Doc opts)

313 | fun' ns name prim as us rt =

314 |   let vs      := take (length as) (unShadowingArgNames name)

316 |       appVs   := zipWith adjVal vs as ++ map line us

318 |       primNS  := "\{kindToString ns}.\{prim}"

320 |       primCall :=

321 |         if sameType rt

322 |            then "primJS"

323 |            else "tryJS " ++ namespacedIdent ns name

325 |       lhs     := unwords $ "\{name}" :: vs

327 |       firstLine := line "\{lhs} = \{primCall} $"

329 |       rhs     := prettyCon Open primNS appVs

331 |       sl      := firstLine <++> rhs

333 |       impl    := ifMultiline sl (vappend firstLine $ indent 2 rhs)

335 |    in [line "", line "export", funType name rt as, impl]

337 |   where

338 |     adjVal : String -> CGArg -> Doc opts

339 |     adjVal v a =

340 |       -- If the same type is used at the FFI and the API,

341 |       -- there is no need to convert the value.

342 |       -- If the value should be upcast to a parent type (`inheritance` returns

343 |       -- a `Just`), we upcast the value using a number of nested `map`s,

344 |       -- corresponding to the number of functors around

345 |       -- the type (at most two layers: `Optional` and `Maybe`),

346 |       -- otherwise, we just use `toFFI` to convert it.

347 |       case (sameType a, snd <$> inheritance a) of

348 |         (True,_)            => line v

349 |         (False,Nothing)     => parens ("toFFI" <++> line v)

350 |         (False,Just Direct) => parens ("up" <++> line v)

351 |         (False,Just May)    => parens ("mayUp" <++> line v)

352 |         (False,Just Opt)    => parens ("optUp" <++> line v)

353 |         (False,Just OptMay) => parens ("omyUp" <++> line v)

356 | fun :

357 |      (ns   : Kind)

358 |   -> (name : IdrisIdent)

359 |   -> (prim : IdrisIdent)

360 |   -> Args

361 |   -> ReturnType

362 |   -> String

363 | fun ns name prim as t =

364 |   let -- mandatory arguments

365 |       as2      := filter (not . isOptional) as

366 |       undefs   := List.replicate (length as `minus` length as2) "undef"

368 |       mainName := if null undefs then name else name2

370 |       funImpl  := fun' ns mainName prim as [] t

372 |       -- function without optional args

373 |       funImpl2 :=

374 |         if null undefs

375 |            then []

376 |            else fun' ns name prim as2 undefs t

378 |    in render80 . indent 2 $ vsep (funImpl ++ funImpl2)

380 |   where

381 |     name2 : IdrisIdent

382 |     name2 = case name of

383 |       II v         => fromString $ v ++ "'"

384 |       Prim v       => Prim (v ++ "'")

385 |       Underscore v => fromString $ v ++ "'"