Si un fixpoint a plusieurs arguments, mais un seul de type inductif,

ce patch dispense d'ecrire le { struct .. }

En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, 
l'index de l'argument inductif devient un int option au lieu d'un int. 
Les deux cas possibles:
- Some n : les situations autorisées auparavant, a savoir {struct}
 explicite, ou bien un seul argument au total
- None : le cas nouveau, qui redonne un entier lors du passage de
 rawconstr à constr si l'on trouve effectivement un unique argument
 ayant un type inductif, et une erreur sinon.

Pour l'instant, on cherche l'inductif dans le type de manière
syntaxique, mais il est jouable de rajouter un poil de reduction
(au moins delta). 

Dans le détail, voici les coins que ce patch influence:

- parsing/g_xml.ml4: continue pour l'instant a attendre un index
  explicite via un element xml "recIndex"

- contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà
  un cas ctv_ID_OPT_NONE correspondant à l'absence de struct.  Par
  contre, dans le détail, le code pour un CFix utilise l'index de
  recurrence pour recouper au besoin le type du fixpoint en deux.
  Est-ce que je me gourre en supposant que si l'on a besoin de couper
  ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de
  l'impression d'un constr, et donc que l'index aura été correctement
  résolu ?

- contrib/subtac/subtac_command.ml:
- contrib/funind/indfun.ml:
  dans les deux cas, j'ai fait le service minimum, le struct reste
  obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas
  dur à adapter pour ceux qui comprennent ces parties.



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

18 files changed, 114 insertions, 56 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 2fcdd3a75d..d7c045a60d 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -317,7 +317,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 			 (Topconstr.names_of_local_assums args) 
 		     in 
 		     let annot = 
-		       try Util.list_index (Name id) names - 1, Topconstr.CStructRec 
+		       try Some (Util.list_index (Name id) names - 1), Topconstr.CStructRec 
 		       with Not_found -> raise (UserError("",str "Cannot find argument " ++ Ppconstr.pr_id id)) 
 		     in 
  		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation) 
@@ -328,7 +328,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 			 (Util.dummy_loc,"GenFixpoint",
 			  Pp.str "the recursive argument needs to be specified")
 		     else 
-		       (name,(0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
+		       (name,(Some 0, Topconstr.CStructRec),args,types,body),(None:Vernacexpr.decl_notation)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> 
 		     error 
 		       ("Cannot use mutual definition with well-founded recursion")
@@ -417,7 +417,7 @@ let make_graph (id:identifier) =
 			 )
 		     in 
 		     let rec_id = 
-		       match List.nth nal n  with |(_,Name id) -> id | _ -> anomaly ""
+		       match List.nth nal (out_some n)  with |(_,Name id) -> id | _ -> anomaly ""
 		     in
 		     (id, Some (Struct rec_id),bl,t,b)
 		  )
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index da87086e29..a78c35d1dd 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -298,9 +298,11 @@ let rec decompose_last = function
 let make_fix_struct (n,bl) =
   let names = names_of_local_assums bl in
   let nn = List.length names in
-  if nn = 1 then ctv_ID_OPT_NONE
-  else if n < nn then xlate_id_opt(List.nth names n)
-  else xlate_error "unexpected result of parsing for Fixpoint";;
+  if nn = 1 || n = None then ctv_ID_OPT_NONE
+  else 
+    let n = out_some n in 
+    if n < nn then xlate_id_opt(List.nth names n)
+    else xlate_error "unexpected result of parsing for Fixpoint";;
 
 
 let rec xlate_binder = function
@@ -417,7 +419,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CFix (_, (_, id), lm::lmi) ->       
      let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
         let (struct_arg,bl,arf,ardef) =
+	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
+	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
          if bl = [] then
+	   let n = out_some n in 
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
@@ -1875,7 +1880,10 @@ let rec xlate_vernac =
    | VernacFixpoint ((lm :: lmi),boxed) ->
       let strip_mutrec ((fid, (n, ro), bl, arf, ardef), ntn) =
         let (struct_arg,bl,arf,ardef) =
