diff options
Diffstat (limited to 'verilog/Builtins1.v')
| -rw-r--r-- | verilog/Builtins1.v | 36 |
1 files changed, 17 insertions, 19 deletions
diff --git a/verilog/Builtins1.v b/verilog/Builtins1.v index e5233ff5..6691d15c 100644 --- a/verilog/Builtins1.v +++ b/verilog/Builtins1.v @@ -19,37 +19,35 @@ Require Import String Coqlib. Require Import AST Integers Floats Values. Require Import Builtins0. +Require ExtValues. Inductive platform_builtin : Type := - | BI_fmin - | BI_fmax. +| BI_bits_of_float +| BI_bits_of_double +| BI_float_of_bits +| BI_double_of_bits. Local Open Scope string_scope. Definition platform_builtin_table : list (string * platform_builtin) := - ("__builtin_fmin", BI_fmin) - :: ("__builtin_fmax", BI_fmax) + ("__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) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := match b with - | BI_fmin | BI_fmax => - mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default + | BI_bits_of_float => mksignature (Tsingle :: nil) Tint cc_default + | BI_bits_of_double => mksignature (Tfloat :: nil) Tlong cc_default + | BI_float_of_bits => mksignature (Tint :: nil) Tsingle cc_default + | BI_double_of_bits => mksignature (Tlong :: nil) Tfloat cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := match b with - | BI_fmin => - mkbuiltin_n2t Tfloat Tfloat Tfloat - (fun f1 f2 => match Float.compare f1 f2 with - | Some Eq | Some Lt => f1 - | Some Gt | None => f2 - end) - | BI_fmax => - mkbuiltin_n2t Tfloat Tfloat Tfloat - (fun f1 f2 => match Float.compare f1 f2 with - | Some Eq | Some Gt => f1 - | Some Lt | None => f2 - end) + | BI_bits_of_float => mkbuiltin_n1t Tsingle Tint Float32.to_bits + | BI_bits_of_double => mkbuiltin_n1t Tfloat Tlong Float.to_bits + | BI_float_of_bits => mkbuiltin_n1t Tint Tsingle Float32.of_bits + | BI_double_of_bits => mkbuiltin_n1t Tlong Tfloat Float.of_bits end. - |