Fix float ops (#768)

* Remove extraction hack for hexadecimalString/decimalString
Fix string_of_float

* Fix equality decision on primitive values

.gitignore

@@ -362,3 +362,6 @@ test-suite/metacoq-config
 test-suite/plugin-demo/_CoqProject
 test-suite/plugin-demo/_PluginProject
 test-suite/plugin-demo/metacoq-config
+erasure/META
+safechecker/META
+template-coq/META

pcuic/theories/utils/PCUICPrimitive.v

@@ -71,38 +71,44 @@ Qed.
 
 #[global]
 Instance reflect_eq_spec_float : ReflectEq SpecFloat.spec_float := EqDec_ReflectEq _.
-
-(* #[program]
-#[global]
-Instance reflect_eq_float64 : ReflectEq float64_model := 
-  { eqb x y := eqb (proj1_sig x) (proj1_sig y) }.
-Next Obligation.
-  cbn -[eqb].
-  intros x y.
-  elim: eqb_spec. constructor.
-  now apply exist_irrel_eq.
-  intros neq; constructor => H'; apply neq; now subst x.
-Qed. *)
 
-(** Propositional UIP is needed below *)
-Set Equations With UIP.
-
-#[global]
-Instance prim_model_eqdec {term} (*e : EqDec term*) : forall p : prim_tag, EqDec (prim_model term p).
-Proof. eqdec_proof. Qed.
+Equations eqb_prim_model {term} {t : prim_tag} (x y : prim_model term t) : bool :=
+  | primIntModel x, primIntModel y := ReflectEq.eqb x y
+  | primFloatModel x, primFloatModel y := ReflectEq.eqb x y.
+
+#[global, program]
+Instance prim_model_reflecteq {term} {p : prim_tag} : ReflectEq (prim_model term p) := 
+  {| ReflectEq.eqb := eqb_prim_model |}.
+Next Obligation. 
+  intros. depelim x; depelim y; simp eqb_prim_model.
+  case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
+  case: ReflectEq.eqb_spec; constructor; subst; auto. congruence.
+Qed.
 
 #[global]
-Instance prim_tag_model_eqdec term : EqDec (prim_val term).
-Proof. eqdec_proof. Defined.
+Instance prim_model_eqdec {term} : forall p : prim_tag, EqDec (prim_model term p) := _.
+
+Equations eqb_prim_val {term} (x y : prim_val term) : bool :=
+  | (primInt; i), (primInt; i') := ReflectEq.eqb i i'
+  | (primFloat; f), (primFloat; f') := ReflectEq.eqb f f'
+  | x, y := false.
+
+#[global, program]
+Instance prim_val_reflect_eq {term} : ReflectEq (prim_val term) := 
+  {| ReflectEq.eqb := eqb_prim_val |}.
+Next Obligation. 
+  intros. funelim (eqb_prim_val x y); simp eqb_prim_val.
+  case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H. cbn in n. auto.
+  constructor. intros H; noconf H; auto.
+  constructor. intros H; noconf H; auto.
+  case: ReflectEq.eqb_spec; constructor; subst; auto. intros H; noconf H; auto.
+Qed.
 
 #[global]
-Instance prim_val_reflect_eq term : ReflectEq (prim_val term) := EqDec_ReflectEq _.
+Instance prim_tag_model_eqdec term : EqDec (prim_val term) := _.
 
 (** Printing *)
 
-Definition string_of_float64_model (f : float64_model) := 
-  "<>".
-
 Definition string_of_prim {term} (soft : term -> string) (p : prim_val term) : string :=
   match p.π2 return string with
   | primIntModel f => "(int: " ^ string_of_prim_int f ^ ")"

safechecker/theories/Extraction.v

@@ -8,13 +8,7 @@ From MetaCoq.SafeChecker Require Import PCUICSafeChecker PCUICSafeConversion
 
     Any extracted code planning to link with the plugin's OCaml reifier
     should use these same directives for consistency.
-*)
-
-(* Ignore [Decimal.int] before the extraction issue is solved:
-    https://github.com/coq/coq/issues/7017. *)
-Extract Inductive Decimal.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
-Extract Inductive Hexadecimal.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
-Extract Inductive Number.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
+*)      
 
 (** Here we could extract uint63_from/to_model to the identity *)
 

template-coq/_PluginProject

@@ -122,8 +122,10 @@ gen-src/mCReflect.mli
 gen-src/mCReflect.ml
 gen-src/primFloat.mli
 gen-src/primFloat.ml
-#gen-src/decimalString.mli
-#gen-src/decimalString.ml
+gen-src/hexadecimalString.mli
+gen-src/hexadecimalString.ml
+gen-src/decimalString.mli
+gen-src/decimalString.ml
 gen-src/mCString.ml
 gen-src/mCString.mli
 gen-src/mCUtils.ml

template-coq/gen-src/metacoq_template_plugin.mlpack

@@ -25,6 +25,7 @@ Caml_byte
 ByteCompare
 ByteCompareSpec
 String0
+HexadecimalString
 Orders
 OrdersTac
 OrdersFacts
@@ -71,6 +72,7 @@ Zpower
 SpecFloat
 PrimFloat
 FloatOps
+DecimalString
 MCString
 MCUtils
 Signature

template-coq/theories/BasicAst.v

@@ -749,6 +749,3 @@ Definition prec := 53%Z.
 Definition emax := 1024%Z.
 (** We consider valid binary encordings of floats as our model *)
 Definition float64_model := sig (SpecFloat.valid_binary prec emax).
-
-Definition string_of_float64_model (i : float64_model) := 
-  "<float>".

template-coq/theories/EnvironmentTyping.v

@@ -1149,7 +1149,7 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT
     Definition fresh_global (s : kername) (g : global_declarations) : Prop :=
       Forall (fun g => g.1 <> s) g.
 
-    Record on_global_decls_data {cf:checker_flags} (univs : ContextSet.t) retro (Σ : global_declarations) (kn : kername) (d : global_decl) :=
+    Record on_global_decls_data (univs : ContextSet.t) retro (Σ : global_declarations) (kn : kername) (d : global_decl) :=
         {
           kn_fresh :  fresh_global kn Σ ;
           udecl := universes_decl_of_decl d ;

template-coq/theories/Extraction.v

@@ -9,12 +9,6 @@ From Coq Require Ascii Extraction ZArith NArith.
 From MetaCoq.Template Require Import utils Ast Reflect Induction.
 From Coq Require Import FSets ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63.
 
-(* Ignore [Decimal.int] before the extraction issue is solved:
-  https://github.com/coq/coq/issues/7017. *)
-Extract Inductive Decimal.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
-Extract Inductive Hexadecimal.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
-Extract Inductive Number.int => unit [ "(fun _ -> ())" "(fun _ -> ())" ] "(fun _ _ _ -> assert false)".
-
 Extract Inductive Equations.Init.sigma => "( * )" ["(,)"].
 Extract Constant Equations.Init.pr1 => "fst".
 Extract Constant Equations.Init.pr2 => "snd".

template-coq/theories/Primitive.v

@@ -1,6 +1,6 @@
 (* Primitive types *)
 
-From Coq Require Import Uint63 PrimFloat.
+From Coq Require Import Uint63 PrimFloat SpecFloat FloatOps ZArith HexadecimalString.
 From MetaCoq.Template Require Import bytestring MCString.
 Local Open Scope bs.
 
@@ -14,5 +14,13 @@ Definition string_of_prim_int (i:Uint63.int) : string :=
   (* Better? DecimalString.NilZero.string_of_uint (BinNat.N.to_uint (BinInt.Z.to_N (Int63.to_Z i))). ? *)
   string_of_Z (Uint63.to_Z i).
 
-Definition string_of_float (f : PrimFloat.float) :=
-  "<float>".
+Definition string_of_float (f : PrimFloat.float) : string :=
+  match Prim2SF f with
+  | S754_zero sign => if sign then "-0" else "0"
+  | S754_infinity sign => if sign then "-INFINITY" else "INFINITY"
+  | S754_nan => "NAN"
+  | S754_finite sign p z =>
+    let abs := "0x" ++ bytestring.String.of_string (Numbers.HexadecimalString.NilZero.string_of_uint (Pos.to_hex_uint p)) ++ "p" ++ 
+      bytestring.String.of_string (Numbers.DecimalString.NilZero.string_of_int (Z.to_int z))
+    in if sign then "-" ++ abs else abs
+  end.