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

4 files changed, 32 insertions, 15 deletions

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