Module Qcert.WasmAst.Lang.WasmAst

Require Import String.
Require Import Utils.
Require Import ForeignEJson.
Require Import EJson.
Require Import BrandRelation.
Require Import DataRuntime.
Require Import ForeignDataToEJson.
Require Import DataToEJson.

Section WasmAst.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.

  Parameter wasm_ast : Set.
  Parameter wasm_ast_eval : wasm_ast -> @jbindings foreign_ejson_model -> option (@ejson foreign_ejson_model).
  Parameter wasm_ast_to_string : wasm_ast -> string.
End WasmAst.

Extract Constant wasm_ast => "Wasm_ast.t".
Extract Constant wasm_ast_eval => "Wasm_ast.eval".
Extract Constant wasm_ast_to_string => "Wasm_ast.to_string".

Section Top.
  Context {foreign_ejson_model:Set}.
  Context {fejson:foreign_ejson foreign_ejson_model}.
  Context {fruntime:foreign_runtime}.
  Context {foreign_ejson_runtime_op : Set}.
  Context {fdatatoejson:foreign_to_ejson foreign_ejson_model foreign_ejson_runtime_op}.

  Definition wasm_ast_eval_top (cenv: bindings) (q:wasm_ast) : option data :=
    let jenv := List.map (fun xy => (fst xy, data_to_ejson(snd xy))) cenv in
    lift ejson_to_data (wasm_ast_eval q jenv).
End Top.