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.