Module OpHelpers

Require Import Coqlib.
Require Import AST Integers Floats.
Require Import Op CminorSel.


Class helper_functions := mk_helper_functions {
  i64_dtos: ident; (* float64 -> signed long *)
  i64_dtou: ident; (* float64 -> unsigned long *)
  i64_stod: ident; (* signed long -> float64 *)
  i64_utod: ident; (* unsigned long -> float64 *)
  i64_stof: ident; (* signed long -> float32 *)
  i64_utof: ident; (* unsigned long -> float32 *)
  i64_sdiv: ident; (* signed division *)
  i64_udiv: ident; (* unsigned division *)
  i64_smod: ident; (* signed remainder *)
  i64_umod: ident; (* unsigned remainder *)
  i64_shl: ident; (* shift left *)
  i64_shr: ident; (* shift right unsigned *)
  i64_sar: ident; (* shift right signed *)
  i64_umulh: ident; (* unsigned multiply high *)
  i64_smulh: ident; (* signed multiply high *)
  i32_sdiv: ident; (* signed division *)
  i32_udiv: ident; (* unsigned division *)
  i32_smod: ident; (* signed remainder *)
  i32_umod: ident; (* unsigned remainder *)
  f64_div: ident;
  f32_div: ident;
}.

Definition sig_l_l := [Xlong ---> Xlong]%asttyp.
Definition sig_l_f := [Xlong ---> Xfloat]%asttyp.
Definition sig_l_s := [Xlong ---> Xsingle]%asttyp.
Definition sig_f_l := [Xfloat ---> Xlong]%asttyp.
Definition sig_ll_l := [Xlong; Xlong ---> Xlong]%asttyp.
Definition sig_li_l := [Xlong; Xint ---> Xlong]%asttyp.
Definition sig_ii_l := [Xint; Xint ---> Xlong]%asttyp.
Definition sig_ii_i := [Xint; Xint ---> Xint]%asttyp.
Definition sig_ff_f := [Xfloat; Xfloat ---> Xfloat]%asttyp.
Definition sig_ss_s := [Xsingle; Xsingle ---> Xsingle]%asttyp.