Statically separate the three kinds of δ-resolvers.

Except for the broken upper layers, there were actually three distinct
kinds of δ-resolvers.

1. Resolvers from module bodies without any inlining information, as
it makes no sense there.
2. Resolvers from module types, which may carry inlining parameter
information, i.e. an inlining level for some constants.
3. Resolvers from module substitutions, which may carry actual inlining
payload as terms attached to some constant to replace them.

The upper layers used to gladly break these invariants to carry both the
aliasing and inlining information through the same channel, but this was
fixed in the last commit.

This commit annotates the type of δ-resolvers to statically separate the
various kinds in the code.

Author: ppedrot

checker/mod_checking.ml

@@ -267,7 +267,9 @@ let rec check_mexpr env mse mp_mse res = match mse with
       | NoFunctor _ -> mod_delta mb
       | MoreFunctor _ -> Mod_subst.empty_delta_resolver mp
     in
-    let subst = Mod_subst.map_mbid farg_id mp mp_delta in
+    let subst =
+      Mod_subst.map_mbid farg_id mp (Mod_subst.of_body_delta_resolver mp_delta)
+    in
     Modops.subst_signature subst mp_mse fbody_b, Mod_subst.subst_codom_delta_resolver subst delta
   | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
@@ -279,7 +281,7 @@ let rec check_mexpression env sign mbtyp mp_mse res = match sign with
     MoreFunctor(arg_id,mtb,body), delta
   | MENoFunctor me -> check_mexpr env me mp_mse res
 
-let rec check_module env opac mp mb opacify =
+let rec check_module env opac mp (mb : Mod_declarations.module_body) opacify =
   Flags.if_verbose Feedback.msg_notice (str "  checking module: " ++ str (ModPath.to_string mp));
   let delta_mb = mod_delta mb in
   let opac =
@@ -298,22 +300,23 @@ let rec check_module env opac mp mb opacify =
   let () = match optsign with
   | None -> ()
   | Some (sign,delta) ->
-    let mtb1 = mk_mtb sign delta
-    and mtb2 = mk_mtb (mod_type mb) delta_mb in
+    let mtb1 = mk_mtb sign (Mod_subst.of_body_delta_resolver delta)
+    and mtb2 = mk_mtb (mod_type mb) (Mod_subst.of_body_delta_resolver delta_mb) in
     let state = (Environ.universes env, Conversion.checked_universes) in
     let env = Modops.add_module mp (module_body_of_type mtb1) env in
     let _ : UGraph.t = Subtyping.check_subtypes state env mp mp mtb2 in
     ()
   in
   opac
 
-and check_module_type env mp mty =
+and check_module_type env mp (mty : Mod_declarations.module_type_body) =
   Flags.if_verbose Feedback.msg_notice (str "  checking module type: " ++ str (ModPath.to_string @@ mp));
   let _ : check_state =
     check_signature env empty_state (mod_type mty) mp (mod_delta mty) empty_cset in
   ()
 
-and check_structure_field env opac mp lab res opacify = function
+and check_structure_field : type a. _ -> _ -> _ -> _ -> a Mod_subst.delta_resolver -> _ -> _ -> _ =
+  fun env opac mp lab res opacify -> function
   | SFBconst cb ->
       let kn = KerName.make mp lab in
       let kn = Mod_subst.constant_of_delta_kn res kn in
@@ -342,7 +345,8 @@ and check_structure_field env opac mp lab res opacify = function
       check_rewrite_rules_body env lab rrb;
       Environ.add_rewrite_rules rrb.rewrules_rules env, opac
 
-and check_signature env opac sign mp_mse res opacify = match sign with
+and check_signature : type a. _ -> _ -> _ -> _ -> a Mod_subst.delta_resolver -> _ -> _ =
+  fun env opac sign mp_mse res opacify -> match sign with
   | MoreFunctor (arg_id, mtb, body) ->
       let () = check_module_type env (MPbound arg_id) mtb in
       let env' = Modops.add_module_parameter arg_id mtb env in

checker/values.ml

@@ -297,16 +297,35 @@ let v_section_ctxt = v_enum "emptylist" 1
 
 let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|]
 
-let v_delta_hint =
-  v_sum "delta_hint" 0 [|[|v_int; v_opt (v_univ_abstracted v_constr)|];[|v_kn|]|]
+let v_modbody_delta_hint =
+  v_sum "delta_hint" 0
+    [|[|v_kn|]; [|v_fail "inline"|]; [|v_fail "inline"|]|]
 
