Merge PR #10950: [declare] Split universe and inductive declaration code to vernac/

Ack-by: Janno
Reviewed-by: SkySkimmer

2 files changed, 4 insertions, 243 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 7d32f1a7e8..57eeddb847 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -266,6 +266,7 @@ let get_roles export eff =
   List.map map export
 
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
+
 let is_unsafe_typing_flags () =
   let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
@@ -375,132 +376,6 @@ let declare_variable ~name ~kind d =
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
-(** Declaration of inductive blocks *)
-let declare_inductive_argument_scopes kn mie =
-  List.iteri (fun i {mind_entry_consnames=lc} ->
-    Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i));
-    for j=1 to List.length lc do
-      Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j));
-    done) mie.mind_entry_inds
-
-type inductive_obj = {
-  ind_names : (Id.t * Id.t list) list
-  (* For each block, name of the type + name of constructors *)
-}
-
-let inductive_names sp kn obj =
-  let (dp,_) = Libnames.repr_path sp in
-  let kn = Global.mind_of_delta_kn kn in
-  let names, _ =
-    List.fold_left
-      (fun (names, n) (typename, consnames) ->
-         let ind_p = (kn,n) in
-         let names, _ =
-           List.fold_left
-             (fun (names, p) l ->
-                let sp =
-                  Libnames.make_path dp l
-                in
-                  ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1))
-             (names, 1) consnames in
-         let sp = Libnames.make_path dp typename
-         in
-           ((sp, GlobRef.IndRef ind_p) :: names, n+1))
-      ([], 0) obj.ind_names
-  in names
-
-let load_inductive i ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
-
-let open_inductive i ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names
-
-let cache_inductive ((sp, kn), names) =
-  let names = inductive_names sp kn names in
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
-
-let discharge_inductive ((sp, kn), names) =
-  Some names
-
-let inInductive : inductive_obj -> obj =
-  declare_object {(default_object "INDUCTIVE") with
-    cache_function = cache_inductive;
-    load_function = load_inductive;
-    open_function = open_inductive;
-    classify_function = (fun a -> Substitute a);
-    subst_function = ident_subst_function;
-    discharge_function = discharge_inductive;
-  }
-
-let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
-
-let load_prim _ p = cache_prim p
-
-let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c
-
-let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
-
-let inPrim : (Projection.Repr.t * Constant.t) -> obj =
-  declare_object {
-    (default_object "PRIMPROJS") with
-    cache_function = cache_prim ;
-    load_function = load_prim;
-    subst_function = subst_prim;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_prim }
-
-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 name = Label.to_id label in
-  let univs, u = match univs with
-    | Monomorphic_entry _ ->
-      (* Global constraints already defined through the inductive *)
-      default_univ_entry, Univ.Instance.empty
-    | Polymorphic_entry (nas, ctx) ->
-      Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
-  in
-  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 ~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
-
-let declare_projections univs mind =
-  let env = Global.env () in
-  let mib = Environ.lookup_mind mind env in
-  match mib.mind_record with
-  | PrimRecord info ->
-    let iter_ind i (_, labs, _, _) =
-      let ind = (mind, i) in
-      let projs = Inductiveops.compute_projections env ind in
-      Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
-    in
-    let () = Array.iteri iter_ind info in
-    true
-  | FakeRecord -> false
-  | NotRecord -> false
-
-(* for initial declaration *)
-let declare_mind mie =
-  let id = match mie.mind_entry_inds with
-    | ind::_ -> ind.mind_entry_typename
-    | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
-  let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in
-  let names = List.map map_names mie.mind_entry_inds in
-  List.iter (fun (typ, cons) -> check_exists typ; List.iter check_exists cons) names;
-  let _kn' = Global.add_mind id mie in
-  let (sp,kn as oname) = add_leaf id (inInductive { ind_names = names }) in
-  if is_unsafe_typing_flags() then feedback_axiom();
-  let mind = Global.mind_of_delta_kn kn in
-  let isprim = declare_projections mie.mind_entry_universes mind in
-  Impargs.declare_mib_implicits mind;
-  declare_inductive_argument_scopes mind mie;
-  oname, isprim
-
 (* Declaration messages *)
 
 let pr_rank i = pr_nth (i+1)
