diff options
Diffstat (limited to 'plugins/micromega')
25 files changed, 95 insertions, 100 deletions
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v index dd4d596f21..a19e9df904 100644 --- a/plugins/micromega/Env.v +++ b/plugins/micromega/Env.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 62a7333d55..fd4bb248bf 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 7242558552..52bf5ed3df 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/MExtraction.v b/plugins/micromega/MExtraction.v index 8b959c2784..0a41af4543 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index 34b8bbdd33..72b4dcb6e3 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 31d051cb4d..fafd8a5f21 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 := @@ -69,7 +69,7 @@ Ltac xpsatz dom d := end in tac. Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. -Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). Ltac psatzl dom := let tac := lazymatch dom with diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v index 6c157def8f..b13285f537 100644 --- a/plugins/micromega/QMicromega.v +++ b/plugins/micromega/QMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 e9ab696264..2352d78d63 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/Refl.v b/plugins/micromega/Refl.v index 499a8c4c48..32ddb3cf4c 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index a0545637dd..ed49c3df43 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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/Tauto.v b/plugins/micromega/Tauto.v index 39d0c6b197..391231afd9 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 6e1fe2220e..4981ddb302 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index 4c4b81a07f..bd425e6bbf 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 84a8d13c2d..5aa8d03f99 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 63485ab269..1561c811cd 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 ef1169342f..e4aa1448eb 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,7 +18,6 @@ open Pp open Mutils -open Proofview open Goptions (** @@ -81,10 +80,10 @@ let _ = optread = (fun () -> !lia_enum); optwrite = (fun x -> lia_enum := x) } in - ignore (declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth)) ; - ignore (declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth)) ; - ignore (declare_bool_option lia_enum_opt) - + let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in + let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in + let _ = declare_bool_option lia_enum_opt in + () (** * Initialize a tag type to the Tag module declaration (see Mutils). @@ -352,7 +351,8 @@ struct let r_modules = [["Coq";"Reals" ; "Rdefinitions"]; ["Coq";"Reals" ; "Rpow_def"] ; -] + ["Coq";"Reals" ; "Raxioms"] ; + ] let z_modules = [["Coq";"ZArith";"BinInt"]] @@ -465,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") @@ -887,7 +888,7 @@ struct let is_convertible gl t1 t2 = - Reductionops.is_conv (Tacmach.New.pf_env gl) (Goal.sigma gl) t1 t2 + Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2 let parse_zop gl (op,args) = match kind_of_term op with @@ -960,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 = @@ -1044,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 = @@ -1066,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 @@ -1077,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) ; @@ -1117,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 @@ -1168,8 +1173,8 @@ struct with e when Errors.noncritical e -> (X(t),env,tg) in let is_prop term = - let ty = Typing.unsafe_type_of (Goal.env gl) (Goal.sigma gl) term in - let sort = Typing.sort_of (Goal.env gl) (ref (Goal.sigma gl)) ty in + let ty = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in + let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in Term.is_prop_sort sort in let rec xparse_formula env tg term = @@ -1444,8 +1449,8 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) env in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter - begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1457,12 +1462,12 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.New.pf_concl gl)) + (Tacmach.pf_concl gl)) ; - Tactics.new_generalize env ; + Tactics.generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - end + end } (** @@ -1646,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 @@ -1671,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; @@ -1707,11 +1712,10 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec prover = - Proofview.Goal.nf_enter - begin - fun gl -> - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in + let concl = Tacmach.pf_concl gl in + let hyps = Tacmach.pf_hyps_types gl in try let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in let env = Env.elements env in @@ -1722,20 +1726,20 @@ 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" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end + end } let micromega_gen parse_arith (negate:'cst atom -> 'cst mc_cnf) @@ -1756,9 +1760,8 @@ let micromega_order_changer cert env ff = let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in - Proofview.Goal.nf_enter - begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -1770,11 +1773,11 @@ let micromega_order_changer cert env ff = [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.New.pf_concl gl))); - Tactics.new_generalize env ; + (Tacmach.pf_concl gl))); + Tactics.generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - end + end } let micromega_genr prover = @@ -1790,11 +1793,10 @@ let micromega_genr prover = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter - begin - fun gl -> - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in + Proofview.Goal.nf_enter { enter = begin fun gl -> + let gl = Tacmach.New.of_old (fun x -> x) gl in + let concl = Tacmach.pf_concl gl in + let hyps = Tacmach.pf_hyps_types gl in try let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in let env = Env.elements env in @@ -1810,19 +1812,19 @@ 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" ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) - end + end } let micromega_genr prover = (micromega_genr prover) @@ -1901,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/csdpcert.ml b/plugins/micromega/csdpcert.ml index b41f29c981..2536005ede 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 62f0ae5037..e6b5cc60d4 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,17 +16,12 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Errors -open Misctypes +open Constrarg DECLARE PLUGIN "micromega_plugin" -let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") - | ArgArg x -> x - TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) ] -> [ (Coq_micromega.psatz_Z (out_arg i)) ] +| [ "psatz_Z" int_or_var(i) ] -> [ (Coq_micromega.psatz_Z i) ] | [ "psatz_Z" ] -> [ (Coq_micromega.psatz_Z (-1)) ] END @@ -63,12 +58,12 @@ TACTIC EXTEND LRA_R END TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) ] -> [ (Coq_micromega.psatz_R (out_arg i)) ] +| [ "psatz_R" int_or_var(i) ] -> [ (Coq_micromega.psatz_R i) ] | [ "psatz_R" ] -> [ (Coq_micromega.psatz_R (-1)) ] END TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) ] -> [ (Coq_micromega.psatz_Q (out_arg i)) ] +| [ "psatz_Q" int_or_var(i) ] -> [ (Coq_micromega.psatz_Q i) ] | [ "psatz_Q" ] -> [ (Coq_micromega.psatz_Q (-1)) ] END diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 0247204490..e22fe58434 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -23,7 +23,7 @@ struct - None , Some v -> \]-oo,v\] - Some v, None -> \[v,+oo\[ - Some v, Some v' -> \[v,v'\] - Intervals needs to be explicitely normalised. + Intervals needs to be explicitly normalised. *) type who = Left | Right @@ -120,7 +120,7 @@ and cstr_info = { (** A system of constraints has the form [\{sys = s ; vars = v\}]. [s] is a hashtable mapping a normalised vector to a [cstr_info] record where - [bound] is an interval - - [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint. + - [prf_idx] is the set of hypothesis indexes (i.e. constraints in the initial system) used to obtain the current constraint. In the initial system, each constraint is given an unique singleton proof_idx. When a new constraint c is computed by a function f(c1,...,cn), its proof_idx is ISet.fold union (List.map (fun x -> x.proof_idx) [c1;...;cn] - [pos] is the number of positive values of the vector @@ -872,7 +872,7 @@ let mk_proof hyps prf = | Elim(v,prf1,prf2) -> let prfsl = mk_proof prf1 and prfsr = mk_proof prf2 in - (* I take only the pairs for which the elimination is meaningfull *) + (* I take only the pairs for which the elimination is meaningful *) forall_pairs (pivot v) prfsl prfsr | And(prf1,prf2) -> let prfsl1 = mk_proof prf1 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/mutils.ml b/plugins/micromega/mutils.ml index 465c7afcee..c13e8fc28f 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 2dc0d00323..88b13abf9a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index b8b42a3f25..90a108a3b7 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli index fc0b2fd466..1ca27ea20a 100644 --- a/plugins/micromega/sos.mli +++ b/plugins/micromega/sos.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml index e95437141c..615ac5a2fb 100644 --- a/plugins/micromega/sos_types.ml +++ b/plugins/micromega/sos_types.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |