Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 39 insertions, 35 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index c141a02a..08ee67b4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -32,15 +32,18 @@ type namedobject =
   | Constant of constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
   | Module of module_body
   | Modtype of module_type_body
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
 
-let add_nameobjects_of_mib ln mib map =
-  let add_nameobjects_of_one j oib map =
-    let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+  let ind = make_mind mp empty_dirpath l in
+  let add_mip_nameobjects j oib map =
+    let ip = (ind,j) in
     let map =
       array_fold_right_i
       (fun i id map ->
@@ -50,22 +53,33 @@ let add_nameobjects_of_mib ln mib map =
     in
       Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
   in
-    array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+  array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
+
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
 
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
 
-(* creates namedobject map for the whole signature *)
+let get_obj mp map l =
+  try Labmap.find l map.objs
+  with Not_found -> error_no_such_label_sub l (string_of_mp mp)
 
-let make_label_map mp list =
+let get_mod mp map l =
+  try Labmap.find l map.mods
+  with Not_found -> error_no_such_label_sub l (string_of_mp mp)
+
+let make_labmap mp list =
   let add_one (l,e) map =
-   let add_map obj = Labmap.add l obj map in
    match e with
-    | SFBconst cb -> add_map (Constant cb)
-    | SFBmind mib ->
-       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
-    | SFBmodule mb -> add_map (Module mb)
-    | SFBmodtype mtb -> add_map (Modtype mtb)
+    | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+    | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+    | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+    | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
   in
-    List.fold_right add_one list Labmap.empty
+  List.fold_right add_one list empty_labmap
+
 
 let check_conv_error error why cst f env a1 a2 =
   try
@@ -299,7 +313,6 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv NotConvertibleTypeField cst conv env ty1 ty2
-   | _ -> error DefinitionFieldExpected
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
@@ -308,33 +321,24 @@ let rec check_modules cst env msb1 msb2 subst1 subst2 =
     cst
 
 and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
-  let map1 = make_label_map mp1 sig1 in
+  let map1 = make_labmap mp1 sig1 in
   let check_one_body cst (l,spec2) =
-    let info1 =
-      try
-	Labmap.find l map1
-      with
-	  Not_found -> error_no_such_label_sub l
-	    (string_of_mp mp1)
-    in
-      match spec2 with
+    match spec2 with
 	| SFBconst cb2 ->
-	    check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
+	    check_constant cst env mp1 l (get_obj mp1 map1 l)
+	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
-	    check_inductive cst env
-	      mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
+	    check_inductive cst env mp1 l (get_obj mp1 map1 l)
+	      mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	| SFBmodule msb2 ->
-	    begin
-	      match info1 with
-		| Module msb -> check_modules cst env msb msb2 
-		    subst1 subst2
-		| _ -> error_signature_mismatch l spec2 ModuleFieldExpected
+	    begin match get_mod mp1 map1 l with
+	      | Module msb -> check_modules cst env msb msb2 subst1 subst2
+	      | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
 	    end
 	| SFBmodtype mtb2 ->
-	    let mtb1 =
-	      match info1 with
-		| Modtype mtb -> mtb
-		| _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
+	    let mtb1 = match get_mod mp1 map1 l with
+	      | Modtype mtb -> mtb
+	      | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
 	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
 	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in