Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 137 insertions, 149 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 98ee1dbb..e07af3ba 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 11453 2008-10-15 14:42:34Z soubiran $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Util
@@ -27,22 +27,21 @@ open Entries
 (* This local type is used to subtype a constant with a constructor or
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
-type namedobject = 
+type namedobject =
   | Constant of constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_body
   | Modtype of module_type_body
-  | Alias of module_path * struct_expr_body option
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
 
-let add_nameobjects_of_mib ln mib map = 
+let add_nameobjects_of_mib ln mib map =
   let add_nameobjects_of_one j oib map =
     let ip = (ln,j) in
-    let map = 
-      array_fold_right_i 
+    let map =
+      array_fold_right_i
       (fun i id map ->
         Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
       oib.mind_consnames
@@ -55,16 +54,15 @@ let add_nameobjects_of_mib ln mib map =
 
 (* creates namedobject map for the whole signature *)
 
-let make_label_map mp list = 
-  let add_one (l,e) map = 
+let make_label_map 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_kn mp empty_dirpath l) mib map
+       add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
     | SFBmodule mb -> add_map (Module mb)
     | SFBmodtype mtb -> add_map (Modtype mtb)
-    | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt))
   in
     List.fold_right add_one list Labmap.empty
 
@@ -75,20 +73,23 @@ let check_conv_error error cst f env a1 a2 =
       NotConvertible -> error ()
 
 (* for now we do not allow reorderings *)
-let check_inductive cst env msid1 l info1 mib2 spec2 = 
-  let kn = make_kn (MPself msid1) empty_dirpath l in
+
+let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
+  let kn1 = make_mind mp1 empty_dirpath l in
+  let kn2 = make_mind mp2 empty_dirpath l in
   let error () = error_not_match l spec2 in
   let check_conv cst f = check_conv_error error cst f in
-  let mib1 = 
+  let mib1 =
     match info1 with
-      | IndType ((_,0), mib) -> mib
+      | IndType ((_,0), mib) -> subst_mind subst1 mib
       | _ -> error ()
   in
+  let mib2 =  subst_mind subst2 mib2 in
   let check_inductive_type cst env t1 t2 =
 
     (* Due to sort-polymorphism in inductive types, the conclusions of
        t1 and t2, if in Type, are generated as the least upper bounds
-       of the types of the constructors. 
+       of the types of the constructors.
 
        By monotonicity of the infered l.u.b.  wrt subtyping (i.e.  if X:U
        |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
@@ -115,8 +116,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
       | (Prop _, Type _) | (Type _,Prop _) -> error ()
       | _ -> (s1, s2) in
-    check_conv cst conv_leq env 
-      (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2))
+    check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -139,17 +139,17 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
 	cst
   in
   let check_cons_types i cst p1 p2 =
-    array_fold_left2 
+    array_fold_left2
       (fun cst t1 t2 -> check_conv cst conv env t1 t2)
       cst
-      (arities_of_specif kn (mib1,p1))
-      (arities_of_specif kn (mib2,p2))
+      (arities_of_specif kn1 (mib1,p1))
+      (arities_of_specif kn1 (mib2,p2))
   in
   let check f = if f mib1 <> f mib2 then error () in
   check (fun mib -> mib.mind_finite);
   check (fun mib -> mib.mind_ntypes);
   assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
-  assert (Array.length mib1.mind_packets >= 1 
+  assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
 
   (* Check that the expected numbers of uniform parameters are the same *)
@@ -159,46 +159,43 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams);
 
-  begin 
-    match mib2.mind_equiv with
-      | None -> ()
-      | Some kn2' -> 
-	  let kn2 = scrape_mind env kn2' in
-	  let kn1 = match mib1.mind_equiv with
-	      None -> kn
-	    | Some kn1' -> scrape_mind env kn1'
-	  in
-	    if kn1 <> kn2 then error ()
+  begin  
+  match mind_of_delta reso2 kn2  with
+      | kn2' when kn2=kn2' -> ()
+      | kn2' -> 
+	  if not (eq_mind (mind_of_delta reso1 kn1) kn2') then 
+	    error ()
   end;
   (* we check that records and their field names are preserved. *)
   check (fun mib -> mib.mind_record);
-  if mib1.mind_record then begin 
-    let rec names_prod_letin t = match kind_of_term t with 
+  if mib1.mind_record then begin
+    let rec names_prod_letin t = match kind_of_term t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
       | Cast(t,_,_) -> names_prod_letin t
       | _ -> []
-    in 
+    in
     assert (Array.length mib1.mind_packets = 1);
     assert (Array.length mib2.mind_packets = 1);
-    assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); 
-    assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); 
+    assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
+    assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
     check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
   end;
   (* we first check simple things *)
-  let cst = 
+  let cst =
     array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
   in
   (* and constructor types in the end *)
-  let cst = 
+  let cst =
     array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
   in
     cst
+
     
-let check_constant cst env msid1 l info1 cb2 spec2 = 
+let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
   let error () = error_not_match l spec2 in
   let check_conv cst f = check_conv_error error cst f in
