Intégration initiale du Cases

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

5 files changed, 21 insertions, 16 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6722b023fb..2c7829ef94 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -63,8 +63,9 @@ let rec execute mf env cstr =
     | IsMutInd _ ->
 	(make_judge cstr (type_of_inductive env Evd.empty cstr), cst0)
 	  
-    | IsMutConstruct _ -> 
-	let (typ,kind) = destCast (type_of_constructor env Evd.empty cstr) in
+    | IsMutConstruct (sp,i,j,args) -> 
+	let (typ,kind) =
+	  destCast (type_of_constructor env Evd.empty (((sp,i),j),args)) in
         ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
 	  
     | IsMutCase (_,p,c,lf) ->
diff --git a/kernel/term.ml b/kernel/term.ml
index 31e52ebb3f..f2e8d34227 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -592,7 +592,7 @@ let lambda_implicit_lift n a = iterate lambda_implicit n (lift n a)
 (* prod_it b [x1:T1;..xn:Tn] = (x1:T1)..(xn:Tn)b *)
 let prod_it = List.fold_left (fun c (n,t)  -> mkProd n t c)
 
-(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b *)
+(* lam_it b [x1:T1;..xn:Tn] = [x1:T1]..[xn:Tn]b with xn *)
 let lam_it = List.fold_left (fun c (n,t)  -> mkLambda n t c)
 
 (* prodn n ([x1:T1]..[xn:Tn]Gamma) b = (x1:T1)..(xn:Tn)b *)
@@ -665,19 +665,19 @@ let rec to_prod n lam =
  * if this does not work, then we use the string S as part of our
  * error message. *)
 
-let prod_app s t n =
+let prod_app t n =
   match strip_outer_cast t with
     | DOP2(Prod,_,b) -> sAPP b n
     | _ ->
-	errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ;
-			  'sTR s ; 'fNL >]
+	errorlabstrm "prod_app"
+	  [< 'sTR"Needed a product, but didn't find one" ; 'fNL >]
 
 
-(* prod_appvect s T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_appvect s t nL = Array.fold_left (prod_app s) t nL
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_appvect t nL = Array.fold_left prod_app t nL
 
-(* prod_applist s T [ a1 ; ... ; an ] -> (T a1 ... an) *)
-let prod_applist s t nL = List.fold_left (prod_app s) t nL
+(* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
+let prod_applist t nL = List.fold_left prod_app t nL
 
 
 (*********************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index ff296c2dd3..9935aebe53 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -359,6 +359,9 @@ val lam_it : constr -> (name * constr) list -> constr
 val to_lambda : int -> constr -> constr
 val to_prod : int -> constr -> constr
 
+(* pseudo-reduction rule *)
+(* prod_applist (x1:B1;...;xn:Bn)B a1...an --> B[a1...an] *)
+val prod_applist : constr -> constr list -> constr
 
 (*s Other term destructors. *)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 5c2aa643b2..9fb263c59d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -110,11 +110,9 @@ let instantiate_lc mis =
   let lc = mis.mis_mip.mind_lc in
   instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
 
-let type_of_constructor env sigma c =
-  let (sp,i,j,args) = destMutConstruct c in
-  let mind = DOPN (MutInd (sp,i), args) in
-  let recmind = check_mrectype_spec env sigma mind in
-  let mis = lookup_mind_specif recmind env in
+let type_of_constructor env sigma ((ind_sp,j),args) =
+  let mind = DOPN (MutInd ind_sp, args) in
+  let mis = lookup_mind_specif mind env in
   check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps);
   let specif = instantiate_lc mis in
   let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 20cec7273a..55191e284f 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -31,10 +31,13 @@ val type_of_constant : env -> 'a evar_map -> constr -> typed_type
 
 val type_of_inductive : env -> 'a evar_map -> constr -> typed_type
 
-val type_of_constructor : env -> 'a evar_map -> constr -> constr
+val type_of_constructor :
+  env -> 'a evar_map -> (constructor_path * constr array) -> constr
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
+val sort_of_arity : env -> 'a Evd.evar_map -> constr -> constr 
+
 val type_of_case : env -> 'a evar_map 
   -> unsafe_judgment -> unsafe_judgment 
     -> unsafe_judgment array -> unsafe_judgment