From 36f669f769fa23eb897adfa0450875a3c0db3476 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Oct 2015 12:01:38 +0200 Subject: Exporting the original unprocessed hint in the hint running function. --- plugins/firstorder/sequent.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 96c4eb01eb..a77af03dc1 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -212,6 +212,7 @@ let extend_with_auto_hints l seq gl= match repr_hint p_a_t.code with Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> + let (c, _, _) = c in (try let gr = global_of_constr c in let typ=(pf_unsafe_type_of gl c) in -- cgit v1.2.3 From daa7cb065a238c7d4ee394e00315d66d023e5259 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Dec 2015 17:55:25 +0100 Subject: Removing auto from the tactic AST. --- plugins/firstorder/g_ground.ml4 | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c28da42aea..9d853a79a7 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -52,8 +52,15 @@ let _= in declare_int_option gdopt +let default_intuition_tac = + let tac _ _ = Auto.h_auto None [] None in + let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in + let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in + Tacenv.register_ml_tactic name [| tac |]; + Tacexpr.TacML (Loc.ghost, entry, []) + let (set_default_solver, default_solver, print_default_solver) = - Tactic_option.declare_tactic_option ~default:(<:tactic>) "Firstorder default solver" + Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ -- cgit v1.2.3 From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jan 2016 00:58:42 +0100 Subject: Protect code against changes in Map interface. The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. --- plugins/firstorder/sequent.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index dc3f05be69..760168c9f6 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -13,7 +13,7 @@ open Globnames module OrderedConstr: Set.OrderedType with type t=constr -module CM: Map.S with type key=constr +module CM: CSig.MapS with type key=constr type h_item = global_reference * (int*constr) option -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- plugins/firstorder/formula.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 6c7b093838..d306112ce7 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -7,7 +7,6 @@ (************************************************************************) open Term -open Context open Globnames val qflag : bool ref @@ -27,7 +26,7 @@ type counter = bool -> metavariable val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array val ind_hyps : int -> pinductive -> constr list -> - Proof_type.goal Tacmach.sigma -> rel_context array + Proof_type.goal Tacmach.sigma -> Context.Rel.t array type atoms = {positive:constr list;negative:constr list} -- 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/firstorder/formula.ml | 2 +- plugins/firstorder/formula.mli | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- plugins/firstorder/ground.ml | 2 +- plugins/firstorder/ground.mli | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/instances.mli | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/firstorder/rules.mli | 2 +- plugins/firstorder/sequent.ml | 2 +- plugins/firstorder/sequent.mli | 2 +- plugins/firstorder/unify.ml | 2 +- plugins/firstorder/unify.mli | 2 +- 13 files changed, 13 insertions(+), 13 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 62a8605a3d..ae2d059fa2 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- plugins/firstorder/formula.ml | 11 ++++++----- plugins/firstorder/instances.ml | 3 ++- plugins/firstorder/rules.ml | 6 ++++-- 3 files changed, 12 insertions(+), 8 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index ae2d059fa2..2ed436c6bf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,6 +15,7 @@ open Tacmach open Util open Declarations open Globnames +open Context.Rel.Declaration let qflag=ref true @@ -139,8 +140,8 @@ let build_atoms gl metagen side cciterm = negative:= unsigned :: !negative end; let v = ind_hyps 0 i l gl in - let g i _ (_,_,t) = - build_rec env polarity (lift i t) in + let g i _ decl = + build_rec env polarity (lift i (get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -150,8 +151,8 @@ let build_atoms gl metagen side cciterm = | Exists(i,l)-> let var=mkMeta (metagen true) in let v =(ind_hyps 1 i l gl).(0) in - let g i _ (_,_,t) = - build_rec (var::env) polarity (lift i t) in + let g i _ decl = + build_rec (var::env) polarity (lift i (get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -224,7 +225,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in + let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a717cc91ea..797f43f2a0 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,6 +22,7 @@ open Formula open Sequent open Names open Misctypes +open Context.Rel.Declaration let compare_instance inst1 inst2= match inst1,inst2 with @@ -117,7 +118,7 @@ let mk_open_instance id idc gl m t= if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in - let decl = (Name nid,None,c) in + let decl = LocalAssum (Name nid,c) in aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in evmap, decls, revt diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index e676a8a936..b0e8f7d25c 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -19,6 +19,7 @@ open Formula open Sequent open Globnames open Locus +open Context.Named.Declaration type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic @@ -34,12 +35,13 @@ let wrap n b continue seq gls= if i<=0 then seq else match nc with []->anomaly (Pp.str "Not the expected number of hyps") - | ((id,_,typ) as nd)::q-> + | nd::q-> + let id = get_id nd in if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) (get_type nd) (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in -- cgit v1.2.3 From 968dfdb15cc11d48783017b2a91147b25c854ad6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Dec 2015 19:45:01 +0100 Subject: Monotonizing the Evarutil module. Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now. --- plugins/firstorder/instances.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a717cc91ea..fcbad46d46 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -22,6 +22,7 @@ open Formula open Sequent open Names open Misctypes +open Sigma.Notations let compare_instance inst1 inst2= match inst1,inst2 with @@ -116,7 +117,9 @@ let mk_open_instance id idc gl m t= let rec aux n avoid env evmap decls = if Int.equal n 0 then evmap, decls else let nid=(fresh_id avoid var_id gl) in - let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + let evmap = Sigma.Unsafe.of_evar_map evmap in + let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in + let evmap = Sigma.to_evar_map evmap in let decl = (Name nid,None,c) in aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in let evmap, decls = aux m [] env evmap [] in -- cgit v1.2.3 From 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 14:26:43 +0100 Subject: Moving conversion functions to the new tactic API. --- plugins/firstorder/rules.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index e676a8a936..d539eda579 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -210,6 +210,6 @@ let defined_connectives=lazy let normalize_evaluables= onAllHypsAndConcl (function - None->unfold_in_concl (Lazy.force defined_connectives) + None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives)) | Some id -> - unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) + Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))) -- cgit v1.2.3 From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Feb 2016 10:32:57 +0100 Subject: The tactic generic argument now returns a value rather than a glob_expr. The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. --- plugins/firstorder/g_ground.ml4 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 25509b4b5f..3e8be36993 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -135,17 +135,17 @@ END TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) firstorder_using(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l []) ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l []) ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) [] l) ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) [] l) ] | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> - [ Proofview.V82.tactic (gen_ground_tac true (Option.map eval_tactic t) l l') ] + [ Proofview.V82.tactic (gen_ground_tac true (Option.map (tactic_of_value ist) t) l l') ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ Proofview.V82.tactic (gen_ground_tac false (Option.map eval_tactic t) [] []) ] + [ Proofview.V82.tactic (gen_ground_tac false (Option.map (tactic_of_value ist) t) [] []) ] END open Proofview.Notations -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- plugins/firstorder/g_ground.ml4 | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 3e8be36993..587d10d1cc 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -15,6 +15,10 @@ open Goptions open Tacticals open Tacinterp open Libnames +open Constrarg +open Stdarg +open Pcoq.Prim +open Pcoq.Tactic DECLARE PLUGIN "ground_plugin" -- cgit v1.2.3