From fd0fc9a8bd820d9ae1466a941a0a903efb8be7b6 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Mon, 18 Apr 2016 13:56:55 +0200
Subject: Bugfix micromega: more careful syntaxification of terms of the form
 (Rinv t)

Bug uncovered by ekcburak@hotmail.com
https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00006.html
Now, terms of the the form (Rinv t) are only syntaxified when t evaluates to a non-zero constant.
---
 plugins/micromega/certificate.ml   |  3 ---
 plugins/micromega/coq_micromega.ml | 20 +++++++++++++-------
 2 files changed, 13 insertions(+), 10 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 914881db0d..1561c811cd 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -430,9 +430,6 @@ let nlinear_prover prfdepth (sys: (Mc.q Mc.pExpr * Mc.op1) list) =
   
   MonMap.fold (fun s m acc -> ((pol_of_mon m , Mc.NonStrict), Mc.PsatzSquare(norm0 (pol_of_mon s)))::acc) square [] in
 
- Printf.printf "#square %i\n" (List.length square) ;
- flush stdout ;
-
  let sys = sys @ square in
 
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 27daa7e3c6..5fef6d3fc6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -353,7 +353,8 @@ struct
   let r_modules =
     [["Coq";"Reals" ; "Rdefinitions"];
      ["Coq";"Reals" ; "Rpow_def"] ;
-]
+     ["Coq";"Reals" ; "Raxioms"] ;
+    ]
 
   let z_modules = [["Coq";"ZArith";"BinInt"]]
 
@@ -466,8 +467,9 @@ struct
   let coq_Rdiv = lazy (r_constant "Rdiv")
   let coq_Rinv = lazy (r_constant "Rinv")
   let coq_Rpower = lazy (r_constant "pow")
+  let coq_IZR    = lazy (r_constant "IZR")
   let coq_IQR    = lazy (constant "IQR")
-  let coq_IZR    = lazy (constant "IZR")
+
 
   let coq_PEX = lazy (constant "PEX" )
   let coq_PEc = lazy (constant"PEc")
@@ -1045,7 +1047,7 @@ struct
       coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ;
       coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ; 
       coq_Rmult  , (fun x y -> Mc.CMult(x,y)) ; 
-      coq_Rdiv   , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;
+    (*      coq_Rdiv   , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*)
     ]
 
   let rec rconstant term =
@@ -1067,10 +1069,14 @@ struct
 	  with
 	      ParseError -> 
 		match op with
-		  | op when Constr.equal op (Lazy.force coq_Rinv) -> Mc.CInv(rconstant args.(0))
-		  | op when Constr.equal op (Lazy.force coq_IQR)  -> Mc.CQ (parse_q args.(0))
-(*		  | op when op = Lazy.force coq_IZR  -> Mc.CZ (parse_z args.(0))*)
-		  | _ ->  raise ParseError
+		| op when Constr.equal op (Lazy.force coq_Rinv) ->
+                  let arg = rconstant args.(0) in 
+                  if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0 ; Mc.qden = Mc.XH}
+                  then raise ParseError (* This is a division by zero -- no semantics *)
+                  else Mc.CInv(arg) 
+		| op when Constr.equal op (Lazy.force coq_IQR)  -> Mc.CQ (parse_q args.(0))
+		| op when Constr.equal op   (Lazy.force coq_IZR)  -> Mc.CZ (parse_z args.(0))
+		| _ ->  raise ParseError
 	end
 
     |  _ -> raise ParseError
-- 
cgit v1.2.3