open InterpreterAux

module Wasm_Interpreter_Printing : sig
  val wasm_execution_ocaml_e_is_trap :
    (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
      ImplWrapperTypes.host_function_t)
      Wasm.e ->
      bool
  val wasm_execution_ocaml_es_is_trap :
    (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
      ImplWrapperTypes.host_function_t)
      Wasm.e list ->
      bool
  val wasm_execution_ocaml_smem_ind :
    ('a, 'b, 'c, 'd, ImplWrapperTypes.memory, 'e, unit) Wasm.s_ext ->
      Arith.nat -> Arith.nat option
  val wasm_execution_ocaml_bitzero :
    Wasm.t -> (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v
  val wasm_execution_ocaml_n_zeros :
    Wasm.t list ->
      (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v list
  val wasm_execution_ocaml_bits :
    (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v -> Int64.t
  val wasm_execution_ocaml_cvt_i64 :
    Wasm.sx option ->
      (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v ->
        I64Wrapper.t option
  val wasm_execution_ocaml_cvt_i32 :
    Wasm.sx option ->
      (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v ->
        I32Wrapper.t option
  val wasm_execution_ocaml_cvt_f64 :
    Wasm.sx option ->
      (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v ->
        F64Wrapper.t option
  val wasm_execution_ocaml_cvt_f32 :
    Wasm.sx option ->
      (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v ->
        F32Wrapper.t option
  val wasm_execution_ocaml_cvt :
    Wasm.t ->
      Wasm.sx option ->
        (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v ->
          (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v option
  val wasm_execution_ocaml_run_step :
    Arith.nat ->
      Arith.nat ->
        (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
          ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
          Wasm.s_ext *
          ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
             Wasm.v list *
            (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
              ImplWrapperTypes.host_function_t)
              Wasm.e list) ->
          (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
            ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
            Wasm.s_ext *
            ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
               Wasm.v list *
              (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
                ImplWrapperTypes.host_function_t)
                Wasm_Interpreter.res_step)
  val wasm_execution_ocaml_run_one_step :
    Arith.nat ->
      Arith.nat ->
        (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
          ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
          Wasm.s_ext *
          ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
             Wasm.v list *
            ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
               Wasm.v list *
              (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
                ImplWrapperTypes.host_function_t)
                Wasm.e)) ->
          (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
            ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
            Wasm.s_ext *
            ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
               Wasm.v list *
              (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
                ImplWrapperTypes.host_function_t)
                Wasm_Interpreter.res_step)
  val wasm_execution_ocaml_run_v :
    Arith.nat ->
      Arith.nat ->
        Arith.nat ->
          (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
            ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
            Wasm.s_ext *
            ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
               Wasm.v list *
              (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
                ImplWrapperTypes.host_function_t)
                Wasm.e list) ->
            (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
              ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
              Wasm.s_ext *
              (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
                Wasm_Interpreter.res
  val run :
    Arith.nat ->
      (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
        ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
        Wasm.s_ext *
        ((I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t) Wasm.v list *
          (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
            ImplWrapperTypes.host_function_t)
            Wasm.e list) ->
        (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t,
          ImplWrapperTypes.memory, ImplWrapperTypes.host_function_t, unit)
          Wasm.s_ext *
          (I32Wrapper.t, I64Wrapper.t, F32Wrapper.t, F64Wrapper.t)
            Wasm_Interpreter.res
end = struct

let rec wasm_execution_ocaml_e_is_trap
  e = (match e with Wasm.Basic _ -> false | Wasm.Trap -> true
        | Wasm.Callcl _ -> false | Wasm.Label (_, _, _) -> false
        | Wasm.Local (_, _, _, _) -> false);;

let rec wasm_execution_ocaml_es_is_trap
  es = (match es with [] -> false | [e] -> wasm_execution_ocaml_e_is_trap e
         | _ :: _ :: _ -> false);;

let rec wasm_execution_ocaml_smem_ind
  s i = Wasm.mema (List.nth (Wasm.inst s) i);;

let rec wasm_execution_ocaml_bitzero
  t = (match t with Wasm.T_i32 -> Wasm.ConstInt32 I32Wrapper.zero
        | Wasm.T_i64 -> Wasm.ConstInt64 I64Wrapper.zero
        | Wasm.T_f32 -> Wasm.ConstFloat32 F32Wrapper.zero
        | Wasm.T_f64 -> Wasm.ConstFloat64 F64Wrapper.zero);;

let rec wasm_execution_ocaml_n_zeros
  ts = List.map wasm_execution_ocaml_bitzero ts;;

let rec wasm_execution_ocaml_bits
  v = (match v with Wasm.ConstInt32 a -> Int64.of_int32 a
        | Wasm.ConstInt64 a -> (fun i -> i) a
        | Wasm.ConstFloat32 a -> (Int64.of_int32 (F32Wrapper.to_bits a))
        | Wasm.ConstFloat64 a -> F64Wrapper.to_bits a);;

let rec wasm_execution_ocaml_cvt_i64
  sx v =
    (match v
      with Wasm.ConstInt32 c ->
        (match sx with None -> None
          | Some Wasm.S -> Some ((I64Wrapper_convert.extend_s_i32) c)
          | Some Wasm.U -> Some ((I64Wrapper_convert.extend_u_i32) c))
      | Wasm.ConstInt64 _ -> None
      | Wasm.ConstFloat32 c ->
        (match sx with None -> None
          | Some Wasm.S -> I64Wrapper_convert.trunc_s_f32 c
          | Some Wasm.U -> I64Wrapper_convert.trunc_u_f32 c)
      | Wasm.ConstFloat64 c ->
        (match sx with None -> None
          | Some Wasm.S -> I64Wrapper_convert.trunc_s_f64 c
          | Some Wasm.U -> I64Wrapper_convert.trunc_u_f64 c));;

let rec wasm_execution_ocaml_cvt_i32
  sx v =
    (match v with Wasm.ConstInt32 _ -> None
      | Wasm.ConstInt64 c -> Some ((I32Wrapper_convert.wrap_i64) c)
      | Wasm.ConstFloat32 c ->
        (match sx with None -> None
          | Some Wasm.S -> I32Wrapper_convert.trunc_s_f32 c
          | Some Wasm.U -> I32Wrapper_convert.trunc_u_f32 c)
      | Wasm.ConstFloat64 c ->
        (match sx with None -> None
          | Some Wasm.S -> I32Wrapper_convert.trunc_s_f64 c
          | Some Wasm.U -> I32Wrapper_convert.trunc_u_f64 c));;

let rec wasm_execution_ocaml_cvt_f64
  sx v =
    (match v
      with Wasm.ConstInt32 c ->
        (match sx with None -> None
          | Some Wasm.S -> Some (F64Wrapper_convert.convert_s_i32 c)
          | Some Wasm.U -> Some (F64Wrapper_convert.convert_u_i32 c))
      | Wasm.ConstInt64 c ->
        (match sx with None -> None
          | Some Wasm.S -> Some (F64Wrapper_convert.convert_s_i64 c)
          | Some Wasm.U -> Some (F64Wrapper_convert.convert_u_i64 c))
      | Wasm.ConstFloat32 c -> Some ((F64Wrapper_convert.promote_f32) c)
      | Wasm.ConstFloat64 _ -> None);;

let rec wasm_execution_ocaml_cvt_f32
  sx v =
    (match v
      with Wasm.ConstInt32 c ->
        (match sx with None -> None
          | Some Wasm.S -> Some (F32Wrapper_convert.convert_s_i32 c)
          | Some Wasm.U -> Some (F32Wrapper_convert.convert_u_i32 c))
      | Wasm.ConstInt64 c ->
        (match sx with None -> None
          | Some Wasm.S -> Some (F32Wrapper_convert.convert_s_i64 c)
          | Some Wasm.U -> Some (F32Wrapper_convert.convert_u_i64 c))
      | Wasm.ConstFloat32 _ -> None
      | Wasm.ConstFloat64 c -> Some ((F32Wrapper_convert.demote_f64) c));;

let rec wasm_execution_ocaml_cvt
  t sx v =
    (match t
      with Wasm.T_i32 ->
        (match wasm_execution_ocaml_cvt_i32 sx v with None -> None
          | Some c -> Some (Wasm.ConstInt32 c))
      | Wasm.T_i64 ->
        (match wasm_execution_ocaml_cvt_i64 sx v with None -> None
          | Some c -> Some (Wasm.ConstInt64 c))
      | Wasm.T_f32 ->
        (match wasm_execution_ocaml_cvt_f32 sx v with None -> None
          | Some c -> Some (Wasm.ConstFloat32 c))
      | Wasm.T_f64 ->
        (match wasm_execution_ocaml_cvt_f64 sx v with None -> None
          | Some c -> Some (Wasm.ConstFloat64 c)));;

let rec wasm_execution_ocaml_run_step
  d i (s, (vs, es)) =
    (match Wasm_Interpreter.split_vals_e es
      with (_, []) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | (ves, e :: esa) ->
        (if wasm_execution_ocaml_e_is_trap e
          then (if not (List.null esa) || not (List.null ves)
                 then (s, (vs, Wasm_Interpreter.RSNormal [Wasm.Trap]))
                 else (s, (vs, Wasm_Interpreter.RSCrash
                                 Wasm_Interpreter.CError)))
          else (let (sa, (vsa, r)) =
                  wasm_execution_ocaml_run_one_step d i
                    (s, (vs, (List.rev ves, e)))
                  in
                 (match r with Wasm_Interpreter.RSCrash _ -> (sa, (vsa, r))
                   | Wasm_Interpreter.RSBreak (_, _) -> (sa, (vsa, r))
                   | Wasm_Interpreter.RSReturn _ -> (sa, (vsa, r))
                   | Wasm_Interpreter.RSNormal res ->
                     (sa, (vsa, Wasm_Interpreter.RSNormal (res @ esa)))))))
and wasm_execution_ocaml_run_one_step
  d i (s, (vs, (ves, e))) =
    (match e
      with Wasm.Basic Wasm.Unreachable ->
        (s, (vs, Wasm_Interpreter.RSNormal
                   (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                      (List.rev ves) @
                     [Wasm.Trap])))
      | Wasm.Basic Wasm.Nop ->
        (s, (vs, Wasm_Interpreter.RSNormal
                   (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                     (List.rev ves))))
      | Wasm.Basic Wasm.Drop ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | _ :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev vesa)))))
      | Wasm.Basic Wasm.Select ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstInt32 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstInt32 _; _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: v2 :: v1 :: vesa ->
            (if I32Wrapper.eq c I32Wrapper.zero
              then (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                (List.rev (v2 :: vesa)))))
              else (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                (List.rev (v1 :: vesa))))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Block (Wasm.Tf (t1s, t2s), es)) ->
        (if Arith.less_eq_nat (List.size_list t1s) (List.size_list ves)
          then (let (vesb, vesa) =
                  Wasm_Interpreter.split_n ves (List.size_list t1s) in
                 (s, (vs, Wasm_Interpreter.RSNormal
                            (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                               (List.rev vesa) @
                              [Wasm.Label
                                 (List.size_list t2s, [],
                                   List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesb) @
                                     List.map (fun a -> Wasm.Basic a) es)]))))
          else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Loop (Wasm.Tf (t1s, t2s), es)) ->
        (if Arith.less_eq_nat (List.size_list t1s) (List.size_list ves)
          then (let (vesb, vesa) =
                  Wasm_Interpreter.split_n ves (List.size_list t1s) in
                 (s, (vs, Wasm_Interpreter.RSNormal
                            (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                               (List.rev vesa) @
                              [Wasm.Label
                                 (List.size_list t1s,
                                   [Wasm.Basic
                                      (Wasm.Loop (Wasm.Tf (t1s, t2s), es))],
                                   List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesb) @
                                     List.map (fun a -> Wasm.Basic a) es)]))))
          else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.If (tf, es1, es2)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: vesa ->
            (if I32Wrapper.eq c I32Wrapper.zero
              then (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev vesa) @
                                [Wasm.Basic (Wasm.Block (tf, es2))])))
              else (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev vesa) @
                                [Wasm.Basic (Wasm.Block (tf, es1))]))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Br j) -> (s, (vs, Wasm_Interpreter.RSBreak (j, ves)))
      | Wasm.Basic (Wasm.Br_if j) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: vesa ->
            (if I32Wrapper.eq c I32Wrapper.zero
              then (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                (List.rev vesa))))
              else (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev vesa) @
                                [Wasm.Basic (Wasm.Br j)]))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Br_table nejs) ->
        (let js = Wasm.to_list nejs in
          (match ves
            with [] ->
              (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
            | Wasm.ConstInt32 c :: vesa ->
              (let j = Arith.Nat (I32Wrapper.big_int_of_int32 c) in
                (if Arith.less_nat j (List.size_list js)
                  then (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesa) @
                                    [Wasm.Basic (Wasm.Br (List.nth js j))])))
                  else (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesa) @
                                    [Wasm.Basic (Wasm.Br (List.last js))])))))
            | Wasm.ConstInt64 _ :: _ ->
              (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
            | Wasm.ConstFloat32 _ :: _ ->
              (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
            | Wasm.ConstFloat64 _ :: _ ->
              (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))))
      | Wasm.Basic Wasm.Return -> (s, (vs, Wasm_Interpreter.RSReturn ves))
      | Wasm.Basic (Wasm.Call j) ->
        (s, (vs, Wasm_Interpreter.RSNormal
                   (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                      (List.rev ves) @
                     [Wasm.Callcl (Wasm.sfunc s i j)])))
      | Wasm.Basic (Wasm.Call_indirect j) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: vesa ->
            (match Wasm.stab s i (Arith.Nat (I32Wrapper.big_int_of_int32 c))
              with None ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                              (List.rev vesa) @
                             [Wasm.Trap])))
              | Some cl ->
                (if Wasm.equal_tf (Wasm.stypes s i j) (Wasm.cl_type cl)
                  then (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesa) @
                                    [Wasm.Callcl cl])))
                  else (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesa) @
                                    [Wasm.Trap])))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Get_local j) ->
        (if Arith.less_nat j (List.size_list vs)
          then (s, (vs, Wasm_Interpreter.RSNormal
                          (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                            (List.rev (List.nth vs j :: ves)))))
          else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Set_local j) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: vesa ->
            (if Arith.less_nat j (List.size_list vs)
              then (s, (List.list_update vs j v,
                         Wasm_Interpreter.RSNormal
                           (List.map (fun va -> Wasm.Basic (Wasm.EConst va))
                             (List.rev vesa))))
              else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))))
      | Wasm.Basic (Wasm.Tee_local j) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: _ ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun va -> Wasm.Basic (Wasm.EConst va))
                          (List.rev (v :: ves)) @
                         [Wasm.Basic (Wasm.Set_local j)]))))
      | Wasm.Basic (Wasm.Get_global j) ->
        (s, (vs, Wasm_Interpreter.RSNormal
                   (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                     (List.rev (Wasm.sglob_val s i j :: ves)))))
      | Wasm.Basic (Wasm.Set_global j) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: vesa ->
            (Wasm.supdate_glob s i j v,
              (vs, Wasm_Interpreter.RSNormal
                     (List.map (fun va -> Wasm.Basic (Wasm.EConst va))
                       (List.rev vesa)))))
      | Wasm.Basic (Wasm.Load (t, None, _, off)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 k :: vesa ->
            (match wasm_execution_ocaml_smem_ind s i
              with None ->
                (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
              | Some a ->
                (match
                  ImplWrapper.load (List.nth (Wasm.mem s) a)
                    (Arith.Nat (I32Wrapper.big_int_of_int32 k)) off
                    (Wasm.t_length t)
                  with None ->
                    (s, (vs, Wasm_Interpreter.RSNormal
                               (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                  (List.rev vesa) @
                                 [Wasm.Trap])))
                  | Some aa ->
                    (s, (vs, Wasm_Interpreter.RSNormal
                               (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev
                                   (ImplWrapper.deserialise aa t :: vesa)))))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Load (t, Some (tp, sx), _, off)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 k :: vesa ->
            (match wasm_execution_ocaml_smem_ind s i
              with None ->
                (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
              | Some a ->
                (match
                  ImplWrapper.load_packed sx (List.nth (Wasm.mem s) a)
                    (Arith.Nat (I32Wrapper.big_int_of_int32 k)) off
                    (Wasm.tp_length tp)
                  with None ->
                    (s, (vs, Wasm_Interpreter.RSNormal
                               (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                  (List.rev vesa) @
                                 [Wasm.Trap])))
                  | Some aa ->
                    (s, (vs, Wasm_Interpreter.RSNormal
                               (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev
                                   (ImplWrapper.deserialise aa t :: vesa)))))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Store (t, None, _, off)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [_] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: Wasm.ConstInt32 k :: vesa ->
            (if Wasm.types_agree t v
              then (match wasm_execution_ocaml_smem_ind s i
                     with None ->
                       (s, (vs, Wasm_Interpreter.RSCrash
                                  Wasm_Interpreter.CError))
                     | Some a ->
                       (match
                         ImplWrapper.store (List.nth (Wasm.mem s) a)
                           (Arith.Nat (I32Wrapper.big_int_of_int32 k)) off
                           (wasm_execution_ocaml_bits v) (Wasm.t_length t)
                         with None ->
                           (s, (vs, Wasm_Interpreter.RSNormal
                                      (List.map
 (fun va -> Wasm.Basic (Wasm.EConst va)) (List.rev vesa) @
[Wasm.Trap])))
                         | Some a_a ->
                           (Wasm.mem_update
                              (fun _ -> List.list_update (Wasm.mem s) a a_a) s,
                             (vs, Wasm_Interpreter.RSNormal
                                    (List.map
                                      (fun va -> Wasm.Basic (Wasm.EConst va))
                                      (List.rev vesa))))))
              else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
          | _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Store (t, Some tp, _, off)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [_] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: Wasm.ConstInt32 k :: vesa ->
            (if Wasm.types_agree t v
              then (match wasm_execution_ocaml_smem_ind s i
                     with None ->
                       (s, (vs, Wasm_Interpreter.RSCrash
                                  Wasm_Interpreter.CError))
                     | Some a ->
                       (match
                         ImplWrapper.store_packed (List.nth (Wasm.mem s) a)
                           (Arith.Nat (I32Wrapper.big_int_of_int32 k)) off
                           (wasm_execution_ocaml_bits v) (Wasm.tp_length tp)
                         with None ->
                           (s, (vs, Wasm_Interpreter.RSNormal
                                      (List.map
 (fun va -> Wasm.Basic (Wasm.EConst va)) (List.rev vesa) @
[Wasm.Trap])))
                         | Some a_a ->
                           (Wasm.mem_update
                              (fun _ -> List.list_update (Wasm.mem s) a a_a) s,
                             (vs, Wasm_Interpreter.RSNormal
                                    (List.map
                                      (fun va -> Wasm.Basic (Wasm.EConst va))
                                      (List.rev vesa))))))
              else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
          | _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic Wasm.Current_memory ->
        (match wasm_execution_ocaml_smem_ind s i
          with None ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Some a ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (I32Wrapper.int32_of_big_int (Arith.integer_of_nat (ImplWrapper.size
   (List.nth (Wasm.mem s) a)))) ::
                             ves))))))
      | Wasm.Basic Wasm.Grow_memory ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: vesa ->
            (match wasm_execution_ocaml_smem_ind s i
              with None ->
                (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
              | Some a ->
                (let l = ImplWrapper.size (List.nth (Wasm.mem s) a) in
                  (match
                    ImplWrapper.grow (List.nth (Wasm.mem s) a)
                      (Arith.Nat (I32Wrapper.big_int_of_int32 c))
                    with None ->
                      (s, (vs, Wasm_Interpreter.RSNormal
                                 (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                   (List.rev
                                     (Wasm.ConstInt32 I32Wrapper.minus_one ::
                                       vesa)))))
                    | Some a_a ->
                      (Wasm.mem_update
                         (fun _ -> List.list_update (Wasm.mem s) a a_a) s,
                        (vs, Wasm_Interpreter.RSNormal
                               (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev
                                   (Wasm.ConstInt32
                                      (I32Wrapper.int32_of_big_int (Arith.integer_of_nat l)) ::
                                     vesa))))))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.EConst _) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Unop_i (Wasm.T_i32, iop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (Wasm.app_unop_i
                                Wasm_Type_Abs_Printing.wasm_int_int32_impl iop
                                c) ::
                             vesa)))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Unop_i (Wasm.T_i64, iop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 c :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt64
                              (Wasm.app_unop_i
                                Wasm_Type_Abs_Printing.wasm_int_int64_impl iop
                                c) ::
                             vesa)))))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Unop_i (Wasm.T_f32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Unop_i (Wasm.T_f64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Unop_f (Wasm.T_i32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Unop_f (Wasm.T_i64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Unop_f (Wasm.T_f32, fop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 c :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstFloat32
                              (Wasm.app_unop_f
                                Wasm_Type_Abs_Printing.wasm_float_float32_impl
                                fop c) ::
                             vesa)))))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Unop_f (Wasm.T_f64, fop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 c :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstFloat64
                              (Wasm.app_unop_f
                                Wasm_Type_Abs_Printing.wasm_float_float64_impl
                                fop c) ::
                             vesa))))))
      | Wasm.Basic (Wasm.Binop_i (Wasm.T_i32, iop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstInt32 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c2 :: Wasm.ConstInt32 c1 :: vesa ->
            (match
              Wasm.app_binop_i Wasm_Type_Abs_Printing.wasm_int_int32_impl iop c1
                c2
              with None ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                              (List.rev vesa) @
                             [Wasm.Trap])))
              | Some a ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                             (List.rev (Wasm.ConstInt32 a :: vesa))))))
          | Wasm.ConstInt32 _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Binop_i (Wasm.T_i64, iop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstInt64 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 c2 :: Wasm.ConstInt64 c1 :: vesa ->
            (match
              Wasm.app_binop_i Wasm_Type_Abs_Printing.wasm_int_int64_impl iop c1
                c2
              with None ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                              (List.rev vesa) @
                             [Wasm.Trap])))
              | Some a ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                             (List.rev (Wasm.ConstInt64 a :: vesa))))))
          | Wasm.ConstInt64 _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Binop_i (Wasm.T_f32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Binop_i (Wasm.T_f64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Binop_f (Wasm.T_i32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Binop_f (Wasm.T_i64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Binop_f (Wasm.T_f32, fop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstFloat32 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 c2 :: Wasm.ConstFloat32 c1 :: vesa ->
            (match
              Wasm.app_binop_f Wasm_Type_Abs_Printing.wasm_float_float32_impl
                fop c1 c2
              with None ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                              (List.rev vesa) @
                             [Wasm.Trap])))
              | Some a ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                             (List.rev (Wasm.ConstFloat32 a :: vesa))))))
          | Wasm.ConstFloat32 _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Binop_f (Wasm.T_f64, fop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstFloat64 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 c2 :: Wasm.ConstFloat64 c1 :: vesa ->
            (match
              Wasm.app_binop_f Wasm_Type_Abs_Printing.wasm_float_float64_impl
                fop c1 c2
              with None ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                              (List.rev vesa) @
                             [Wasm.Trap])))
              | Some a ->
                (s, (vs, Wasm_Interpreter.RSNormal
                           (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                             (List.rev (Wasm.ConstFloat64 a :: vesa)))))))
      | Wasm.Basic (Wasm.Testop (Wasm.T_i32, testop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (ImplWrapper.bool
                                (Wasm.app_testop_i
                                  Wasm_Type_Abs_Printing.wasm_int_int32_impl
                                  testop c)) ::
                             vesa)))))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Testop (Wasm.T_i64, testop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 c :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (ImplWrapper.bool
                                (Wasm.app_testop_i
                                  Wasm_Type_Abs_Printing.wasm_int_int64_impl
                                  testop c)) ::
                             vesa)))))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Testop (Wasm.T_f32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Testop (Wasm.T_f64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Relop_i (Wasm.T_i32, iop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstInt32 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 c2 :: Wasm.ConstInt32 c1 :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (ImplWrapper.bool
                                (Wasm.app_relop_i
                                  Wasm_Type_Abs_Printing.wasm_int_int32_impl iop
                                  c1 c2)) ::
                             vesa)))))
          | Wasm.ConstInt32 _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Relop_i (Wasm.T_i64, iop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstInt64 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 c2 :: Wasm.ConstInt64 c1 :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (ImplWrapper.bool
                                (Wasm.app_relop_i
                                  Wasm_Type_Abs_Printing.wasm_int_int64_impl iop
                                  c1 c2)) ::
                             vesa)))))
          | Wasm.ConstInt64 _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Relop_i (Wasm.T_f32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Relop_i (Wasm.T_f64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Relop_f (Wasm.T_i32, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Relop_f (Wasm.T_i64, _)) ->
        (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Basic (Wasm.Relop_f (Wasm.T_f32, fop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstFloat32 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 c2 :: Wasm.ConstFloat32 c1 :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (ImplWrapper.bool
                                (Wasm.app_relop_f
                                  Wasm_Type_Abs_Printing.wasm_float_float32_impl
                                  fop c1 c2)) ::
                             vesa)))))
          | Wasm.ConstFloat32 _ :: Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
      | Wasm.Basic (Wasm.Relop_f (Wasm.T_f64, fop)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | [Wasm.ConstFloat64 _] ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: Wasm.ConstInt32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: Wasm.ConstInt64 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 _ :: Wasm.ConstFloat32 _ :: _ ->
            (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | Wasm.ConstFloat64 c2 :: Wasm.ConstFloat64 c1 :: vesa ->
            (s, (vs, Wasm_Interpreter.RSNormal
                       (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                         (List.rev
                           (Wasm.ConstInt32
                              (ImplWrapper.bool
                                (Wasm.app_relop_f
                                  Wasm_Type_Abs_Printing.wasm_float_float64_impl
                                  fop c1 c2)) ::
                             vesa))))))
      | Wasm.Basic (Wasm.Cvtop (t2, Wasm.Convert, t1, sx)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: vesa ->
            (if Wasm.types_agree t1 v
              then (match wasm_execution_ocaml_cvt t2 sx v
                     with None ->
                       (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                     (fun va -> Wasm.Basic (Wasm.EConst va))
                                     (List.rev vesa) @
                                    [Wasm.Trap])))
                     | Some a ->
                       (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                    (fun va -> Wasm.Basic (Wasm.EConst va))
                                    (List.rev (a :: vesa))))))
              else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))))
      | Wasm.Basic (Wasm.Cvtop (t2, Wasm.Reinterpret, t1, sx)) ->
        (match ves
          with [] -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
          | v :: vesa ->
            (if Wasm.types_agree t1 v && Option.is_none sx
              then (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun va -> Wasm.Basic (Wasm.EConst va))
                                (List.rev
                                  (ImplWrapper.deserialise
                                     (wasm_execution_ocaml_bits v) t2 ::
                                    vesa)))))
              else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))))
      | Wasm.Trap -> (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))
      | Wasm.Callcl (Wasm.Func_native (ia, Wasm.Tf (t1s, t2s), ts, es)) ->
        (let n = List.size_list t1s in
         let m = List.size_list t2s in
          (if Arith.less_eq_nat n (List.size_list ves)
            then (let (vesb, vesa) = Wasm_Interpreter.split_n ves n in
                  let zs = wasm_execution_ocaml_n_zeros ts in
                   (s, (vs, Wasm_Interpreter.RSNormal
                              (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                 (List.rev vesa) @
                                [Wasm.Local
                                   (m, ia, List.rev vesb @ zs,
                                     [Wasm.Basic
(Wasm.Block (Wasm.Tf ([], t2s), es))])]))))
            else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))))
      | Wasm.Callcl (Wasm.Func_host (Wasm.Tf (t1s, t2s), f)) ->
        (let n = List.size_list t1s in
         let _ = List.size_list t2s in
          (if Arith.less_eq_nat n (List.size_list ves)
            then (let (vesb, vesa) = Wasm_Interpreter.split_n ves n in
                   (match
                     ImplWrapper.host_apply s (Wasm.Tf (t1s, t2s)) f
                       (List.rev vesb)
                     with None ->
                       (s, (vs, Wasm_Interpreter.RSNormal
                                  (List.map
                                     (fun v -> Wasm.Basic (Wasm.EConst v))
                                     (List.rev vesa) @
                                    [Wasm.Trap])))
                     | Some (sa, rves) ->
                       (if List.list_all2 Wasm.types_agree t2s rves
                         then (sa, (vs, Wasm_Interpreter.RSNormal
  (List.map (fun v -> Wasm.Basic (Wasm.EConst v)) (List.rev vesa) @
    List.map (fun v -> Wasm.Basic (Wasm.EConst v)) rves)))
                         else (sa, (vs, Wasm_Interpreter.RSCrash
  Wasm_Interpreter.CError)))))
            else (s, (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError))))
      | Wasm.Label (ln, les, es) ->
        (if wasm_execution_ocaml_es_is_trap es
          then (s, (vs, Wasm_Interpreter.RSNormal
                          (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                             (List.rev ves) @
                            [Wasm.Trap])))
          else (if Wasm.const_list es
                 then (s, (vs, Wasm_Interpreter.RSNormal
                                 (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                                    (List.rev ves) @
                                   es)))
                 else (match wasm_execution_ocaml_run_step d i (s, (vs, es))
                        with (sa, (vsa, Wasm_Interpreter.RSCrash _)) ->
                          (sa, (vsa, Wasm_Interpreter.RSCrash
                                       Wasm_Interpreter.CError))
                        | (sa, (vsa, Wasm_Interpreter.RSBreak (nat, bvs))) ->
                          (if Arith.equal_nat nat Arith.zero_nat
                            then (if Arith.less_eq_nat ln (List.size_list bvs)
                                   then (sa,
  (vsa, Wasm_Interpreter.RSNormal
          (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
             (List.rev (List.take ln bvs @ ves)) @
            les)))
                                   else (sa,
  (vsa, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
                            else (sa, (vsa,
Wasm_Interpreter.RSBreak (Arith.minus_nat nat Arith.one_nata, bvs))))
                        | (sa, (vsa, Wasm_Interpreter.RSReturn rvs)) ->
                          (sa, (vsa, Wasm_Interpreter.RSReturn rvs))
                        | (sa, (vsa, Wasm_Interpreter.RSNormal esa)) ->
                          (sa, (vsa, Wasm_Interpreter.RSNormal
                                       (List.map
  (fun v -> Wasm.Basic (Wasm.EConst v)) (List.rev ves) @
 [Wasm.Label (ln, les, esa)]))))))
      | Wasm.Local (ln, j, vls, es) ->
        (if wasm_execution_ocaml_es_is_trap es
          then (s, (vs, Wasm_Interpreter.RSNormal
                          (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
                             (List.rev ves) @
                            [Wasm.Trap])))
          else (if Wasm.const_list es
                 then (if Arith.equal_nat (List.size_list es) ln
                        then (s, (vs, Wasm_Interpreter.RSNormal
(List.map (fun v -> Wasm.Basic (Wasm.EConst v)) (List.rev ves) @ es)))
                        else (s, (vs, Wasm_Interpreter.RSCrash
Wasm_Interpreter.CError)))
                 else (if Arith.equal_nat d Arith.zero_nat
                        then (s, (vs, Wasm_Interpreter.RSCrash
Wasm_Interpreter.CError))
                        else (match
                               wasm_execution_ocaml_run_step
                                 (Arith.minus_nat d Arith.one_nata) j
                                 (s, (vls, es))
                               with (sa, (_, Wasm_Interpreter.RSCrash _)) ->
                                 (sa, (vs,
Wasm_Interpreter.RSCrash Wasm_Interpreter.CExhaustion))
                               | (sa, (_, Wasm_Interpreter.RSBreak (_, _))) ->
                                 (sa, (vs,
Wasm_Interpreter.RSCrash Wasm_Interpreter.CExhaustion))
                               | (sa, (_, Wasm_Interpreter.RSReturn rvs)) ->
                                 (if Arith.less_eq_nat ln (List.size_list rvs)
                                   then (sa,
  (vs, Wasm_Interpreter.RSNormal
         (List.map (fun v -> Wasm.Basic (Wasm.EConst v))
           (List.rev (List.take ln rvs @ ves)))))
                                   else (sa,
  (vs, Wasm_Interpreter.RSCrash Wasm_Interpreter.CError)))
                               | (sa, (vlsa, Wasm_Interpreter.RSNormal esa)) ->
                                 (sa, (vs,
Wasm_Interpreter.RSNormal
  (List.map (fun v -> Wasm.Basic (Wasm.EConst v)) (List.rev ves) @
    [Wasm.Local (ln, j, vlsa, esa)]))))))));;

let rec wasm_execution_ocaml_run_v
  n d i (s, (vs, es)) =
    (if Arith.equal_nat n Arith.zero_nat
      then (s, Wasm_Interpreter.RCrash Wasm_Interpreter.CExhaustion)
      else (if wasm_execution_ocaml_es_is_trap es
             then (s, Wasm_Interpreter.RTrap)
             else (if Wasm.const_list es
                    then (s, Wasm_Interpreter.RValue
                               (Product_Type.fst
                                 (Wasm_Interpreter.split_vals_e es)))
                    else (match wasm_execution_ocaml_run_step d i (s, (vs, es))
                           with (_, (_, Wasm_Interpreter.RSCrash error)) ->
                             (s, Wasm_Interpreter.RCrash error)
                           | (_, (_, Wasm_Interpreter.RSBreak (_, _))) ->
                             (s, Wasm_Interpreter.RCrash
                                   Wasm_Interpreter.CError)
                           | (_, (_, Wasm_Interpreter.RSReturn _)) ->
                             (s, Wasm_Interpreter.RCrash
                                   Wasm_Interpreter.CError)
                           | (sa, (vsa, Wasm_Interpreter.RSNormal esa)) ->
                             wasm_execution_ocaml_run_v
                               (Arith.minus_nat n Arith.one_nata) d i
                               (sa, (vsa, esa))))));;

let rec run
  x = wasm_execution_ocaml_run_v
        (Arith.power Arith.power_nat
          (Arith.nat_of_integer (Big_int.big_int_of_int 2))
          (Arith.nat_of_integer (Big_int.big_int_of_int 63)))
        (Arith.nat_of_integer (Big_int.big_int_of_int 300)) x;;

end;; (*struct Wasm_Interpreter_Printing*)
