module HOL : sig
  type 'a equal = {equal : 'a -> 'a -> bool}
  val equal : 'a equal -> 'a -> 'a -> bool
  val eq : 'a equal -> 'a -> 'a -> bool
end = struct

type 'a equal = {equal : 'a -> 'a -> bool};;
let equal _A = _A.equal;;

let rec eq _A a b = equal _A a b;;

end;; (*struct HOL*)

module Orderings : sig
  type 'a ord = {less_eq : 'a -> 'a -> bool; less : 'a -> 'a -> bool}
  val less_eq : 'a ord -> 'a -> 'a -> bool
  val less : 'a ord -> 'a -> 'a -> bool
  val max : 'a ord -> 'a -> 'a -> 'a
end = struct

type 'a ord = {less_eq : 'a -> 'a -> bool; less : 'a -> 'a -> bool};;
let less_eq _A = _A.less_eq;;
let less _A = _A.less;;

let rec max _A a b = (if less_eq _A a b then b else a);;

end;; (*struct Orderings*)

module Arith : sig
  type nat = Nat of Big_int.big_int
  type num = One | Bit0 of num | Bit1 of num
  val one_nata : nat
  type 'a one = {one : 'a}
  val one : 'a one -> 'a
  val one_nat : nat one
  val integer_of_nat : nat -> Big_int.big_int
  val times_nata : nat -> nat -> nat
  type 'a times = {times : 'a -> 'a -> 'a}
  val times : 'a times -> 'a -> 'a -> 'a
  type 'a power = {one_power : 'a one; times_power : 'a times}
  val times_nat : nat times
  val power_nat : nat power
  val ord_integer : Big_int.big_int Orderings.ord
  type 'a zero = {zero : 'a}
  val zero : 'a zero -> 'a
  val plus_nat : nat -> nat -> nat
  val suc : nat -> nat
  val minus_nat : nat -> nat -> nat
  val equal_nat : nat -> nat -> bool
  val zero_nat : nat
  val power : 'a power -> 'a -> nat -> 'a
  val less_nat : nat -> nat -> bool
  val nat_of_integer : Big_int.big_int -> nat
  val less_eq_nat : nat -> nat -> bool
end = struct

type nat = Nat of Big_int.big_int;;

type num = One | Bit0 of num | Bit1 of num;;

let one_nata : nat = Nat (Big_int.big_int_of_int 1);;

type 'a one = {one : 'a};;
let one _A = _A.one;;

let one_nat = ({one = one_nata} : nat one);;

let rec integer_of_nat (Nat x) = x;;

let rec times_nata
  m n = Nat (Big_int.mult_big_int (integer_of_nat m) (integer_of_nat n));;

type 'a times = {times : 'a -> 'a -> 'a};;
let times _A = _A.times;;

type 'a power = {one_power : 'a one; times_power : 'a times};;

let times_nat = ({times = times_nata} : nat times);;

let power_nat = ({one_power = one_nat; times_power = times_nat} : nat power);;

let ord_integer =
  ({Orderings.less_eq = Big_int.le_big_int; Orderings.less = Big_int.lt_big_int}
    : Big_int.big_int Orderings.ord);;

type 'a zero = {zero : 'a};;
let zero _A = _A.zero;;

let rec plus_nat
  m n = Nat (Big_int.add_big_int (integer_of_nat m) (integer_of_nat n));;

let rec suc n = plus_nat n one_nata;;

let rec minus_nat
  m n = Nat (Orderings.max ord_integer Big_int.zero_big_int
              (Big_int.sub_big_int (integer_of_nat m) (integer_of_nat n)));;

let rec equal_nat
  m n = Big_int.eq_big_int (integer_of_nat m) (integer_of_nat n);;

let zero_nat : nat = Nat Big_int.zero_big_int;;

let rec power _A
  a n = (if equal_nat n zero_nat then one _A.one_power
          else times _A.times_power a (power _A a (minus_nat n one_nata)));;

let rec less_nat
  m n = Big_int.lt_big_int (integer_of_nat m) (integer_of_nat n);;

let rec nat_of_integer
  k = Nat (Orderings.max ord_integer Big_int.zero_big_int k);;

let rec less_eq_nat
  m n = Big_int.le_big_int (integer_of_nat m) (integer_of_nat n);;

end;; (*struct Arith*)

module List : sig
  val nth : 'a list -> Arith.nat -> 'a
  val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
  val rev : 'a list -> 'a list
  val null : 'a list -> bool
  val last : 'a list -> 'a
  val take : Arith.nat -> 'a list -> 'a list
  val map : ('a -> 'b) -> 'a list -> 'b list
  val gen_length : Arith.nat -> 'a list -> Arith.nat
  val list_update : 'a list -> Arith.nat -> 'a -> 'a list
  val list_all : ('a -> bool) -> 'a list -> bool
  val list_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
  val size_list : 'a list -> Arith.nat
  val equal_list : 'a HOL.equal -> 'a list -> 'a list -> bool
end = struct

let rec nth
  (x :: xs) n =
    (if Arith.equal_nat n Arith.zero_nat then x
      else nth xs (Arith.minus_nat n Arith.one_nata));;

let rec fold f x1 s = match f, x1, s with f, x :: xs, s -> fold f xs (f x s)
               | f, [], s -> s;;

let rec rev xs = fold (fun a b -> a :: b) xs [];;

let rec null = function [] -> true
               | x :: xs -> false;;

let rec last (x :: xs) = (if null xs then x else last xs);;

let rec take
  n x1 = match n, x1 with n, [] -> []
    | n, x :: xs ->
        (if Arith.equal_nat n Arith.zero_nat then []
          else x :: take (Arith.minus_nat n Arith.one_nata) xs);;

let rec map f x1 = match f, x1 with f, [] -> []
              | f, x21 :: x22 -> f x21 :: map f x22;;

let rec gen_length
  n x1 = match n, x1 with n, x :: xs -> gen_length (Arith.suc n) xs
    | n, [] -> n;;

let rec list_update
  x0 i y = match x0, i, y with [], i, y -> []
    | x :: xs, i, y ->
        (if Arith.equal_nat i Arith.zero_nat then y :: xs
          else x :: list_update xs (Arith.minus_nat i Arith.one_nata) y);;

let rec list_all p x1 = match p, x1 with p, [] -> true
                   | p, x :: xs -> p x && list_all p xs;;

let rec list_all2
  p xs ys = match p, xs, ys with
    p, x :: xs, y :: ys -> p x y && list_all2 p xs ys
    | p, xs, [] -> null xs
    | p, [], ys -> null ys;;

let rec size_list x = gen_length Arith.zero_nat x;;

let rec equal_list _A
  x0 x1 = match x0, x1 with [], x21 :: x22 -> false
    | x21 :: x22, [] -> false
    | x21 :: x22, y21 :: y22 -> HOL.eq _A x21 y21 && equal_list _A x22 y22
    | [], [] -> true;;

end;; (*struct List*)

module Wasm_Type_Abs : sig
  type 'a wasm_base = {zero_wasm_base : 'a Arith.zero}
  type 'a wasm_int =
    {wasm_base_wasm_int : 'a wasm_base; int_clz : 'a -> 'a; int_ctz : 'a -> 'a;
      int_popcnt : 'a -> 'a; int_add : 'a -> 'a -> 'a option;
      int_sub : 'a -> 'a -> 'a option; int_mul : 'a -> 'a -> 'a option;
      int_div_u : 'a -> 'a -> 'a option; int_div_s : 'a -> 'a -> 'a option;
      int_rem_u : 'a -> 'a -> 'a option; int_rem_s : 'a -> 'a -> 'a option;
      int_and : 'a -> 'a -> 'a option; int_or : 'a -> 'a -> 'a option;
      int_xor : 'a -> 'a -> 'a option; int_shl : 'a -> 'a -> 'a option;
      int_shr_u : 'a -> 'a -> 'a option; int_shr_s : 'a -> 'a -> 'a option;
      int_rotl : 'a -> 'a -> 'a option; int_rotr : 'a -> 'a -> 'a option;
      int_eqz : 'a -> bool; int_eq : 'a -> 'a -> bool;
      int_lt_u : 'a -> 'a -> bool; int_lt_s : 'a -> 'a -> bool;
      int_gt_u : 'a -> 'a -> bool; int_gt_s : 'a -> 'a -> bool;
      int_le_u : 'a -> 'a -> bool; int_le_s : 'a -> 'a -> bool;
      int_ge_u : 'a -> 'a -> bool; int_ge_s : 'a -> 'a -> bool;
      int_of_nat : Arith.nat -> 'a; nat_of_int : 'a -> Arith.nat}
  val int_clz : 'a wasm_int -> 'a -> 'a
  val int_ctz : 'a wasm_int -> 'a -> 'a
  val int_popcnt : 'a wasm_int -> 'a -> 'a
  val int_add : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_sub : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_mul : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_div_u : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_div_s : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_rem_u : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_rem_s : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_and : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_or : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_xor : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_shl : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_shr_u : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_shr_s : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_rotl : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_rotr : 'a wasm_int -> 'a -> 'a -> 'a option
  val int_eqz : 'a wasm_int -> 'a -> bool
  val int_eq : 'a wasm_int -> 'a -> 'a -> bool
  val int_lt_u : 'a wasm_int -> 'a -> 'a -> bool
  val int_lt_s : 'a wasm_int -> 'a -> 'a -> bool
  val int_gt_u : 'a wasm_int -> 'a -> 'a -> bool
  val int_gt_s : 'a wasm_int -> 'a -> 'a -> bool
  val int_le_u : 'a wasm_int -> 'a -> 'a -> bool
  val int_le_s : 'a wasm_int -> 'a -> 'a -> bool
  val int_ge_u : 'a wasm_int -> 'a -> 'a -> bool
  val int_ge_s : 'a wasm_int -> 'a -> 'a -> bool
  val int_of_nat : 'a wasm_int -> Arith.nat -> 'a
  val nat_of_int : 'a wasm_int -> 'a -> Arith.nat
  type 'a wasm_float =
    {wasm_base_wasm_float : 'a wasm_base; float_neg : 'a -> 'a;
      float_abs : 'a -> 'a; float_ceil : 'a -> 'a; float_floor : 'a -> 'a;
      float_trunc : 'a -> 'a; float_nearest : 'a -> 'a; float_sqrt : 'a -> 'a;
      float_add : 'a -> 'a -> 'a; float_sub : 'a -> 'a -> 'a;
      float_mul : 'a -> 'a -> 'a; float_div : 'a -> 'a -> 'a;
      float_min : 'a -> 'a -> 'a; float_max : 'a -> 'a -> 'a;
      float_copysign : 'a -> 'a -> 'a; float_eq : 'a -> 'a -> bool;
      float_lt : 'a -> 'a -> bool; float_gt : 'a -> 'a -> bool;
      float_le : 'a -> 'a -> bool; float_ge : 'a -> 'a -> bool}
  val float_neg : 'a wasm_float -> 'a -> 'a
  val float_abs : 'a wasm_float -> 'a -> 'a
  val float_ceil : 'a wasm_float -> 'a -> 'a
  val float_floor : 'a wasm_float -> 'a -> 'a
  val float_trunc : 'a wasm_float -> 'a -> 'a
  val float_nearest : 'a wasm_float -> 'a -> 'a
  val float_sqrt : 'a wasm_float -> 'a -> 'a
  val float_add : 'a wasm_float -> 'a -> 'a -> 'a
  val float_sub : 'a wasm_float -> 'a -> 'a -> 'a
  val float_mul : 'a wasm_float -> 'a -> 'a -> 'a
  val float_div : 'a wasm_float -> 'a -> 'a -> 'a
  val float_min : 'a wasm_float -> 'a -> 'a -> 'a
  val float_max : 'a wasm_float -> 'a -> 'a -> 'a
  val float_copysign : 'a wasm_float -> 'a -> 'a -> 'a
  val float_eq : 'a wasm_float -> 'a -> 'a -> bool
  val float_lt : 'a wasm_float -> 'a -> 'a -> bool
  val float_gt : 'a wasm_float -> 'a -> 'a -> bool
  val float_le : 'a wasm_float -> 'a -> 'a -> bool
  val float_ge : 'a wasm_float -> 'a -> 'a -> bool
