Module Qcert.WasmBinary.Lang.WasmBinary

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

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

  Parameter wasm : Set.
  Parameter wasm_eval : wasm -> @jbindings foreign_ejson_model -> option (@ejson foreign_ejson_model).
End Wasm.

Extract Constant wasm => "string".
Extract Constant wasm_eval => "(fun q -> fun env -> failwith (""Cannot evaluate binary Wasm""))".

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_eval_top (cenv: bindings) (q:wasm) : option data :=
    let jenv := List.map (fun xy => (fst xy, data_to_ejson(snd xy))) cenv in
    lift ejson_to_data (wasm_eval q jenv).
End Top.