Merge PR#415: Use a compact representation for real literals

2 files changed, 28 insertions, 14 deletions

diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 293722125b..facd2e0625 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -59,11 +59,12 @@ Notation Rset := (Eqsth R).
 Notation Rext := (Eq_ext Rplus Rmult Ropp).
 
 Lemma Rlt_0_2 : 0 < 2.
+Proof.
 apply Rlt_trans with (0 + 1).
  apply Rlt_n_Sn.
  rewrite Rplus_comm.
    apply Rplus_lt_compat_l.
-    replace 1 with (0 + 1).
+    replace R1 with (0 + 1).
   apply Rlt_n_Sn.
   apply Rplus_0_l.
 Qed.
@@ -126,9 +127,17 @@ Ltac Rpow_tac t :=
   | _ => constr:(N.of_nat t)
   end.
 
-Add Field RField : Rfield
-   (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
-
-
-
+Ltac IZR_tac t :=
+  match t with
+  | R0 => constr:(0%Z)
+  | R1 => constr:(1%Z)
+  | IZR ?u =>
+    match isZcst u with
+    | true => u
+    | _ => constr:(InitialRing.NotConstant)
+    end
+  | _ => constr:(InitialRing.NotConstant)
+  end.
 
+Add Field RField : Rfield
+   (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]).
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index eb35d3f806..87ee666605 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -323,14 +323,16 @@ let _ = add_map "ring"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
     (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
     pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)])
+    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -756,12 +758,14 @@ let _ = add_map "field"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
     my_reference "display_linear",
       (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
     my_reference "display_pow_linear",
-     (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot);
+     (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
     pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
@@ -769,19 +773,20 @@ let _ = add_map "field"
           (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
+    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot);
     (* FEeval: evaluate morphism, protect field
        operations and make recursive call on the var map *)
-    my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
   (map_without_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
      coq_nil, (function -1->Eval|_ -> Prot);
-    (* PCond: evaluate morphism and denum list, protect ring
+     my_reference "IDphi", (function _->Eval);
+     my_reference "gen_phiZ", (function _->Eval);
+    (* PCond: evaluate denum list, protect ring
        operations and make recursive call on the var map *)
-     my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
-(*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
+     my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);;
 
 
 let _ = Redexpr.declare_reduction "simpl_field_expr"