diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 74 | ||||
| -rw-r--r-- | tactics/abstract.mli | 8 | ||||
| -rw-r--r-- | tactics/declare.ml | 88 | ||||
| -rw-r--r-- | tactics/declare.mli | 60 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 11 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 22 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 5 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 14 |
8 files changed, 179 insertions, 103 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 9b4a628871..1e18028e7b 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 @@ -39,54 +36,6 @@ let interpretable_as_section_decl env sigma d1 d2 = e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2 | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma 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 @@ -103,9 +52,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 @@ -141,7 +91,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 sigma 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 @@ -152,16 +102,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..9f104590e7 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 = @@ -326,6 +347,12 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff +let inline_private_constants ~univs env ce = + let body, eff = Future.force ce.proof_entry_body in + let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let univs = UState.merge ~sideff:true Evd.univ_rigid univs ctx in + cb, univs + (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry @@ -413,3 +440,64 @@ 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 get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body + + 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..a4d3f17594 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 @@ -83,6 +108,15 @@ val declare_private_constant -> unit proof_entry -> Constant.t * Evd.side_effects +(** [inline_private_constants ~sideff ~univs env ce] will inline the + constants in [ce]'s body and return the body plus the updated + [UState.t]. *) +val inline_private_constants + : univs:UState.t + -> Environ.env + -> Evd.side_effects proof_entry + -> Constr.t * UState.t + (** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : @@ -101,3 +135,19 @@ 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 + + (* TODO: This is only used in DeclareDef to forward the fix to + hooks, should eventually go away *) + val get_fix_exn : 'a proof_entry -> Future.fix_exn + + 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..3c9803432a 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -55,8 +55,7 @@ let get_current_goal_context pf = let env = Global.env () in Evd.from_env env, env -let get_current_context pf = - let p = Proof_global.get_proof pf in +let get_proof_context p = try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -64,6 +63,10 @@ let get_current_context pf = let { Proof.sigma } = Proof.data p in sigma, Global.env () +let get_current_context pf = + let p = Proof_global.get_proof pf in + get_proof_context p + let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac @@ -114,14 +117,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 @@ -135,12 +138,13 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Declare.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body + let cb, univs = + if side_eff then Declare.inline_private_constants ~univs env ce + else + (* GG: side effects won't get reset: no need to treat their universes specially *) + let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in + cb, UState.merge ~sideff:false Evd.univ_rigid univs ctx in - let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic ~name ~poly env sigma ty tac = diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 30514191fa..a2e742c0d7 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : Proof.t -> Evd.evar_map * env + (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. @@ -59,6 +63,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 |