-let v_resolver =
+let v_modtype_delta_hint =
+  v_sum "delta_hint" 0
+    [|[|v_kn|]; [|v_int|]; [|v_fail "inline"|]|]
+
+let v_modsubs_delta_hint =
+  v_sum "delta_hint" 0
+    [|[|v_kn|]; [|v_fail "inline"|]; [|v_univ_abstracted v_constr|]|]
+
+let v_modbody_resolver =
+  v_tuple "delta_resolver"
+    [|v_mp; v_map v_mp v_mp;
+      v_hmap v_kn v_modbody_delta_hint|]
+
+let v_modtype_resolver =
+  v_tuple "delta_resolver"
+    [|v_mp; v_map v_mp v_mp;
+      v_hmap v_kn v_modtype_delta_hint|]
+
+let v_modsubs_resolver =
   v_tuple "delta_resolver"
     [|v_mp; v_map v_mp v_mp;
-      v_hmap v_kn v_delta_hint|]
+      v_hmap v_kn v_modsubs_delta_hint|]
 
 let v_subst =
-  v_annot_c ("substitution", v_map v_mp v_resolver)
+  v_annot_c ("substitution", v_map v_mp v_modsubs_resolver)
 
 (** kernel/lazyconstr *)
 
@@ -586,13 +605,13 @@ let [_v_sfb;_v_struc;_v_sign;_v_mexpr;_v_impl;v_module;_v_modtype] : _ Vector.t
   and v_impl =
     v_sum_c ("module_impl",2, (* Abstract, FullStruct *)
          [|[|v_mexpr|];  (* Algebraic *)
-           [|v_resolver; v_struc|]|])  (* Struct *)
+           [|v_modbody_resolver; v_struc|]|])  (* Struct *)
   and v_module =
     v_tuple_c ("module_body",
-           [|v_sum_c ("when_mod_body", 0, [|[|v_impl|]|]);v_sign;v_opt v_mexpr;v_resolver|])
+           [|v_sum_c ("when_mod_body", 0, [|[|v_impl|]|]);v_sign;v_opt v_mexpr;v_modbody_resolver|])
   and v_modtype =
     v_tuple_c ("module_type_body",
-           [|v_noimpl;v_sign;v_opt v_mexpr;v_resolver|])
+           [|v_noimpl;v_sign;v_opt v_mexpr;v_modtype_resolver|])
   in
   [v_sfb;v_struc;v_sign;v_mexpr;v_impl;v_module;v_modtype])
 

dev/top_printers.mli