end = struct

type 'a wasm_base = {zero_wasm_base : 'a Arith.zero};;

type 'a wasm_int =
  {wasm_base_wasm_int : 'a wasm_base; int_clz : 'a -> 'a; int_ctz : 'a -> 'a;
    int_popcnt : 'a -> 'a; int_add : 'a -> 'a -> 'a option;
    int_sub : 'a -> 'a -> 'a option; int_mul : 'a -> 'a -> 'a option;
    int_div_u : 'a -> 'a -> 'a option; int_div_s : 'a -> 'a -> 'a option;
    int_rem_u : 'a -> 'a -> 'a option; int_rem_s : 'a -> 'a -> 'a option;
    int_and : 'a -> 'a -> 'a option; int_or : 'a -> 'a -> 'a option;
    int_xor : 'a -> 'a -> 'a option; int_shl : 'a -> 'a -> 'a option;
    int_shr_u : 'a -> 'a -> 'a option; int_shr_s : 'a -> 'a -> 'a option;
    int_rotl : 'a -> 'a -> 'a option; int_rotr : 'a -> 'a -> 'a option;
    int_eqz : 'a -> bool; int_eq : 'a -> 'a -> bool;
    int_lt_u : 'a -> 'a -> bool; int_lt_s : 'a -> 'a -> bool;
    int_gt_u : 'a -> 'a -> bool; int_gt_s : 'a -> 'a -> bool;
    int_le_u : 'a -> 'a -> bool; int_le_s : 'a -> 'a -> bool;
    int_ge_u : 'a -> 'a -> bool; int_ge_s : 'a -> 'a -> bool;
    int_of_nat : Arith.nat -> 'a; nat_of_int : 'a -> Arith.nat};;
let int_clz _A = _A.int_clz;;
let int_ctz _A = _A.int_ctz;;
let int_popcnt _A = _A.int_popcnt;;
let int_add _A = _A.int_add;;
let int_sub _A = _A.int_sub;;
let int_mul _A = _A.int_mul;;
let int_div_u _A = _A.int_div_u;;
let int_div_s _A = _A.int_div_s;;
let int_rem_u _A = _A.int_rem_u;;
let int_rem_s _A = _A.int_rem_s;;
let int_and _A = _A.int_and;;
let int_or _A = _A.int_or;;
let int_xor _A = _A.int_xor;;
let int_shl _A = _A.int_shl;;
let int_shr_u _A = _A.int_shr_u;;
let int_shr_s _A = _A.int_shr_s;;
let int_rotl _A = _A.int_rotl;;
let int_rotr _A = _A.int_rotr;;
let int_eqz _A = _A.int_eqz;;
let int_eq _A = _A.int_eq;;
let int_lt_u _A = _A.int_lt_u;;
let int_lt_s _A = _A.int_lt_s;;
let int_gt_u _A = _A.int_gt_u;;
let int_gt_s _A = _A.int_gt_s;;
let int_le_u _A = _A.int_le_u;;
let int_le_s _A = _A.int_le_s;;
let int_ge_u _A = _A.int_ge_u;;
let int_ge_s _A = _A.int_ge_s;;
let int_of_nat _A = _A.int_of_nat;;
let nat_of_int _A = _A.nat_of_int;;

type 'a wasm_float =
  {wasm_base_wasm_float : 'a wasm_base; float_neg : 'a -> 'a;
    float_abs : 'a -> 'a; float_ceil : 'a -> 'a; float_floor : 'a -> 'a;
    float_trunc : 'a -> 'a; float_nearest : 'a -> 'a; float_sqrt : 'a -> 'a;
    float_add : 'a -> 'a -> 'a; float_sub : 'a -> 'a -> 'a;
    float_mul : 'a -> 'a -> 'a; float_div : 'a -> 'a -> 'a;
    float_min : 'a -> 'a -> 'a; float_max : 'a -> 'a -> 'a;
    float_copysign : 'a -> 'a -> 'a; float_eq : 'a -> 'a -> bool;
    float_lt : 'a -> 'a -> bool; float_gt : 'a -> 'a -> bool;
    float_le : 'a -> 'a -> bool; float_ge : 'a -> 'a -> bool};;
let float_neg _A = _A.float_neg;;
let float_abs _A = _A.float_abs;;
let float_ceil _A = _A.float_ceil;;
let float_floor _A = _A.float_floor;;
let float_trunc _A = _A.float_trunc;;
let float_nearest _A = _A.float_nearest;;
let float_sqrt _A = _A.float_sqrt;;
let float_add _A = _A.float_add;;
let float_sub _A = _A.float_sub;;
let float_mul _A = _A.float_mul;;
let float_div _A = _A.float_div;;
let float_min _A = _A.float_min;;
let float_max _A = _A.float_max;;
let float_copysign _A = _A.float_copysign;;
let float_eq _A = _A.float_eq;;
let float_lt _A = _A.float_lt;;
let float_gt _A = _A.float_gt;;
let float_le _A = _A.float_le;;
let float_ge _A = _A.float_ge;;

end;; (*struct Wasm_Type_Abs*)

module Product_Type : sig
  val fst : 'a * 'b -> 'a
  val equal_bool : bool -> bool -> bool
end = struct

let rec fst (x1, x2) = x1;;

let rec equal_bool p pa = match p, pa with p, true -> p
                     | p, false -> not p
                     | true, p -> p
                     | false, p -> not p;;

end;; (*struct Product_Type*)

module Option : sig
  val is_none : 'a option -> bool
end = struct

let rec is_none = function Some x -> false
                  | None -> true;;

end;; (*struct Option*)

