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

3 files changed, 67 insertions, 70 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index b98be6c6c7..2825344e45 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -76,7 +76,7 @@ let pr_notation pr s env =
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let surround p = str"(" ++ p ++ str")"
+let surround p = hov 1 (str"(" ++ p ++ str")")
 
 let pr_located pr ((b,e),x) =
   if Options.do_translate() && (b,e)<>dummy_loc then
@@ -350,24 +350,15 @@ let pr_recursive_decl pr id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr ltop) c
 
-let name_of_binder = function
-  | LocalRawAssum (nal,_) -> nal
-  | LocalRawDef (_,_) -> []
-
-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
-    if List.length ids <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
+let pr_fixdecl pr (id,n,bl,t,c) =
   let annot =
-    let ids = List.flatten (List.map name_of_binder bl) in
+    let ids = names_of_local_assums bl in
     if List.length ids > 1 then 
       spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
     else mt() in
   pr_recursive_decl pr id bl annot t c
 
-let pr_cofixdecl pr (id,t,c) =
-  let (bl,c,t) = extract_def_binders c t in
+let pr_cofixdecl pr (id,bl,t,c) =
   pr_recursive_decl pr id bl (mt()) t c
 
 let pr_recursive pr_decl id = function
@@ -588,6 +579,20 @@ let rec pr sep inherited a =
 
 let pr = pr mt
 
+let rec abstract_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+      (abstract_constr_expr c bl)
+      
+let rec prod_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+      (prod_constr_expr c bl)
+
 let rec strip_context n iscast t =
   if n = 0 then
     [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
@@ -619,12 +624,15 @@ let rec strip_context n iscast t =
 	LocalRawDef (na,b) :: bl', c
     | _ -> anomaly "ppconstrnew: strip_context"
 
-let transf istype env n iscast c =
+let transf istype env iscast bl c =
+  let c' =
+    if istype then abstract_constr_expr c bl 
+    else prod_constr_expr c bl in
   if Options.do_translate() then
     let r = 
       Constrintern.for_grammar
         (Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[]))
-	c in
+	c' in
     begin try
       (* Try to infer old case and type annotations *)
       let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in 
@@ -634,11 +642,12 @@ let transf istype env n iscast c =
       (if istype then Constrextern.extern_rawtype
       else Constrextern.extern_rawconstr)
       (Termops.vars_of_env env) r in
+    let n = local_binders_length bl in
     strip_context n iscast c
-  else [], c
+  else bl, c
 
-let pr_constr_env env c = pr lsimple (snd (transf false env 0 false c))
-let pr_lconstr_env env c = pr ltop (snd (transf false env 0 false c))
+let pr_constr_env env c = pr lsimple (snd (transf false env false [] c))
+let pr_lconstr_env env c = pr ltop (snd (transf false env false [] c))
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
@@ -658,10 +667,11 @@ let is_Eval_key c =
 let pr_protect_eval c =
   if is_Eval_key c then h 0 (str "(" ++ pr ltop c ++ str ")") else pr ltop c
 
-let pr_lconstr_env_n env n b c =
-  let bl, c = transf false env n b c in bl, pr_protect_eval c
-let pr_type_env_n env n c = pr ltop (snd (transf true env n false c))
-let pr_type c = pr ltop (snd (transf true (Global.env()) 0 false c))
+let pr_lconstr_env_n env iscast bl c =
+  let bl, c = transf false env iscast bl c in
+  bl, pr_protect_eval c
+let pr_type_env_n env bl c = pr ltop (snd (transf true env false bl c))
+let pr_type c = pr ltop (snd (transf true (Global.env()) false [] c))
 
 let transf_pattern env c =
   if Options.do_translate() then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 542549f74e..2b79c6b71b 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -65,14 +65,17 @@ val pr_constr : constr_expr -> std_ppcmds
 val pr_lconstr : constr_expr -> std_ppcmds
 val pr_constr_env : env -> constr_expr -> std_ppcmds
 val pr_lconstr_env : env -> constr_expr -> std_ppcmds
-val pr_lconstr_env_n : env -> int -> bool -> constr_expr -> 
+val pr_lconstr_env_n : env -> bool -> local_binder list -> constr_expr -> 
   local_binder list * std_ppcmds
-val pr_type_env_n : env -> int -> constr_expr -> std_ppcmds
+val pr_type_env_n : env -> local_binder list -> constr_expr -> std_ppcmds
 val pr_type : constr_expr -> std_ppcmds
 val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
     -> std_ppcmds
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
 
 val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
 val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index cfeb12f06c..2fd54a006a 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -259,7 +259,8 @@ let pr_module_vardecls pr_c (idl,mty) =
       [make_mbid lib_dir (string_of_id id),
        Modintern.interp_modtype (Global.env()) mty]) idl;
   (* Builds the stream *)
