modif des fixpoints pour que si on donne une notation au produit, les pts fixes s'affichent correctement

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

7 files changed, 114 insertions, 56 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 27f52e73a1..c8f167eb3b 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -237,9 +237,19 @@ 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,on, t,d) -> (id,n, on,subst t,subst d)) dl)
+      CFix (loc,id,List.map (fun (id,n,bl, t,d) ->
+        (id,n,
+         List.map(function
+             LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
+           | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
+         subst t,subst d)) dl)
   | CCoFix (_,id,dl) ->
-      CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
+      CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+        (id,
+         List.map(function
+             LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
+           | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
+         subst t,subst d)) dl)
   in subst a
 
 let make_rule univ assoc etyp rule =
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e513f0719..2f606ffd30 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -339,21 +339,19 @@ GEXTEND Gram
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
-          (id, recarg-1, None, type_, def)
+          (id, recarg-1, [], 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, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+          let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+	  (id, ni, bl, type_, def) ] ]
   ;
   fixbinders:
     [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
   ;
   cofixbinder:
     [ [ id = base_ident; ":"; type_ = constr; ":="; def = constr ->
-          (id, type_, def) ] ]
+          (id, [],type_, def) ] ]
   ;
   cofixbinders:
     [ [ fbs = LIST1 cofixbinder SEP "with" -> fbs ] ]
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index fb770768a9..606949e5f9 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -68,37 +68,33 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
-let rec decls_of_binders = function
-  | [] -> []
-  | LocalRawDef _::bl -> decls_of_binders bl
-  | LocalRawAssum (idl,_)::bl -> idl @ decls_of_binders bl
-
-let rec index_of_annot bl ann =
-  match decls_of_binders bl,ann with
+let rec index_of_annot loc bl ann =
+  match names_of_local_assums bl,ann with
     | [_], None -> 0
     | lids, Some x ->
         let ids = List.map snd lids in
         (try list_index (snd x) ids - 1
-        with Not_found -> error "no such fix variable")
-    | _ -> error "cannot guess decreasing argument of fix"
+        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")
 
-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 mk_fixb (id,bl,ann,body,(loc,tyc)) =
+  let n = index_of_annot (fst id) bl ann in
   let ty = match tyc with
-      None -> CHole tloc
-    | Some t -> mkCProdN loc bl t in
-  (snd id,n,Some nargs,ty,mkCLambdaN loc bl body)
+      Some ty -> ty
+    | None -> CHole loc in
+  (snd id,n,bl,ty,body)
 
-let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
+let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
        Pp.str"Annotation forbidden in cofix expression")) ann in
   let ty = match tyc with
-      None -> CHole tloc
-    | Some t -> mkCProdN loc bl t in
-  (snd id,ty,mkCLambdaN loc bl body)
+      Some ty -> ty
+    | None -> CHole loc in
+  (snd id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
   if kw then 
@@ -109,7 +105,7 @@ let mk_fix(loc,kw,id,dcls) =
     CCoFix(loc,id,fb)
 
 let mk_single_fix (loc,kw,dcl) =
-  let (_,id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
+  let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
 
 let binder_constr =
   create_constr_entry (get_univ "constr") "binder_constr"
@@ -255,7 +251,7 @@ GEXTEND Gram
   ;
   fix_decl:
     [ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":=";
-        c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ]
+        c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ]
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index def4b9fbf9..cde9061b3d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -252,17 +252,15 @@ GEXTEND Gram
     [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
         ":="; def = constr; ntn = OPT decl_notation ->
           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, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
+          let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+	  ((id, ni, bl, type_, def), ntn) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
   ;
   onecorec:
     [ [ id = base_ident; ":"; c = constr; ":="; def = constr ->
-          (id,c,def) ] ]
+          (id,[],c,def) ] ]
   ;
   specifcorec:
     [ [ l = LIST1 onecorec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 70235d9ecf..75222eaa43 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -204,8 +204,7 @@ GEXTEND Gram
     [ [ id = base_ident; bl = LIST1 binder_let;
         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 names = List.map snd (names_of_local_assums bl) in
           let ni =
             match annot with
                 Some id ->
@@ -219,17 +218,12 @@ GEXTEND Gram
                       (loc,"Fixpoint",
                        Pp.str "the recursive argument needs to be specified");
                   0 in
-          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, Some nargs, G_constrnew.mkCProdN loc1 bl type_,
-	    G_constrnew.mkCLambdaN loc2 bl def),ntn) ] ]
+	  ((id, ni, bl, type_, def),ntn) ] ]
   ;
   corec_definition:
     [ [ id = base_ident; bl = LIST0 binder_let; c = type_cstr; ":=";
         def = lconstr ->
-          (id,G_constrnew.mkCProdN loc bl c ,
-	   G_constrnew.mkCLambdaN loc bl def) ] ]
+          (id,bl,c ,def) ] ]
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 77853c5e1a..335d3b7964 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -110,6 +110,13 @@ let pr_binder pr (nal,t) =
 let pr_binders pr bl =
   hv 0 (prlist_with_sep pr_semicolon (pr_binder pr) bl)
 
+let pr_local_binder pr = function
+    LocalRawAssum(nal,t) -> pr_binder pr (nal,t)
+  | LocalRawDef((_,na),t) -> pr_let_binder pr na t
+
+let pr_local_binders pr bl =
+  hv 0 (prlist_with_sep pr_semicolon (pr_local_binder pr) bl)
+
 let pr_global vars ref = pr_global_env vars ref
 
 let rec pr_lambda_tail pr bll = function
