Keep structure information for Fixpoint declaration and Fix terms

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

14 files changed, 39 insertions, 30 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ee85a81635..64b5539f17 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -293,6 +293,11 @@ let rec decompose_last = function
   | [a] -> [], a
   | a::tl -> let rl, b = decompose_last tl in (a::rl), b;;
 
+(* The boolean argument should be false if a name is not really necessary, 
+   for instance if there is only one argument.  On the other hand, all
+   recursive calls in this function should have the boolean argument to true,
+   because recursive calls mean that there is more than one argument. *)
+
 let rec make_fix_struct b = function
     0, CProdN(_, [(na::tl,_)], CProdN(_, _,_)) -> xlate_id_opt na
   | 0, CProdN(_, [([na],_)], _) ->
@@ -430,9 +435,12 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
         CT_cofixc(xlate_ident id,
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
-     let strip_mutrec (fid, n, arf, ardef) =
+     let strip_mutrec (fid, n, optional_nargs, arf, ardef) =
        let struct_arg = make_fix_struct false (n, arf) in
-        let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+       let split_rank = match optional_nargs with
+	   Some v -> v
+	 | None -> n+1 in
+        let (bl,arf,ardef) = Ppconstr.split_fix split_rank arf ardef in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match cvt_fixpoint_binders bl with
@@ -1870,13 +1878,12 @@ let rec xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
-      let strip_mutrec ((fid, n, arf, ardef), ntn) =
-(* The boolean argument should be false if a name is not really necessary, 
-   for instance if there is only one argument.  On the other hand, all
-   recursive calls in this function should have the boolean argument to true,
-   because recursive calls mean that there is more than one argument. *)
+      let strip_mutrec ((fid, n, optional_nargs, arf, ardef), ntn) =
 	let struct_arg = make_fix_struct false (n, arf) in
-        let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+	let split_rank = match optional_nargs with
+	    Some v -> v
+	  | None -> n+1 in
+        let (bl,arf,ardef) = Ppconstr.split_fix split_rank arf ardef in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
 	match cvt_fixpoint_binders bl with
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e28065afd8..fa1faf9cf3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1009,7 +1009,7 @@ let rec check_same_type ty1 ty2 =
   match ty1, ty2 with
   | CRef r1, CRef r2 -> check_same_ref r1 r2
   | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
-      List.iter2 (fun (id1,i1,a1,b1) (id2,i2,a2,b2) ->
+      List.iter2 (fun (id1,i1,_,a1,b1) (id2,i2,_,a2,b2) ->
         if id1<>id2 || i1<>i2 then failwith "not same fix";
         check_same_type a1 a2;
         check_same_type b1 b2)
@@ -1508,7 +1508,7 @@ let rec extern inctx scopes vars r =
 	 | RFix (nv,n) ->
 	     let listdecl = 
 	       Array.mapi (fun i fi ->
-		 (fi,nv.(i),extern_type scopes vars tyv.(i),
+		 (fi,nv.(i), None, extern_type scopes vars tyv.(i),
                   extern false scopes vars' bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c6a819d440..bfd74a5aa2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -528,7 +528,7 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
 
 let rec intern_fix = function
   | [] -> ([],[],[],[])
-  | (fi, n, c, t)::rest->
+  | (fi, n, on, c, t)::rest->
       let (lf,ln,lc,lt) = intern_fix rest in
       (fi::lf, n::ln, c::lc, t::lt)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7dda9a3175..3d26e9d7f8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -361,7 +361,7 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr = identifier * int * constr_expr * constr_expr
+and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
 
 and cofixpoint_expr = identifier * constr_expr * constr_expr
 
@@ -518,7 +518,7 @@ let map_constr_expr_with_binders f g e = function
       let e' = option_fold_right (name_fold g) ona e in
       CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
-      CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl)
+      CFix (loc,id,List.map (fun (id,n,on,t,d) -> (id,n,on,f e t,f e d)) dl)
   | CCoFix (loc,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index c6be360284..d35418b515 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -107,7 +107,7 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr = identifier * int * constr_expr * constr_expr
+and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
 
 and cofixpoint_expr = identifier * constr_expr * constr_expr
 
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 533919b676..8e3820c3a5 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -237,7 +237,7 @@ let subst_constr_expr a loc subs =
       let na = option_app (name_app (subst_id subs)) na in
       CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
   | CFix (_,id,dl) ->
-      CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl)
+      CFix (loc,id,List.map (fun (id,n,on, t,d) -> (id,n, on,subst t,subst d)) dl)
   | CCoFix (_,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
   in subst a
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4e0d1118f3..3e513f0719 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -339,14 +339,14 @@ GEXTEND Gram
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
-          (id, recarg-1, type_, def)
+          (id, recarg-1, None, type_, def)
       | id = base_ident; bl = ne_simple_binders_list; ":"; type_ = constr;
 	":="; def = constr ->
           let ni = List.length (List.flatten (List.map fst bl)) -1 in
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  (id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+	  (id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
   ;
   fixbinders:
     [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 101c29d31f..fb770768a9 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -84,10 +84,11 @@ let rec index_of_annot bl ann =
 
 let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
   let n = index_of_annot bl ann in
+  let nargs = List.length (decls_of_binders bl) in
   let ty = match tyc with
       None -> CHole tloc
     | Some t -> mkCProdN loc bl t in
-  (snd id,n,ty,mkCLambdaN loc bl body)
+  (snd id,n,Some nargs,ty,mkCLambdaN loc bl body)
 
 let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ad3862388e..def4b9fbf9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -255,7 +255,7 @@ GEXTEND Gram
           let loc0 = fst (List.hd (fst (List.hd bl))) in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
+	  ((id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index c7fdcdc576..fd4647a620 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -205,6 +205,7 @@ GEXTEND Gram
         annot = OPT rec_annotation; type_ = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (G_constrnew.decls_of_binders bl) in
+	  let nargs = List.length names in
           let ni =
             match annot with
                 Some id ->
@@ -221,7 +222,7 @@ GEXTEND Gram
           let loc0 = G_constrnew.loc_of_binder_let bl in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  ((id, ni, G_constrnew.mkCProdN loc1 bl type_,
+	  ((id, ni, Some nargs, G_constrnew.mkCProdN loc1 bl type_,
 	    G_constrnew.mkCLambdaN loc2 bl def),ntn) ] ]
   ;
   corec_definition:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index cdc7cc6f76..77853c5e1a 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -155,7 +155,7 @@ let rec split_fix n typ def =
     let (bl,typ,def) = split_fix (n-1) typ def in
     (concat_binder na t bl,typ,def)
 
-let pr_fixdecl pr (id,n,t,c) =
+let pr_fixdecl pr (id,n,_,t,c) =
   let (bl,t,c) = split_fix (n+1) t c in
   pr_recursive_decl pr id 
     (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5c0b5818c5..46de560b46 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -447,16 +447,16 @@ let collect_non_rec env =
   in 
   searchrec [] 
 
-let build_recursive lnameargsardef =
-  let lrecnames = List.map (fun ((f,_,_,_),_) -> f) lnameargsardef 
+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) in
   let fs = States.freeze() in
   (* Declare the notations for the recursive types pushed in local context*)
   let (rec_sign,arityl) = 
     List.fold_left 
-      (fun (env,arl) ((recname,_,arityc,_),_) -> 
+      (fun (env,arl) ((recname,_,_,arityc,_),_) -> 
         let arity = interp_type sigma env0 arityc in
         (Environ.push_named (recname,None,arity) env, (arity::arl)))
       (env0,[]) lnameargsardef in
@@ -479,7 +479,7 @@ let build_recursive lnameargsardef =
 	      (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
 	    ()) lrecnames arityl;
 	List.map2
-	  (fun ((_,_,_,def),_) arity ->
+	  (fun ((_,_,_,_,def),_) arity ->
             interp_casted_constr sigma rec_sign def arity)
           lnameargsardef arityl
       with e ->
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 9b2faf4ba9..b98be6c6c7 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -354,7 +354,7 @@ let name_of_binder = function
   | LocalRawAssum (nal,_) -> nal
   | LocalRawDef (_,_) -> []
 
-let pr_fixdecl pr (id,n,t0,c0) =
+let pr_fixdecl pr (id,n,_,t0,c0) =
   let (bl,c,t) = extract_def_binders c0 t0 in
   let (bl,t,c) =
     let ids = List.flatten (List.map name_of_binder bl) in
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 85dae24ae3..44599e72f5 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -755,7 +755,7 @@ let rec pr_vernac = function
       let notations = 
 	List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) recs [] in
       let impl = List.map
-        (fun ((recname,_,arityc,_),_) -> 
+        (fun ((recname,_, _, arityc,_),_) -> 
           let arity = Constrintern.interp_type sigma env0 arityc in
 	  let impl_in =
 	    if Impargs.is_implicit_args()
@@ -777,7 +777,7 @@ let rec pr_vernac = function
 
       let rec_sign = 
         List.fold_left 
-          (fun env ((recname,_,arityc,_),_) -> 
+          (fun env ((recname,_,_,arityc,_),_) -> 
             let arity = Constrintern.interp_type sigma env0 arityc in
             Environ.push_named (recname,None,arity) env)
           (Global.env()) recs in
@@ -786,7 +786,7 @@ let rec pr_vernac = function
         | LocalRawAssum (nal,_) -> nal
         | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | (id,n,type_0,def0),ntn ->
+        | (id,n,_,type_0,def0),ntn ->
             let (bl,def,type_) = extract_def_binders def0 type_0 in
             let ids = List.flatten (List.map name_of_binder bl) in
             let (bl,def,type_) =