@@ -538,106 +413,3 @@ 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")
-
-(** Global universes are not substitutive objects but global objects
-   bound at the *library* or *module* level. The polymorphic flag is
-   used to distinguish universes declared in polymorphic sections, which
-   are discharged and do not remain in scope. *)
-
-type universe_source =
-  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
-  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
-  | UnqualifiedUniv (* other global universe *)
-
-type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
-
-let check_exists_universe sp =
-  if Nametab.exists_universe sp then
-    raise (AlreadyDeclared (Some "Universe", Libnames.basename sp))
-  else ()
-
-let qualify_univ i dp src id =
-  match src with
-  | BoundUniv | UnqualifiedUniv ->
-    i,  Libnames.make_path dp id
-  | QualifiedUniv l ->
-    let dp = DirPath.repr dp in
-    Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
-
-let do_univ_name ~check i dp src (id,univ) =
-  let i, sp = qualify_univ i dp src id in
-  if check then check_exists_universe sp;
-  Nametab.push_universe i sp univ
-
-let cache_univ_names ((sp, _), (src, univs)) =
-  let depth = sections_depth () in
-  let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in
-  List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
-
-let load_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs
-
-let open_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs
-
-let discharge_univ_names = function
-  | _, (BoundUniv, _) -> None
-  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
-
-let input_univ_names : universe_name_decl -> Libobject.obj =
-  declare_object
-    { (default_object "Global universe name state") with
-      cache_function = cache_univ_names;
-      load_function = load_univ_names;
-      open_function = open_univ_names;
-      discharge_function = discharge_univ_names;
-      subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
-      classify_function = (fun a -> Substitute a) }
-
-let declare_univ_binders gr pl =
-  if Global.is_polymorphic gr then
-    ()
-  else
-    let l = let open GlobRef in match gr with
-      | ConstRef c -> Label.to_id @@ Constant.label c
-      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
-      | VarRef id ->
-        CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
-      | ConstructRef _ ->
-        CErrors.anomaly ~label:"declare_univ_binders"
-          Pp.(str "declare_univ_binders on an constructor reference")
-    in
-    let univs = Id.Map.fold (fun id univ univs ->
-        match Univ.Level.name univ with
-        | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
-        | Some univ -> (id,univ)::univs) pl []
-    in
-    Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
-
-let do_universe ~poly l =
-  let in_section = Global.sections_are_opened () in
-  let () =
-    if poly && not in_section then
-      CErrors.user_err ~hdr:"Constraint"
-                   (str"Cannot declare polymorphic universes outside sections")
-  in
-  let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
-  let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
-      Univ.LSet.empty l, Univ.Constraint.empty
-  in
-  let src = if poly then BoundUniv else UnqualifiedUniv in
-  let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
-  declare_universe_context ~poly ctx
-
-let do_constraint ~poly l =
-  let open Univ in
-  let u_of_id x =
-    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
-  in
-  let constraints = List.fold_left (fun acc (l, d, r) ->
-      let lu = u_of_id l and ru = u_of_id r in
-      Constraint.add (lu, d, ru) acc)
-      Constraint.empty l
-  in
-  let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  declare_universe_context ~poly uctx
diff --git a/tactics/declare.mli b/tactics/declare.mli
index a6c1374a77..1a037ef937 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -43,6 +43,8 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
+
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
@@ -86,11 +88,6 @@ val declare_private_constant
 val set_declare_scheme :
   (string -> (inductive * Constant.t) array -> unit) -> unit
 
-(** [declare_mind me] declares a block of inductive types with
-   their constructors in the current section; it returns the path of
-   the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
-
 (** Declaration messages *)
 
 val definition_message : Id.t -> unit
@@ -100,15 +97,7 @@ val cofixpoint_message : Id.t list -> unit
 val recursive_message : bool (** true = fixpoint *) ->
   int array option -> Id.t list -> unit
 
-val exists_name : Id.t -> bool
-
-(** Global universe contexts, names and constraints *)
-val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
-
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
-val do_universe : poly:bool -> lident list -> unit
-val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
+val check_exists : Id.t -> unit
 
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)