aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/abstract.ml74
-rw-r--r--tactics/abstract.mli8
-rw-r--r--tactics/declare.ml80
-rw-r--r--tactics/declare.mli47
-rw-r--r--tactics/ind_tables.ml11
-rw-r--r--tactics/pfedit.ml4
-rw-r--r--tactics/pfedit.mli1
-rw-r--r--tactics/proof_global.ml14
8 files changed, 143 insertions, 96 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 03ab0a1c13..4ddd29f973 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -8,14 +8,11 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-module CVars = Vars
-
open Util
open Termops
open EConstr
open Evarutil
-module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(* tactical to save as name a subproof such that the generalisation of
@@ -37,54 +34,6 @@ let interpretable_as_section_decl env evd d1 d2 =
e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
| LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2)
-let rec decompose len c t accu =
- let open Constr in
- let open Context.Rel.Declaration in
- if len = 0 then (c, t, accu)
- else match kind c, kind t with
- | Lambda (na, u, c), Prod (_, _, t) ->
- decompose (pred len) c t (LocalAssum (na, u) :: accu)
- | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
- decompose (pred len) c t (LocalDef (na, b, u) :: accu)
- | _ -> assert false
-
-let rec shrink ctx sign c t accu =
- let open Constr in
- let open CVars in
- match ctx, sign with
- | [], [] -> (c, t, accu)
- | p :: ctx, decl :: sign ->
- if noccurn 1 c && noccurn 1 t then
- let c = subst1 mkProp c in
- let t = subst1 mkProp t in
- shrink ctx sign c t accu
- else
- let c = Term.mkLambda_or_LetIn p c in
- let t = Term.mkProd_or_LetIn p t in
- let accu = if RelDecl.is_local_assum p
- then mkVar (NamedDecl.get_id decl) :: accu
- else accu
- in
- shrink ctx sign c t accu
-| _ -> assert false
-
-let shrink_entry sign const =
- let open Declare in
- let typ = match const.proof_entry_type with
- | None -> assert false
- | Some t -> t
- in
- (* The body has been forced by the call to [build_constant_by_tactic] *)
- let () = assert (Future.is_over const.proof_entry_body) in
- let ((body, uctx), eff) = Future.force const.proof_entry_body in
- let (body, typ, ctx) = decompose (List.length sign) body typ [] in
- let (body, typ, args) = shrink ctx sign body typ [] in
- let const = { const with
- proof_entry_body = Future.from_val ((body, uctx), eff);
- proof_entry_type = Some typ;
- } in
- (const, args)
-
let name_op_to_name ~name_op ~name suffix =
match name_op with
| Some s -> s
@@ -101,9 +50,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
redundancy on constant declaration. This opens up an interesting
question, how does abstract behave when discharge is local for example?
*)
- let suffix = if opaque
- then "_subproof"
- else "_subterm" in
+ let suffix, kind = if opaque
+ then "_subproof", Decls.(IsProof Lemma)
+ else "_subterm", Decls.(IsDefinition Definition)
+ in
let name = name_op_to_name ~name_op ~name suffix in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -140,7 +90,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
let ectx = Evd.evar_universe_context evd in
let (const, safe, ectx) =
- try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac
+ try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ectx secsign concl solve_tac
with Logic_monad.TacticFailure e as src ->
(* if the tactic [tac] fails, it reports a [TacticFailure e],
which is an error irrelevant to the proof system (in fact it
@@ -151,16 +101,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
in
let body, effs = Future.force const.Declare.proof_entry_body in
(* We drop the side-effects from the entry, they already exist in the ambient environment *)
- let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in
- let const, args = shrink_entry sign const in
+ let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in
+ (* EJGA: Hack related to the above call to
+ `build_constant_by_tactic` with `~opaque:Transparent`. Even if
+ the abstracted term is destined to be opaque, if we trigger the
+ `if poly && opaque && private_poly_univs ()` in `Proof_global`
+ kernel will boom. This deserves more investigation. *)
+ let const = Declare.Internal.set_opacity ~opaque const in
+ let const, args = Declare.Internal.shrink_entry sign const in
let args = List.map EConstr.of_constr args in
- let cd = { const with Declare.proof_entry_opaque = opaque } in
- let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in
let cst () =
(* do not compute the implicit arguments, it may be costly *)
let () = Impargs.make_implicit_args false in
(* ppedrot: seems legit to have abstracted subproofs as local*)
- Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
+ Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const
in
let cst, eff = Impargs.with_implicit_protection cst () in
let inst = match const.Declare.proof_entry_universes with
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 96ddbea7b2..779e46cd49 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,11 +20,3 @@ val cache_term_by_tactic_then
-> unit Proofview.tactic
val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
-
-(* Internal but used in a few places; should likely be made intro a
- proper library function, or incorporated into the generic constant
- save path *)
-val shrink_entry
- : ('a, 'b) Context.Named.Declaration.pt list
- -> 'c Declare.proof_entry
- -> 'c Declare.proof_entry * Constr.t list
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 57eeddb847..eb17cf67d1 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -174,6 +174,7 @@ let record_aux env s_ty s_bo =
Aux_file.record_in_aux "context_used" v
let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
+
let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
{ proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
@@ -184,6 +185,26 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
proof_entry_feedback = None;
proof_entry_inline_code = inline}
+let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+ ?(univs=default_univ_entry) body =
+ { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
+ proof_entry_secctx = None;
+ proof_entry_type = types;
+ proof_entry_universes = univs;
+ proof_entry_opaque = opaque;
+ proof_entry_feedback = None;
+ proof_entry_inline_code = inline}
+
+let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body =
+ { proof_entry_body = body
+ ; proof_entry_secctx = section_vars
+ ; proof_entry_type = types
+ ; proof_entry_universes = univs
+ ; proof_entry_opaque = opaque
+ ; proof_entry_feedback = feedback_id
+ ; proof_entry_inline_code = inline
+ }
+
let cast_proof_entry e =
let (body, ctx), () = Future.force e.proof_entry_body in
let univs =
@@ -413,3 +434,62 @@ let assumption_message id =
the type of the object than to the name of the object (see
discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
+
+module Internal = struct
+
+ let map_entry_body ~f entry =
+ { entry with proof_entry_body = Future.chain entry.proof_entry_body f }
+
+ let map_entry_type ~f entry =
+ { entry with proof_entry_type = f entry.proof_entry_type }
+
+ let set_opacity ~opaque entry =
+ { entry with proof_entry_opaque = opaque }
+
+ let rec decompose len c t accu =
+ let open Constr in
+ let open Context.Rel.Declaration in
+ if len = 0 then (c, t, accu)
+ else match kind c, kind t with
+ | Lambda (na, u, c), Prod (_, _, t) ->
+ decompose (pred len) c t (LocalAssum (na, u) :: accu)
+ | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
+ decompose (pred len) c t (LocalDef (na, b, u) :: accu)
+ | _ -> assert false
+
+ let rec shrink ctx sign c t accu =
+ let open Constr in
+ let open Vars in
+ match ctx, sign with
+ | [], [] -> (c, t, accu)
+ | p :: ctx, decl :: sign ->
+ if noccurn 1 c && noccurn 1 t then
+ let c = subst1 mkProp c in
+ let t = subst1 mkProp t in
+ shrink ctx sign c t accu
+ else
+ let c = Term.mkLambda_or_LetIn p c in
+ let t = Term.mkProd_or_LetIn p t in
+ let accu = if Context.Rel.Declaration.is_local_assum p
+ then mkVar (NamedDecl.get_id decl) :: accu
+ else accu
+ in
+ shrink ctx sign c t accu
+ | _ -> assert false
+
+ let shrink_entry sign const =
+ let typ = match const.proof_entry_type with
+ | None -> assert false
+ | Some t -> t
+ in
+ (* The body has been forced by the call to [build_constant_by_tactic] *)
+ let () = assert (Future.is_over const.proof_entry_body) in
+ let ((body, uctx), eff) = Future.force const.proof_entry_body in
+ let (body, typ, ctx) = decompose (List.length sign) body typ [] in
+ let (body, typ, args) = shrink ctx sign body typ [] in
+ { const with
+ proof_entry_body = Future.from_val ((body, uctx), eff)
+ ; proof_entry_type = Some typ
+ }, args
+
+end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 1a037ef937..0cdf317fe4 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -20,7 +20,7 @@ open Entries
[Nametab] and [Impargs]. *)
(** Proof entries *)
-type 'a proof_entry = {
+type 'a proof_entry = private {
proof_entry_body : 'a Entries.const_entry_body;
(* List of section variables *)
proof_entry_secctx : Id.Set.t option;
@@ -55,10 +55,35 @@ val declare_variable
i.e. Definition/Theorem/Axiom/Parameter/... *)
(* Default definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?fix_exn:Future.fix_exn ->
- ?opaque:bool -> ?inline:bool -> ?types:types ->
- ?univs:Entries.universes_entry ->
- ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry
+val definition_entry
+ : ?fix_exn:Future.fix_exn
+ -> ?opaque:bool
+ -> ?inline:bool
+ -> ?types:types
+ -> ?univs:Entries.universes_entry
+ -> ?eff:Evd.side_effects
+ -> constr
+ -> Evd.side_effects proof_entry
+
+val pure_definition_entry
+ : ?fix_exn:Future.fix_exn
+ -> ?opaque:bool
+ -> ?inline:bool
+ -> ?types:types
+ -> ?univs:Entries.universes_entry
+ -> constr
+ -> unit proof_entry
+
+(* Delayed definition entries *)
+val delayed_definition_entry
+ : ?opaque:bool
+ -> ?inline:bool
+ -> ?feedback_id:Stateid.t
+ -> ?section_vars:Id.Set.t
+ -> ?univs:Entries.universes_entry
+ -> ?types:types
+ -> 'a Entries.const_entry_body
+ -> 'a proof_entry
type import_status = ImportDefaultBehavior | ImportNeedQualified
@@ -101,3 +126,15 @@ val check_exists : Id.t -> unit
(* Used outside this module only in indschemes *)
exception AlreadyDeclared of (string option * Id.t)
+
+(* For legacy support, do not use *)
+module Internal : sig
+
+ val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
+ val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
+ (* Overriding opacity is indeed really hacky *)
+ val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
+
+ val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
+
+end
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 3f824a94bf..ac98b5f116 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,16 +124,7 @@ let define internal role id c poly univs =
let ctx = UState.minimize univs in
let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs = UState.univ_entry ~poly ctx in
- let entry = {
- Declare.proof_entry_body =
- Future.from_val ((c,Univ.ContextSet.empty), ());
- proof_entry_secctx = None;
- proof_entry_type = None;
- proof_entry_universes = univs;
- proof_entry_opaque = false;
- proof_entry_inline_code = false;
- proof_entry_feedback = None;
- } in
+ let entry = Declare.pure_definition_entry ~univs c in
let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
let () = match internal with
| InternalTacticRequest -> ()
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 413c6540a3..3e057190ac 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -114,14 +114,14 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
let next = let n = ref 0 in fun () -> incr n; !n
-let build_constant_by_tactic ~name ctx sign ~poly typ tac =
+let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~poly typ tac =
let evd = Evd.from_ctx ctx in
let goals = [ (Global.env_of_context sign , typ) ] in
let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
try
let pf, status = by tac pf in
let open Proof_global in
- let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
+ let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
match entries with
| [entry] ->
entry, status, universes
diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli
index 30514191fa..a780b2d96e 100644
--- a/tactics/pfedit.mli
+++ b/tactics/pfedit.mli
@@ -59,6 +59,7 @@ val use_unification_heuristics : unit -> bool
val build_constant_by_tactic
: name:Id.t
+ -> ?opaque:Proof_global.opacity_flag
-> UState.t
-> named_context_val
-> poly:bool
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index b723922642..b1fd34e43c 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -238,18 +238,10 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
let t = EConstr.Unsafe.to_constr t in
let univstyp, body = make_body t p in
let univs, typ = Future.force univstyp in
- let open Declare in
- {
- proof_entry_body = body;
- proof_entry_secctx = section_vars;
- proof_entry_feedback = feedback_id;
- proof_entry_type = Some typ;
- proof_entry_inline_code = false;
- proof_entry_opaque = opaque;
- proof_entry_universes = univs; }
+ Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
in
- let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
- { name; entries = entries; poly; universes; udecl }
+ let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
+ { name; entries; poly; universes; udecl }
let return_proof ?(allow_partial=false) ps =
let { proof } = ps in
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:24:25 +0000