aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/Lia.v2
-rw-r--r--plugins/micromega/Psatz.v2
-rw-r--r--plugins/micromega/QMicromega.v2
-rw-r--r--plugins/micromega/RMicromega.v2
-rw-r--r--plugins/micromega/RingMicromega.v2
-rw-r--r--plugins/micromega/ZMicromega.v2
-rw-r--r--plugins/micromega/certificate.ml3
-rw-r--r--plugins/micromega/coq_micromega.ml52
-rw-r--r--plugins/micromega/g_micromega.ml45
-rw-r--r--plugins/micromega/micromega_plugin.mlpack (renamed from plugins/micromega/micromega_plugin.mllib)1
-rw-r--r--plugins/micromega/persistent_cache.ml8
11 files changed, 39 insertions, 42 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 3e58e81ac2..52bf5ed3df 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -16,7 +16,7 @@ Require Import ZMicromega.
Require Import ZArith.
Require Import RingMicromega.
Require Import VarMap.
-Require Tauto.
+Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
Ltac preprocess :=
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index ba1f8956e3..fafd8a5f21 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -20,7 +20,7 @@ Require Import ZArith.
Require Import Rdefinitions.
Require Import RingMicromega.
Require Import VarMap.
-Require Tauto.
+Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
Ltac preprocess :=
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index 432683635f..b13285f537 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -168,7 +168,7 @@ Proof.
exact H.
Qed.
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 72353a99e5..2352d78d63 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -533,7 +533,7 @@ Proof.
exact H.
Qed.
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 751a81df12..ed49c3df43 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -794,7 +794,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) :=
| OpLe => (psub lhs rhs ,Strict) :: nil
end.
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
List.map (fun x => x::nil) (xnormalise t).
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index d7ddef2be4..5aa8d03f99 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -198,7 +198,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z) :=
| OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
end.
-Require Import Tauto BinNums.
+Require Import Coq.micromega.Tauto BinNums.
Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
List.map (fun x => x::nil) (xnormalise t).
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..e4aa1448eb 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -18,9 +18,7 @@
open Pp
open Mutils
-open Proofview
open Goptions
-open Proofview.Notations
(**
* Debug flag
@@ -353,7 +351,8 @@ struct
let r_modules =
[["Coq";"Reals" ; "Rdefinitions"];
["Coq";"Reals" ; "Rpow_def"] ;
-]
+ ["Coq";"Reals" ; "Raxioms"] ;
+ ]
let z_modules = [["Coq";"ZArith";"BinInt"]]
@@ -466,8 +465,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")
@@ -961,7 +961,7 @@ struct
let parse_expr parse_constant parse_exp ops_spec env term =
if debug
- then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
+ then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
(*
let constant_or_variable env term =
@@ -1045,7 +1045,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 +1067,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
@@ -1078,7 +1082,7 @@ struct
let rconstant term =
if debug
- then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
+ then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
let res = rconstant term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1118,7 +1122,7 @@ struct
let parse_arith parse_op parse_expr env cstr gl =
if debug
- then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
+ then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
match kind_of_term cstr with
| App(op,args) ->
let (op,lhs,rhs) = parse_op gl (op,args) in
@@ -1460,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
]
(Tacmach.pf_concl gl))
;
- Tactics.new_generalize env ;
+ Tactics.generalize env ;
Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)
]
end }
@@ -1647,12 +1651,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "Formula....\n") ;
+ Feedback.msg_notice (Pp.str "Formula....\n") ;
let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+ Feedback.msg_notice (Printer.prterm ff);
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
match witness_list_tags prover cnf_ff with
@@ -1672,11 +1676,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "\nAFormula\n") ;
+ Feedback.msg_notice (Pp.str "\nAFormula\n") ;
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff' in
- Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
+ Feedback.msg_notice (Printer.prterm ff');
Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
@@ -1722,14 +1726,14 @@ let micromega_gen
| Some (ids,ff',res') ->
(Tacticals.New.tclTHENLIST
[
- Tactics.new_generalize (List.map Term.mkVar ids) ;
+ Tactics.generalize (List.map Term.mkVar ids) ;
micromega_order_change spec res'
(Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
])
with
| ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
| Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ | CsdpNotFound -> flush stdout ;
Tacticals.New.tclFAIL 0 (Pp.str
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
@@ -1770,7 +1774,7 @@ let micromega_order_changer cert env ff =
("__wit", cert, cert_typ)
]
(Tacmach.pf_concl gl)));
- Tactics.new_generalize env ;
+ Tactics.generalize env ;
Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)
]
end }
@@ -1808,13 +1812,13 @@ let micromega_genr prover =
(List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
(Tacticals.New.tclTHENLIST
[
- Tactics.new_generalize (List.map Term.mkVar ids) ;
+ Tactics.generalize (List.map Term.mkVar ids) ;
micromega_order_changer res' env (abstract_wrt_formula ff' ff)
])
with
| Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut")
| ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ | CsdpNotFound ->
Tacticals.New.tclFAIL 0 (Pp.str
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
@@ -1899,7 +1903,7 @@ let call_csdpcert_q provername poly =
let cert = Certificate.q_cert_of_pos cert in
if Mc.qWeakChecker poly cert
then Some cert
- else ((print_string "buggy certificate" ; flush stdout) ;None)
+ else ((print_string "buggy certificate") ;None)
let call_csdpcert_z provername poly =
let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bca1c2febd..e6b5cc60d4 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,12 +16,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Errors
-open Misctypes
-open Stdarg
open Constrarg
-open Pcoq.Prim
-open Pcoq.Tactic
DECLARE PLUGIN "micromega_plugin"
diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mlpack
index f53a9e3797..ed253da3fd 100644
--- a/plugins/micromega/micromega_plugin.mllib
+++ b/plugins/micromega/micromega_plugin.mlpack
@@ -7,4 +7,3 @@ Certificate
Persistent_cache
Coq_micromega
G_micromega
-Micromega_plugin_mod
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 6a03e2d61f..88b13abf9a 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -212,9 +212,11 @@ let find t k =
res
let memo cache f =
- let tbl = lazy (open_in cache) in
- fun x ->
- let tbl = Lazy.force tbl in
+ let tbl = lazy (try Some (open_in cache) with _ -> None) in
+ fun x ->
+ match Lazy.force tbl with
+ | None -> f x
+ | Some tbl ->
try
find tbl x
with
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:13:52 +0000