1 files changed, 76 insertions, 92 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 447e062a..c141a02a 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -1,12 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+
+(* This module checks subtyping of module types *)
 
 (*i*)
 open Util
@@ -22,8 +25,6 @@ open Mod_subst
 open Entries
 (*i*)
 
-
-
 (* 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 *)
@@ -66,26 +67,26 @@ let make_label_map mp list =
   in
     List.fold_right add_one list Labmap.empty
 
-let check_conv_error error cst f env a1 a2 =
+let check_conv_error error why cst f env a1 a2 =
   try
-    Constraint.union cst (f env a1 a2)
+    union_constraints cst (f env a1 a2)
   with
-      NotConvertible -> error ()
+      NotConvertible -> error why
 
 (* for now we do not allow reorderings *)
 
 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 error why = error_signature_mismatch l spec2 why in
+  let check_conv why cst f = check_conv_error error why cst f in
   let mib1 =
     match info1 with
       | IndType ((_,0), mib) -> subst_mind subst1 mib
-      | _ -> error ()
+      | _ -> error (InductiveFieldExpected mib2)
   in
   let mib2 =  subst_mind subst2 mib2 in
-  let check_inductive_type cst env t1 t2 =
+  let check_inductive_type cst name 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
@@ -114,40 +115,43 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     let s1,s2 =
       match s1, s2 with
       | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
-      | (Prop _, Type _) | (Type _,Prop _) -> error ()
+      | (Prop _, Type _) | (Type _,Prop _) ->
+	error (NotConvertibleInductiveField name)
       | _ -> (s1, s2) in
-    check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+    check_conv (NotConvertibleInductiveField name)
+      cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
-    let check f = if f p1 <> f p2 then error () in
-      check (fun p -> p.mind_consnames);
-      check (fun p -> p.mind_typename);
+    let check f why = if f p1 <> f p2 then error why in
+      check (fun p -> p.mind_consnames) NotSameConstructorNamesField;
+      check (fun p -> p.mind_typename) NotSameInductiveNameInBlockField;
       (* nf_lc later *)
       (* nf_arity later *)
       (* user_lc ignored *)
       (* user_arity ignored *)
-      check (fun p -> p.mind_nrealargs);
+      check (fun p -> p.mind_nrealargs) (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *)
       (* kelim ignored *)
       (* listrec ignored *)
       (* finite done *)
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_inductive_type cst env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+      let cst = check_inductive_type cst p2.mind_typename env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
   let check_cons_types i cst p1 p2 =
-    array_fold_left2
-      (fun cst t1 t2 -> check_conv cst conv env t1 t2)
+    array_fold_left3
+      (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2)
       cst
+      p2.mind_consnames
       (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);
+  let check f why = if f mib1 <> f mib2 then error (why (f mib2)) in
+  check (fun mib -> mib.mind_finite) (fun x -> FiniteInductiveFieldExpected x);
+  check (fun mib -> mib.mind_ntypes) (fun x -> InductiveNumbersFieldExpected x);
   assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
   assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
@@ -157,17 +161,17 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   (* at the time of checking the inductive arities in check_packet. *)
   (* Notice that we don't expect the local definitions to match: only *)
   (* the inductive types and constructors types have to be convertible *)
-  check (fun mib -> mib.mind_nparams);
+  check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x);
 
-  begin  
+  begin
   match mind_of_delta reso2 kn2  with
       | kn2' when kn2=kn2' -> ()
       | kn2' -> 
 	  if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then 
-	    error ()
+	    error NotEqualInductiveAliases
   end;
   (* we check that records and their field names are preserved. *)
-  check (fun mib -> mib.mind_record);
+  check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x);
   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)
@@ -179,7 +183,11 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     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);
-    check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+    check (fun mib ->
+      let nparamdecls = List.length mib.mind_params_ctxt in
+      let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
+      snd (list_chop nparamdecls names))
+      (fun x -> RecordProjectionsExpected x);
   end;
   (* we first check simple things *)
   let cst =
