Module Builtins1

Require Import String Coqlib.
Require Import AST Integers Floats Values.
Require Import Builtins0.
Require ExtValues.

Inductive platform_builtin : Type :=
| BI_bits_of_float
| BI_bits_of_double
| BI_float_of_bits
| BI_double_of_bits
| BI_secu_wd (t: typ).

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_bits_of_double", BI_bits_of_double)
  :: ("__builtin_float_of_bits", BI_float_of_bits)
  :: ("__builtin_double_of_bits", BI_double_of_bits)
  :: ("__builtin_secu_wd_int", BI_secu_wd Tint)
  :: ("__builtin_secu_wd_uint", BI_secu_wd Tint)
  :: ("__builtin_secu_wd_long", BI_secu_wd Tlong)
  :: ("__builtin_secu_wd_ulong", BI_secu_wd Tlong)
  :: ("__builtin_secu_wd_llong", BI_secu_wd Tlong)
  :: ("__builtin_secu_wd_ullong", BI_secu_wd Tlong)
  :: ("__builtin_secu_wd_float", BI_secu_wd Tsingle)
  :: ("__builtin_secu_wd_double", BI_secu_wd Tfloat)
  :: nil.

Definition platform_builtin_sig (b: platform_builtin) : signature :=
  match b with
  | BI_bits_of_float => [Xsingle ---> Xint]
  | BI_bits_of_double => [Xfloat ---> Xlong]
  | BI_float_of_bits => [Xint ---> Xsingle]
  | BI_double_of_bits => [Xlong ---> Xfloat]
  | BI_secu_wd t => let t' := inj_type t in [t' ---> t' ]
  end.

Program 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_bits_of_double => mkbuiltin_n1t Tfloat Xlong Float.to_bits
  | BI_float_of_bits => mkbuiltin_n1t Tint Xsingle Float32.of_bits
  | BI_double_of_bits => mkbuiltin_n1t Tlong Xfloat Float.of_bits
  | BI_secu_wd ty =>
      mkbuiltin_v1p (inj_type ty) (fun (x : val) => Val.welldefined x ty) _ _
  end.