Fix float ops 8.15 (#769)

* Support for printing floating point primitive values (#767) * Fix defs in PCUICPrimitive
MetaCoq · Oct 11, 2022 · 970afec · 970afec
1 parent adc60da
commit 970afec
Show file tree

Hide file tree

Showing 6 changed files with 50 additions and 23 deletions.
diff --git a/pcuic/theories/PCUICCanonicity.v b/pcuic/theories/PCUICCanonicity.v
@@ -562,6 +562,8 @@ End Spines.
 
 Tactic Notation "redt" uconstr(y) := eapply (CRelationClasses.transitivity (R:=red _ _) (y:=y)).
 
+Require Import Equations.Type.Relation_Properties.
+
 Section WeakNormalization.
   Context {cf:checker_flags} {Σ : global_env_ext}.
   Context {wfΣ : wf Σ}.
@@ -772,8 +774,6 @@ Section WeakNormalization.
     False.
   Proof. eauto using wh_neutral_empty_gen. Qed.
 
-  Require Import Equations.Type.Relation_Properties.
-
   (* TODO move *)
   Lemma invert_red_axiom {Γ cst u cdecl T} :
     declared_constant Σ cst cdecl -> 

diff --git a/pcuic/theories/utils/PCUICPrimitive.v b/pcuic/theories/utils/PCUICPrimitive.v
@@ -53,9 +53,6 @@ Proof.
   now destruct (uip p q).
 Qed.
 
-#[global]
-Instance reflect_eq_Z : ReflectEq Z := EqDec_ReflectEq _.
-
 Local Obligation Tactic := idtac.
 #[program]
 #[global]
@@ -84,25 +81,43 @@ Next Obligation.
   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 ^ ")"

diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject
@@ -120,8 +120,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/decimalString.mli
+gen-src/decimalString.ml
+gen-src/hexadecimalString.mli
+gen-src/hexadecimalString.ml
 gen-src/mCString.ml
 gen-src/mCString.mli
 gen-src/mCUtils.ml

diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -77,6 +77,8 @@ Signature
 All_Forall
 Config0
 Kernames
+DecimalString
+HexadecimalString
 Primitive
 BasicAst
 Universes0

diff --git a/template-coq/theories/EnvironmentTyping.v b/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 ;

diff --git a/template-coq/theories/Primitive.v b/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 Numbers.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.