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