[declare] Separate kinds from entries in constant declaration

They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.

6 files changed, 55 insertions, 44 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 56f432ee1d..09d7e0278a 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -152,12 +152,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
   let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
-  let decl = (cd, if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition)) 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 decl
+    Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd
   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 6a7f728abc..1e87a4b6ac 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -44,8 +44,6 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
-
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn), obj) =
@@ -235,7 +233,7 @@ let get_roles export eff =
   in
   List.map map export
 
-let define_constant ~side_effect id cd =
+let define_constant ~side_effect ~name cd =
   let open Proof_global in
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let is_poly de = match de.proof_entry_universes with
@@ -270,19 +268,19 @@ let define_constant ~side_effect id cd =
     | PrimitiveEntry e ->
       [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
   in
-  let kn, eff = Global.add_constant ~side_effect ~in_section id decl in
+  let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
   kn, eff, export
 
-let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) =
-  let () = check_exists id in
-  let kn, (), export = define_constant ~side_effect:PureEntry id cd in
+let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+  let () = check_exists name in
+  let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in
   (* Register the libobjects attached to the constants and its subproofs *)
   let () = List.iter register_side_effect export in
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind) =
-  let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd =
+  let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in
   let () = assert (List.is_empty export) in
   let () = register_constant kn kind local in
   let seff_roles = match role with
@@ -294,24 +292,22 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind
 
 let declare_definition
   ?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior)
-  id ?types (body,univs) =
-  let cb =
-    definition_entry ?types ~univs ~opaque body
-  in
-    declare_constant ~local id
-      (DefinitionEntry cb, Decls.IsDefinition kind)
+  ~name ?types (body,univs) =
+  let cb = definition_entry ?types ~univs ~opaque body in
+  declare_constant ~local ~name ~kind:Decls.(IsDefinition kind)
+    (DefinitionEntry cb)
 
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
-type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
+type variable_declaration = DirPath.t * section_variable_entry
 
 let cache_variable ((sp,_),o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(path,d,kind)) ->
+  | Inr (id,(path,d),kind) ->
   (* Constr raisonne sur les noms courts *)
   if Decls.variable_exists id then
     alreadydeclared (Id.print id ++ str " already exists");
@@ -351,13 +347,13 @@ let cache_variable ((sp,_),o) =
   Decls.(add_variable_data id {path;opaque;univs;poly;kind})
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) ->
+  | Inr (id,_,_) ->
     if Decls.variable_polymorphic id then None
     else Some (Inl (Decls.variable_context id))
   | Inl _ -> Some o
 
 type variable_obj =
-    (Univ.ContextSet.t, Id.t * variable_declaration) union
+    (Univ.ContextSet.t, Id.t * variable_declaration * Decls.logical_kind) union
 
 let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
@@ -366,10 +362,10 @@ let inVariable : variable_obj -> obj =
     classify_function = (fun _ -> Dispose) }
 
 (* for initial declaration *)
-let declare_variable id obj =
-  let oname = add_leaf id (inVariable (Inr (id,obj))) in
-  declare_var_implicits id;
-  Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
+let declare_variable ~name ~kind obj =
+  let oname = add_leaf name (inVariable (Inr (name,obj,kind))) in
+  declare_var_implicits name;
+  Notation.declare_ref_arguments_scope Evd.empty (VarRef name);
   oname
 
 (** Declaration of inductive blocks *)
@@ -479,7 +475,7 @@ let inPrim : (Projection.Repr.t * Constant.t) -> obj =
 let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
 
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
-  let id = Label.to_id label in
+  let name = Label.to_id label in
   let univs, u = match univs with
     | Monomorphic_entry _ ->
       (* Global constraints already defined through the inductive *)
@@ -490,7 +486,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let term = Vars.subst_instance_constr u term in
   let types = Vars.subst_instance_constr u types in
   let entry = definition_entry ~types ~univs term in
-  let cst = declare_constant id (DefinitionEntry entry, Decls.(IsDefinition StructureComponent)) in
+  let cst = declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (DefinitionEntry entry) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
   declare_primitive_projection p cst
 
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0fc22f26c4..ae5c93db6a 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -30,15 +30,17 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
+type variable_declaration = DirPath.t * section_variable_entry
 
-val declare_variable : variable -> variable_declaration -> Libobject.object_name
+val declare_variable
+  :  name:variable
+  -> kind:Decls.logical_kind
+  -> variable_declaration
+  -> Libobject.object_name
 
 (** Declaration of global constructions
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
-
 (* Default definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
@@ -53,16 +55,29 @@ 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 :
- ?local:import_status -> Id.t -> constant_declaration -> Constant.t
-
-val declare_private_constant :
-  ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
-
-val declare_definition :
-  ?opaque:bool -> ?kind:Decls.definition_object_kind ->
-  ?local:import_status -> Id.t -> ?types:constr ->
-  constr Entries.in_universes_entry -> Constant.t
+val declare_constant
+  :  ?local:import_status
+  -> name:Id.t
+  -> kind:Decls.logical_kind
+  -> Evd.side_effects constant_entry
+  -> Constant.t
+
+val declare_private_constant
+  :  ?role:Evd.side_effect_role
+  -> ?local:import_status
+  -> name:Id.t
+  -> kind:Decls.logical_kind
+  -> Evd.side_effects constant_entry
+  -> Constant.t * Evd.side_effects
+
+val declare_definition
+  :  ?opaque:bool
+  -> ?kind:Decls.definition_object_kind
+  -> ?local:import_status
+  -> name:Id.t
+  -> ?types:constr
+  -> constr Entries.in_universes_entry
+  -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3a3a6b94dc..90c43a1cb4 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 id (c,ctx) in
+  let c = Declare.declare_definition ~name: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 29963bc105..e2ef05461b 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -135,7 +135,7 @@ let define internal role id c poly univs =
     proof_entry_inline_code = false;
     proof_entry_feedback = None;
   } in
-  let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decls.(IsDefinition Scheme)) in
+  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> Declare.definition_message id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2ef06d2246..2af3947dd1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -235,7 +235,7 @@ 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 = Declare.definition_entry ~univs invProof in
-  let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, Decls.(IsProof Lemma)) in
+  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
   ()
 
 (* inv_op = Inv (derives de complete inv. lemma)