+	 (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
+	 (* By the way, how could [bl = []] happen in V8 syntax ?  *)
          if bl = [] then
+	   let n = out_some n in 
            let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 1b92c69110..727ba82ae3 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -200,6 +200,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
 		  (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
 	    | CWfRec r -> 		    
+		let n = out_some n in 
 		let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
 			       Ppconstr.pr_binders bl ++ str " : " ++ 
 			       Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
@@ -279,7 +280,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 
   let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
     collect_non_rec env0 lrecnames recdef arityl nv in
-  let nvrec' = Array.map fst nvrec in(* ignore rec order *)
+  let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
   let declare arrec defrec =
     let recvec = 
       Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2057eb5b27..0be6b9dc6f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -793,7 +793,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
 		     RStructRec,
 		     List.fold_left intern_local_binder (env,[]) bl
 		 | CWfRec c -> 
-		     let before, after = list_chop (succ n) bl in
+		     let before, after = list_chop (succ (out_some n)) bl in
 		     let ((ids',_,_),rafter) =
 		       List.fold_left intern_local_binder (env,[]) after in
 		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4d4e3f88a0..d82c04e077 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -532,7 +532,7 @@ type constr_expr =
 
 
 and fixpoint_expr =
-    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 073f9ba0b3..4e2017f44d 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -114,7 +114,7 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+    identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
diff --git a/lib/util.ml b/lib/util.ml
index 33f91b04ee..8b0b1e2424 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -214,6 +214,16 @@ let list_index x =
   in 
   index_x 1
 
+let list_unique_index x = 
+  let rec index_x n = function
+    | y::l -> 
+	if x = y then 
+	  if List.mem x l then raise Not_found
+	  else n 
+	else index_x (succ n) l
+    | [] -> raise Not_found 
+  in index_x 1
+
 let list_fold_left_i f = 
   let rec it_list_f i a = function
     | [] -> a 
diff --git a/lib/util.mli b/lib/util.mli
index f330ef8e00..1a2fedbdfc 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -100,6 +100,8 @@ val list_map2_i :
 val list_map3 :
   ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
 val list_index : 'a -> 'a list -> int
+(* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+val list_unique_index : 'a -> 'a list -> int 
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9c39878c7d..ed9e1fa06d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -59,14 +59,13 @@ let rec mkCLambdaN loc bll c =
 
 let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
-    | [_], (None, r) -> 0, r
+    | [_], (None, r) -> Some 0, r
     | lids, (Some x, ro) ->
         let ids = List.map snd lids in
-        (try list_index (snd x) ids - 1, ro
+        (try Some (list_index (snd x) ids - 1), ro
         with Not_found ->
           user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
-    | _ -> user_err_loc(loc,"index_of_annot",
-      Pp.str "cannot guess decreasing argument of fix")
+    | _, (None, r) -> None, r
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 87f388a748..0a0df6fb21 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -218,16 +218,15 @@ GEXTEND Gram
           let ni =
             match fst annot with
                 Some id ->
-                  (try list_index (Name id) names - 1
-                  with Not_found ->  Util.user_err_loc
-                      (loc,"Fixpoint",
-                       Pp.str "No argument named " ++ Nameops.pr_id id))
+                  (try Some (list_index (Name id) names - 1)
+                   with Not_found ->  Util.user_err_loc
+                     (loc,"Fixpoint",
+                      Pp.str "No argument named " ++ Nameops.pr_id id))
               | None -> 
-                  if List.length names > 1 then
-                    Util.user_err_loc
-                      (loc,"Fixpoint",
-                       Pp.str "the recursive argument needs to be specified");
-                  0 in
+		  (* If there is only one argument, it is the recursive one, 
+		     otherwise, we search the recursive index later *)
+		  if List.length names = 1 then Some 0 else None	  
+	  in 
 	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
   ;
   corec_definition:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 1df3d1f256..8b3661dbe6 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -205,11 +205,11 @@ and interp_xml_recursionOrder x =
 and interp_xml_FixFunction x =
   match interp_xml_tag "FixFunction" x with
   | (loc,al,[x1;x2;x3]) ->
-      ((nmtoken (get_xml_attr "recIndex" al),
+      ((Some (nmtoken (get_xml_attr "recIndex" al)),
 	interp_xml_recursionOrder x1),
        (get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
   | (loc,al,[x1;x2]) -> (* For backwards compatibility *)
-      ((nmtoken (get_xml_attr "recIndex" al), RStructRec),
+      ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
        (get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
   | (loc,_,_) -> 
         user_err_loc (loc,"",str "wrong number of arguments (expect one)")
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a95fa4bad8..e4cc3cd916 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
     let ids = names_of_local_assums bl in
       match ro with
 	  CStructRec ->
-	    if List.length ids > 1 then 
-	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+	    if List.length ids > 1 && n <> None then 
+	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
 	    else mt() 
 	| CWfRec c ->
-	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}"
+	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c08b076173..f43f93bd90 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -555,18 +555,23 @@ let rec pr_vernac = function
               else ([],def,type_) in
             let bl = bl @ bl' in
             let ids = List.flatten (List.map name_of_binder bl) in
-            let name =
-              try snd (List.nth ids n)
-              with Failure _ ->
-                warn (str "non-printable fixpoint \""++pr_id id++str"\"");
-                Anonymous in
             let annot =
-	      match (ro : Topconstr.recursion_order_expr) with
-		  CStructRec -> 
-		    if List.length ids > 1 then 
-                      spc() ++ str "{struct " ++ pr_name name ++ str"}"
-		    else mt()
-		| CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}"
+	      match n with 
+		| None -> mt () 
+		| Some n -> 
+		    let name =
+		      try snd (List.nth ids n)
+		      with Failure _ ->
+			warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+			Anonymous in
+		    match (ro : Topconstr.recursion_order_expr) with
+			CStructRec -> 
+			  if List.length ids > 1 then 
+			    spc() ++ str "{struct " ++ pr_name name ++ str"}"
+			  else mt()
+		      | CWfRec c -> 
+			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
+			    pr_lconstr_expr c ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a815e5d2f8..edbbbb3294 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -421,7 +421,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  RRec(dl,RFix (Array.map (fun i -> i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+  RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f48ec74624..64ea0bbb88 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -329,18 +329,35 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
-	  evar_type_fixpoint loc env isevars names ftys vdefj;
-	  let fixj =
-	    match fixkind with
-	      | RFix (vn,i) ->
-		  let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in
-		    (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-		    make_judge (mkFix fix) ftys.(i)
-	      | RCoFix i -> 
-		  let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
-		    (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
-		    make_judge (mkCoFix cofix) ftys.(i) in
-	    inh_conv_coerce_to_tycon loc env isevars fixj tycon
+	evar_type_fixpoint loc env isevars names ftys vdefj;
+	let fixj = match fixkind with
+	  | RFix (vn,i) ->
+	      let guard_indexes = Array.mapi 
+		(fun i (n,_) -> match n with 
+		   | Some n -> n 
+		   | None -> 
+		       (* Recursive argument was not given by the user : We
+			  check that there is only one inductive argument *)
+		       let ctx = ctxtv.(i) in 
+		       let isIndApp t = 
+			 isInd (fst (decompose_app (strip_head_cast t))) in
+			 (* This could be more precise (e.g. do some delta) *)
+		       let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+		       try (list_unique_index true lb) - 1
+		       with Not_found -> 
+			 Util.user_err_loc
+			   (loc,"pretype",
+			    Pp.str "cannot guess decreasing argument of fix"))
+		vn 
+	      in
+	      let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
+	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
+	      make_judge (mkFix fix) ftys.(i)
+	  | RCoFix i -> 
+	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+	      make_judge (mkCoFix cofix) ftys.(i) in
+	inh_conv_coerce_to_tycon loc env isevars fixj tycon
 
     | RSort (loc,s) ->
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 1c59004175..36edf519bd 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -73,7 +73,7 @@ and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index cbd215d85e..8ef0cb9397 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -70,7 +70,7 @@ and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
 
 val cases_predicate_names : 
   (rawconstr * (name * (loc * inductive * name list) option)) list -> name list
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b103b83824..b70cfb62f1 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -457,7 +457,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and sigma = Evd.empty
   and env0 = Global.env()
-  and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) in
+  and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef)
+  and bl = Array.of_list (List.map (fun ((_,_,bl,_,_),_) -> bl) lnameargsardef) 
+  in 
   (* Build the recursive context and notations for the recursive types *)
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
@@ -502,9 +504,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
   let recvec = 
     Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
   let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
+  let nvrec = Array.mapi 
+    (fun i (n,_) -> match n with 
+       | Some n -> n 
+       | None -> 
+	   (* Recursive argument was not given by the user : 
+	      We check that there is only one inductive argument *)
+	   let ctx = snd (interp_context sigma env0 bl.(i)) in 
+	   let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in 
+	   (* This could be more precise (e.g. do some delta) *)
+	   let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+	   try (list_unique_index true lb) - 1
+	   with Not_found -> 
+	     error "the recursive argument needs to be specified")
+    nvrec
+  in  
   let rec declare i fi =
     let ce = 
-      { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
+      { const_entry_body = mkFix ((nvrec,i),recdecls); (* ignore rec order *)
         const_entry_type = Some arrec.(i);
         const_entry_opaque = false;
         const_entry_boxed = boxed} in