diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 71 | ||||
| -rw-r--r-- | tactics/declare.mli | 11 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 11 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 6 | ||||
| -rw-r--r-- | tactics/leminv.ml | 5 |
7 files changed, 76 insertions, 32 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 465f736032..662a2fc22c 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* 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 ~internal:Declare.InternalTacticRequest ~local:Declare.ImportNeedQualified name decl + Declare.declare_private_constant ~local:Declare.ImportNeedQualified name decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Proof_global.proof_entry_universes with diff --git a/tactics/declare.ml b/tactics/declare.ml index 4a4e2cf60a..aa94ab5a25 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -27,11 +27,7 @@ open Cooking open Decls open Decl_kinds -(** flag for internal message display *) -type internal_flag = - | UserAutomaticRequest (* kernel action, a message is displayed *) - | InternalTacticRequest (* kernel action, no message is displayed *) - | UserIndividualRequest (* user action, a message is displayed *) +module NamedDecl = Context.Named.Declaration type import_status = ImportDefaultBehavior | ImportNeedQualified @@ -150,6 +146,18 @@ let register_side_effect (c, role) = | None -> () | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] +let record_aux env s_ty s_bo = + let open Environ in + let in_ty = keep_hyps env s_ty in + let v = + String.concat " " + (CList.map_filter (fun decl -> + let id = NamedDecl.get_id decl in + if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None + else Some (Id.to_string id)) + (keep_hyps env s_bo)) in + 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 = @@ -165,24 +173,57 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types let cast_proof_entry e = let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in + let univs = + if Univ.ContextSet.is_empty ctx then e.proof_entry_universes + else match e.proof_entry_universes with + | Monomorphic_entry ctx' -> + (* This can actually happen, try compiling EqdepFacts for instance *) + Monomorphic_entry (Univ.ContextSet.union ctx' ctx) + | Polymorphic_entry _ -> + anomaly Pp.(str "Local universes in non-opaque polymorphic definition."); + in { - const_entry_body = (body, ctx); + const_entry_body = body; const_entry_secctx = e.proof_entry_secctx; const_entry_feedback = e.proof_entry_feedback; const_entry_type = e.proof_entry_type; - const_entry_universes = e.proof_entry_universes; + const_entry_universes = univs; const_entry_inline_code = e.proof_entry_inline_code; } -let cast_opaque_proof_entry e = +let cast_opaque_proof_entry (type a) (pure : a Safe_typing.effect_entry) (e : a Proof_global.proof_entry) = let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ in + let secctx = match e.proof_entry_secctx with + | None -> + let open Environ in + let env = Global.env () in + let hyp_typ, hyp_def = + if List.is_empty (Environ.named_context env) then + Id.Set.empty, Id.Set.empty + else + let ids_typ = global_vars_set env typ in + let pf, env = match pure with + | PureEntry -> + let (pf, _), () = Future.force e.proof_entry_body in + pf, env + | EffectEntry -> + let (pf, _), eff = Future.force e.proof_entry_body in + pf, Safe_typing.push_private_constants env eff + in + let vars = global_vars_set env pf in + ids_typ, vars + in + let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in + keep_hyps env (Id.Set.union hyp_typ hyp_def) + | Some hyps -> hyps + in { opaque_entry_body = e.proof_entry_body; - opaque_entry_secctx = e.proof_entry_secctx; + opaque_entry_secctx = secctx; opaque_entry_feedback = e.proof_entry_feedback; opaque_entry_type = typ; opaque_entry_universes = e.proof_entry_universes; @@ -214,7 +255,7 @@ let define_constant ~side_effect id cd = let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = match de.proof_entry_opaque with - | true -> Entries.OpaqueEntry (cast_opaque_proof_entry de) + | true -> Entries.OpaqueEntry (cast_opaque_proof_entry PureEntry de) | false -> Entries.DefinitionEntry (cast_proof_entry de) in export, ConstantEntry (PureEntry, cd) @@ -223,7 +264,7 @@ let define_constant ~side_effect id cd = let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry de in + let de = cast_opaque_proof_entry EffectEntry de in [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) | ParameterEntry e -> [], ConstantEntry (PureEntry, Entries.ParameterEntry e) @@ -233,7 +274,7 @@ let define_constant ~side_effect id cd = let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export -let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) = let () = check_exists id in let kn, (), export = define_constant ~side_effect:PureEntry id cd in (* Register the libobjects attached to the constants and its subproofs *) @@ -241,7 +282,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefault let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) = let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in let () = assert (List.is_empty export) in let () = register_constant kn kind local in @@ -252,13 +293,13 @@ let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = I let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition ?(internal=UserIndividualRequest) +let declare_definition ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) id ?types (body,univs) = let cb = definition_entry ?types ~univs ~opaque body in - declare_constant ~internal ~local id + declare_constant ~local id (DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) diff --git a/tactics/declare.mli b/tactics/declare.mli index d87c096119..1f72fff30e 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -40,11 +40,6 @@ val declare_variable : variable -> variable_declaration -> Libobject.object_name type constant_declaration = Evd.side_effects constant_entry * logical_kind -type internal_flag = - | UserAutomaticRequest - | InternalTacticRequest - | UserIndividualRequest - (* Default definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> @@ -60,13 +55,13 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t + ?local:import_status -> Id.t -> constant_declaration -> Constant.t val declare_private_constant : - ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects + ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : - ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> + ?opaque:bool -> ?kind:definition_object_kind -> ?local:import_status -> Id.t -> ?types:constr -> constr Entries.in_universes_entry -> Constant.t diff --git a/tactics/hints.ml b/tactics/hints.ml index 014e54158d..3a3a6b94dc 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1320,7 +1320,7 @@ let project_hint ~poly pri l2r r = in let ctx = Evd.univ_entry ~poly sigma in let c = EConstr.to_constr sigma c in - let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let c = Declare.declare_definition id (c,ctx) in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 8526bdd373..e01f3ab961 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -22,13 +22,18 @@ open Declarations open Constr open CErrors open Util -open Declare open Decl_kinds open Pp (**********************************************************************) (* Registering schemes in the environment *) +(** flag for internal message display *) +type internal_flag = + | UserAutomaticRequest (* kernel action, a message is displayed *) + | InternalTacticRequest (* kernel action, no message is displayed *) + | UserIndividualRequest (* user action, a message is displayed *) + type mutual_scheme_object_function = internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = @@ -131,10 +136,10 @@ let define internal role id c poly univs = proof_entry_inline_code = false; proof_entry_feedback = None; } in - let kn, eff = declare_private_constant ~role ~internal id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in let () = match internal with | InternalTacticRequest -> () - | _-> definition_message id + | _-> Declare.definition_message id in kn, eff diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 109fb64b2b..17e9c7ef42 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -10,7 +10,6 @@ open Names open Constr -open Declare (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) @@ -21,6 +20,11 @@ type mutual type individual type 'a scheme_kind +type internal_flag = + | UserAutomaticRequest + | InternalTacticRequest + | UserIndividualRequest + type mutual_scheme_object_function = internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = diff --git a/tactics/leminv.ml b/tactics/leminv.ml index d8f4b66d0e..e242b10d33 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -25,7 +25,6 @@ open Reductionops open Inductiveops open Tacmach.New open Clenv -open Declare open Tacticals.New open Tactics open Decl_kinds @@ -236,8 +235,8 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in let univs = Evd.univ_entry ~poly sigma in - let entry = definition_entry ~univs invProof in - let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in + let entry = Declare.definition_entry ~univs invProof in + let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in () (* inv_op = Inv (derives de complete inv. lemma) |