-  let check_type cst env t1 t2 = 
+  let check_type cst env t1 t2 =
 
     (* If the type of a constant is generated, it may mention
        non-variable algebraic universes that the general conversion
@@ -209,9 +206,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
        Hence they don't have to be checked again *)
 
-    let t1,t2 = 
-      if Sign.isArity t2 then
-        let (ctx2,s2) = Sign.destArity t2 in
+    let t1,t2 =
+      if isArity t2 then
+        let (ctx2,s2) = destArity t2 in
         match s2 with
         | Type v when not (is_univ_variable v) ->
           (* The type in the interface is inferred and is made of algebraic
@@ -222,13 +219,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
             | Type u when not (is_univ_variable u) ->
               (* Both types are inferred, no need to recheck them. We
                  cheat and collapse the types to Prop *)
-                Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort)
+                mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort)
             | Prop _ ->
               (* The type in the interface is inferred, it may be the case
                  that the type in the implementation is smaller because
                  the body is more reduced. We safely collapse the upper
                  type to Prop *)
-                Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort)
+                mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort)
             | Type _ ->
               (* The type in the interface is inferred and the type in the
                  implementation is not inferred or is inferred but from a
@@ -246,32 +243,40 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
   in
 
   match info1 with
-   | Constant cb1 ->
-      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
-      (*Start by checking types*)
+    | Constant cb1 ->
+	assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+	(*Start by checking types*)
+	let cb1 = subst_const_body subst1 cb1 in
+	let cb2 = subst_const_body subst2 cb2 in
       let typ1 = Typeops.type_of_constant_type env cb1.const_type in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
       let cst = check_type cst env typ1 typ2 in
-      let con = make_con (MPself msid1) empty_dirpath l in
+      let con = make_con mp1 empty_dirpath l in
       let cst =
 	if cb2.const_opaque then
+	  (* In this case we compare opaque definitions, we need to bypass
+	     the opacity and do a delta step*)
 	  match cb2.const_body with
             | None -> cst
             | Some lc2 ->
 		let c2 = Declarations.force lc2 in
 		let c1 = match cb1.const_body with
-		  | Some lc1 -> 
+		  | Some lc1 ->
 		      let c = Declarations.force lc1 in
 			begin
-			  match (kind_of_term c) with
-			      Const n -> 
-				let cb = lookup_constant n env in
+			  match (kind_of_term c),(kind_of_term c2) with
+			      Const n1,Const n2 when (eq_constant n1 n2) -> c
+				(* c1 may have been strenghtened 
+				   we need to unfold it*)
+			    | Const n,_ ->
+				let cb = subst_const_body subst1
+				  (lookup_constant n env) in
 				  (match cb.const_opaque,
 				     cb.const_body with
-				       | true, Some lc1 -> 
+				       | true, Some lc1 ->
 					   Declarations.force lc1
 				       | _,_ -> c)
-			    | _ -> c
+			    | _ ,_-> c
 			end
 		  | None -> mkConst con
 		in
@@ -311,120 +316,103 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv cst conv env ty1 ty2
    | _ -> error ()
-	      
-let rec check_modules cst env msid1 l msb1 msb2 alias =
-  let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = module_type_of_module (Some mp) msb1 in
-  let alias1,struct_expr = match eval_struct env mty1.typ_expr with
-    	| SEBstruct (msid,sign) as str ->
-	    update_subst alias (map_msid msid mp),str
-	| _ as str -> empty_subst,str in
-  let mty1 = {mty1 with 
-		typ_expr = struct_expr;
-		typ_alias = join alias1 mty1.typ_alias } in
-  let mty2 =  module_type_of_module None msb2 in
-  let cst = check_modtypes cst env mty1 mty2 false in
+
+let rec check_modules cst env msb1 msb2 subst1 subst2 =
+  let mty1 = module_type_of_module env None msb1 in
+  let mty2 =  module_type_of_module env None msb2 in
+  let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
     cst
-	
 
-and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = 
-  let mp1 = MPself msid1 in
-  let env = add_signature mp1 sig1 env in 
-  let sig1 = subst_structure alias sig1 in
-  let alias1 = update_subst alias (map_msid msid2 mp1) in
-  let sig2 = subst_structure alias1 sig2' in
-  let sig2 = subst_signature_msid msid2 mp1 sig2 in
+and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
   let map1 = make_label_map 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_msid msid1) (string_of_msid msid2)
+  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
 	| SFBconst cb2 ->
-	    check_constant cst env msid1 l info1 cb2 spec2
-	| SFBmind mib2 -> 
-	    check_inductive cst env msid1 l info1 mib2 spec2
-	| SFBmodule msb2 ->  
+	    check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
+	| SFBmind mib2 ->
+	    check_inductive cst env
+	      mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
+	| SFBmodule msb2 ->
 	    begin
 	      match info1 with
