From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- plugins/micromega/mfourier.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 88c1a78366..a36369d220 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 -- cgit v1.2.3 From cc42541eeaaec0371940e07efdb009a4ee74e468 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 13:04:45 +0200 Subject: Boxing the Goal.enter primitive into a record type. --- plugins/micromega/coq_micromega.ml | 24 +++++++++--------------- 1 file changed, 9 insertions(+), 15 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ef1169342f..a0e61623c7 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -20,6 +20,7 @@ open Pp open Mutils open Proofview open Goptions +open Proofview.Notations (** * Debug flag @@ -1444,8 +1445,7 @@ 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 -> Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1462,7 +1462,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* Tactics.new_generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - end + end } (** @@ -1707,9 +1707,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec prover = - Proofview.Goal.nf_enter - begin - fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try @@ -1735,7 +1733,7 @@ let micromega_gen ^ "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 +1754,7 @@ 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 -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -1774,7 +1770,7 @@ let micromega_order_changer cert env ff = Tactics.new_generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] - end + end } let micromega_genr prover = @@ -1790,9 +1786,7 @@ 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 -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in try @@ -1822,7 +1816,7 @@ let micromega_genr prover = ^ "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) -- cgit v1.2.3 From 4cc1714ac9b0944b6203c23af8c46145e7239ad3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 14:45:31 +0200 Subject: Indexing Proofview.goals with a stage. This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level. --- plugins/micromega/coq_micromega.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a0e61623c7..470e21c820 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -888,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 @@ -1169,8 +1169,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.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 = @@ -1446,6 +1446,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let vm = dump_varmap (spec.typ) env in (* todo : directly generate the proof term - or generalize before conversion? *) 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,7 +1458,7 @@ 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 ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) @@ -1708,8 +1709,9 @@ let micromega_gen unsat deduce spec prover = Proofview.Goal.nf_enter { enter = begin fun gl -> - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in + 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 @@ -1755,6 +1757,7 @@ let micromega_order_changer cert env ff = let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) env in 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 @@ -1766,7 +1769,7 @@ let micromega_order_changer cert env ff = [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) ] - (Tacmach.New.pf_concl gl))); + (Tacmach.pf_concl gl))); Tactics.new_generalize env ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] @@ -1787,8 +1790,9 @@ let micromega_genr prover = dump_proof = dump_psatz coq_Q dump_q } in Proofview.Goal.nf_enter { enter = begin fun gl -> - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_hyps_types gl in + 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 -- cgit v1.2.3 From a593bb93b3047986bf9ac335ab21530621962885 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 22:37:13 +0100 Subject: Preventing an unwanted warning 5 "this function application is partial" which e.g. OCaml 4.02.1 displays. --- plugins/micromega/coq_micromega.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 470e21c820..c008a3aa71 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -82,10 +82,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). -- cgit v1.2.3 From 589130e87d68227d25800e7506666eaf1d47a25a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:30:09 +0100 Subject: Changing the toplevel type of the int_or_var generic type to int. --- plugins/micromega/g_micromega.ml4 | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 62f0ae5037..3c46e1eea0 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -21,12 +21,8 @@ open Misctypes 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 +59,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 -- cgit v1.2.3 From d5b1807e65f7ea29d435c3f894aa551370c5989f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:47:59 +0100 Subject: Fix typos. --- plugins/micromega/mfourier.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/micromega') diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 0261d73490..e22fe58434 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -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 -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/micromega/Env.v | 2 +- plugins/micromega/EnvRing.v | 2 +- plugins/micromega/Lia.v | 2 +- plugins/micromega/MExtraction.v | 2 +- plugins/micromega/OrderedRing.v | 2 +- plugins/micromega/Psatz.v | 2 +- plugins/micromega/QMicromega.v | 2 +- plugins/micromega/RMicromega.v | 2 +- plugins/micromega/Refl.v | 2 +- plugins/micromega/RingMicromega.v | 2 +- plugins/micromega/Tauto.v | 2 +- plugins/micromega/VarMap.v | 2 +- plugins/micromega/ZCoeff.v | 2 +- plugins/micromega/ZMicromega.v | 2 +- plugins/micromega/certificate.ml | 2 +- plugins/micromega/coq_micromega.ml | 2 +- plugins/micromega/csdpcert.ml | 2 +- plugins/micromega/g_micromega.ml4 | 2 +- plugins/micromega/mutils.ml | 2 +- plugins/micromega/persistent_cache.ml | 2 +- plugins/micromega/polynomial.ml | 2 +- plugins/micromega/sos.mli | 2 +- plugins/micromega/sos_types.ml | 2 +- 23 files changed, 23 insertions(+), 23 deletions(-) (limited to 'plugins/micromega') 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 *) -(*