Module Qcert.JavaScriptAst.Lang.JavaScriptAstUtil
Require
Import
List
.
Require
Import
Utils
.
Require
Import
JsAst.JsSyntax
.
Require
Import
JavaScriptAst
.
Section
JavaScriptAstUtil
.
Import
ListNotations
.
Definition
empty_array
:=
expr_array
nil
.
Definition
array_push
e1
e2
:=
expr_call
(
expr_member
e1
"
push
") [
e2
].
Definition
array_get
e1
e2
:=
expr_access
e1
e2
.
Definition
object_hasOwnProperty
e1
e2
:=
expr_call
(
expr_member
e1
"
hasOwnProperty
") [
e2
].
Definition
object_toString
e1
:=
expr_call
(
expr_member
e1
"
toString
") [ ].
Runtime functions
Definition
brands_to_js_ast
sl
:
expr
:=
expr_array
(
List.map
(
fun
s
=>
Some
(
expr_literal
(
literal_string
s
)))
sl
).
Definition
call_js_function
(
f
:
string
) (
args
:
list
expr
) :
expr
:=
expr_call
(
expr_identifier
f
)
args
.
Definition
call_runtime
:=
call_js_function
.
End
JavaScriptAstUtil
.