Theory Wasm_Type_Abs

section ‹Syntactic Typeclasses›

theory Wasm_Type_Abs imports Main begin

class wasm_base = zero

class wasm_int = wasm_base +
  (* unops*)
  fixes int_clz :: "'a ⇒ 'a"
  fixes int_ctz :: "'a ⇒ 'a"
  fixes int_popcnt :: "'a ⇒ 'a"
  (* binops *)
  fixes int_add :: "'a ⇒ 'a ⇒ 'a"
  fixes int_sub :: "'a ⇒ 'a ⇒ 'a"
  fixes int_mul :: "'a ⇒ 'a ⇒ 'a"
  fixes int_div_u :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_div_s :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_rem_u :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_rem_s :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_and :: "'a ⇒ 'a ⇒ 'a"
  fixes int_or :: "'a ⇒ 'a ⇒ 'a"
  fixes int_xor :: "'a ⇒ 'a ⇒ 'a"
  fixes int_shl :: "'a ⇒ 'a ⇒ 'a"
  fixes int_shr_u :: "'a ⇒ 'a ⇒ 'a"
  fixes int_shr_s :: "'a ⇒ 'a ⇒ 'a"
  fixes int_rotl :: "'a ⇒ 'a ⇒ 'a"
  fixes int_rotr :: "'a ⇒ 'a ⇒ 'a"
  (* testops *)
  fixes int_eqz :: "'a ⇒ bool"
  (* relops *)
  fixes int_eq :: "'a ⇒ 'a ⇒ bool"
  fixes int_lt_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_lt_s :: "'a ⇒ 'a ⇒ bool"
  fixes int_gt_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_gt_s :: "'a ⇒ 'a ⇒ bool"
  fixes int_le_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_le_s :: "'a ⇒ 'a ⇒ bool"
  fixes int_ge_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_ge_s :: "'a ⇒ 'a ⇒ bool"
  (* value conversions *)
  fixes int_of_nat :: "nat ⇒ 'a"
  fixes nat_of_int :: "'a ⇒ nat"
begin
  abbreviation (input)
  int_ne where
    "int_ne x y ≡ ¬ (int_eq x y)"
end

class wasm_float = wasm_base +
  (* unops *)
  fixes float_neg     :: "'a ⇒ 'a"
  fixes float_abs     :: "'a ⇒ 'a"
  fixes float_ceil    :: "'a ⇒ 'a"
  fixes float_floor   :: "'a ⇒ 'a"
  fixes float_trunc   :: "'a ⇒ 'a"
  fixes float_nearest :: "'a ⇒ 'a"
  fixes float_sqrt    :: "'a ⇒ 'a"
  (* binops *)
  fixes float_add :: "'a ⇒ 'a ⇒ 'a"
  fixes float_sub :: "'a ⇒ 'a ⇒ 'a"
  fixes float_mul :: "'a ⇒ 'a ⇒ 'a"
  fixes float_div :: "'a ⇒ 'a ⇒ 'a"
  fixes float_min :: "'a ⇒ 'a ⇒ 'a"
  fixes float_max :: "'a ⇒ 'a ⇒ 'a"
  fixes float_copysign :: "'a ⇒ 'a ⇒ 'a"
  (* relops *)
  fixes float_eq :: "'a ⇒ 'a ⇒ bool"
  fixes float_lt :: "'a ⇒ 'a ⇒ bool"
  fixes float_gt :: "'a ⇒ 'a ⇒ bool"
  fixes float_le :: "'a ⇒ 'a ⇒ bool"
  fixes float_ge :: "'a ⇒ 'a ⇒ bool"
begin
  abbreviation (input)
  float_ne where
    "float_ne x y ≡ ¬ (float_eq x y)"
end
end