Theory Wasm_Interpreter_Printing

theory Wasm_Interpreter_Printing imports "../Wasm_Interpreter_Properties" begin

definition "run = run_v (2^63) 300"

code_printing
  constant host_apply_impl ⇀ (OCaml) "ImplWrapper.host'_apply'_impl"
| constant mem_grow_impl ⇀ (OCaml) "ImplWrapper.mem'_grow'_impl"

(* memory *)

declare Rep_bytes_inverse[code abstype]
declare Rep_mem_inverse[code abstype]

code_printing
  type_constructor bytes ⇀ (OCaml) "Int64.t"
| type_constructor mem ⇀ (OCaml) "ImplWrapperTypes.memory"

code_printing
  constant mem_size ⇀ (OCaml) "ImplWrapper.size"
(* | constant mem_grow ⇀ (OCaml) "ImplWrapper.grow" *)
| constant load ⇀ (OCaml) "ImplWrapper.load"
| constant store ⇀ (OCaml) "ImplWrapper.store"
| constant load_packed ⇀ (OCaml) "ImplWrapper.load'_packed"
| constant store_packed ⇀ (OCaml) "ImplWrapper.store'_packed"

declare mem_size_def[code del]
declare store_def[code del]
declare load_def[code del]
declare store_packed_def[code del]
declare load_packed_def[code del]

end