-		| Module msb -> check_modules cst env msid1 l msb msb2 alias
-		| Alias (mp,typ_opt) ->let msb = 
-		    {mod_expr = Some (SEBident mp);
-		     mod_type = typ_opt;
-		     mod_constraints = Constraint.empty;
-		     mod_alias = (lookup_modtype mp env).typ_alias;
-		     mod_retroknowledge = []} in
-		    check_modules cst env msid1 l msb msb2 alias
-		| _ -> error_not_match l spec2
-	    end
-	| SFBalias (mp,typ_opt,_) ->
-	    begin	
-	      match info1 with
-		| Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst
-		| Module msb -> 
-		    let msb1 = 
-		      {mod_expr = Some (SEBident mp);
-		       mod_type = typ_opt;
-		       mod_constraints = Constraint.empty;
-		       mod_alias = (lookup_modtype mp env).typ_alias;
-		       mod_retroknowledge = []} in
-			check_modules cst env msid1 l msb msb1 alias
+		| Module msb -> check_modules cst env msb msb2 
+		    subst1 subst2
 		| _ -> error_not_match l spec2
 	    end
 	| SFBmodtype mtb2 ->
-	    let mtb1 = 
+	    let mtb1 =
 	      match info1 with
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in
-	      check_modtypes cst env mtb1 mtb2 true
+	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
+	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
+	      check_modtypes cst env mtb1 mtb2 subst1 subst2 true
   in
     List.fold_left check_one_body cst sig2
-    
 
-and check_modtypes cst env mtb1 mtb2 equiv = 
-  if mtb1==mtb2 then cst else (* just in case  :) *)
-  let mtb1',mtb2'=
-    (match mtb1.typ_strength with
-	 None -> eval_struct env mtb1.typ_expr,
-	   eval_struct env mtb2.typ_expr
-       | Some mp -> strengthen  env mtb1.typ_expr mp,
-	   eval_struct env mtb2.typ_expr) in
-      let rec check_structure cst env str1 str2 equiv = 
-	match str1, str2 with
-	  | SEBstruct (msid1,list1), 
-	    SEBstruct (msid2,list2) -> 
-	      let cst = check_signatures cst env
-		(msid1,list1) mtb1.typ_alias (msid2,list2) in
-		if equiv then
-		  check_signatures cst env 
-		    (msid2,list2) mtb2.typ_alias  (msid1,list1) 
-		else
-		  cst
-	  | SEBfunctor (arg_id1,arg_t1,body_t1), 
+and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = 
+  if mtb1==mtb2 then cst else 
+  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
+  let rec check_structure cst env str1 str2 equiv subst1 subst2 = 
+	match str1,str2 with
+	  | SEBstruct (list1), 
+	    SEBstruct (list2) -> 
+	      if equiv then
+		let subst2 = 
+		  add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
+		Univ.Constraint.union 
+		  (check_signatures cst env
+		     mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+		  mtb1.typ_delta mtb2.typ_delta) 
+		  (check_signatures cst env 
+		     mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
+		  mtb2.typ_delta  mtb1.typ_delta)
+	      else
+		check_signatures cst env
+		  mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+		  mtb1.typ_delta  mtb2.typ_delta
+	  | SEBfunctor (arg_id1,arg_t1,body_t1),
 	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	      let cst = check_modtypes cst env arg_t2 arg_t1 equiv in 
+	      let subst1 = 
+		(join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in
+	      let cst = check_modtypes cst env 
+		arg_t2 arg_t1 subst2 subst1
+		equiv in 
 		(* contravariant *)
-	      let env = 
-		add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
+	      let env = add_module 
+		(module_body_of_type (MPbound arg_id2) arg_t2) env 
 	      in
-	      let body_t1' = 
-		(* since we are just checking well-typedness we do not need
-		   to expand any constant. Hence the identity resolver. *)
-		subst_struct_expr
-		  (map_mbid arg_id1 (MPbound arg_id2) None)
-		  body_t1
+	      let env = match body_t1 with
+		  SEBstruct str -> 
+		    add_module {mod_mp = mtb1.typ_mp;
+				mod_expr = None;
+				mod_type = subst_struct_expr subst1 body_t1;
+				mod_type_alg= None;
+				mod_constraints=mtb1.typ_constraints;
+				mod_retroknowledge = [];
+				mod_delta = mtb1.typ_delta} env
+		| _ -> env
 	      in
-		check_structure cst env (eval_struct env body_t1')
-		  (eval_struct env body_t2) equiv
+		check_structure cst env body_t1 body_t2 equiv 
+		  subst1
+		  subst2
 	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
-      in 
-     if mtb1'== mtb2' then cst 
-     else check_structure cst env mtb1' mtb2' equiv
-	  
-let check_subtypes env sup super = 
-  check_modtypes Constraint.empty env sup super false
+      in
+     if mtb1'== mtb2' then cst
+     else check_structure cst env mtb1' mtb2' equiv subst1 subst2
+
+let check_subtypes env sup super =
+  let env = add_module 
+		(module_body_of_type sup.typ_mp sup) env in
+  check_modtypes Constraint.empty env 
+    (strengthen env sup sup.typ_mp) super empty_subst 
+    (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
+