Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonction

qui permet de changer la façon dont on imprime certains sous-termes sans
avoir à réécrire entièrement un printer de constr.

Dans le même esprit que les commits sur le parser et le lexer, je
cherche à donner une flexibilité aux plugins pour changer l'aspect de
Coq pour le plier à d'autres conventions.


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

2 files changed, 39 insertions, 13 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 8282895855..74a4d5e5dc 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -487,18 +487,24 @@ let pr_fun () =
 
 let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>")
 
-let rec pr sep inherited a =
+
+let pr_dangling_with_for sep pr inherited a =
+  match a with
+  | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a
+  | _ -> pr sep inherited a
+
+let pr pr sep inherited a =
   let (strm,prec) = match a with
   | CRef r -> pr_reference r, latom
   | CFix (_,id,fix) ->
       hov 0 (str"fix " ++
              pr_recursive
-               (pr_fixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) fix),
+               (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix),
       lfix
   | CCoFix (_,id,cofix) ->
       hov 0 (str "cofix " ++
              pr_recursive
-              (pr_cofixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) cofix),
+              (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
       lfix
   | CArrow (_,a,b) ->
       hov 0 (pr mt (larrow,L) a ++ str " ->" ++
@@ -568,9 +574,9 @@ let rec pr sep inherited a =
       hv 0 (
 	str "let '" ++ 
 	  hov 0 (pr_patt ltop p ++ 
-		 pr_asin (pr_dangling_with_for mt) asin ++
+		 pr_asin (pr_dangling_with_for mt pr) asin ++
 		 str " :=" ++ pr spc ltop c ++ 
-		 pr_case_type (pr_dangling_with_for mt) rtntypopt ++
+		 pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++
 		 str " in" ++ pr spc ltop b)),
 	lletpattern
   | CCases(_,_,rtntypopt,c,eqns) ->
@@ -578,8 +584,8 @@ let rec pr sep inherited a =
         (hv 0 (str "match" ++ brk (1,2) ++
 		  hov 0 (
 		    prlist_with_sep sep_v
-		      (pr_case_item (pr_dangling_with_for mt)) c
-		    ++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++
+		      (pr_case_item (pr_dangling_with_for mt pr)) c
+		    ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt) ++
 		  spc () ++ str "with") ++
 		  prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
       latom
@@ -626,12 +632,6 @@ let rec pr sep inherited a =
   pr_with_comments loc
     (sep() ++ if prec_less prec inherited then strm else surround strm)
 
-and pr_dangling_with_for sep inherited a =
-  match a with
-  | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a
-  | _ -> pr sep inherited a
-
-let pr = pr mt
 
 let rec strip_context n iscast t =
   if n = 0 then
@@ -671,6 +671,11 @@ type term_pr = {
   pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
 }
 
+type precedence =  Ppextend.precedence * Ppextend.parenRelation
+let modular_constr_pr = pr
+let rec fix rf x =rf (fix rf) x
+let pr = fix modular_constr_pr mt
+
 let default_term_pr = {
   pr_constr_expr   = pr lsimple;
   pr_lconstr_expr  = pr ltop;
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index d7fdd1ed95..ad2afa97d2 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -81,3 +81,24 @@ type term_pr = {
 
 val set_term_pr : term_pr -> unit
 val default_term_pr : term_pr
+
+(* The modular constr printer. 
+    [modular_constr_pr pr s p t] prints the head of the term [t] and calls
+    [pr] on its subterms. 
+    [s] is typically {!Pp.mt} and [p] is [lsimple] for "constr" printers and [ltop]
+    for "lconstr" printers (spiwack: we might need more specification here).
+    We can make a new modular constr printer by overriding certain branches,
+    for instance if we want to build a printer which prints "Prop" as "Omega"
+    instead we can proceed as follows:
+    let my_modular_constr_pr pr s p = function
+      | CSort (_,RProp Null) -> str "Omega"
+      | t -> modular_constr_pr pr s p t 
+    Which has the same type. We can turn a modular printer into a printer by
+    taking its fixpoint. *)
+
+type precedence
+val lsimple : precedence
+val ltop : precedence
+val modular_constr_pr : 
+               ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> 
+                (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds