diff options
| -rw-r--r-- | tactics/abstract.ml | 74 | ||||
| -rw-r--r-- | tactics/abstract.mli | 8 | ||||
| -rw-r--r-- | tactics/declare.ml | 80 | ||||
| -rw-r--r-- | tactics/declare.mli | 47 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 11 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 4 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 1 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 14 | ||||
| -rw-r--r-- | vernac/declareDef.mli | 15 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 38 |
10 files changed, 168 insertions, 124 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 diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index d6001f5970..1bb6620886 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -62,11 +62,16 @@ val declare_fix -> Impargs.manual_implicits -> GlobRef.t -val prepare_definition : allow_evars:bool -> - ?opaque:bool -> ?inline:bool -> poly:bool -> - Evd.evar_map -> UState.universe_decl -> - types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_definition + : allow_evars:bool + -> ?opaque:bool + -> ?inline:bool + -> poly:bool + -> Evd.evar_map + -> UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 5ace8b917c..93c3f900bb 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -384,17 +384,14 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with - Declare.proof_entry_body = - Future.chain const.Declare.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) - } + Declare.Internal.map_entry_body const + ~f:(fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) let finish_proved env sigma idopt po info = let open Proof_global in @@ -452,7 +449,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Declare.proof_entry_opaque = false } in + let f_def = Declare.Internal.set_opacity ~opaque:false f_def in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,20 +460,15 @@ let finish_derived ~f ~name ~idopt ~entries = performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match lemma_def.Declare.proof_entry_type with - | Some t -> t + let lemma_pretype typ = + match typ with + | Some t -> Some (substf t) | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in + let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = - { lemma_def with - Declare.proof_entry_body = lemma_body; - proof_entry_type = Some lemma_type } - in + let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = Declare.DefinitionEntry lemma_def in let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () @@ -491,7 +483,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = | Some id -> id | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in - let entry, args = Abstract.shrink_entry local_context entry in + let entry, args = Declare.Internal.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in |