@@ -119,7 +119,7 @@ val genppj : ('a -> Pp.t * Pp.t) -> 'a -> Pp.t
 val ppj : EConstr.unsafe_judgment -> unit
 
 val ppsubst : Mod_subst.substitution -> unit
-val ppdelta : Mod_subst.delta_resolver -> unit
+val ppdelta : 'a Mod_subst.delta_resolver -> unit
 
 val pp_idpred : Names.Id.Pred.t -> unit
 val pp_cpred : Names.Cpred.t -> unit

kernel/environ.ml

@@ -1346,7 +1346,8 @@ module Internal = struct
     let new_mods = ModPath.Map.add mp mb env.env_modules in
     { env with env_modules = new_mods }
 
-  let rec overwrite_structure mp sign resolver env =
+  let rec overwrite_structure : type a. _ -> _ -> a Mod_subst.delta_resolver -> _ -> _ =
+    fun mp sign resolver env ->
     let add_field env (l,elem) = match elem with
       | SFBconst cb ->
         let c = Mod_subst.constant_of_delta_kn resolver (KerName.make mp l) in

kernel/environ.mli

@@ -556,7 +556,7 @@ module Internal : sig
   val overwrite_module_parameter : MBId.t -> module_type_body -> env -> env
   (** Overwriting variant of Modops.add_module_parameter, see above. *)
 
-  val overwrite_structure : ModPath.t -> structure_body -> Mod_subst.delta_resolver -> env -> env
+  val overwrite_structure : ModPath.t -> structure_body -> 'a Mod_subst.delta_resolver -> env -> env
   (** Overwriting variant of Modops.add_structure, see above. *)
 
 end

kernel/mod_declarations.ml

@@ -31,14 +31,14 @@ and module_signature = (module_type_body,structure_body) functorize
 and module_implementation =
   | Abstract (** no accessible implementation *)
   | Algebraic of module_expression (** non-interactive algebraic expression *)
-  | Struct of delta_resolver * structure_body (** interactive body living in the parameter context of [mod_type] *)
+  | Struct of mod_body delta_resolver * structure_body (** interactive body living in the parameter context of [mod_type] *)
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 and 'a generic_module_body =
   { mod_expr : ('a, module_implementation) when_mod_body; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     mod_type_alg : module_expression option; (** algebraic type *)
-    mod_delta : Mod_subst.delta_resolver; (**
+    mod_delta : 'a Mod_subst.delta_resolver; (**
       quotiented set of equivalent constants and inductive names *) }
 
 (** For a module, there are five possible situations:
@@ -104,11 +104,22 @@ let replace_module_body struc delta mb =
     mod_type_alg = None;
     mod_delta = delta }
 
-let module_type_of_module mb =
-  { mb with mod_expr = ModTypeNul; mod_type_alg = None; }
+let module_type_of_module mb = {
+  mod_expr = ModTypeNul;
+  mod_type = mb.mod_type;
+  mod_type_alg = None;
+  mod_delta = of_body_delta_resolver mb.mod_delta;
+}
 
-let module_body_of_type mtb =
-  { mtb with mod_expr = ModBodyVal Abstract; }
+let module_body_of_type mtb = {
+  mod_expr = ModBodyVal Abstract;
+  mod_type = mtb.mod_type;
+  mod_type_alg = mtb.mod_type_alg;
+  (* The inlining declarations of [mtb] are not inherited: they are a property
+     of the module type, and a module implementing it does not declare
+     anything. *)
+  mod_delta = forget_inline_delta_resolver mtb.mod_delta;
+}
 
 (** Setters *)
 
@@ -118,7 +129,7 @@ let set_implementation e mb =
 let set_algebraic_type mb alg =
   { mb with mod_type_alg = Some alg }
 
-let set_delta : type a. delta_resolver -> a generic_module_body -> a generic_module_body =
+let set_delta : type a. a delta_resolver -> a generic_module_body -> a generic_module_body =
   fun delta mb -> { mb with mod_delta = delta }
 
 (** Accessors *)

kernel/mod_declarations.mli

@@ -42,7 +42,7 @@ type module_signature = (module_type_body,structure_body) functorize
 type module_implementation =
   | Abstract (** no accessible implementation *)
   | Algebraic of module_expression (** non-interactive algebraic expression *)
-  | Struct of delta_resolver * structure_body (** interactive body living in the parameter context of [mod_type] *)
+  | Struct of mod_body delta_resolver * structure_body (** interactive body living in the parameter context of [mod_type] *)
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 (** Extra invariants :
@@ -60,23 +60,23 @@ type module_implementation =
 val mod_expr : module_body -> module_implementation
 val mod_type : 'a generic_module_body -> module_signature
 val mod_type_alg : 'a generic_module_body -> module_expression option
-val mod_delta : 'a generic_module_body -> delta_resolver
+val mod_delta : 'a generic_module_body -> 'a delta_resolver
 
-val mod_global_delta : 'a generic_module_body -> delta_resolver option
+val mod_global_delta : 'a generic_module_body -> 'a delta_resolver option
 (** [None] if the argument is a functor, [mod_delta] otherwise *)
 
 (** {6 Builders} *)
 
-val make_module_body : module_signature -> Mod_subst.delta_resolver -> module_body
-val make_module_type : module_signature -> Mod_subst.delta_resolver -> module_type_body
+val make_module_body : module_signature -> Mod_subst.mod_body Mod_subst.delta_resolver -> module_body
+val make_module_type : module_signature -> Mod_subst.mod_type Mod_subst.delta_resolver -> module_type_body
 
 val strengthen_module_body : src:ModPath.t ->
-  module_signature -> delta_resolver -> module_body -> module_body
+  module_signature -> mod_body delta_resolver -> module_body -> module_body
 
 val strengthen_module_type :
-  structure_body -> delta_resolver -> module_type_body -> module_type_body
+  structure_body -> mod_type delta_resolver -> module_type_body -> module_type_body
 
-val replace_module_body : structure_body -> delta_resolver -> module_body -> module_body
+val replace_module_body : structure_body -> mod_body delta_resolver -> module_body -> module_body
 
 val module_type_of_module : module_body -> module_type_body
 val module_body_of_type : module_type_body -> module_body
@@ -89,7 +89,7 @@ val functorize_module : (Names.MBId.t * module_type_body) list -> module_body ->
 
 val set_implementation : module_implementation -> module_body -> module_body
 val set_algebraic_type : module_type_body -> module_expression -> module_type_body
-val set_delta : Mod_subst.delta_resolver -> 'a generic_module_body -> 'a generic_module_body
+val set_delta : 'a Mod_subst.delta_resolver -> 'a generic_module_body -> 'a generic_module_body
 
 (** {6 Substitution} *)