@@ -193,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 
     
 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
-  let error () = error_not_match l spec2 in
+  let error why = error_signature_mismatch l spec2 why in
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
@@ -233,66 +241,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
                  constraints of the form "univ <= max(...)" are not
                  expressible in the system of algebraic universes: we fail
                  (the user has to use an explicit type in the interface *)
-                error ()
-          with UserError _ (* "not an arity" *) ->
-            error () end
-        | _ -> t1,t2
+                error NoTypeConstraintExpected
+          with NotArity ->
+            error NotConvertibleTypeField end
+        | _ ->
+	  t1,t2
       else
         (t1,t2) in
-    check_conv cst conv_leq env t1 t2
+    check_conv NotConvertibleTypeField cst conv_leq env t1 t2
   in
 
   match info1 with
     | 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
+      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+      let cb1 = subst_const_body subst1 cb1 in
+      let cb2 = subst_const_body subst2 cb2 in
+      (* Start by checking types*)
       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 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 ->
-		      let c = Declarations.force lc1 in
-			begin
-			  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 ->
-					   Declarations.force lc1
-				       | _,_ -> c)
-			    | _ ,_-> c
-			end
-		  | None -> mkConst con
-		in
-		  check_conv cst conv env c1 c2
-	else
-	  match cb2.const_body with
-            | None -> cst
-            | Some lc2 ->
-		let c2 = Declarations.force lc2 in
-		let c1 = match cb1.const_body with
-		  | Some lc1 -> Declarations.force lc1
-		  | None -> mkConst con
-		in
-		  check_conv cst conv env c1 c2
-      in
-	cst
+      (* Now we check the bodies:
+	 - A transparent constant can only be implemented by a compatible
+	   transparent constant.
+         - In the signature, an opaque is handled just as a parameter:
+           anything of the right type can implement it, even if bodies differ.
+      *)
+      (match cb2.const_body with
+	| Undef _ | OpaqueDef _ -> cst
+	| Def lc2 ->
+	  (match cb1.const_body with
+	    | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
+	    | Def lc1 ->
+	      (* NB: cb1 might have been strengthened and appear as transparent.
+		 Anyway [check_conv] will handle that afterwards. *)
+	      let c1 = Declarations.force lc1 in
+	      let c2 = Declarations.force lc2 in
+	      check_conv NotConvertibleBodyField cst conv env c1 c2))
    | IndType ((kn,i),mind1) ->
        ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -300,10 +284,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "inductive type and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error () ;
+      if constant_has_body cb2 then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv cst conv_leq env arity1 typ2
+       check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -311,15 +295,15 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "constructor and give a definition to map the old name to the new " ^
        "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
-      if cb2.const_body <> None then error () ;
+      if constant_has_body cb2 then error DefinitionFieldExpected;
       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 cst conv env ty1 ty2
-   | _ -> error ()
+       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 env None msb1 in
-  let mty2 =  module_type_of_module env None msb2 in
+  let mty1 = module_type_of_module None msb1 in
+  let mty2 =  module_type_of_module None msb2 in
   let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
     cst
 
@@ -344,13 +328,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      match info1 with
 		| Module msb -> check_modules cst env msb msb2 
 		    subst1 subst2
-		| _ -> error_not_match l spec2
+		| _ -> error_signature_mismatch l spec2 ModuleFieldExpected
 	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 =
 	      match info1 with
 		| Modtype mtb -> mtb
-		| _ -> error_not_match l spec2
+		| _ -> 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
@@ -368,7 +352,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 	      if equiv then
 		let subst2 = 
 		  add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
-		Univ.Constraint.union 
+		Univ.union_constraints 
 		  (check_signatures cst env
 		     mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
 		  mtb1.typ_delta mtb2.typ_delta) 
@@ -412,7 +396,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 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 
+  check_modtypes empty_constraint env 
+    (strengthen sup sup.typ_mp) super empty_subst
     (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false