1. added code to handle the inclusion of inductive types and constructors in

   parameters.
2. however, the code is still not working if the parameters are referenced
   later on in the module signature. To fix this the representation of
   terms must be changed to unify references to constants, inductive types and
   constructors.
3. thus the code above is prefixed by an error that suggest to the user how
   to avoid the problem right now. Note: the above code has not been commented
   out to keep it in synch with the other changes in the kernel. However, it
   is dead code for now.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6600 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 60 insertions, 45 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 9f03b57c5d..033eeec793 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -19,6 +19,7 @@ open Reduction
 open Inductive
 open Modops
 open Mod_subst
+open Entries
 (*i*)
 
 (* This local type is used to subtype a constant with a constructor or
@@ -27,7 +28,6 @@ open Mod_subst
 
 type namedobject = 
   | Constant of constant_body
-  | Mind of mutual_inductive_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_specification_body
@@ -41,31 +41,27 @@ let add_nameobjects_of_mib ln mib map =
     let ip = (ln,j) in
     let map = 
       array_fold_right_i 
-	(fun i id map -> Idmap.add id (IndConstr ((ip,i), mib)) map)
-	oib.mind_consnames
-	map
+      (fun i id map ->
+        Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
+      oib.mind_consnames
+      map
     in
-      Idmap.add oib.mind_typename (IndType (ip, mib)) map
+      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
 
+
 (* creates namedobject map for the whole signature *)
 
-let make_label_map msid list = 
+let make_label_map mp list = 
   let add_one (l,e) map = 
-    let obj = 
-      match e with
-	| SPBconst cb -> Constant cb
-	| SPBmind mib -> Mind mib
-	| SPBmodule mb -> Module mb
-	| SPBmodtype mtb -> Modtype mtb
-    in
-(*    let map = match obj with
-      | Mind mib -> 
-	  add_nameobjects_of_mib (make_ln (MPself msid) l) mib map
-      | _ -> map
-    in *)
-      Labmap.add l obj map
+   let add_map obj = Labmap.add l obj map in
+   match e with
+    | SPBconst cb -> add_map (Constant cb)
+    | SPBmind mib ->
+       add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
+    | SPBmodule mb -> add_map (Module mb)
+    | SPBmodtype mtb -> add_map (Modtype mtb)
   in
     List.fold_right add_one list Labmap.empty
 
@@ -82,8 +78,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   let check_conv cst f = check_conv_error error cst f in
   let mib1 = 
     match info1 with
-      | Mind mib -> mib
-    (*  | IndType (_,mib) -> mib   we will enable this later*)
+      | IndType ((_,0), mib) -> mib
       | _ -> error ()
   in
   let check_packet cst p1 p2 =
@@ -161,23 +156,43 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
 let check_constant cst env msid1 l info1 cb2 spec2 = 
   let error () = error_not_match l spec2 in
   let check_conv cst f = check_conv_error error cst f in
-  let cb1 = 
-    match info1 with
-      | Constant cb -> cb
-      | _ -> error ()
-  in 
-    assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
-  (*Start by checking types*)
-    let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
-    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 (make_con (MPself msid1) empty_dirpath l)
-	  in
-	    check_conv cst conv env c1 c2
+  match info1 with
+   | Constant cb1 ->
+      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+      (*Start by checking types*)
+      let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
+      let con = make_con (MPself msid1) empty_dirpath l in
+      let cst =
+       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
+   | IndType ((kn,i) as ind,mind1) ->
+      Util.error ("The kernel does not recognize yet that a parameter can be " ^
+       "instantiated by an inductive type. Hint: you can rename the " ^
+       "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 () ;
+      let arity1 = mind1.mind_packets.(i).mind_user_arity in
+       check_conv cst conv_leq env arity1 cb2.const_type
+   | IndConstr (((kn,i),j) as cstr,mind1) ->
+      Util.error ("The kernel does not recognize yet that a parameter can be " ^
+       "instantiated by a constructor. Hint: you can rename the " ^
+       "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 () ;
+      let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
+       check_conv cst conv env ty1 cb2.const_type
+   | _ -> error ()
 	      
 let rec check_modules cst env msid1 l msb1 msb2 =
   let mp = (MPdot(MPself msid1,l)) in
@@ -194,11 +209,11 @@ let rec check_modules cst env msid1 l msb1 msb2 =
   cst
 	
 
-and check_signatures cst env' (msid1,sig1) (msid2,sig2') = 
+and check_signatures cst env (msid1,sig1) (msid2,sig2') = 
   let mp1 = MPself msid1 in
-  let env = add_signature mp1 sig1 env' in 
+  let env = add_signature mp1 sig1 env in 
   let sig2 = subst_signature_msid msid2 mp1 sig2' in
-  let map1 = make_label_map msid1 sig1 in
+  let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
     let info1 = 
       try 
@@ -229,10 +244,10 @@ and check_signatures cst env' (msid1,sig1) (msid2,sig2') =
     List.fold_left check_one_body cst sig2
     
 and check_modtypes cst env mtb1 mtb2 equiv = 
-  if mtb1==mtb2 then (); (* just in case  :) *)
+  if mtb1==mtb2 then cst else (* just in case  :) *)
   let mtb1' = scrape_modtype env mtb1 in
   let mtb2' = scrape_modtype env mtb2 in
-    if mtb1'==mtb2' then ();
+    if mtb1'==mtb2' then cst else
     match mtb1', mtb2' with
       | MTBsig (msid1,list1), 
 	MTBsig (msid2,list2) -> 
@@ -245,7 +260,7 @@ and check_modtypes cst env mtb1 mtb2 equiv =
 	MTBfunsig (arg_id2,arg_t2,body_t2) ->
 	  let cst = check_modtypes cst env arg_t2 arg_t1 equiv in 
 	    (* contravariant *)
-	  let env' = 
+	  let env = 
 	    add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
 	  in
 	  let body_t1' = 
@@ -255,7 +270,7 @@ and check_modtypes cst env mtb1 mtb2 equiv =
               (map_mbid arg_id1 (MPbound arg_id2) None)
 	      body_t1
 	  in
-	  check_modtypes cst env' body_t1' body_t2 equiv
+	  check_modtypes cst env body_t1' body_t2 equiv
       | MTBident _ , _ -> anomaly "Subtyping: scrape failed"
       | _ , MTBident _ -> anomaly "Subtyping: scrape failed"
       | _ , _ -> error_incompatible_modtypes mtb1 mtb2