- Distinction explicite des parties paramètres et arguments dans le type

  des inductifs de la clause "in" du filtrage.
- Débogage et extension du parseur xml (g_xml.ml4)


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

9 files changed, 28 insertions, 55 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4252216758..f709ab450e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -66,13 +66,10 @@ let error_needs_inversion env x t =
 module type S = sig
   val compile_cases :
     loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
-    env ->
-    rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list *
-      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
     unsafe_judgment
 end
 
@@ -344,7 +341,7 @@ let unify_tomatch_with_patterns isevars env typ tm =
 
 let find_tomatch_tycon isevars env loc = function
   (* Try first if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_),_ 
+  | Some (_,ind,_,_),_ 
   (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
   | None, Some (_,(ind,_)) ->
       mk_tycon (inductive_template isevars env loc ind)
@@ -1539,7 +1536,7 @@ let extract_arity_signature env0 tomatchl tmsign =
       | NotInd (bo,typ) -> 
 	  (match t with
 	    | None -> [na,option_map (lift n) bo,lift n typ]
-	    | Some (loc,_,_) -> 
+	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
       | IsInd (_,IndType(indf,realargs)) ->
@@ -1548,18 +1545,9 @@ let extract_arity_signature env0 tomatchl tmsign =
 	  let nrealargs = List.length realargs in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',nal) ->
-		  let nparams = List.length params in
-		  if ind <> ind' then
+	      | Some (loc,ind',nparams,realnal) ->
+		  if ind <> ind' or List.length params <> nparams then
 		    user_err_loc (loc,"",str "Wrong inductive type");
-		  let nindargs = nparams + nrealargs in
-		  (* Normally done at interning time *)
-		  if List.length nal <> nindargs then
-		    error_wrong_numarg_inductive_loc loc env0 ind' nindargs;
-		  let parnal,realnal = list_chop nparams nal in
-		  if List.exists ((<>) Anonymous) parnal then
-		    user_err_loc (loc,"",
-		    str "The parameters of inductive type must be implicit");
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf') in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 25cf2aedd3..1f6e4a86b7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -314,9 +314,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all ((=) Anonymous) nl then None
-	      else 
-		let pars = list_tabulate (fun _ -> Anonymous) nparams in
-		Some (dl,indsp,pars@nl) in
+	      else Some (dl,indsp,nparams,nl) in
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -577,9 +575,9 @@ let rec subst_rawconstr subst raw =
         let a' = subst_rawconstr subst a in
         let (n,topt) = x in 
         let topt' = option_smartmap
-          (fun (loc,(sp,i),x as t) ->
+          (fun (loc,(sp,i),x,y as t) ->
             let sp' = subst_kn subst sp in
-            if sp == sp' then t else (loc,(sp',i),x)) topt in
+            if sp == sp' then t else (loc,(sp',i),x,y)) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = list_smartmap 
 			(fun (loc,idl,cpl,r as branch) ->
@@ -647,6 +645,6 @@ let simple_cases_matrix_of_branches ind brns brs =
       (dummy_loc,ids,[p],c))
     0 brns brs
 
-let return_type_of_predicate ind n pred =
+let return_type_of_predicate ind nparams n pred =
   let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in
-  (List.hd nal, Some (dummy_loc,ind,List.tl nal)), Some p
+  (List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 4b0adabbd3..3068f97c28 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -54,5 +54,5 @@ val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
 val simple_cases_matrix_of_branches : 
   inductive -> int list -> rawconstr list -> cases_clauses
 val return_type_of_predicate :
-  inductive -> int -> rawconstr -> predicate_pattern * rawconstr option
+  inductive -> int -> int -> rawconstr -> predicate_pattern * rawconstr option
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index c0902526ac..1c290e877f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -120,7 +120,7 @@ let constructor_nrealhyps env (ind,j) =
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt
+  mib.mind_nparams, mip.mind_nrealargs
 
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 91425fe79a..b4acaafbb8 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -60,7 +60,8 @@ val mis_constructor_nargs_env : env -> constructor -> int
 val constructor_nrealargs : env -> constructor -> int
 val constructor_nrealhyps : env -> constructor -> int
 
-val inductive_nargs : env -> inductive -> int
+(* Return number of expected parameters and of expected real arguments *)
+val inductive_nargs : env -> inductive -> int * int
 
 type constructor_summary = {
   cs_cstr : constructor;
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 5b3eafb305..1453aa218b 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -39,7 +39,7 @@ type constr_pattern =
   | PSort of rawsort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of (case_style * int array * inductive option * int option)
+  | PCase of (case_style * int array * inductive option * (int * int) option)
       * constr_pattern * constr_pattern * constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
@@ -107,7 +107,8 @@ let rec pattern_of_constr t =
     | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
     | Case (ci,p,a,br) ->
 	let cip = ci.ci_pp_info in
-	PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,Some cip.ind_nargs),
+	let no = Some (ci.ci_npar,cip.ind_nargs) in
+	PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,no),
 	       pattern_of_constr p,pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
@@ -143,23 +144,6 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-(*
-let rec inst lvar = function
-  | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
-  | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
-  | PSoApp (n,pl) -> PSoApp (n, List.map (inst lvar) pl)
-  | PLambda (n,a,b) -> PLambda (n,inst lvar a,inst lvar b)
-  | PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
-  | PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
-  | PCase (ci,po,p,pl) ->
-      PCase (ci,option_map (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
-  (* Non recursive *)
-  | (PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x 
-  (* Bound to terms *)
-  | (PFix _ | PCoFix _) ->
-      error ("Not instantiable pattern")
-*)
-
 let rec subst_pattern subst pat = match pat with
   | PRef ref ->
       let ref',t = subst_global subst ref in
@@ -263,9 +247,9 @@ let rec pat_of_raw metas vars = function
              [|pat_of_raw metas vars c|])
   | RCases (loc,p,[c,(na,indnames)],brs) ->
       let pred,ind_nargs, ind = match p,indnames with
-	| Some p, Some (_,ind,nal) ->
+	| Some p, Some (_,ind,n,nal) ->
 	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
-	    Some (List.length nal),Some ind
+	    Some (n,List.length nal),Some ind
 	| _ -> PMeta None, None, None in
       let ind = match ind with Some _ -> ind | None ->
 	match brs with
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 4093f5e110..2ecb85ba4a 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -40,7 +40,7 @@ type constr_pattern =
   | PSort of rawsort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of (case_style * int array * inductive option * int option)
+  | PCase of (case_style * int array * inductive option * (int * int) option)
       * constr_pattern * constr_pattern * constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 0fafb916d5..d536adcb0e 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,8 +47,6 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type predicate_pattern = name * (loc * inductive * name list) option
-
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -77,6 +75,9 @@ and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
   | RCoFix of int
 
+and predicate_pattern =
+    name * (loc * inductive * int * name list) option
+
 and tomatch_tuple = (rawconstr * predicate_pattern) list
 
 and cases_clauses =
@@ -85,7 +86,7 @@ and cases_clauses =
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
-    | (tm,(na,Some (_,_,nal))) -> na::nal) tml)
+    | (tm,(na,Some (_,_,_,nal))) -> na::nal) tml)
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index d20b3fce46..d85ca0158a 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -44,8 +44,6 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
-type predicate_pattern = name * (loc * inductive * name list) option
-
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -74,6 +72,9 @@ and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
   | RCoFix of int
 
+and predicate_pattern =
+    name * (loc * inductive * int * name list) option
+
 and tomatch_tuple = (rawconstr * predicate_pattern) list
 
 and cases_clauses =