Factorisation des produits de même type; parenthèses autour des x:=c et n:=c dans les 'with bindings'; mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2)

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

5 files changed, 105 insertions, 34 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 96c65b54c..aa1c3af11 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -92,7 +92,7 @@ let pr_expl_args pr (a,expl) =
 
 let pr_opt_type pr = function
   | CHole _ -> mt ()
-  | t -> cut () ++ str ":" ++ pr ltop t
+  | t -> cut () ++ str ":" ++ pr (if !Options.p1 then ltop else (latom,E)) t
 
 let pr_opt_type_spc pr = function
   | CHole _ -> mt ()
@@ -136,16 +136,64 @@ let pr_binder pr (nal,t) =
     prlist_with_sep sep (pr_located pr_name) nal ++
     pr_opt_type pr t)
 *)
+(* Option 1a *)
 let pr_oneb pr t na =
   match t with
       CHole _ -> pr_located pr_name na
     | _ -> hov 1
         (str "(" ++  pr_located pr_name na ++ pr_opt_type pr t ++ str ")")
-let pr_binder pr (nal,t) =
+let pr_binder1 pr (nal,t) =
   hov 0 (prlist_with_sep sep (pr_oneb pr t) nal)
 
-let pr_binders pr bl =
-  hv 0 (prlist_with_sep sep (pr_binder pr) bl)
+let pr_binders1 pr bl =
+  hv 0 (prlist_with_sep sep (pr_binder1 pr) bl)
+
+(* Option 1b *)
+let pr_binder1 pr (nal,t) =
+  match t with
+      CHole _ -> prlist_with_sep sep (pr_located pr_name) nal
+    | _ -> hov 1
+	(str "(" ++ prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++
+	 pr ltop t ++ str ")")
+
+let pr_binders1 pr bl =
+  hv 0 (prlist_with_sep sep (pr_binder1 pr) bl)
+
+let pr_opt_type' pr = function
+  | CHole _ -> mt ()
+  | t -> cut () ++ str ":" ++ pr (latom,E) t
+
+let pr_prod_binders1 pr = function
+(*  | [nal,t] -> hov 1 (prlist_with_sep sep (pr_located pr_name) nal ++ pr_opt_type' pr t)*)
+  | bl -> pr_binders1 pr bl
+
+(* Option 2 *)
+let pr_let_binder pr x a =
+  hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a)
+
+let pr_binder2 pr (nal,t) =
+  hov 0 (
+    prlist_with_sep sep (pr_located pr_name) nal ++
+    pr_opt_type pr t)
+
+let pr_binders2 pr bl =
+  hv 0 (prlist_with_sep sep (pr_binder2 pr) bl)
+
+let pr_prod_binder2 pr (nal,t) =
+  str "for " ++ hov 0 (
+    prlist_with_sep sep (pr_located pr_name) nal ++
+    pr_opt_type pr t) ++ str ","
+
+let pr_prod_binders2 pr bl =
+  hv 0 (prlist_with_sep sep (pr_prod_binder2 pr) bl)
+
+(**)
+let pr_binders pr = (if !Options.p1 then pr_binders1 else pr_binders2) pr
+let pr_prod_binders pr bl = 
+  if !Options.p1 then 
+    str "!" ++ pr_prod_binders1 pr bl ++ str "."
+  else
+    pr_prod_binders2 pr bl
 
 let pr_arg_binders pr bl =
   if bl = [] then mt() else (spc() ++ pr_binders pr bl)
@@ -369,13 +417,14 @@ let rec pr inherited a =
       larrow
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
-      hv 0 (str "!" ++ pr_binders pr bl ++ str "." ++ spc() ++ pr ltop a),
+      hv 0 (pr_prod_binders pr bl ++ spc() ++ pr ltop a),
       lprod
   | CLambdaN _ ->
       let (bl,a) = extract_lam_binders a in
+      let left, mid = str"fun" ++ spc(), " =>" in
       hov 2 (
-	str "fun" ++ spc () ++ pr_binders pr bl ++
-        str " =>" ++ spc() ++ pr ltop a),
+	left ++ pr_binders pr bl ++
+        str mid ++ spc() ++ pr ltop a),
       llambda
   | CLetIn (_,x,a,b) ->
       let (bl,a) = extract_lam_binders a in
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 9cd75607b..5f7cc2c07 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -36,6 +36,7 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
  
 val pr_global : Idset.t -> global_reference -> std_ppcmds
  
+val pr_tight_coma : unit -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index acff5e164..3ee8e0d76 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -39,28 +39,31 @@ let pr_quantified_hypothesis = function
 
 let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
 
+(*
 let pr_binding prc = function
-  | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c)
-  | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c)
+  | NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+  | AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+*)
 
 let pr_esubst prc l =
   let pr_qhyp = function
