Discharge on the fly in the kernel

interp/impargs.ml

@@ -570,19 +570,24 @@ let add_section_impls vars extra_impls (cond,impls) =
   let p = List.length vars - List.length extra_impls in
   adjust_side_condition p cond, extra_impls @ List.map (Option.map (lift_implicits p)) impls
 
+let discharge_request = function
+  | ImplMutualInductive (mind,flags) -> ImplMutualInductive (Lib.discharge_mind mind, flags)
+  | ImplInteractive _ | ImplConstant _ | ImplLocal as req -> req
+
 let discharge_implicits (req,l) =
   match req with
   | ImplLocal -> None
   | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ ->
      let l' =
-       try
-         List.map (fun (gr, l) ->
-             let vars = Array.map_to_list Constr.destVar (Lib.section_instance gr) in
+       List.map (fun (gr, l) ->
+           match Lib.discharge_global_reference_with_instance gr with
+           | Some (gr,inst) ->
+             let vars = Array.map_to_list Constr.destVar inst in
              let extra_impls = impls_of_context vars in
              let newimpls = List.map (add_section_impls vars extra_impls) l in
-             (gr, newimpls)) l
-       with Not_found -> l in
-     Some (req,l')
+             (gr, newimpls)
+           | None -> assert false (* Would be ImplLocal *)) l in
+     Some (discharge_request req,l')
 
 let rebuild_implicits (req,l) =
   match req with
@@ -591,8 +596,8 @@ let rebuild_implicits (req,l) =
       let ref,oldimpls = List.hd l in
       let newimpls = compute_global_implicits flags ref in
       req, [ref, List.map2 merge_impls oldimpls newimpls]
-  | ImplMutualInductive (kn,flags) ->
-      let newimpls = compute_all_mib_implicits flags kn in
+  | ImplMutualInductive (mind,flags) ->
+      let newimpls = compute_all_mib_implicits flags mind in
       let rec aux olds news =
        match olds, news with
        | (_, oldimpls) :: old, (gr, newimpls) :: tl ->

interp/notation.ml

@@ -1911,13 +1911,12 @@ let discharge_available_scopes map =
       if List.is_empty ltop && List.is_empty lbot then None else Some (ltop, lbot)) map
 
 let discharge_arguments_scope (req,r,scs,_cls,available_scopes) =
-  if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
+  if req == ArgsScopeNoDischarge then None
   else
-    let n =
-      try
-        Array.length (Lib.section_instance r)
-      with
-        Not_found (* Not a ref defined in this section *) -> 0 in
+    match Lib.discharge_global_reference_with_instance r with
+    | None -> None
+    | Some (r, inst) ->
+    let n = Array.length inst in
     let available_scopes = discharge_available_scopes available_scopes in
     (* Hack: use list cls to encode an integer to pass to rebuild for Manual case *)
     (* since cls is anyway recomputed in rebuild *)

kernel/cooking.ml

@@ -125,11 +125,19 @@ type cooking_cache = {
   rel_ctx : rel_context Lazy.t;
 }
 
+let discharge_mind {info = {expand_info = (_csttab, mindtab);_};_} mind =
+  if Mindmap.mem mind mindtab then MutInd.pop mind else mind
+
+let discharge_inductive cache (mind,i) = (discharge_mind cache mind, i)
+
+let discharge_constant {info = {expand_info = (csttab, _mindtab);_};_} cst =
+  if Cmap.mem cst csttab then Constant.pop cst else cst
+
 let instantiate_my_gr gr u =
   match gr with
-  | ConstRef c -> mkConstU (c, u)
-  | IndRef i -> mkIndU (i, u)
-  | ConstructRef c -> mkConstructU (c, u)
+  | ConstRef c -> mkConstU (Constant.pop c, u)
+  | IndRef i -> mkIndU (Ind.pop i, u)
+  | ConstructRef c -> mkConstructU (Construct.pop c, u)
 
 let discharge_inst top_abst_subst sub_abst_rev_inst =
   let rec aux k relargs top_abst_subst sub_abst_rev_inst =
@@ -172,11 +180,11 @@ let share_univs cache top_abst_subst k r u l =
 let discharge_proj_repr r p = (* To merge with discharge_proj *)
   let nnewpars = List.count NamedDecl.is_local_assum r.abstr_info.abstr_ctx in
   let map npars = npars + nnewpars in
-  Projection.Repr.map_npars map p
+  Projection.Repr.map_npars map (Projection.Repr.pop p)
 
 let discharge_proj (_,_,abstr_inst_length) p =
   let map npars = npars + abstr_inst_length in
-  Projection.map_npars map p
+  Projection.map_npars map (Projection.pop p)
 
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
@@ -190,7 +198,7 @@ let expand_constr cache modlist top_abst_subst c =
         | (abstr_uinst, abstr_inst_rel, abstr_inst_length) ->
           let u = Instance.append abstr_uinst u in
           let pms = Array.append (make_inst k abstr_inst_rel) pms in
-          let ci = { ci with ci_npar = ci.ci_npar + abstr_inst_length } in
+          let ci = { ci with ci_npar = ci.ci_npar + abstr_inst_length; ci_ind = Ind.pop ci.ci_ind } in
           Constr.map_with_binders succ substrec k (mkCase (ci,u,pms,p,iv,t,br))
         | exception Not_found ->
           Constr.map_with_binders succ substrec k c

kernel/cooking.mli

@@ -58,6 +58,9 @@ val create_cache : cooking_info -> cooking_cache
 val instance_of_cooking_cache : cooking_cache -> Constr.t array
 val rel_context_of_cooking_cache : cooking_cache -> rel_context
 
+val discharge_inductive : cooking_cache -> Ind.t -> Ind.t
+val discharge_constant : cooking_cache -> Constant.t -> Constant.t
+
 val abstract_as_type : cooking_cache -> types -> types
 
 val abstract_as_body : cooking_cache -> constr -> constr

kernel/discharge.ml

@@ -111,6 +111,15 @@ let cook_projection cache ~params t =
   let _, t = decompose_prod_n_decls (Context.Rel.length params + 1 + nrels) t in
   t
 
+let cook_nested_type cache = function
+  | NestedInd ind -> NestedInd (Cooking.discharge_inductive cache ind)
+  | NestedPrimitive cst -> NestedPrimitive (Cooking.discharge_constant cache cst)
+
+let cook_recargs cache = function
+  | Mrec ind -> Mrec (Ind.pop ind)
+  | Norec -> Norec
+  | Nested t -> Nested (cook_nested_type cache t)
+
 let cook_one_ind cache ~ntypes mip =
   let mind_arity = match mip.mind_arity with
     | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
@@ -139,7 +148,7 @@ let cook_one_ind cache ~ntypes mip =
     mind_nf_lc;
     mind_consnrealargs = mip.mind_consnrealargs;
     mind_consnrealdecls = mip.mind_consnrealdecls;
-    mind_recargs = mip.mind_recargs;
+    mind_recargs = Rtree.Smart.map (cook_recargs cache) mip.mind_recargs;
     mind_relevance = mip.mind_relevance;
     mind_nb_constant = mip.mind_nb_constant;
     mind_nb_args = mip.mind_nb_args;

kernel/names.ml

@@ -381,6 +381,12 @@ module KerName = struct
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
 
+  let pop kn =
+    let mp = match kn.modpath with
+    | ModPath.MPdot (mp,_) -> mp
+    | _ -> CErrors.anomaly (str "No field to pop.") in
+    make mp kn.knlabel
+
   let to_string_gen mp_to_string kn =
     mp_to_string kn.modpath ^ "." ^ Label.to_string kn.knlabel
 
@@ -514,6 +520,10 @@ module KerPair = struct
       if mp1 == mp2 then same kn
       else make kn (KerName.make mp2 lbl)
 
+  let pop = function
+    | Same kn -> Same (KerName.pop kn)
+    | Dual (knu,knc) -> Dual (KerName.pop knu, KerName.pop knc)
+
   let to_string kp = KerName.to_string (user kp)
   let print kp = str (to_string kp)
 
@@ -625,6 +635,8 @@ struct
                                     BEWARE: indexing starts from 0. *)
   let modpath (mind, _) = MutInd.modpath mind
 
