Merge PR #8434: Canonical representation of kernel substitutions

5 files changed, 38 insertions, 75 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 17259bb438..4162903b04 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -132,7 +132,7 @@ type delta_hint =
 
 type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t
 
-type 'a umap_t = 'a MPmap.t * 'a MBImap.t
+type 'a umap_t = 'a MPmap.t
 type substitution = (ModPath.t * delta_resolver) umap_t
 
 (** {6 Delayed constr} *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 0540227ccb..03fee1ab51 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -28,18 +28,13 @@ let empty_delta_resolver = Deltamap.empty
 module Umap = struct
   [@@@ocaml.warning "-32-34"]
   type 'a t = 'a umap_t
-  let empty = MPmap.empty, MBImap.empty
-  let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
-  let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
-  let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
-  let find_mp mp map = MPmap.find mp (fst map)
-  let find_mbi mbi map = MBImap.find mbi (snd map)
-  let mem_mp mp map = MPmap.mem mp (fst map)
-  let mem_mbi mbi map = MBImap.mem mbi (snd map)
-  let iter_mbi f map = MBImap.iter f (snd map)
-  let fold fmp fmbi (m1,m2) i =
-    MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
-  let join map1 map2 = fold add_mp add_mbi map1 map2
+  let empty = MPmap.empty
+  let is_empty m = MPmap.is_empty m
+  let add_mbi mbi x m = MPmap.add (MPbound mbi) x m
+  let add_mp mp x m = MPmap.add mp x m
+  let find = MPmap.find
+  let fold = MPmap.fold
+  let join map1 map2 = fold add_mp map1 map2
 end
 
 type 'a subst_fun = substitution -> 'a -> 'a
@@ -117,15 +112,10 @@ let constant_of_delta_with_inline resolve con =
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPfile sid -> Umap.find_mp mp sub
-    | MPbound bid ->
-	begin
-	  try Umap.find_mbi bid sub
-	  with Not_found -> Umap.find_mp mp sub
-	end
+    | MPfile _ | MPbound _ -> Umap.find mp sub
     | MPdot (mp1,l) as mp2 ->
 	begin
-	  try Umap.find_mp mp2 sub
+          try Umap.find mp2 sub
 	  with Not_found ->
 	    let mp1',resolve = aux mp1 in
 	    MPdot (mp1',l),resolve
@@ -382,9 +372,7 @@ let substition_prefixed_by k mp subst =
       Umap.add_mp new_key (mp_to,reso) sub
     else sub
   in
-  let mbi_prefixmp mbi _ sub = sub
-  in
-  Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst
+  Umap.fold mp_prefixmp subst empty_subst
 
 let join subst1 subst2 =
   let apply_subst mpk add (mp,resolve) res =
@@ -404,8 +392,7 @@ let join subst1 subst2 =
     Umap.join prefixed_subst (add (mp',resolve'') res)
   in
   let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in
-  let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in
-  let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
+  let subst = Umap.fold mp_apply_subst subst1 empty_subst in
   Umap.join subst2 subst
 
 let from_val x = { subst_value = x; subst_subst = []; }
diff --git a/checker/values.ml b/checker/values.ml
index e1b5a949ac..801874773a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli
+MD5 a127e0c2322c7846914bbca9921309c7 checker/cic.mli
 
 *)
 
@@ -185,10 +185,7 @@ let v_resolver =
 let v_mp_resolver = v_tuple "" [|v_mp;v_resolver|]
 
 let v_subst =
-  v_tuple "substitution"
-    [|v_map v_mp v_mp_resolver;
-      v_map v_uid v_mp_resolver|]
-
+  Annot ("substitution", v_map v_mp v_mp_resolver)
 
 (** kernel/lazyconstr *)
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index b35b9dda31..f1d08ef6dd 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -53,18 +53,25 @@ type delta_resolver = Deltamap.t
 
 let empty_delta_resolver = Deltamap.empty
 
-module Umap = struct
-  type 'a t = 'a MPmap.t * 'a MBImap.t
-  let empty = MPmap.empty, MBImap.empty
-  let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2
-  let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2)
-  let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
-  let find_mp mp map = MPmap.find mp (fst map)
-  let find_mbi mbi map = MBImap.find mbi (snd map)
-  let iter_mbi f map = MBImap.iter f (snd map)
-  let fold fmp fmbi (m1,m2) i =
-    MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
-  let join map1 map2 = fold add_mp add_mbi map1 map2
+module Umap :
+  sig
+    type 'a t
+    val empty : 'a t
+    val is_empty : 'a t -> bool
+    val add_mbi : MBId.t -> 'a -> 'a t -> 'a t
+    val add_mp : ModPath.t -> 'a -> 'a t -> 'a t
+    val find : ModPath.t -> 'a t -> 'a
+    val join : 'a t -> 'a t -> 'a t
+    val fold : (ModPath.t -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  end = struct
+  type 'a t = 'a MPmap.t
+  let empty = MPmap.empty
+  let is_empty m = MPmap.is_empty m
+  let add_mbi mbi x m = MPmap.add (MPbound mbi) x m
+  let add_mp mp x m = MPmap.add mp x m
+  let find = MPmap.find
+  let fold = MPmap.fold
+  let join map1 map2 = fold add_mp map1 map2
 end
 
 type substitution = (ModPath.t * delta_resolver) Umap.t
@@ -93,8 +100,7 @@ let debug_string_of_delta resolve =
 let list_contents sub =
   let one_pair (mp,reso) = (ModPath.to_string mp,debug_string_of_delta reso) in
   let mp_one_pair mp0 p l = (ModPath.to_string mp0, one_pair p)::l in
-  let mbi_one_pair mbi p l = (MBId.debug_to_string mbi, one_pair p)::l in
-  Umap.fold mp_one_pair mbi_one_pair sub []
+  Umap.fold mp_one_pair sub []
 
 let debug_string_of_subst sub =
   let l = List.map (fun (s1,(s2,s3)) -> s1^"|->"^s2^"["^s3^"]")
@@ -222,15 +228,10 @@ let search_delta_inline resolve kn1 kn2 =
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPfile sid -> Umap.find_mp mp sub
-    | MPbound bid ->
-	begin
-	  try Umap.find_mbi bid sub
-	  with Not_found -> Umap.find_mp mp sub
-	end
+    | MPfile _ | MPbound _ -> Umap.find mp sub
     | MPdot (mp1,l) as mp2 ->
 	begin
-	  try Umap.find_mp mp2 sub
+          try Umap.find mp2 sub
 	  with Not_found ->
 	    let mp1',resolve = aux mp1 in
 	    MPdot (mp1',l),resolve
@@ -525,9 +526,7 @@ let substition_prefixed_by k mp subst =
       Umap.add_mp new_key (mp_to,reso) sub
     else sub
   in
-  let mbi_prefixmp mbi _ sub = sub
-  in
-  Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst
+  Umap.fold mp_prefixmp subst empty_subst
 
 let join subst1 subst2 =
   let apply_subst mpk add (mp,resolve) res =
@@ -547,24 +546,9 @@ let join subst1 subst2 =
     Umap.join prefixed_subst (add (mp',resolve'') res)
   in
   let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in
-  let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in
-  let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
+  let subst = Umap.fold mp_apply_subst subst1 empty_subst in
   Umap.join subst2 subst
 
-let rec occur_in_path mbi = function
-  | MPbound bid' -> MBId.equal mbi bid'
-  | MPdot (mp1,_) -> occur_in_path mbi mp1
-  | _ -> false
-
-let occur_mbid mbi sub =
-  let check_one mbi' (mp,_) =
-    if MBId.equal mbi mbi' || occur_in_path mbi mp then raise Exit
-  in
-  try
-    Umap.iter_mbi check_one sub;
-    false
-  with Exit -> true
-
 type 'a substituted = {
   mutable subst_value : 'a;
   mutable subst_subst : substitution list;
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 2e5211c770..8416094063 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -165,11 +165,6 @@ val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
    names appearing in [c] *)
 val subst_mps : substitution -> constr -> constr
 
-(** [occur_*id id sub] returns true iff [id] occurs in [sub]
-   on either side *)
-
-val occur_mbid : MBId.t -> substitution -> bool
-
 (** [repr_substituted r] dumps the representation of a substituted:
     - [None, a] when r is a value
     - [Some s, a] when r is a delayed substitution [s] applied to [a] *)