-      (_,AnonHyp n,c) -> int n ++ str":=" ++ prc c
-    | (_,NamedHyp id,c) -> pr_id id ++ str":=" ++ prc c in
+      (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+    | (_,NamedHyp id,c) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
+  in
   prlist_with_sep spc pr_qhyp l
 
-let pr_bindings_gen for_ex prc = function
+let pr_bindings_gen for_ex prlc prc = function
   | ImplicitBindings l ->
       spc () ++ (if for_ex then mt() else str "with ") ++
       hv 0 (prlist_with_sep spc prc l)
   | ExplicitBindings l ->
       spc () ++ (if for_ex then mt() else str "with ") ++
-      hv 0 (pr_esubst prc l)
+      hv 0 (pr_esubst prlc l)
   | NoBindings -> mt ()
 
-let pr_bindings prc = pr_bindings_gen false prc
+let pr_bindings prlc prc = pr_bindings_gen false prlc prc
 
-let pr_with_bindings prc (c,bl) = prc c ++ pr_bindings prc bl
+let pr_with_bindings prlc prc (c,bl) = prc c ++ pr_bindings prlc prc bl
 
 let pr_with_names = function
   | [] -> mt ()
@@ -175,9 +178,9 @@ open Closure
 
 let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
 
-let pr_bindings env = pr_bindings (pr_constr env) in
-let pr_ex_bindings env = pr_bindings_gen true (pr_constr env) in
-let pr_with_bindings env = pr_with_bindings (pr_constr env) in
+let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
+let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
+let pr_with_bindings env = pr_with_bindings (pr_lconstr env) (pr_constr env) in
 let pr_eliminator env cb = str "using" ++ pr_arg (pr_with_bindings env) cb in
 let pr_constrarg env c = spc () ++ pr_constr env c in
 let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
@@ -201,9 +204,9 @@ let rec pr_atom0 env = function
   (* Main tactic printer *)
 and pr_atom1 env = function
   | TacExtend (_,s,l) ->
-      pr_extend (pr_constr env) (pr_tac env) s l
+      pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l
   | TacAlias (_,s,l,_) ->
-      pr_extend (pr_constr env) (pr_tac env) s (List.map snd l)
+      pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s (List.map snd l)
 
   (* Basic tactics *)
   | TacIntroPattern [] as t -> pr_atom0 env t
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 1480c765c..161232a5f 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -34,6 +34,7 @@ let pr_raw_tactic_env l env t =
 
 let pr_gen env t =
   Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env)
+    (Ppconstrnew.pr_lconstr_env env)
     (Pptacticnew.pr_raw_tactic env) t
 
 let pr_raw_tactic tac =
@@ -241,20 +242,23 @@ let anonymize_binder na c =
         (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
   else c
 
+let surround_binder p = 
+  if !Options.p1 then str"(" ++ p ++ str")" else p
+
 let pr_binder pr_c ty na =
   match anonymize_binder (snd na) ty with
       CHole _ -> pr_located pr_name na
     | _ ->
         hov 1
-          (str "(" ++ pr_located pr_name na ++ str ":" ++ cut() ++
-           pr_c ty ++ str")")
+        (surround_binder (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty))
 
 let pr_valdecls pr_c = function
   | LocalRawAssum (na,c) ->
-      prlist_with_sep spc (pr_binder pr_c c) na
+      let sep = if !Options.p1 then spc else pr_tight_coma in
+      prlist_with_sep sep (pr_binder pr_c c) na
   | LocalRawDef (na,c) ->
-      hov 1 (str"(" ++ pr_located pr_name na ++ str":=" ++ cut() ++
-             pr_c c ++ str")")
+      hov 1
+        (surround_binder (pr_located pr_name na ++ str":=" ++ cut() ++ pr_c c))
 
 let pr_vbinders pr_c l =
   hv 0 (prlist_with_sep spc (pr_valdecls pr_c) l)
@@ -280,12 +284,21 @@ let pr_assumption_token = function
   | (Decl_kinds.Global,Decl_kinds.Logical) -> str"Axiom"
   | (Decl_kinds.Global,Decl_kinds.Definitional) -> str"Parameter"
 
-let pr_params pr_c (a,(b,c)) =
-  hov 2 (str"(" ++ pr_id b ++ spc() ++
-         (if a then str":>" else str":") ++
-         spc() ++ pr_c c ++ str")")
+let pr_params pr_c (xl,(c,t)) =
+  hov 2 (surround_binder (prlist_with_sep sep pr_id xl ++ spc() ++
+         (if c then str":>" else str":") ++
+         spc() ++ pr_c t))
+
+let rec factorize = function
+  | [] -> []
+  | (c,(x,t))::l ->
+      match factorize l with
+	| (xl,t')::l' when t' = (c,t) & not !Options.p1 -> (x::xl,t')::l'
+	| l' -> ([x],(c,t))::l'
 
-let pr_ne_params_list pr_c l = prlist_with_sep spc (pr_params pr_c) l
+let pr_ne_params_list pr_c l =
+  let sep = if !Options.p1 then spc else pr_coma in
+  prlist_with_sep sep (pr_params pr_c) (factorize l)
 
 let pr_thm_token = function
   | Decl_kinds.Theorem -> str"Theorem"
@@ -354,7 +367,7 @@ let pr_syntax_entry (p,rl) =
   str"level" ++ spc() ++ int p ++ str" :" ++ fnl() ++
   prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl
 
-let sep_end = str";"
+let sep_end () = if !Options.p1 then str";" else str"."
 
 (**************************************)
 (* Pretty printer for vernac commands *)
@@ -411,7 +424,7 @@ let rec pr_vernac = function
   | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s
 
   (* Control *)
-  | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") 
+  | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") 
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc()  ++ str s
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
   | VernacVar id -> pr_id id
@@ -447,7 +460,12 @@ let rec pr_vernac = function
       let (s,l) = match mv8 with
           None -> (s,l)
         | Some ml -> ml in
-      hov 2( str"Notation" ++ spc() ++ pr_locality local ++ qs s ++
+      let ps =
+	let n = String.length s in
+	if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' 
+	then str (String.sub s 1 (n-2))
+	else qs s in
+      hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
       str " :=" ++ pr_constrarg c ++
       (match l with
         | [] -> mt()
diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli
index 0e4bde50e..a444bb537 100644
--- a/translate/ppvernacnew.mli
+++ b/translate/ppvernacnew.mli
@@ -26,6 +26,6 @@ open Libnames
 open Ppextend
 open Topconstr
 
-val sep_end : std_ppcmds
+val sep_end : unit -> std_ppcmds
 
 val pr_vernac : vernac_expr -> std_ppcmds