From 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Jun 2016 18:58:24 -0400 Subject: Add support for transparent abstract (no syntax) This is a small change that allows a transparent version of tclABSTRACT. Additionally, it factors the machinery of [abstract] through a plugin-accessible function which allows alternate continuations (other than exact_no_check. It might be nice to factor it further, into a cache_term function that caches a term, and a separate bit that calls cache_term with the result of running the tactic. --- tactics/tactics.ml | 28 ++++++++++++++++++---------- tactics/tactics.mli | 4 +++- 2 files changed, 21 insertions(+), 11 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e79258582..19627eb53 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4907,7 +4907,7 @@ let shrink_entry sign const = } in (const, args) -let abstract_subproof id gk tac = +let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -4957,8 +4957,8 @@ let abstract_subproof id gk tac = else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) in let args = List.map EConstr.of_constr args in - let cd = Entries.DefinitionEntry const in - let decl = (cd, IsProof Lemma) in + let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in + let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in let cst () = (** do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in @@ -4976,18 +4976,21 @@ let abstract_subproof id gk tac = Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> - exact_no_check (applist (lem, args)) + tacK lem args in let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in Sigma.Unsafe.of_pair (tac, evd) end } +let abstract_subproof id gk tac ?(opaque=true) = + cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args))) + let anon_id = Id.of_string "anonymous" -let tclABSTRACT name_op tac = +let name_op_to_name name_op object_kind suffix = let open Proof_global in - let default_gk = (Global, false, Proof Theorem) in - let s, gk = match name_op with + let default_gk = (Global, false, object_kind) in + match name_op with | Some s -> (try let _, gk, _ = current_proof_statement () in s, gk with NoCurrentProof -> s, default_gk) @@ -4995,9 +4998,14 @@ let tclABSTRACT name_op tac = let name, gk = try let name, gk, _ = current_proof_statement () in name, gk with NoCurrentProof -> anon_id, default_gk in - add_suffix name "_subproof", gk - in - abstract_subproof s gk tac + add_suffix name suffix, gk + +let tclABSTRACT ?(opaque=true) name_op tac = + let open Proof_global in + let s, gk = if opaque + then name_op_to_name name_op (Proof Theorem) "_subproof" + else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in + abstract_subproof s gk tac ~opaque:opaque let unify ?(state=full_transparent_state) x y = Proofview.Goal.s_enter { s_enter = begin fun gl -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ba4a9706d..d206011ee 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -401,7 +401,9 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic +val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic + +val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic -- cgit v1.2.3 From 12f34b2ebfcbe958ba53b49399c3fcaf01f7a18c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Apr 2017 09:50:55 -0400 Subject: Generalize cache_term_by_tactic_then This will allow a cache_term tactic that doesn't suffer from the Not_found anomalies of abstract in typeclass resolution. --- tactics/tactics.ml | 7 +++++-- tactics/tactics.mli | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 19627eb53..20de56645 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4907,7 +4907,7 @@ let shrink_entry sign const = } in (const, args) -let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK = +let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -4927,7 +4927,10 @@ let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK = else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in - let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in + let concl = match goal_type with + | None -> Proofview.Goal.concl gl + | Some ty -> ty in + let concl = it_mkNamedProd_or_LetIn concl sign in let concl = try flush_and_check_evars !evdref concl with Uninstantiated_evar _ -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d206011ee..082812c5a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -401,7 +401,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic +val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic -- cgit v1.2.3 From b348a11ccc4913598b72e4ecbb58811bcccd7bfc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Apr 2017 12:34:07 -0400 Subject: Make opaque optional only for tclABSTRACT Also move named arguments to the beginning of the functions. As per https://github.com/coq/coq/pull/201#discussion_r110928302 --- tactics/tactics.ml | 8 ++++---- tactics/tactics.mli | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 20de56645..8f791cdcf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4907,7 +4907,7 @@ let shrink_entry sign const = } in (const, args) -let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK = +let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -4985,8 +4985,8 @@ let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK = Sigma.Unsafe.of_pair (tac, evd) end } -let abstract_subproof id gk tac ?(opaque=true) = - cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args))) +let abstract_subproof ~opaque id gk tac = + cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) let anon_id = Id.of_string "anonymous" @@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac = let s, gk = if opaque then name_op_to_name name_op (Proof Theorem) "_subproof" else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof s gk tac ~opaque:opaque + abstract_subproof ~opaque:opaque s gk tac let unify ?(state=full_transparent_state) x y = Proofview.Goal.s_enter { s_enter = begin fun gl -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 082812c5a..07a803542 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -401,7 +401,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic +val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic -- cgit v1.2.3 From 1e046726dc9352f7979ebdeba0d750e44016fea5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Apr 2017 12:48:23 -0400 Subject: transparent abstract: Respond to review comment https://github.com/coq/coq/pull/201#discussion_r110952601 --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8f791cdcf..d02fe8665 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4986,7 +4986,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = end } let abstract_subproof ~opaque id gk tac = - cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) + cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) let anon_id = Id.of_string "anonymous" -- cgit v1.2.3 From e4262a89d7bc3d9b985d9a4a939f34176581abcb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Apr 2017 13:05:54 -0400 Subject: transparent abstract: Respond to review comment https://github.com/coq/coq/pull/201#discussion_r110957570 --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d02fe8665..465481703 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac = let s, gk = if opaque then name_op_to_name name_op (Proof Theorem) "_subproof" else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof ~opaque:opaque s gk tac + abstract_subproof ~opaque s gk tac let unify ?(state=full_transparent_state) x y = Proofview.Goal.s_enter { s_enter = begin fun gl -> -- cgit v1.2.3 From 2553e4bf5735a2bd127832e2d26609c6a8096fb7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 1 May 2017 17:24:29 +0200 Subject: Removing dead code in Autorewrite. Since 260965d, an imperative code was semantically the identity because the closure allocation was not performed at the right moment. Because of it intricacy, I cannot really tell the original motivations of this piece of code, although it looks like it was for there for pretty-printing of errors. Anyway, both because the code was dubious and its effect not observed, it cannot hurt to remove it. --- tactics/autorewrite.ml | 44 ++++++-------------------------------------- 1 file changed, 6 insertions(+), 38 deletions(-) (limited to 'tactics') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index e58ec5a31..3c430cb17 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -127,45 +127,13 @@ let autorewrite ?(conds=Naive) tac_main lbas = (Proofview.tclUNIT()) lbas)) let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) - let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in - let general_rewrite_in id = - let id = ref id in - let to_be_cleared = ref false in - fun dir cstr tac gl -> - let last_hyp_id = - match Tacmach.pf_hyps gl with - d :: _ -> Context.Named.Declaration.get_id d - | _ -> (* even the hypothesis id is missing *) - raise (Logic.RefinerError (Logic.NoSuchHyp !id)) - in - let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in - let gls = gl'.Evd.it in - match gls with - g::_ -> - (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with - d ::_ -> - let lastid = Context.Named.Declaration.get_id d in - if not (Id.equal last_hyp_id lastid) then - begin - let gl'' = - if !to_be_cleared then - tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl - else gl' in - id := lastid ; - to_be_cleared := true ; - gl'' - end - else - begin - to_be_cleared := false ; - gl' - end - | _ -> assert false) (* there must be at least an hypothesis *) - | _ -> assert false (* rewriting cannot complete a proof *) - in - let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in + let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in + let general_rewrite_in id dir cstr tac = + let cstr = EConstr.of_constr cstr in + general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false id cstr false + in Tacticals.New.tclMAP (fun id -> Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac bas -> -- cgit v1.2.3 From cea40f37ab638031b9d5c6434ee5651a16ea1f3e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 1 May 2017 09:04:17 +0200 Subject: Fixing Set Rewriting Schemes bugs introduced in v8.5. - Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test. --- tactics/eqschemes.ml | 8 +++++++- test-suite/success/Scheme.v | 23 +++++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 1a45217a4..e39159fb8 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -89,6 +89,11 @@ let get_coq_eq ctx = with Not_found -> error "eq not found." +let univ_of_eq env eq = + match kind_of_term (Retyping.get_type_of env Evd.empty eq) with + | Prod (_,t,_) -> (match kind_of_term t with Sort (Type u) -> u | _ -> assert false) + | _ -> assert false + (**********************************************************************) (* Check if an inductive type [ind] has the form *) (* *) @@ -744,7 +749,7 @@ let build_congr env (eq,refl,ctx) ind = let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in let _,constrargs = decompose_app ccl in - if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then + if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then error "Constructor must have no arguments"; let b = List.nth constrargs (i + mib.mind_nparams - 1) in let varB = fresh env (Id.of_string "B") in @@ -752,6 +757,7 @@ let build_congr env (eq,refl,ctx) ind = let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt (mkNamedLambda varB (mkSort (Type uni)) diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index dd5aa81d1..855f26698 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -2,3 +2,26 @@ Scheme Induction for eq Sort Prop. Check eq_ind_dep. + +(* This was broken in v8.5 *) + +Set Rewriting Schemes. +Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a. +Unset Rewriting Schemes. + +Check myeq_rect. +Check myeq_ind. +Check myeq_rec. +Check myeq_congr. +Check myeq_sym_internal. +Check myeq_rew. +Check myeq_rew_dep. +Check myeq_rew_fwd_dep. +Check myeq_rew_r. +Check internal_myeq_sym_involutive. +Check myeq_rew_r_dep. +Check myeq_rew_fwd_r_dep. + +Set Rewriting Schemes. +Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. +Unset Rewriting Schemes. -- cgit v1.2.3 From 5548e5f6bc5446f7541cfc7d93b0b47e4b751e86 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 5 May 2017 15:39:17 +0200 Subject: Remove unused open. --- tactics/eqdecide.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'tactics') diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 472cd8f22..641929a77 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -67,7 +67,6 @@ let choose_noteq eqonleft = left_with_bindings false Misctypes.NoBindings open Sigma.Notations -open Context.Rel.Declaration (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) -- cgit v1.2.3 From a76a71eda10b054b04de4ff56f0637a32077edd4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 5 May 2017 18:09:30 +0200 Subject: Remove two unused opens. --- tactics/autorewrite.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'tactics') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 3c430cb17..2d54b61c7 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -9,8 +9,6 @@ open Equality open Names open Pp -open Tacticals -open Tactics open Term open Termops open CErrors -- cgit v1.2.3 From e0577588056110ea13a904aa1f01c86dbc931f02 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 11 May 2017 13:14:27 +0200 Subject: Remove an unused open introduced by the previous commit. --- tactics/tactics.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3842b432d..556df6e55 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5004,7 +5004,6 @@ let name_op_to_name name_op object_kind suffix = add_suffix name suffix, gk let tclABSTRACT ?(opaque=true) name_op tac = - let open Proof_global in let s, gk = if opaque then name_op_to_name name_op (Proof Theorem) "_subproof" else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in -- cgit v1.2.3 From e3550a0acc39e235e01a727267b12a7c06f23b2c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 26 Aug 2016 14:46:33 +0200 Subject: Uniformity of style for selecting plural or not; spacing for comma. --- tactics/class_tactics.ml | 2 +- vernac/obligations.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2d6dffdd2..05eb0a976 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1202,7 +1202,7 @@ module Search = struct Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ Printer.pr_econstr_env (Goal.env gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ + str ", " ++ int (List.length poss) ++ str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e0520216b..5233fab15 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit Defined cst) else ( let len = Array.length obls in - let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in progmap_add n (CEphemeron.create prg); let res = auto_solve_obligations (Some n) tactic in match res with -- cgit v1.2.3