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

1 files changed, 21 insertions, 0 deletions

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