- 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

4 files changed, 29 insertions, 24 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4fbeff526..e3d4d1a4d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -260,7 +260,7 @@ let rec same_raw c d =
         (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
           same_raw t1 t2;
           if al1 <> al2 then failwith "RCases";
-          option_iter2(fun (_,i1,nl1) (_,i2,nl2) ->
+          option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
             if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
       List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
         List.iter2 same_patt pl1 pl2;
@@ -690,11 +690,13 @@ let rec extern inctx scopes vars r =
           | Name id, RVar (_,id') when id=id' -> None
           | Name _, _ -> Some na in
 	(sub_extern false scopes vars tm,
-	(na',option_map (fun (loc,ind,nal) ->
+	(na',option_map (fun (loc,ind,n,nal) ->
+	  let params = list_tabulate
+	    (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
 	  let args = List.map (function
 	    | Anonymous -> RHole (dummy_loc,Evd.InternalHole) 
 	    | Name id -> RVar (dummy_loc,id)) nal in
-	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
+	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
       let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in 
       CCases (loc,rtntypopt',tml,eqns)
@@ -920,8 +922,8 @@ let rec raw_of_pat env = function
       let indnames,rtn =
 	if p = PMeta None then (Anonymous,None),None
 	else 
-	  let n = out_some ind_nargs in
-	  return_type_of_predicate ind n (raw_of_pat env p) in
+	  let nparams,n = out_some ind_nargs in
+	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
       RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 376360046..1e8c7fdef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,6 +22,7 @@ open Cases
 open Topconstr
 open Nametab
 open Notation
+open Inductiveops
 
 (* To interpret implicits and arg scopes of recursive variables in
    inductive types and recursive definitions *)
@@ -382,11 +383,6 @@ let check_constructor_length env loc cstr pl pl0 =
   if n <> nargs && n <> nhyps (* i.e. with let's *) then
     error_wrong_numarg_constructor_loc loc env cstr nargs
 
-let check_inductive_length env (loc,ind,nal) =
-  let n = Inductiveops.inductive_nargs env ind in
-  if n <> List.length nal then
-    error_wrong_numarg_inductive_loc loc env ind n
-
 (* Manage multiple aliases *)
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
@@ -950,18 +946,25 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	let tids = names_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
 	let t = intern_type (tids,None,scopes) t in
-	let (_,_,nal as indsign) =
+	let (_,_,_,nal as indsign) =
 	  match t with
-	  | RRef (loc,IndRef ind) -> (loc,ind,[])
+	  | RRef (loc,IndRef ind) -> (loc,ind,0,[])
 	  | RApp (loc,RRef (_,IndRef ind),l) ->
+	      let nparams, nrealargs = inductive_nargs globalenv ind in
+	      let nindargs = nparams + nrealargs in
+	      if List.length l <> nindargs then
+		error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
 	      let nal = List.map (function
 		| RHole _ -> Anonymous
 		| RVar (_,id) -> Name id
 		| c ->
 		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
-	      (loc,ind,nal)
+	      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");
+	      (loc,ind,nparams,nal)
 	  | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
-	check_inductive_length globalenv indsign;
 	nal, Some indsign
     | None -> 
 	[], None in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cc84d0c10..7a634a71a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -38,7 +38,7 @@ type aconstr =
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
+      (aconstr * (name * (inductive * int * name list) option)) list *
       (identifier list * cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
@@ -76,10 +76,10 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
-	| Some (ind,nal) -> 
+	| Some (ind,npar,nal) -> 
 	  let e',nal' = List.fold_right (fun na (e',nal) -> 
 	      let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in
-	  e',Some (loc,ind,nal') in
+	  e',Some (loc,ind,npar,nal') in
 	let e',na' = name_app g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
@@ -186,8 +186,8 @@ let aconstr_and_vars_of_rawconstr a =
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  option_iter
-	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,option_map (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+	    (fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
+          (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
         List.map f eqnl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
@@ -289,9 +289,9 @@ let rec subst_aconstr subst bound raw =
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) -> 
 	  let a' = subst_aconstr subst bound a in
-	  let signopt' = option_map (fun ((indkn,i),nal as z) ->
+	  let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
 	    let indkn' = subst_kn subst indkn in
-	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+	    if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
 	  if a' == a && signopt' == signopt then x else (a',(n,signopt')))
         rl
       and branches' = list_smartmap 
@@ -349,11 +349,11 @@ let abstract_return_type_context pi mklam tml rtno =
     rtno
 
 let abstract_return_type_context_rawconstr =
-  abstract_return_type_context pi3
+  abstract_return_type_context (fun (_,_,_,nal) -> nal)
     (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
 
 let abstract_return_type_context_aconstr =
-  abstract_return_type_context snd
+  abstract_return_type_context pi3
     (fun na c -> ALambda(na,AHole Evd.InternalHole,c))
 
 let rec adjust_scopes = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 4e2017f44..d5b718d34 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -34,7 +34,7 @@ type aconstr =
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
   | ACases of aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
+      (aconstr * (name * (inductive * int * name list) option)) list *
       (identifier list * cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
   | AIf of aconstr * (name * aconstr option) * aconstr * aconstr