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

3 files changed, 16 insertions, 7 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