Module OpHelpers

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


Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default.
Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default.
Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default.
Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default.
Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default.
Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default.
Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default.
Definition sig_ii_i := mksignature (Tint :: Tint :: nil) Tint cc_default.
Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default.
Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default.

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;
}.