-  spc() ++ str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")"
+  spc() ++
+  hov 1 (str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
 
 let pr_module_binders l pr_c = 
   (* Effet de bord complexe pour garantir la declaration des noms des
@@ -275,7 +276,8 @@ let rec pr_module_expr = function
   | CMEapply (me1,(CMEident _ as me2)) ->
       pr_module_expr me1 ++ spc() ++ pr_module_expr me2
   | CMEapply (me1,me2) ->
-      pr_module_expr me1 ++ spc() ++ str"(" ++ pr_module_expr me2 ++ str")"
+      pr_module_expr me1 ++ spc() ++
+      hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
 
 (*
 let pr_opt_casted_constr pr_c = function
@@ -285,7 +287,7 @@ let pr_opt_casted_constr pr_c = function
 
 let pr_type_option pr_c = function
   | CHole loc -> mt()
-  | _ as c -> str":" ++ pr_c c
+  | _ as c -> brk(0,2) ++ str":" ++ pr_c c
 
 let without_translation f x =
   let old = Options.do_translate () in
@@ -299,20 +301,6 @@ let pr_decl_notation prc =
     str "where " ++ qsnew ntn ++ str " := " ++ without_translation prc c ++
     pr_opt (fun sc -> str ": " ++ str sc) scopt)
 
-let rec abstract_rawconstr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
-      (abstract_rawconstr c bl)
-      
-let rec prod_rawconstr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-      (prod_rawconstr c bl)
-
 let pr_vbinders l =
   hv 0 (pr_binders l)
 
@@ -320,9 +308,7 @@ let pr_binders_arg =
   pr_ne_sep spc pr_binders
 
 let pr_and_type_binders_arg bl =
-  let n = local_binders_length bl in
-  let c = abstract_rawconstr (CHole dummy_loc) bl in
-  let bl, _ = pr_lconstr_env_n (Global.env()) n false c in
+  let bl, _ = pr_lconstr_env_n (Global.env()) false bl (CHole dummy_loc) in
   pr_binders_arg bl
 
 let pr_onescheme (id,dep,ind,s) =
@@ -369,7 +355,8 @@ let pr_ne_params_list pr_c l =
   match factorize l with
     | [p] -> pr_params pr_c p
     | l ->
-	prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")") l
+	prlist_with_sep spc
+          (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
 (*
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
@@ -403,7 +390,7 @@ let pr_syntax_modifier = function
 let pr_syntax_modifiers = function
   | [] -> mt()
   | l -> spc() ++ 
-      hov 0 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+      hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
 let pr_grammar_tactic_rule (name,(s,pil),t) =
 (*
@@ -619,14 +606,10 @@ let rec pr_vernac = function
                   (bl2,CCast (dummy_loc,body,ty'),
                    spc() ++ str":" ++
                    pr_sep_com spc
-                     (pr_type_env_n (Global.env())
-                       (local_binders_length bl + local_binders_length bl2))
-                     (prod_rawconstr ty bl)) in
-	    let n = local_binders_length bl + local_binders_length bl2 in
+                     (pr_type_env_n (Global.env()) (bl@bl2)) ty') in
 	    let iscast = d <> None in
             let bindings,ppred =
-	      pr_lconstr_env_n (Global.env()) n iscast
-		(abstract_rawconstr (abstract_rawconstr body bl2) bl) in
+	      pr_lconstr_env_n (Global.env()) iscast (bl@bl2) body in
             (pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
         | ProveBody (bl,t) ->
             (pr_and_type_binders_arg bl, str" :" ++ pr_spc_type t, None)
@@ -720,7 +703,7 @@ let rec pr_vernac = function
       let pr_constructor (coe,(id,c)) =
         hov 2 (pr_lident id ++ str" " ++
                (if coe then str":>" else str":") ++
-                pr_sep_com spc (pr_type_env_n ind_env_params 0) c) in
+                pr_sep_com spc (pr_type_env_n ind_env_params []) c) in
       let pr_constructor_list l = match l with
         | [] -> mt()
         | _ ->
@@ -754,8 +737,10 @@ 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,_),_) -> 
-          let arity = Constrintern.interp_type sigma env0 arityc in
+        (fun ((recname,_, bl, arityc,_),_) -> 
+          let arity =
+            Constrintern.interp_type sigma env0
+              (prod_constr_expr arityc bl) in
 	  let impl_in =
 	    if Impargs.is_implicit_args()
 	    then Impargs.compute_implicits false env0 arity
@@ -776,8 +761,10 @@ let rec pr_vernac = function
 
       let rec_sign = 
         List.fold_left 
-          (fun env ((recname,_,_,arityc,_),_) -> 
-            let arity = Constrintern.interp_type sigma env0 arityc in
+          (fun env ((recname,_,bl,arityc,_),_) -> 
+            let arity =
+              Constrintern.interp_type sigma env0
+                (prod_constr_expr arityc bl) in
             Environ.push_named (recname,None,arity) env)
           (Global.env()) recs in
       
@@ -785,21 +772,19 @@ let rec pr_vernac = function
         | LocalRawAssum (nal,_) -> nal
         | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | (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_) =
-              if List.length ids <= n then split_fix (n+1) def0 type_0
-              else (bl,def,type_) in
+        | (id,n,bl,type_,def),ntn ->
             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 =
               if List.length ids > 1 then 
-                spc() ++ str "{struct " ++
-                pr_name (snd (List.nth ids n)) ++ str"}"
+                spc() ++ str "{struct " ++ pr_name name ++ str"}"
               else mt() in
-	    let bl, ppc = 
-              pr_lconstr_env_n rec_sign (local_binders_length bl)
-		true (abstract_rawconstr (CCast (dummy_loc,def,type_)) bl) in
+	    let bl,ppc =
+              pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_type c) type_
             ++ str" :=" ++ brk(1,1) ++ ppc ++ 
@@ -809,8 +794,7 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint corecs ->
-      let pr_onecorec (id,c,def) =
-        let (bl,def,c) = extract_def_binders def c in
+      let pr_onecorec (id,bl,c,def) =
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_type c ++
         str" :=" ++ brk(1,1) ++ pr_lconstr def in