From 836b9faa8797a2802c189e782469f8d2e467d894 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:15:05 +0200 Subject: Univs: fix evar_map leaks bugs in Function The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors. --- plugins/funind/invfun.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 89ceb751a4..d979401424 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let funs_constr = Array.map mkConstU funs in States.with_state_protection_on_exception (fun () -> - let evd = ref Evd.empty in + let env = Global.env () in + let evd = ref (Evd.from_env env) in let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = Util.Array.map2_i @@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( ) funs; - (* let evd = ref Evd.empty in *) let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> @@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by -- cgit v1.2.3 From 6f6b67d3f772205d9481436d62efb6074e975555 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 19 Oct 2015 11:17:56 +0200 Subject: Function debug mode more formatted. --- plugins/funind/invfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d979401424..d074bbabd8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -70,8 +70,8 @@ let do_observe_tac s tac g = with reraise -> let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in - observe (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal " ++ goal ); + observe (hov 0 (str "observation "++ s++str " raised exception " ++ + Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; -- cgit v1.2.3 From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- plugins/funind/invfun.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d074bbabd8..363dd1b3b7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,6 +19,7 @@ open Tactics open Indfun_common open Tacmach open Misctypes +open Termops (* Some pretty printing function for debugging purpose *) -- cgit v1.2.3 From aa99912e9adc566a179b4972ff85a92b967fb134 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 7 Dec 2014 22:44:43 +0100 Subject: Removing redundant versions of generalize. --- plugins/funind/invfun.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 363dd1b3b7..628e582e23 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -458,7 +458,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | (id,None,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id]) + (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -699,7 +699,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = }) Locusops.onConcl ; - Simple.generalize (List.map mkVar ids); + generalize (List.map mkVar ids); thin ids ] else @@ -738,7 +738,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = tclTHENSEQ [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); observe_tac "h_generalize" - (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); + (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); Proofview.V82.of_tactic (Simple.intro graph_principle_id); observe_tac "" (tclTHEN_i (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) @@ -921,7 +921,7 @@ let revert_graph kn post_tac hid g = let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ - Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; + generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); post_tac hid @@ -965,7 +965,7 @@ let functional_inversion kn hid fconst f_correct : tactic = in tclTHENSEQ[ pre_tac hid; - Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; + generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); -- 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/funind/invfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d979401424..a800c186af 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.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/funind/invfun.ml | 40 +++++++++++++++++++++++----------------- 1 file changed, 23 insertions(+), 17 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c9d3bb819..56bc4328d1 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + open Tacexpr open Declarations open Errors @@ -20,6 +21,7 @@ open Indfun_common open Tacmach open Misctypes open Termops +open Context.Rel.Declaration (* Some pretty printing function for debugging purpose *) @@ -134,18 +136,21 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type + | decl :: fun_ctxt -> fun_ctxt, get_type decl in let rec args_from_decl i accu = function | [] -> accu - | (_, Some _, _) :: l -> + | LocalDef _ :: l -> args_from_decl (succ i) accu l | _ :: l -> let t = mkRel i in args_from_decl (succ i) (t :: accu) l in (*i We need to name the vars [res] and [fv] i*) - let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in + let filter = fun decl -> match get_name decl with + | Name id -> Some id + | Anonymous -> None + in let named_ctxt = List.map_filter filter fun_ctxt in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in @@ -171,12 +176,12 @@ let generate_type evd g_to_f f graph i = \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] i*) let pre_ctxt = - (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt + LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt in (*i and we can return the solution depending on which lemma type we are defining i*) if g_to_f - then (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph - else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph + then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -260,10 +265,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* and built the intro pattern for each of them *) let intro_pats = List.map - (fun (_,_,br_type) -> + (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl))))) ) branches in @@ -390,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun ((_,(ctxt,concl))) -> match ctxt with | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") - | hres::res::(x,_,t)::ctxt -> + | hres::res::decl::ctxt -> let res = Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) - ((x,None,t)::ctxt) + (LocalAssum (get_name decl, get_type decl) :: ctxt) in res ) @@ -408,8 +413,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let bindings = let params_bindings,avoid = List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -418,8 +423,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in let lemmas_bindings = List.rev (fst (List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -455,9 +460,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes generalize every hypothesis which depends of [x] but [hyp] *) let generalize_dependent_of x hyp g = + let open Context.Named.Declaration in tclMAP (function - | (id,None,t) when not (Id.equal id hyp) && + | LocalAssum (id,t) when not (Id.equal id hyp) && (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) @@ -663,10 +669,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let branches = List.rev princ_infos.branches in let intro_pats = List.map - (fun (_,_,br_type) -> + (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type)) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl))) ) branches 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/funind/invfun.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c9d3bb819..ae2091a227 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -484,15 +484,15 @@ and intros_with_rewrite_aux : tactic = tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g @@ -703,7 +703,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = thin ids ] else - unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))] + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]) in (* The proof of each branche itself *) let ind_number = ref 0 in -- cgit v1.2.3 From 4ea9b3193eaced958bb277c0723fb54d661ff520 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 15:17:05 +0100 Subject: More conversion functions in the new tactic API. --- plugins/funind/invfun.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ae2091a227..2b45206bb4 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -363,14 +363,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false ; Genredexpr.rConst = [] } ) - Locusops.onConcl; + Locusops.onConcl); observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) @@ -532,12 +532,12 @@ and intros_with_rewrite_aux : tactic = ] g | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -547,12 +547,12 @@ and intros_with_rewrite_aux : tactic = end | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -692,12 +692,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; generalize (List.map mkVar ids); thin ids -- cgit v1.2.3 From 33fe6e61ff2f1f8184373ed8fccc403591c4605a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 21 Feb 2016 17:13:26 +0100 Subject: Moving the Tauto tactic to proper Ltac. This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there. --- plugins/funind/invfun.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'plugins/funind/invfun.ml') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index cdb9c5067f..6a5a5ad533 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -474,6 +474,15 @@ let generalize_dependent_of x hyp g = (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis (unfolding, substituting, destructing cases \ldots) *) +let tauto = + let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in + let mp = ModPath.MPfile (DirPath.make dp) in + let kn = KerName.make2 mp (Label.make "tauto") in + Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> + let body = Tacenv.interp_ltac kn in + Tacinterp.eval_tactic body + end + let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g and intros_with_rewrite_aux : tactic = @@ -530,7 +539,7 @@ and intros_with_rewrite_aux : tactic = ] g end | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> - Proofview.V82.of_tactic Tauto.tauto g + Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ Proofview.V82.of_tactic (simplest_case v); -- cgit v1.2.3