module Wasm : sig
  type t = T_i32 | T_i64 | T_f32 | T_f64
  val equal_ta : t -> t -> bool
  val equal_t : t HOL.equal
  type sx = S | U
  type relop_i = Eq | Ne | Lt of sx | Gt of sx | Le of sx | Ge of sx
  type relop_f = Eqf | Nef | Ltf | Gtf | Lef | Gef
  type 'a ne_list = Base of 'a | Conz of 'a * 'a ne_list
  type binop_i = Add | Sub | Mul | Div of sx | Rem of sx | And | Or | Xor | Shl
    | Shr of sx | Rotl | Rotr
  type binop_f = Addf | Subf | Mulf | Divf | Min | Max | Copysign
  type unop_i = Clz | Ctz | Popcnt
  type unop_f = Neg | Abs | Ceil | Floor | Trunc | Nearest | Sqrt
  type testop = Eqz
  type cvtop = Convert | Reinterpret
  type tp = Tp_i8 | Tp_i16 | Tp_i32
  type tf = Tf of t list * t list
  type ('a, 'b, 'c, 'd) v = ConstInt32 of 'a | ConstInt64 of 'b |
    ConstFloat32 of 'c | ConstFloat64 of 'd
  type ('a, 'b, 'c, 'd) b_e = Unreachable | Nop | Drop | Select |
    Block of tf * ('a, 'b, 'c, 'd) b_e list |
    Loop of tf * ('a, 'b, 'c, 'd) b_e list |
    If of tf * ('a, 'b, 'c, 'd) b_e list * ('a, 'b, 'c, 'd) b_e list |
    Br of Arith.nat | Br_if of Arith.nat | Br_table of Arith.nat ne_list |
    Return | Call of Arith.nat | Call_indirect of Arith.nat |
    Get_local of Arith.nat | Set_local of Arith.nat | Tee_local of Arith.nat |
    Get_global of Arith.nat | Set_global of Arith.nat |
    Load of t * (tp * sx) option * Arith.nat * Arith.nat |
    Store of t * tp option * Arith.nat * Arith.nat | Current_memory |
    Grow_memory | EConst of ('a, 'b, 'c, 'd) v | Unop_i of t * unop_i |
    Unop_f of t * unop_f | Binop_i of t * binop_i | Binop_f of t * binop_f |
    Testop of t * testop | Relop_i of t * relop_i | Relop_f of t * relop_f |
    Cvtop of t * cvtop * t * sx option
  type ('a, 'b, 'c, 'd, 'e) cl =
    Func_native of Arith.nat * tf * t list * ('a, 'b, 'c, 'd) b_e list |
    Func_host of tf * 'e
  type ('a, 'b, 'c, 'd, 'e) e = Basic of ('a, 'b, 'c, 'd) b_e | Trap |
    Callcl of ('a, 'b, 'c, 'd, 'e) cl |
    Label of
      Arith.nat * ('a, 'b, 'c, 'd, 'e) e list * ('a, 'b, 'c, 'd, 'e) e list
    | Local of
        Arith.nat * Arith.nat * ('a, 'b, 'c, 'd) v list *
          ('a, 'b, 'c, 'd, 'e) e list
  type mut = T_immut | T_mut
  type ('a, 'b, 'c, 'd, 'e) global_ext =
    Global_ext of mut * ('a, 'b, 'c, 'd) v * 'e
  type 'a inst_ext =
    Inst_ext of
      tf list * Arith.nat list * Arith.nat option * Arith.nat option *
        Arith.nat list * 'a
  type ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext =
    S_ext of
      unit inst_ext list * ('a, 'b, 'c, 'd, 'f) cl list *
        ((('a, 'b, 'c, 'd, 'f) cl option) list) list * 'e list *
        ('a, 'b, 'c, 'd, unit) global_ext list * 'g
  type 'a tg_ext = Tg_ext of mut * t * 'a
  type 'a t_context_ext =
    T_context_ext of
      tf list * tf list * unit tg_ext list * Arith.nat option *
        Arith.nat option * t list * (t list) list * (t list) option * 'a
  val taba : 'a inst_ext -> Arith.nat option
  val tab :
    ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext ->
      ((('a, 'b, 'c, 'd, 'f) cl option) list) list
  val stab_s :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat -> Arith.nat -> ('a, 'b, 'c, 'd, 'f) cl option
  val inst : ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext -> unit inst_ext list
  val stab :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat -> Arith.nat -> ('a, 'b, 'c, 'd, 'f) cl option
  val mem : ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext -> 'e list
  val funcsa : 'a inst_ext -> Arith.nat list
  val sfunc_ind :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext -> Arith.nat -> Arith.nat -> Arith.nat
  val funcs : ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext -> ('a, 'b, 'c, 'd, 'f) cl list
  val sfunc :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat -> Arith.nat -> ('a, 'b, 'c, 'd, 'f) cl
  val globsa : 'a inst_ext -> Arith.nat list
  val sglob_ind :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext -> Arith.nat -> Arith.nat -> Arith.nat
  val globs :
    ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext -> ('a, 'b, 'c, 'd, unit) global_ext list
  val sglob :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat -> Arith.nat -> ('a, 'b, 'c, 'd, unit) global_ext
  val equal_mut : mut -> mut -> bool
  val tg_mut : 'a tg_ext -> mut
  val is_mut : unit tg_ext -> bool
  val types : 'a inst_ext -> tf list
  val stypes :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext -> Arith.nat -> Arith.nat -> tf
  val typeof : ('a, 'b, 'c, 'd) v -> t
  val cl_type : ('a, 'b, 'c, 'd, 'e) cl -> tf
  val tg_t : 'a tg_ext -> t
  val to_list : 'a ne_list -> 'a list
  val mema : 'a inst_ext -> Arith.nat option
  val is_const : ('a, 'b, 'c, 'd, 'e) e -> bool
  val is_int_t : t -> bool
  val t_length : t -> Arith.nat
  val g_val : ('a, 'b, 'c, 'd, 'e) global_ext -> ('a, 'b, 'c, 'd) v
  val sglob_val :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat -> Arith.nat -> ('a, 'b, 'c, 'd) v
  val tp_length : tp -> Arith.nat
  val app_unop_f : 'a Wasm_Type_Abs.wasm_float -> unop_f -> 'a -> 'a
  val app_unop_i : 'a Wasm_Type_Abs.wasm_int -> unop_i -> 'a -> 'a
  val const_list : ('a, 'b, 'c, 'd, 'e) e list -> bool
  val is_float_t : t -> bool
  val app_binop_f :
    'a Wasm_Type_Abs.wasm_float -> binop_f -> 'a -> 'a -> 'a option
  val app_binop_i :
    'a Wasm_Type_Abs.wasm_int -> binop_i -> 'a -> 'a -> 'a option
  val app_relop_f : 'a Wasm_Type_Abs.wasm_float -> relop_f -> 'a -> 'a -> bool
  val app_relop_i : 'a Wasm_Type_Abs.wasm_int -> relop_i -> 'a -> 'a -> bool
  val types_agree : t -> ('a, 'b, 'c, 'd) v -> bool
  val app_testop_i : 'a Wasm_Type_Abs.wasm_int -> testop -> 'a -> bool
  val option_projl : ('a * 'b) option -> 'a option
  val mem_update :
    ('a list -> 'a list) ->
      ('b, 'c, 'd, 'e, 'a, 'f, 'g) s_ext -> ('b, 'c, 'd, 'e, 'a, 'f, 'g) s_ext
  val g_val_update :
    (('a, 'b, 'c, 'd) v -> ('a, 'b, 'c, 'd) v) ->
      ('a, 'b, 'c, 'd, 'e) global_ext -> ('a, 'b, 'c, 'd, 'e) global_ext
  val globs_update :
    (('a, 'b, 'c, 'd, unit) global_ext list ->
      ('a, 'b, 'c, 'd, unit) global_ext list) ->
      ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext -> ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext
  val supdate_glob_s :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat -> ('a, 'b, 'c, 'd) v -> ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext
  val supdate_glob :
    ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext ->
      Arith.nat ->
        Arith.nat -> ('a, 'b, 'c, 'd) v -> ('a, 'b, 'c, 'd, 'e, 'f, unit) s_ext
  val label : 'a t_context_ext -> (t list) list
  val local : 'a t_context_ext -> t list
  val table : 'a t_context_ext -> Arith.nat option
  val func_t : 'a t_context_ext -> tf list
  val global : 'a t_context_ext -> unit tg_ext list
  val memory : 'a t_context_ext -> Arith.nat option
  val return : 'a t_context_ext -> (t list) option
  val types_t : 'a t_context_ext -> tf list
  val equal_tf : tf -> tf -> bool
  val label_update :
    ((t list) list -> (t list) list) -> 'a t_context_ext -> 'a t_context_ext
  val load_store_t_bounds : Arith.nat -> tp option -> t -> bool
end = struct

type t = T_i32 | T_i64 | T_f32 | T_f64;;

let rec equal_ta x0 x1 = match x0, x1 with T_f32, T_f64 -> false
                   | T_f64, T_f32 -> false
                   | T_i64, T_f64 -> false
                   | T_f64, T_i64 -> false
                   | T_i64, T_f32 -> false
                   | T_f32, T_i64 -> false
                   | T_i32, T_f64 -> false
                   | T_f64, T_i32 -> false
                   | T_i32, T_f32 -> false
                   | T_f32, T_i32 -> false
                   | T_i32, T_i64 -> false
                   | T_i64, T_i32 -> false
                   | T_f64, T_f64 -> true
                   | T_f32, T_f32 -> true
                   | T_i64, T_i64 -> true
                   | T_i32, T_i32 -> true;;

let equal_t = ({HOL.equal = equal_ta} : t HOL.equal);;

type sx = S | U;;

type relop_i = Eq | Ne | Lt of sx | Gt of sx | Le of sx | Ge of sx;;

type relop_f = Eqf | Nef | Ltf | Gtf | Lef | Gef;;

type 'a ne_list = Base of 'a | Conz of 'a * 'a ne_list;;

type binop_i = Add | Sub | Mul | Div of sx | Rem of sx | And | Or | Xor | Shl |
  Shr of sx | Rotl | Rotr;;

type binop_f = Addf | Subf | Mulf | Divf | Min | Max | Copysign;;

type unop_i = Clz | Ctz | Popcnt;;

type unop_f = Neg | Abs | Ceil | Floor | Trunc | Nearest | Sqrt;;

type testop = Eqz;;

type cvtop = Convert | Reinterpret;;

type tp = Tp_i8 | Tp_i16 | Tp_i32;;

type tf = Tf of t list * t list;;

type ('a, 'b, 'c, 'd) v = ConstInt32 of 'a | ConstInt64 of 'b |
  ConstFloat32 of 'c | ConstFloat64 of 'd;;

type ('a, 'b, 'c, 'd) b_e = Unreachable | Nop | Drop | Select |
  Block of tf * ('a, 'b, 'c, 'd) b_e list |
  Loop of tf * ('a, 'b, 'c, 'd) b_e list |
  If of tf * ('a, 'b, 'c, 'd) b_e list * ('a, 'b, 'c, 'd) b_e list |
  Br of Arith.nat | Br_if of Arith.nat | Br_table of Arith.nat ne_list | Return
  | Call of Arith.nat | Call_indirect of Arith.nat | Get_local of Arith.nat |
  Set_local of Arith.nat | Tee_local of Arith.nat | Get_global of Arith.nat |
  Set_global of Arith.nat | Load of t * (tp * sx) option * Arith.nat * Arith.nat
  | Store of t * tp option * Arith.nat * Arith.nat | Current_memory |
  Grow_memory | EConst of ('a, 'b, 'c, 'd) v | Unop_i of t * unop_i |
  Unop_f of t * unop_f | Binop_i of t * binop_i | Binop_f of t * binop_f |
  Testop of t * testop | Relop_i of t * relop_i | Relop_f of t * relop_f |
  Cvtop of t * cvtop * t * sx option;;

type ('a, 'b, 'c, 'd, 'e) cl =
  Func_native of Arith.nat * tf * t list * ('a, 'b, 'c, 'd) b_e list |
  Func_host of tf * 'e;;

type ('a, 'b, 'c, 'd, 'e) e = Basic of ('a, 'b, 'c, 'd) b_e | Trap |
  Callcl of ('a, 'b, 'c, 'd, 'e) cl |
  Label of Arith.nat * ('a, 'b, 'c, 'd, 'e) e list * ('a, 'b, 'c, 'd, 'e) e list
  | Local of
      Arith.nat * Arith.nat * ('a, 'b, 'c, 'd) v list *
        ('a, 'b, 'c, 'd, 'e) e list;;

type mut = T_immut | T_mut;;

type ('a, 'b, 'c, 'd, 'e) global_ext =
  Global_ext of mut * ('a, 'b, 'c, 'd) v * 'e;;

type 'a inst_ext =
  Inst_ext of
    tf list * Arith.nat list * Arith.nat option * Arith.nat option *
      Arith.nat list * 'a;;

type ('a, 'b, 'c, 'd, 'e, 'f, 'g) s_ext =
  S_ext of
    unit inst_ext list * ('a, 'b, 'c, 'd, 'f) cl list *
      ((('a, 'b, 'c, 'd, 'f) cl option) list) list * 'e list *
      ('a, 'b, 'c, 'd, unit) global_ext list * 'g;;

type 'a tg_ext = Tg_ext of mut * t * 'a;;

type 'a t_context_ext =
  T_context_ext of
    tf list * tf list * unit tg_ext list * Arith.nat option * Arith.nat option *
      t list * (t list) list * (t list) option * 'a;;

let rec taba (Inst_ext (types, funcs, tab, mem, globs, more)) = tab;;

let rec tab (S_ext (inst, funcs, tab, mem, globs, more)) = tab;;

let rec stab_s
  s i j =
    (let stabinst = List.nth (tab s) i in
      (if Arith.less_nat j (List.size_list stabinst) then List.nth stabinst j
        else None));;

let rec inst (S_ext (inst, funcs, tab, mem, globs, more)) = inst;;

let rec stab
  s i j =
    (match taba (List.nth (inst s) i) with None -> None
      | Some k -> stab_s s k j);;

let rec mem (S_ext (inst, funcs, tab, mem, globs, more)) = mem;;

let rec funcsa (Inst_ext (types, funcs, tab, mem, globs, more)) = funcs;;

let rec sfunc_ind s i j = List.nth (funcsa (List.nth (inst s) i)) j;;

let rec funcs (S_ext (inst, funcs, tab, mem, globs, more)) = funcs;;

let rec sfunc s i j = List.nth (funcs s) (sfunc_ind s i j);;

let rec globsa (Inst_ext (types, funcs, tab, mem, globs, more)) = globs;;

let rec sglob_ind s i j = List.nth (globsa (List.nth (inst s) i)) j;;

let rec globs (S_ext (inst, funcs, tab, mem, globs, more)) = globs;;

let rec sglob s i j = List.nth (globs s) (sglob_ind s i j);;

let rec equal_mut x0 x1 = match x0, x1 with T_immut, T_mut -> false
                    | T_mut, T_immut -> false
                    | T_mut, T_mut -> true
                    | T_immut, T_immut -> true;;

let rec tg_mut (Tg_ext (tg_mut, tg_t, more)) = tg_mut;;

let rec is_mut tg = equal_mut (tg_mut tg) T_mut;;

let rec types (Inst_ext (types, funcs, tab, mem, globs, more)) = types;;

let rec stypes s i j = List.nth (types (List.nth (inst s) i)) j;;

let rec typeof
  v = (match v with ConstInt32 _ -> T_i32 | ConstInt64 _ -> T_i64
        | ConstFloat32 _ -> T_f32 | ConstFloat64 _ -> T_f64);;

let rec cl_type
  cl = (match cl with Func_native (_, tf, _, _) -> tf
         | Func_host (tf, _) -> tf);;

let rec tg_t (Tg_ext (tg_mut, tg_t, more)) = tg_t;;

let rec to_list = function Base a -> [a]
                  | Conz (a, l) -> a :: to_list l;;

let rec mema (Inst_ext (types, funcs, tab, mem, globs, more)) = mem;;

let rec is_const
  e = (match e with Basic Unreachable -> false | Basic Nop -> false
        | Basic Drop -> false | Basic Select -> false
        | Basic (Block (_, _)) -> false | Basic (Loop (_, _)) -> false
        | Basic (If (_, _, _)) -> false | Basic (Br _) -> false
        | Basic (Br_if _) -> false | Basic (Br_table _) -> false
        | Basic Return -> false | Basic (Call _) -> false
        | Basic (Call_indirect _) -> false | Basic (Get_local _) -> false
        | Basic (Set_local _) -> false | Basic (Tee_local _) -> false
        | Basic (Get_global _) -> false | Basic (Set_global _) -> false
        | Basic (Load (_, _, _, _)) -> false
        | Basic (Store (_, _, _, _)) -> false | Basic Current_memory -> false
        | Basic Grow_memory -> false | Basic (EConst _) -> true
        | Basic (Unop_i (_, _)) -> false | Basic (Unop_f (_, _)) -> false
        | Basic (Binop_i (_, _)) -> false | Basic (Binop_f (_, _)) -> false
        | Basic (Testop (_, _)) -> false | Basic (Relop_i (_, _)) -> false
        | Basic (Relop_f (_, _)) -> false | Basic (Cvtop (_, _, _, _)) -> false
        | Trap -> false | Callcl _ -> false | Label (_, _, _) -> false
        | Local (_, _, _, _) -> false);;

let rec is_int_t
  t = (match t with T_i32 -> true | T_i64 -> true | T_f32 -> false
        | T_f64 -> false);;

let rec t_length
  t = (match t with T_i32 -> Arith.nat_of_integer (Big_int.big_int_of_int 4)
        | T_i64 -> Arith.nat_of_integer (Big_int.big_int_of_int 8)
        | T_f32 -> Arith.nat_of_integer (Big_int.big_int_of_int 4)
        | T_f64 -> Arith.nat_of_integer (Big_int.big_int_of_int 8));;

let rec g_val (Global_ext (g_mut, g_val, more)) = g_val;;

let rec sglob_val s i j = g_val (sglob s i j);;

let rec tp_length
  t = (match t with Tp_i8 -> Arith.one_nata
        | Tp_i16 -> Arith.nat_of_integer (Big_int.big_int_of_int 2)
        | Tp_i32 -> Arith.nat_of_integer (Big_int.big_int_of_int 4));;

let rec app_unop_f _A
  fop c =
    (match fop with Neg -> Wasm_Type_Abs.float_neg _A c
      | Abs -> Wasm_Type_Abs.float_abs _A c
      | Ceil -> Wasm_Type_Abs.float_ceil _A c
      | Floor -> Wasm_Type_Abs.float_floor _A c
      | Trunc -> Wasm_Type_Abs.float_trunc _A c
      | Nearest -> Wasm_Type_Abs.float_nearest _A c
      | Sqrt -> Wasm_Type_Abs.float_sqrt _A c);;

let rec app_unop_i _A
  iop c =
    (match iop with Clz -> Wasm_Type_Abs.int_clz _A c
      | Ctz -> Wasm_Type_Abs.int_ctz _A c
      | Popcnt -> Wasm_Type_Abs.int_popcnt _A c);;

let rec const_list xs = List.list_all is_const xs;;

let rec is_float_t
  t = (match t with T_i32 -> false | T_i64 -> false | T_f32 -> true
        | T_f64 -> true);;

let rec app_binop_f _A
  fop c1 c2 =
    (match fop with Addf -> Some (Wasm_Type_Abs.float_add _A c1 c2)
      | Subf -> Some (Wasm_Type_Abs.float_sub _A c1 c2)
      | Mulf -> Some (Wasm_Type_Abs.float_mul _A c1 c2)
      | Divf -> Some (Wasm_Type_Abs.float_div _A c1 c2)
      | Min -> Some (Wasm_Type_Abs.float_min _A c1 c2)
      | Max -> Some (Wasm_Type_Abs.float_max _A c1 c2)
      | Copysign -> Some (Wasm_Type_Abs.float_copysign _A c1 c2));;

let rec app_binop_i _A
  iop c1 c2 =
    (match iop with Add -> Wasm_Type_Abs.int_add _A c1 c2
      | Sub -> Wasm_Type_Abs.int_sub _A c1 c2
      | Mul -> Wasm_Type_Abs.int_mul _A c1 c2
      | Div S -> Wasm_Type_Abs.int_div_s _A c1 c2
      | Div U -> Wasm_Type_Abs.int_div_u _A c1 c2
      | Rem S -> Wasm_Type_Abs.int_rem_s _A c1 c2
      | Rem U -> Wasm_Type_Abs.int_rem_u _A c1 c2
      | And -> Wasm_Type_Abs.int_and _A c1 c2
      | Or -> Wasm_Type_Abs.int_or _A c1 c2
      | Xor -> Wasm_Type_Abs.int_xor _A c1 c2
      | Shl -> Wasm_Type_Abs.int_shl _A c1 c2
      | Shr S -> Wasm_Type_Abs.int_shr_s _A c1 c2
      | Shr U -> Wasm_Type_Abs.int_shr_u _A c1 c2
      | Rotl -> Wasm_Type_Abs.int_rotl _A c1 c2
      | Rotr -> Wasm_Type_Abs.int_rotr _A c1 c2);;

let rec app_relop_f _A
  rop c1 c2 =
    (match rop with Eqf -> Wasm_Type_Abs.float_eq _A c1 c2
      | Nef -> not (Wasm_Type_Abs.float_eq _A c1 c2)
      | Ltf -> Wasm_Type_Abs.float_lt _A c1 c2
      | Gtf -> Wasm_Type_Abs.float_gt _A c1 c2
      | Lef -> Wasm_Type_Abs.float_le _A c1 c2
      | Gef -> Wasm_Type_Abs.float_ge _A c1 c2);;

let rec app_relop_i _A
  rop c1 c2 =
    (match rop with Eq -> Wasm_Type_Abs.int_eq _A c1 c2
      | Ne -> not (Wasm_Type_Abs.int_eq _A c1 c2)
      | Lt S -> Wasm_Type_Abs.int_lt_s _A c1 c2
      | Lt U -> Wasm_Type_Abs.int_lt_u _A c1 c2
      | Gt S -> Wasm_Type_Abs.int_gt_s _A c1 c2
      | Gt U -> Wasm_Type_Abs.int_gt_u _A c1 c2
      | Le S -> Wasm_Type_Abs.int_le_s _A c1 c2
      | Le U -> Wasm_Type_Abs.int_le_u _A c1 c2
      | Ge S -> Wasm_Type_Abs.int_ge_s _A c1 c2
      | Ge U -> Wasm_Type_Abs.int_ge_u _A c1 c2);;

let rec types_agree t v = equal_ta (typeof v) t;;

let rec app_testop_i _A
  testop c = (let Eqz = testop in Wasm_Type_Abs.int_eqz _A c);;

let rec option_projl
  x = (match x with None -> None | Some a -> (let (aa, _) = a in Some aa));;

let rec mem_update
  mema (S_ext (inst, funcs, tab, mem, globs, more)) =
    S_ext (inst, funcs, tab, mema mem, globs, more);;

let rec g_val_update
  g_vala (Global_ext (g_mut, g_val, more)) =
    Global_ext (g_mut, g_vala g_val, more);;

let rec globs_update
  globsa (S_ext (inst, funcs, tab, mem, globs, more)) =
    S_ext (inst, funcs, tab, mem, globsa globs, more);;

let rec supdate_glob_s
  s k v =
    globs_update
      (fun _ ->
        List.list_update (globs s) k
          (g_val_update (fun _ -> v) (List.nth (globs s) k)))
      s;;

let rec supdate_glob
  s i j v = (let k = sglob_ind s i j in supdate_glob_s s k v);;

let rec label
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = label;;

let rec local
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = local;;

let rec table
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = table;;

let rec func_t
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = func_t;;

let rec global
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = global;;

let rec memory
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = memory;;

let rec return
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = return;;

let rec types_t
  (T_context_ext
    (types_t, func_t, global, table, memory, local, label, return, more))
    = types_t;;

let rec equal_tf
  (Tf (x1, x2)) (Tf (y1, y2)) =
    List.equal_list equal_t x1 y1 && List.equal_list equal_t x2 y2;;

let rec label_update
  labela
    (T_context_ext
      (types_t, func_t, global, table, memory, local, label, return, more))
    = T_context_ext
        (types_t, func_t, global, table, memory, local, labela label, return,
          more);;

let rec load_store_t_bounds
  a tp t =
    (match tp
      with None ->
        Arith.less_eq_nat
          (Arith.power Arith.power_nat
            (Arith.nat_of_integer (Big_int.big_int_of_int 2)) a)
          (t_length t)
      | Some tpa ->
        Arith.less_eq_nat
          (Arith.power Arith.power_nat
            (Arith.nat_of_integer (Big_int.big_int_of_int 2)) a)
          (tp_length tpa) &&
          (Arith.less_nat (tp_length tpa) (t_length t) && is_int_t t));;

end;; (*struct Wasm*)

module Wasm_Checker_Types : sig
  type ct = TAny | TSome of Wasm.t
  type checker_type = TopType of ct list | Type of Wasm.t list | Bot
  val ct_eq : ct -> ct -> bool
  val to_ct_list : Wasm.t list -> ct list
  val ct_prefix : ct list -> ct list -> bool
  val ct_suffix : ct list -> ct list -> bool
  val consume : checker_type -> ct list -> checker_type
  val produce : checker_type -> checker_type -> checker_type
  val type_update : checker_type -> ct list -> checker_type -> checker_type
  val c_types_agree : checker_type -> Wasm.t list -> bool
  val select_return_top : ct list -> ct -> ct -> checker_type
  val type_update_select : checker_type -> checker_type
end = struct

type ct = TAny | TSome of Wasm.t;;

type checker_type = TopType of ct list | Type of Wasm.t list | Bot;;

let rec ct_eq
  x0 uu = match x0, uu with TSome ta, TSome t -> Wasm.equal_ta ta t
    | TAny, uu -> true
    | TSome v, TAny -> true;;

let rec to_ct_list ts = List.map (fun a -> TSome a) ts;;

let rec ct_prefix
  x0 xs = match x0, xs with x :: xs, y :: ys -> ct_eq x y && ct_prefix xs ys
    | x :: xs, [] -> false
    | [], xs -> true;;

let rec ct_suffix xs ys = ct_prefix (List.rev xs) (List.rev ys);;

let rec consume
  x0 cons = match x0, cons with
    Type ts, cons ->
      (if ct_suffix cons (to_ct_list ts)
        then Type (List.take
                    (Arith.minus_nat (List.size_list ts) (List.size_list cons))
                    ts)
        else Bot)
    | TopType cts, cons ->
        (if ct_suffix cons cts
          then TopType
                 (List.take
                   (Arith.minus_nat (List.size_list cts) (List.size_list cons))
                   cts)
          else (if ct_suffix cts cons then TopType [] else Bot))
    | Bot, uv -> Bot;;

let rec produce
  uu uv = match uu, uv with
    TopType tsa, Type ts -> TopType (tsa @ to_ct_list ts)
    | Type tsa, Type ts -> Type (tsa @ ts)
    | Type tsa, TopType ts -> TopType ts
    | TopType tsa, TopType ts -> TopType ts
    | Type v, Bot -> Bot
    | Bot, uv -> Bot
    | uu, Bot -> Bot;;

let rec type_update
  curr_type cons prods = produce (consume curr_type cons) prods;;

let rec c_types_agree
  x0 ts = match x0, ts with Type tsa, ts -> List.equal_list Wasm.equal_t tsa ts
    | TopType tsa, ts -> ct_suffix tsa (to_ct_list ts)
    | Bot, uu -> false;;

let rec select_return_top
  ts ct1 x2 = match ts, ct1, x2 with
    ts, ct1, TAny ->
      TopType
        (List.take
           (Arith.minus_nat (List.size_list ts)
             (Arith.nat_of_integer (Big_int.big_int_of_int 3)))
           ts @
          [ct1])
    | ts, TAny, TSome v ->
        TopType
          (List.take
             (Arith.minus_nat (List.size_list ts)
               (Arith.nat_of_integer (Big_int.big_int_of_int 3)))
             ts @
            [TSome v])
    | ts, TSome t1, TSome t2 ->
        (if Wasm.equal_ta t1 t2
          then TopType
                 (List.take
                    (Arith.minus_nat (List.size_list ts)
                      (Arith.nat_of_integer (Big_int.big_int_of_int 3)))
                    ts @
                   [TSome t1])
          else Bot);;

let rec type_update_select
  = function
    Type ts ->
      (if Arith.less_eq_nat (Arith.nat_of_integer (Big_int.big_int_of_int 3))
            (List.size_list ts) &&
            Wasm.equal_ta
              (List.nth ts
                (Arith.minus_nat (List.size_list ts)
                  (Arith.nat_of_integer (Big_int.big_int_of_int 2))))
              (List.nth ts
                (Arith.minus_nat (List.size_list ts)
                  (Arith.nat_of_integer (Big_int.big_int_of_int 3))))
        then consume (Type ts) [TAny; TSome Wasm.T_i32] else Bot)
    | TopType ts ->
        (if Arith.equal_nat (List.size_list ts) Arith.zero_nat
          then TopType [TAny]
          else (if Arith.equal_nat
                     (Arith.minus_nat (List.size_list ts) Arith.one_nata)
                     Arith.zero_nat
                 then type_update (TopType ts) [TSome Wasm.T_i32]
                        (TopType [TAny])
                 else (if Arith.equal_nat
                            (Arith.minus_nat
                              (Arith.minus_nat (List.size_list ts)
                                Arith.one_nata)
                              Arith.one_nata)
                            Arith.zero_nat
                        then consume (TopType ts) [TSome Wasm.T_i32]
                        else type_update (TopType ts)
                               [TAny; TAny; TSome Wasm.T_i32]
                               (select_return_top ts
                                 (List.nth ts
                                   (Arith.minus_nat (List.size_list ts)
                                     (Arith.nat_of_integer
                                       (Big_int.big_int_of_int 2))))
                                 (List.nth ts
                                   (Arith.minus_nat (List.size_list ts)
                                     (Arith.nat_of_integer
                                       (Big_int.big_int_of_int 3))))))))
    | Bot -> Bot;;

end;; (*struct Wasm_Checker_Types*)

module Wasm_Checker : sig
  val convert_cond : Wasm.t -> Wasm.t -> Wasm.sx option -> bool
  val same_lab_h :
    Arith.nat list -> (Wasm.t list) list -> Wasm.t list -> (Wasm.t list) option
  val same_lab : Arith.nat list -> (Wasm.t list) list -> (Wasm.t list) option
  val check :
    unit Wasm.t_context_ext ->
      ('a, 'b, 'c, 'd) Wasm.b_e list ->
        Wasm_Checker_Types.checker_type -> Wasm_Checker_Types.checker_type
  val b_e_type_checker :
    unit Wasm.t_context_ext -> ('a, 'b, 'c, 'd) Wasm.b_e list -> Wasm.tf -> bool
  val check_single :
    unit Wasm.t_context_ext ->
      ('a, 'b, 'c, 'd) Wasm.b_e ->
        Wasm_Checker_Types.checker_type -> Wasm_Checker_Types.checker_type
end = struct

let rec convert_cond
  t1 t2 sx =
    not (Wasm.equal_ta t1 t2) &&
      Product_Type.equal_bool (Option.is_none sx)
        (Wasm.is_float_t t1 && Wasm.is_float_t t2 ||
          Wasm.is_int_t t1 &&
            (Wasm.is_int_t t2 &&
              Arith.less_nat (Wasm.t_length t1) (Wasm.t_length t2)));;

let rec same_lab_h
  x0 lab_c ts = match x0, lab_c, ts with
    i :: is, lab_c, ts ->
      (if Arith.less_eq_nat (List.size_list lab_c) i then None
        else (if List.equal_list Wasm.equal_t (List.nth lab_c i) ts
               then same_lab_h is lab_c (List.nth lab_c i) else None))
    | [], uu, ts -> Some ts;;

let rec same_lab
  x0 lab_c = match x0, lab_c with
    i :: is, lab_c ->
      (if Arith.less_eq_nat (List.size_list lab_c) i then None
        else same_lab_h is lab_c (List.nth lab_c i))
    | [], lab_c -> None;;

let rec check
  c es ts =
    (match es with [] -> ts
      | e :: esa ->
        (match ts
          with Wasm_Checker_Types.TopType _ -> check c esa (check_single c e ts)
          | Wasm_Checker_Types.Type _ -> check c esa (check_single c e ts)
          | Wasm_Checker_Types.Bot -> Wasm_Checker_Types.Bot))
and b_e_type_checker
  c es (Wasm.Tf (tn, tm)) =
    Wasm_Checker_Types.c_types_agree (check c es (Wasm_Checker_Types.Type tn))
      tm
and check_single
  c x1 ts = match c, x1, ts with
    c, Wasm.Grow_memory, ts ->
      (if not (Option.is_none (Wasm.memory c))
        then Wasm_Checker_Types.type_update ts
               [Wasm_Checker_Types.TSome Wasm.T_i32]
               (Wasm_Checker_Types.Type [Wasm.T_i32])
        else Wasm_Checker_Types.Bot)
    | c, Wasm.Current_memory, ts ->
        (if not (Option.is_none (Wasm.memory c))
          then Wasm_Checker_Types.type_update ts []
                 (Wasm_Checker_Types.Type [Wasm.T_i32])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Store (t, tp, a, off), ts ->
        (if not (Option.is_none (Wasm.memory c)) &&
              Wasm.load_store_t_bounds a tp t
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome Wasm.T_i32;
                   Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Load (t, tp_sx, a, off), ts ->
        (if not (Option.is_none (Wasm.memory c)) &&
              Wasm.load_store_t_bounds a (Wasm.option_projl tp_sx) t
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome Wasm.T_i32]
                 (Wasm_Checker_Types.Type [t])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Set_global i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.global c)) &&
              Wasm.is_mut (List.nth (Wasm.global c) i)
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome
                    (Wasm.tg_t (List.nth (Wasm.global c) i))]
                 (Wasm_Checker_Types.Type [])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Get_global i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.global c))
          then Wasm_Checker_Types.type_update ts []
                 (Wasm_Checker_Types.Type
                   [Wasm.tg_t (List.nth (Wasm.global c) i)])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Tee_local i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.local c))
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome (List.nth (Wasm.local c) i)]
                 (Wasm_Checker_Types.Type [List.nth (Wasm.local c) i])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Set_local i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.local c))
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome (List.nth (Wasm.local c) i)]
                 (Wasm_Checker_Types.Type [])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Get_local i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.local c))
          then Wasm_Checker_Types.type_update ts []
                 (Wasm_Checker_Types.Type [List.nth (Wasm.local c) i])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Call_indirect i, ts ->
        (if not (Option.is_none (Wasm.table c)) &&
              Arith.less_nat i (List.size_list (Wasm.types_t c))
          then (let Wasm.Tf (tn, tm) = List.nth (Wasm.types_t c) i in
                 Wasm_Checker_Types.type_update ts
                   (Wasm_Checker_Types.to_ct_list (tn @ [Wasm.T_i32]))
                   (Wasm_Checker_Types.Type tm))
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Call i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.func_t c))
          then (let Wasm.Tf (tn, tm) = List.nth (Wasm.func_t c) i in
                 Wasm_Checker_Types.type_update ts
                   (Wasm_Checker_Types.to_ct_list tn)
                   (Wasm_Checker_Types.Type tm))
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Return, ts ->
        (match Wasm.return c with None -> Wasm_Checker_Types.Bot
          | Some tls ->
            Wasm_Checker_Types.type_update ts
              (Wasm_Checker_Types.to_ct_list tls)
              (Wasm_Checker_Types.TopType []))
    | c, Wasm.Br_table is, ts ->
        (match same_lab (Wasm.to_list is) (Wasm.label c)
          with None -> Wasm_Checker_Types.Bot
          | Some tls ->
            Wasm_Checker_Types.type_update ts
              (Wasm_Checker_Types.to_ct_list (tls @ [Wasm.T_i32]))
              (Wasm_Checker_Types.TopType []))
    | c, Wasm.Br_if i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.label c))
          then Wasm_Checker_Types.type_update ts
                 (Wasm_Checker_Types.to_ct_list
                   (List.nth (Wasm.label c) i @ [Wasm.T_i32]))
                 (Wasm_Checker_Types.Type (List.nth (Wasm.label c) i))
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Br i, ts ->
        (if Arith.less_nat i (List.size_list (Wasm.label c))
          then Wasm_Checker_Types.type_update ts
                 (Wasm_Checker_Types.to_ct_list (List.nth (Wasm.label c) i))
                 (Wasm_Checker_Types.TopType [])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.If (Wasm.Tf (tn, tm), es1, es2), ts ->
        (if b_e_type_checker
              (Wasm.label_update (fun _ -> [tm] @ Wasm.label c) c) es1
              (Wasm.Tf (tn, tm)) &&
              b_e_type_checker
                (Wasm.label_update (fun _ -> [tm] @ Wasm.label c) c) es2
                (Wasm.Tf (tn, tm))
          then Wasm_Checker_Types.type_update ts
                 (Wasm_Checker_Types.to_ct_list (tn @ [Wasm.T_i32]))
                 (Wasm_Checker_Types.Type tm)
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Loop (Wasm.Tf (tn, tm), es), ts ->
        (if b_e_type_checker
              (Wasm.label_update (fun _ -> [tn] @ Wasm.label c) c) es
              (Wasm.Tf (tn, tm))
          then Wasm_Checker_Types.type_update ts
                 (Wasm_Checker_Types.to_ct_list tn) (Wasm_Checker_Types.Type tm)
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Block (Wasm.Tf (tn, tm), es), ts ->
        (if b_e_type_checker
              (Wasm.label_update (fun _ -> [tm] @ Wasm.label c) c) es
              (Wasm.Tf (tn, tm))
          then Wasm_Checker_Types.type_update ts
                 (Wasm_Checker_Types.to_ct_list tn) (Wasm_Checker_Types.Type tm)
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Select, ts -> Wasm_Checker_Types.type_update_select ts
    | c, Wasm.Drop, ts ->
        Wasm_Checker_Types.type_update ts [Wasm_Checker_Types.TAny]
          (Wasm_Checker_Types.Type [])
    | c, Wasm.Nop, ts -> ts
    | c, Wasm.Unreachable, ts ->
        Wasm_Checker_Types.type_update ts [] (Wasm_Checker_Types.TopType [])
    | c, Wasm.Cvtop (t1, Wasm.Reinterpret, t2, sx), ts ->
        (if not (Wasm.equal_ta t1 t2) &&
              (Arith.equal_nat (Wasm.t_length t1) (Wasm.t_length t2) &&
                Option.is_none sx)
          then Wasm_Checker_Types.type_update ts [Wasm_Checker_Types.TSome t2]
                 (Wasm_Checker_Types.Type [t1])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Cvtop (t1, Wasm.Convert, t2, sx), ts ->
        (if convert_cond t1 t2 sx
          then Wasm_Checker_Types.type_update ts [Wasm_Checker_Types.TSome t2]
                 (Wasm_Checker_Types.Type [t1])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Relop_f (t, va), ts ->
        (if Wasm.is_float_t t
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome t; Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [Wasm.T_i32])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Relop_i (t, uz), ts ->
        (if Wasm.is_int_t t
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome t; Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [Wasm.T_i32])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Testop (t, uy), ts ->
        (if Wasm.is_int_t t
          then Wasm_Checker_Types.type_update ts [Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [Wasm.T_i32])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Binop_f (t, ux), ts ->
        (if Wasm.is_float_t t
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome t; Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [t])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Binop_i (t, uw), ts ->
        (if Wasm.is_int_t t
          then Wasm_Checker_Types.type_update ts
                 [Wasm_Checker_Types.TSome t; Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [t])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Unop_f (t, uv), ts ->
        (if Wasm.is_float_t t
          then Wasm_Checker_Types.type_update ts [Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [t])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.Unop_i (t, uu), ts ->
        (if Wasm.is_int_t t
          then Wasm_Checker_Types.type_update ts [Wasm_Checker_Types.TSome t]
                 (Wasm_Checker_Types.Type [t])
          else Wasm_Checker_Types.Bot)
    | c, Wasm.EConst v, ts ->
        Wasm_Checker_Types.type_update ts []
          (Wasm_Checker_Types.Type [Wasm.typeof v]);;

end;; (*struct Wasm_Checker*)

module Wasm_Interpreter : sig
  type res_crash = CError | CExhaustion
  type ('a, 'b, 'c, 'd) res = RCrash of res_crash | RTrap |
    RValue of ('a, 'b, 'c, 'd) Wasm.v list
  type ('a, 'b, 'c, 'd, 'e) res_step = RSCrash of res_crash |
    RSBreak of Arith.nat * ('a, 'b, 'c, 'd) Wasm.v list |
    RSReturn of ('a, 'b, 'c, 'd) Wasm.v list |
    RSNormal of ('a, 'b, 'c, 'd, 'e) Wasm.e list
  val split_n :
    ('a, 'b, 'c, 'd) Wasm.v list ->
      Arith.nat -> ('a, 'b, 'c, 'd) Wasm.v list * ('a, 'b, 'c, 'd) Wasm.v list
  val split_vals_e :
    ('a, 'b, 'c, 'd, 'e) Wasm.e list ->
      ('a, 'b, 'c, 'd) Wasm.v list * ('a, 'b, 'c, 'd, 'e) Wasm.e list
end = struct

type res_crash = CError | CExhaustion;;

type ('a, 'b, 'c, 'd) res = RCrash of res_crash | RTrap |
  RValue of ('a, 'b, 'c, 'd) Wasm.v list;;

type ('a, 'b, 'c, 'd, 'e) res_step = RSCrash of res_crash |
  RSBreak of Arith.nat * ('a, 'b, 'c, 'd) Wasm.v list |
  RSReturn of ('a, 'b, 'c, 'd) Wasm.v list |
  RSNormal of ('a, 'b, 'c, 'd, 'e) Wasm.e list;;

let rec split_n
  x0 n = match x0, n with [], n -> ([], [])
    | v :: va, n ->
        (if Arith.equal_nat n Arith.zero_nat then ([], v :: va)
          else (let a = split_n va (Arith.minus_nat n Arith.one_nata) in
                let (es, aa) = a in
                 (v :: es, aa)));;

let rec split_vals_e
  = function
    Wasm.Basic (Wasm.EConst v) :: es ->
      (let a = split_vals_e es in
       let (vs, aa) = a in
        (v :: vs, aa))
    | [] -> ([], [])
    | Wasm.Basic Wasm.Unreachable :: va ->
        ([], Wasm.Basic Wasm.Unreachable :: va)
    | Wasm.Basic Wasm.Nop :: va -> ([], Wasm.Basic Wasm.Nop :: va)
    | Wasm.Basic Wasm.Drop :: va -> ([], Wasm.Basic Wasm.Drop :: va)
    | Wasm.Basic Wasm.Select :: va -> ([], Wasm.Basic Wasm.Select :: va)
    | Wasm.Basic (Wasm.Block (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Block (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Loop (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Loop (vc, vd)) :: va)
    | Wasm.Basic (Wasm.If (vc, vd, ve)) :: va ->
        ([], Wasm.Basic (Wasm.If (vc, vd, ve)) :: va)
    | Wasm.Basic (Wasm.Br vc) :: va -> ([], Wasm.Basic (Wasm.Br vc) :: va)
    | Wasm.Basic (Wasm.Br_if vc) :: va -> ([], Wasm.Basic (Wasm.Br_if vc) :: va)
    | Wasm.Basic (Wasm.Br_table vc) :: va ->
        ([], Wasm.Basic (Wasm.Br_table vc) :: va)
    | Wasm.Basic Wasm.Return :: va -> ([], Wasm.Basic Wasm.Return :: va)
    | Wasm.Basic (Wasm.Call vc) :: va -> ([], Wasm.Basic (Wasm.Call vc) :: va)
    | Wasm.Basic (Wasm.Call_indirect vc) :: va ->
        ([], Wasm.Basic (Wasm.Call_indirect vc) :: va)
    | Wasm.Basic (Wasm.Get_local vc) :: va ->
        ([], Wasm.Basic (Wasm.Get_local vc) :: va)
    | Wasm.Basic (Wasm.Set_local vc) :: va ->
        ([], Wasm.Basic (Wasm.Set_local vc) :: va)
    | Wasm.Basic (Wasm.Tee_local vc) :: va ->
        ([], Wasm.Basic (Wasm.Tee_local vc) :: va)
    | Wasm.Basic (Wasm.Get_global vc) :: va ->
        ([], Wasm.Basic (Wasm.Get_global vc) :: va)
    | Wasm.Basic (Wasm.Set_global vc) :: va ->
        ([], Wasm.Basic (Wasm.Set_global vc) :: va)
    | Wasm.Basic (Wasm.Load (vc, vd, ve, vf)) :: va ->
        ([], Wasm.Basic (Wasm.Load (vc, vd, ve, vf)) :: va)
    | Wasm.Basic (Wasm.Store (vc, vd, ve, vf)) :: va ->
        ([], Wasm.Basic (Wasm.Store (vc, vd, ve, vf)) :: va)
    | Wasm.Basic Wasm.Current_memory :: va ->
        ([], Wasm.Basic Wasm.Current_memory :: va)
    | Wasm.Basic Wasm.Grow_memory :: va ->
        ([], Wasm.Basic Wasm.Grow_memory :: va)
    | Wasm.Basic (Wasm.Unop_i (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Unop_i (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Unop_f (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Unop_f (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Binop_i (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Binop_i (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Binop_f (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Binop_f (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Testop (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Testop (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Relop_i (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Relop_i (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Relop_f (vc, vd)) :: va ->
        ([], Wasm.Basic (Wasm.Relop_f (vc, vd)) :: va)
    | Wasm.Basic (Wasm.Cvtop (vc, vd, ve, vf)) :: va ->
        ([], Wasm.Basic (Wasm.Cvtop (vc, vd, ve, vf)) :: va)
    | Wasm.Trap :: va -> ([], Wasm.Trap :: va)
    | Wasm.Callcl vb :: va -> ([], Wasm.Callcl vb :: va)
    | Wasm.Label (vb, vc, vd) :: va -> ([], Wasm.Label (vb, vc, vd) :: va)
    | Wasm.Local (vb, vc, vd, ve) :: va ->
        ([], Wasm.Local (vb, vc, vd, ve) :: va);;

end;; (*struct Wasm_Interpreter*)

module Wasm_Type_Abs_Printing : sig
  val zero_int32_impl : I32Wrapper.t Arith.zero
  val wasm_base_int32_impl : I32Wrapper.t Wasm_Type_Abs.wasm_base
  val wasm_int_int32_impl : I32Wrapper.t Wasm_Type_Abs.wasm_int
  val zero_int64_impl : I64Wrapper.t Arith.zero
  val wasm_base_int64_impl : I64Wrapper.t Wasm_Type_Abs.wasm_base
  val wasm_int_int64_impl : I64Wrapper.t Wasm_Type_Abs.wasm_int
  val zero_float32_impl : F32Wrapper.t Arith.zero
  val wasm_base_float32_impl : F32Wrapper.t Wasm_Type_Abs.wasm_base
  val wasm_float_float32_impl : F32Wrapper.t Wasm_Type_Abs.wasm_float
  val zero_float64_impl : F64Wrapper.t Arith.zero
  val wasm_base_float64_impl : F64Wrapper.t Wasm_Type_Abs.wasm_base
  val wasm_float_float64_impl : F64Wrapper.t Wasm_Type_Abs.wasm_float
end = struct

let zero_int32_impl =
  ({Arith.zero = I32Wrapper.zero} : I32Wrapper.t Arith.zero);;

let wasm_base_int32_impl =
  ({Wasm_Type_Abs.zero_wasm_base = zero_int32_impl} :
    I32Wrapper.t Wasm_Type_Abs.wasm_base);;

let wasm_int_int32_impl =
  ({Wasm_Type_Abs.wasm_base_wasm_int = wasm_base_int32_impl;
     Wasm_Type_Abs.int_clz = I32Wrapper.clz;
     Wasm_Type_Abs.int_ctz = I32Wrapper.ctz;
     Wasm_Type_Abs.int_popcnt = I32Wrapper.popcnt;
     Wasm_Type_Abs.int_add = I32Wrapper.add;
     Wasm_Type_Abs.int_sub = I32Wrapper.sub;
     Wasm_Type_Abs.int_mul = I32Wrapper.mul;
     Wasm_Type_Abs.int_div_u = I32Wrapper.div_u;
     Wasm_Type_Abs.int_div_s = I32Wrapper.div_s;
     Wasm_Type_Abs.int_rem_u = I32Wrapper.rem_u;
     Wasm_Type_Abs.int_rem_s = I32Wrapper.rem_s;
     Wasm_Type_Abs.int_and = I32Wrapper.and_;
     Wasm_Type_Abs.int_or = I32Wrapper.or_;
     Wasm_Type_Abs.int_xor = I32Wrapper.xor;
     Wasm_Type_Abs.int_shl = I32Wrapper.shl;
     Wasm_Type_Abs.int_shr_u = I32Wrapper.shr_u;
     Wasm_Type_Abs.int_shr_s = I32Wrapper.shr_s;
     Wasm_Type_Abs.int_rotl = I32Wrapper.rotl;
     Wasm_Type_Abs.int_rotr = I32Wrapper.rotr;
     Wasm_Type_Abs.int_eqz = I32Wrapper.eqz;
     Wasm_Type_Abs.int_eq = I32Wrapper.eq;
     Wasm_Type_Abs.int_lt_u = I32Wrapper.lt_u;
     Wasm_Type_Abs.int_lt_s = I32Wrapper.lt_s;
     Wasm_Type_Abs.int_gt_u = I32Wrapper.gt_u;
     Wasm_Type_Abs.int_gt_s = I32Wrapper.gt_s;
     Wasm_Type_Abs.int_le_u = I32Wrapper.le_u;
     Wasm_Type_Abs.int_le_s = I32Wrapper.le_s;
     Wasm_Type_Abs.int_ge_u = I32Wrapper.ge_u;
     Wasm_Type_Abs.int_ge_s = I32Wrapper.ge_s;
     Wasm_Type_Abs.int_of_nat =
       (fun a -> I32Wrapper.int32_of_big_int (Arith.integer_of_nat a));
     Wasm_Type_Abs.nat_of_int =
       (fun a -> Arith.Nat (I32Wrapper.big_int_of_int32 a))}
    : I32Wrapper.t Wasm_Type_Abs.wasm_int);;

let zero_int64_impl =
  ({Arith.zero = I64Wrapper.zero} : I64Wrapper.t Arith.zero);;

let wasm_base_int64_impl =
  ({Wasm_Type_Abs.zero_wasm_base = zero_int64_impl} :
    I64Wrapper.t Wasm_Type_Abs.wasm_base);;

let wasm_int_int64_impl =
  ({Wasm_Type_Abs.wasm_base_wasm_int = wasm_base_int64_impl;
     Wasm_Type_Abs.int_clz = I64Wrapper.clz;
     Wasm_Type_Abs.int_ctz = I64Wrapper.ctz;
     Wasm_Type_Abs.int_popcnt = I64Wrapper.popcnt;
     Wasm_Type_Abs.int_add = I64Wrapper.add;
     Wasm_Type_Abs.int_sub = I64Wrapper.sub;
     Wasm_Type_Abs.int_mul = I64Wrapper.mul;
     Wasm_Type_Abs.int_div_u = I64Wrapper.div_u;
     Wasm_Type_Abs.int_div_s = I64Wrapper.div_s;
     Wasm_Type_Abs.int_rem_u = I64Wrapper.rem_u;
     Wasm_Type_Abs.int_rem_s = I64Wrapper.rem_s;
     Wasm_Type_Abs.int_and = I64Wrapper.and_;
     Wasm_Type_Abs.int_or = I64Wrapper.or_;
     Wasm_Type_Abs.int_xor = I64Wrapper.xor;
     Wasm_Type_Abs.int_shl = I64Wrapper.shl;
     Wasm_Type_Abs.int_shr_u = I64Wrapper.shr_u;
     Wasm_Type_Abs.int_shr_s = I64Wrapper.shr_s;
     Wasm_Type_Abs.int_rotl = I64Wrapper.rotl;
     Wasm_Type_Abs.int_rotr = I64Wrapper.rotr;
     Wasm_Type_Abs.int_eqz = I64Wrapper.eqz;
     Wasm_Type_Abs.int_eq = I64Wrapper.eq;
     Wasm_Type_Abs.int_lt_u = I64Wrapper.lt_u;
     Wasm_Type_Abs.int_lt_s = I64Wrapper.lt_s;
     Wasm_Type_Abs.int_gt_u = I64Wrapper.gt_u;
     Wasm_Type_Abs.int_gt_s = I64Wrapper.gt_s;
     Wasm_Type_Abs.int_le_u = I64Wrapper.le_u;
     Wasm_Type_Abs.int_le_s = I64Wrapper.le_s;
     Wasm_Type_Abs.int_ge_u = I64Wrapper.ge_u;
     Wasm_Type_Abs.int_ge_s = I64Wrapper.ge_s;
     Wasm_Type_Abs.int_of_nat =
       (fun a -> I64Wrapper.int64_of_big_int (Arith.integer_of_nat a));
     Wasm_Type_Abs.nat_of_int =
       (fun a -> Arith.Nat (I64Wrapper.big_int_of_int64 a))}
    : I64Wrapper.t Wasm_Type_Abs.wasm_int);;

let zero_float32_impl =
  ({Arith.zero = F32Wrapper.zero} : F32Wrapper.t Arith.zero);;

let wasm_base_float32_impl =
  ({Wasm_Type_Abs.zero_wasm_base = zero_float32_impl} :
    F32Wrapper.t Wasm_Type_Abs.wasm_base);;

let wasm_float_float32_impl =
  ({Wasm_Type_Abs.wasm_base_wasm_float = wasm_base_float32_impl;
     Wasm_Type_Abs.float_neg = F32Wrapper.neg;
     Wasm_Type_Abs.float_abs = F32Wrapper.abs;
     Wasm_Type_Abs.float_ceil = F32Wrapper.ceil;
     Wasm_Type_Abs.float_floor = F32Wrapper.floor;
     Wasm_Type_Abs.float_trunc = F32Wrapper.trunc;
     Wasm_Type_Abs.float_nearest = F32Wrapper.nearest;
     Wasm_Type_Abs.float_sqrt = F32Wrapper.sqrt;
     Wasm_Type_Abs.float_add = F32Wrapper.add;
     Wasm_Type_Abs.float_sub = F32Wrapper.sub;
     Wasm_Type_Abs.float_mul = F32Wrapper.mul;
     Wasm_Type_Abs.float_div = F32Wrapper.div;
     Wasm_Type_Abs.float_min = F32Wrapper.min;
     Wasm_Type_Abs.float_max = F32Wrapper.max;
     Wasm_Type_Abs.float_copysign = F32Wrapper.copysign;
     Wasm_Type_Abs.float_eq = F32Wrapper.eq;
     Wasm_Type_Abs.float_lt = F32Wrapper.lt;
     Wasm_Type_Abs.float_gt = F32Wrapper.gt;
     Wasm_Type_Abs.float_le = F32Wrapper.le;
     Wasm_Type_Abs.float_ge = F32Wrapper.ge}
    : F32Wrapper.t Wasm_Type_Abs.wasm_float);;

let zero_float64_impl =
  ({Arith.zero = F64Wrapper.zero} : F64Wrapper.t Arith.zero);;

let wasm_base_float64_impl =
  ({Wasm_Type_Abs.zero_wasm_base = zero_float64_impl} :
    F64Wrapper.t Wasm_Type_Abs.wasm_base);;

let wasm_float_float64_impl =
  ({Wasm_Type_Abs.wasm_base_wasm_float = wasm_base_float64_impl;
     Wasm_Type_Abs.float_neg = F64Wrapper.neg;
     Wasm_Type_Abs.float_abs = F64Wrapper.abs;
     Wasm_Type_Abs.float_ceil = F64Wrapper.ceil;
     Wasm_Type_Abs.float_floor = F64Wrapper.floor;
     Wasm_Type_Abs.float_trunc = F64Wrapper.trunc;
     Wasm_Type_Abs.float_nearest = F64Wrapper.nearest;
     Wasm_Type_Abs.float_sqrt = F64Wrapper.sqrt;
     Wasm_Type_Abs.float_add = F64Wrapper.add;
     Wasm_Type_Abs.float_sub = F64Wrapper.sub;
     Wasm_Type_Abs.float_mul = F64Wrapper.mul;
     Wasm_Type_Abs.float_div = F64Wrapper.div;
     Wasm_Type_Abs.float_min = F64Wrapper.min;
     Wasm_Type_Abs.float_max = F64Wrapper.max;
     Wasm_Type_Abs.float_copysign = F64Wrapper.copysign;
     Wasm_Type_Abs.float_eq = F64Wrapper.eq;
     Wasm_Type_Abs.float_lt = F64Wrapper.lt;
     Wasm_Type_Abs.float_gt = F64Wrapper.gt;
     Wasm_Type_Abs.float_le = F64Wrapper.le;
     Wasm_Type_Abs.float_ge = F64Wrapper.ge}
    : F64Wrapper.t Wasm_Type_Abs.wasm_float);;

end;; (*struct Wasm_Type_Abs_Printing*)


