Module Builtins1

From Coq Require Import String.
Require Import Coqlib AST Integers Floats Values.
Require Import Builtins0.

Inductive platform_builtin : Type :=
| BI_bits_of_float
| BI_float_of_bits
| BI_clz
| BI_ctz
| BI_reverse_bits.

Local Open Scope string_scope.
Local Open Scope asttyp_scope.

Definition platform_builtin_table : list (string * platform_builtin) :=
     ("__builtin_bits_of_float", BI_bits_of_float)
  :: ("__builtin_float_of_bits", BI_float_of_bits)
  :: ("__builtin_clz", BI_clz)
  :: ("__builtin_ctz", BI_ctz)
  :: ("__builtin_ctzl", BI_ctz)
  :: ("__builtin_reverse_bits", BI_reverse_bits)
  :: nil.

Definition platform_builtin_sig (b: platform_builtin) : signature :=
  match b with
  | BI_bits_of_float => [Xsingle ---> Xint ]
  | BI_float_of_bits => [Xint ---> Xsingle ]
  | BI_clz => [Xint ---> Xint ]
  | BI_ctz => [Xint ---> Xint ]
  | BI_reverse_bits => [Xint ---> Xint ]
  end.

Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
  match b with
  | BI_bits_of_float => mkbuiltin_n1t Tsingle Xint Float32.to_bits
  | BI_float_of_bits => mkbuiltin_n1t Tint Xsingle Float32.of_bits
  | BI_clz => mkbuiltin_n1t Tint Xint Int.clz
  | BI_ctz => mkbuiltin_n1t Tint Xint Int.ctz
  | BI_reverse_bits => mkbuiltin_n1t Tint Xint Int.reverse_bits
  end.

Definition eq_platform_builtin: forall (x y: platform_builtin), {x=y} + {x<>y}.