+  let pop (mind,i) = (MutInd.pop mind, i)
+
   module CanOrd =
   struct
     type nonrec t = t
@@ -673,6 +685,8 @@ struct
 
   let modpath (ind, _) = Ind.modpath ind
 
+  let pop (ind,i) = (Ind.pop ind, i)
+
   module CanOrd =
   struct
     type nonrec t = t
@@ -853,6 +867,8 @@ struct
 
     let relevant c = c.proj_relevant
 
+    let pop p = { p with proj_ind = Ind.pop p.proj_ind }
+
     let hash p =
       Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
 
@@ -960,6 +976,7 @@ struct
   let repr = fst
   let unfolded = snd
   let unfold (c, b as p) = if b then p else (c, true)
+  let pop (p,b) = (Repr.pop p, b)
 
   let equal (c, b) (c', b') = Repr.equal c c' && b == b'
 

kernel/names.mli

@@ -291,6 +291,9 @@ sig
   val modpath : t -> ModPath.t
   val label : t -> Label.t
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   val to_string : t -> string
   (** Encode as a string (not to be used for user-facing messages). *)
 
@@ -395,6 +398,9 @@ sig
   val label : t -> Label.t
   (** Shortcut for [KerName.label (user ...)] *)
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   (** Comparisons *)
 
   include QNameS with type t := t
@@ -466,6 +472,9 @@ sig
   val label : t -> Label.t
   (** Shortcut for [KerName.label (user ...)] *)
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   (** Comparisons *)
 
   include QNameS with type t := t
@@ -504,6 +513,9 @@ sig
                                     BEWARE: indexing starts from 0. *)
   val modpath : t -> ModPath.t
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   include QNameS with type t := t
 
 end
@@ -519,6 +531,9 @@ sig
 
   val modpath : t -> ModPath.t
 
+  (** Remove the last modpath segment *)
+  val pop : t -> t
+
   include QNameS with type t := t
 
 end
@@ -632,6 +647,7 @@ module Projection : sig
     val arg : t -> int
     val label : t -> Label.t
     val relevant : t -> bool
+    val pop : t -> t
 
     val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"]
     val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"]
@@ -662,6 +678,7 @@ module Projection : sig
   val label : t -> Label.t
   val unfolded : t -> bool
   val unfold : t -> t
+  val pop : t -> t
 
   val equal : t -> t -> bool
   [@@ocaml.deprecated "Use QProjection.equal"]