@@ -155,13 +162,15 @@ 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 (bl,t,c) = split_fix (n+1) t c in
+let pr_fixdecl pr (id,n,bl,t,c) =
   pr_recursive_decl pr id 
-    (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
+    (brk (1,2) ++ str "[" ++ pr_local_binders pr bl ++ str "]") t c
 
-let pr_cofixdecl pr (id,t,c) =
-  pr_recursive_decl pr id (mt ()) t c
+let pr_cofixdecl pr (id,bl,t,c) =
+  let  b =
+    if bl=[] then mt() else
+      brk(1,2) ++ str"[" ++ pr_local_binders pr bl ++ str "]" in
+  pr_recursive_decl pr id b t c
 
 let pr_recursive fix pr_decl id = function
   | [] -> anomaly "(co)fixpoint with no definition"
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0e8b84f741..8f00678f1e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -95,6 +95,29 @@ let idopt_of_name = function
   | Name id -> Some id
   | Anonymous -> None
 
+let ast_of_binders bl =
+  List.map (fun (nal,isdef,ty) ->
+    if isdef then ope("LETBINDER",ty::List.map ast_of_name nal)
+    else ope("BINDER",ty::List.map ast_of_name nal)) bl
+
+let ast_type_of_binder bl t =
+  List.fold_right (fun (nal,isdef,ty) ast ->
+    if isdef then
+      ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
+    else
+      ope("PROD",[ty;List.fold_right
+        (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
+    bl t
+
+let ast_body_of_binder bl t =
+  List.fold_right (fun (nal,isdef,ty) ast ->
+    if isdef then
+      ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
+    else
+      ope("LAMBDA",[ty;List.fold_right
+        (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
+    bl t
+
 let ast_of_constant_ref sp =
   ope("CONST", [path_section dummy_loc sp])
 
@@ -259,12 +282,12 @@ let rec ast_of_raw = function
   | RLetTuple _ | RIf _ ->
       error "Let tuple not supported in v7"
 
-  | RRec (_,fk,idv,tyv,bv) ->
+  | RRec (_,fk,idv,blv,tyv,bv) ->
       let alfi = Array.map ast_of_ident idv in
       (match fk with
 	 | RFix (nv,n) ->
              let rec split_lambda binds = function
-	       | (0, t) -> (binds,ast_of_raw t)
+	       | (0, t) -> (List.rev binds,ast_of_raw t)
 	       | (n, RLetIn (_,na,b,c)) ->
 		   let bind = ope("LETBINDER",[ast_of_raw b;ast_of_name na]) in
 		   split_lambda (bind::binds) (n,c)
@@ -280,11 +303,26 @@ let rec ast_of_raw = function
 	     let listdecl = 
 	       Array.mapi
 		 (fun i fi ->
-		    let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
-		    let asttyp = split_product (nv.(i)+1,tyv.(i)) in
-		    ope("FDECL",
-		       	[fi; ope ("BINDERS",List.rev lparams); 
-			 asttyp; astdef]))
+                   if List.length blv.(i) >= nv.(i)+1 then
+                     let (oldfixp,factb) = list_chop (nv.(i)+1) blv.(i) in
+                     let bl = factorize_local_binder oldfixp in
+                     let factb = factorize_local_binder factb in
+                     let asttyp = ast_type_of_binder factb
+                       (ast_of_raw tyv.(i)) in
+                     let astdef = ast_body_of_binder factb
+                       (ast_of_raw bv.(i)) in
+                     ope("FDECL",[fi;ope("BINDERS",ast_of_binders bl);
+                                  asttyp; astdef])
+                   else
+                     let n = nv.(i)+1 - List.length blv.(i) in
+		     let (lparams,astdef) =
+                       split_lambda [] (n,bv.(i)) in
+                     let bl = factorize_local_binder blv.(i) in
+                     let lparams = ast_of_binders bl @ lparams in
+		     let asttyp = split_product (n,tyv.(i)) in
+		     ope("FDECL",
+		         [fi; ope ("BINDERS",lparams); 
+		          asttyp; astdef]))
 		 alfi
 	     in 
 	     ope("FIX", alfi.(n)::(Array.to_list listdecl))
@@ -292,7 +330,10 @@ let rec ast_of_raw = function
 	     let listdecl =
                Array.mapi 
 		 (fun i fi ->
-		    ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
+                   let bl = factorize_local_binder blv.(i) in
+                   let asttyp = ast_type_of_binder bl (ast_of_raw tyv.(i)) in
+                   let astdef = ast_body_of_binder bl (ast_of_raw bv.(i)) in
+		   ope("CFDECL",[fi; asttyp; astdef]))
 		 alfi
 	     in 
 	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
@@ -325,6 +366,18 @@ and factorize_binder n oper na aty c =
   in
   (p,slam(idopt_of_name na, body))
 
+and factorize_local_binder = function
+    [] -> []
+  | (na,Some bd,ty)::l ->
+      ([na],true,ast_of_raw bd) :: factorize_local_binder l
+  | (na,None,ty)::l ->
+      let ty = ast_of_raw ty in
+      (match factorize_local_binder l with
+          (lna,false,ty') :: l when ty=ty' ->
+            (na::lna,false,ty') :: l
+        | l -> ([na],false,ty) :: l)
+
+
 let ast_of_rawconstr = ast_of_raw
 
 (******************************************************************)