sig datatype gravity = TOP | APPL | INFIX of int | WEAK | BOTTOM val gravity_geq : gravity -> gravity -> bool val extend_pp_type : (({depth:int, gravity:gravity} -> Term.Type.hol_type -> PP.ppstream -> unit) -> ({depth:int, gravity:gravity} -> Term.Type.hol_type -> PP.ppstream -> unit)) -> unit val extend_pp_term : (({boundvars:Term.term list, depth:int, gravity:gravity} -> Term.term -> PP.ppstream -> unit) -> ({boundvars:Term.term list, depth:int, gravity:gravity} -> Term.term -> PP.ppstream -> unit)) -> unit val reset_pp_type : unit -> unit val reset_pp_term : unit -> unit endConsidering terms (and by analogy, types), there are two functions: one to extend the printer; the other to reset it to the start-up state. Users can provide a special-purpose pretty-printing function for whatever special printing behaviour they require. This function will be tried first on each call (top-level and recursive) to the pretty-printer. If it fails for any reason, the original printer (or the previously extended version) is called.
The argument types to the extension functions are complex. Let's dissect the type of extend_pp_term; to start, it takes a function and returns `()' (the only value of type unit). This function has the following type:
({boundvars:Term.term list, depth:int, gravity:gravity} -> Term.term -> PP.ppstream -> unit) -> ({boundvars:Term.term list, depth:int, gravity:gravity} -> Term.term -> PP.ppstream -> unit)Its first argument is a pretty-printing function. Let us forget about this argument for the moment, leaving us with a function of type:
{boundvars:Term.term list, depth:int, gravity:gravity} -> Term.term -> PP.ppstream -> unitIf we also ignore the first argument of this function (it represents the changing context that the function will operate in), we are left with a function of type:
Term.term -> PP.ppstream -> unitwhich (ought to) make some sense as a pretty-printing function which takes a term and pretty-prints it on the specified ppstream before returning `()'. The documentation for SML of New Jersey should be consulted for more information on the ppstream type.
Now we return to the context parameter. The special-purpose prettyprinter must handle the context that it is called in. The context is a record with fields boundvars, depth, and gravity. These fields are used to decide how to print the current subterm, and are modified for recursive calls to the prettyprinter.
The use of the extensibility functions is illustrated in the session below in which a function to print conditional expressions as
if term then term else terminstead of as
term => term | termis installed. Note that the call to dest_cond fails if the term is not a conditional expression and so forces the original printer to be used. The following is the definition of the custom prettyprinting function:
local open PP Extend_hol_pp in fun pp_ite pp_tm {boundvars:term list,depth,gravity} tm ppstrm = if (depth = 0) then raise Fail "pp_ite" else let val {cond,larm,rarm} = dest_cond tm val parenth = gravity_geq gravity WEAK val params = {boundvars=boundvars,depth=depth-1,gravity=TOP} in if parenth then add_string ppstrm "(" else (); begin_block ppstrm CONSISTENT 0; add_string ppstrm "if "; (pp_tm params cond ppstrm : unit); add_break ppstrm (1,0); add_string ppstrm "then "; pp_tm params larm ppstrm; add_break ppstrm (1,0); add_string ppstrm "else "; pp_tm params rarm ppstrm; end_block ppstrm; if parenth then add_string ppstrm ")" else () end end;Let us bind a test case:
- val tm = (--`APPEND ((n = 0) => [] | [n]) [1;2;3]`--); val tm = (--`APPEND ((n = 0) => [] | [n]) [1; 2; 3]`--) : termNow, we extend the system prettyprinter and test it:
- Extend_hol_pp.extend_pp_term pp_ite; val it = () : unit - tm; val it = (--`APPEND (if (n = 0) then [] else [n]) [1; 2; 3]`--) : term - Extend_hol_pp.reset_pp_term (); val it = () : unit - tm; val it = (--`APPEND ((n = 0) => [] | [n]) [1; 2; 3]`--) : term
Suppose we want to pretty-print the list APPEND function as an infix (@). First let's bind an example term:
val tm = (--`APPEND [1;2] [3;4;5]`--);and set-up a ppstream to write to std_out:
- val std_pps = System.PrettyPrint.mk_ppstream {consumer = (fn s => output (std_out,s)), flush = (fn () => ()), linewidth = 78}; val std_pps = - : System.PrettyPrint.ppstreamNow, a first attempt at defining a pretty-printing function would be the following:
fun pp_append tm ppstrm = let val {Rator,Rand = list2} = dest_comb tm val {Rator,Rand = list1} = dest_comb Rator in if #Name(dest_const Rator) = "APPEND" then (System.PrettyPrint.begin_block ppstrm System.PrettyPrint.INCONSISTENT 3; pp_term ppstrm list1; System.PrettyPrint.add_break ppstrm (1,0); System.PrettyPrint.add_string ppstrm "@"; System.PrettyPrint.add_break ppstrm (1,0); pp_term ppstrm list2; System.PrettyPrint.end_block ppstrm) else raise Fail "" end;The applications of the destructor functions (dest_comb and dest_const) cause an exception to be raised if the term is anything other than a constant applied to two arguments. An explicit test is included to make sure the constant is APPEND. To process the arguments of APPEND, pp_term (the top-level pretty-printing function for terms) is applied to them.
Let's try this function on our example term:
- pp_append tm std_pps; val it = () : unitNothing is displayed because the ppstream has not been flushed! Let's do that:
- System.PrettyPrint.flush_ppstream std_pps; [1; 2] @ [3; 4; 5]val it = () : unitTo avoid tedium later, we define a function to apply a pretty-printing function and flush the ppstream (and add a newline):
- fun display f x = (System.PrettyPrint.begin_block std_pps System.PrettyPrint.INCONSISTENT 0; f x std_pps; System.PrettyPrint.add_newline std_pps; System.PrettyPrint.end_block std_pps; System.PrettyPrint.flush_ppstream std_pps);Trying the example again we get:
- display pp_append tm; [1; 2] @ [3; 4; 5] val it = () : unitThe custom prettyprinter must fail on non-conforming terms:
- display pp_append (--`1 + 3`--); uncaught exception Fail "" - display pp_append (--`T`--); uncaught exception HOL_ERRIn principle, this is all that needs to be done for this example. We can now define a function suitable for the extension facility by just throwing away the first two arguments:
- fun pp_append_extension _ _ tm = pp_append tm; val pp_append_extension = fn : 'a -> 'b -> term -> System.PrettyPrint.ppstream -> unitLet's install this extension and see whether it works:
- Extend_hol_pp.extend_pp_term pp_append_extension; val it = () : unit - tm; val it = (--`[1; 2] @ [3; 4; 5]`--) : term - Extend_hol_pp.reset_pp_term ();
fun pp_append tm ppstrm = let val {Rator,Rand = list2} = dest_comb tm val {Rator,Rand = list1} = dest_comb Rator in if #Name(dest_const Rator) = "APPEND" then (System.PrettyPrint.begin_block ppstrm System.PrettyPrint.INCONSISTENT 3; pp_term ppstrm list1; System.PrettyPrint.add_break ppstrm (1,0); System.PrettyPrint.add_string ppstrm "@"; System.PrettyPrint.add_break ppstrm (1,0); pp_term ppstrm list2; System.PrettyPrint.end_block ppstrm) else raise Fail "" end;To pretty-print the arguments of APPEND we are calling the top-level term printing function pp_term (bound to Hol_pp.pp_term, in a vanilla hol90 system). This appears to work for the example, but it is not apt to be satisfactory in general because pp_term resets the parameters of the pretty-printer to initial values suitable for a top-level prettyprint. These parameters appear in the second argument to pp_append_extension, which we ignored, the context:
{boundvars:Term.term list, depth:int, gravity:gravity}
So, how do we pass the current context to recursive calls of the term printer when pp_term doesn't take its context as an argument? Well, that's what the first argument we ignored is for; it's a recursor, a "context-sensitive" version of the current pp_term with type:
{boundvars:Term.term list, depth:int, gravity:gravity} -> Term.term -> PP.ppstream -> unitAt run time the system will pass a recursor and a context {boundvars, depth,gravity} as arguments to the following improved version of pp_append_extension. To perform a recursive prettyprint, the recursor should be invoked on an appropriately adjusted context. For example, we might have the following recursive calls and context-sensitive actions in a realistic HOL prettyprinter extension:
local open PP Extend_hol_pp in fun pp_append_extension' recursor {boundvars,depth,gravity} tm ppstrm = if (depth = 0) then add_string ppstrm "<term>" else let val {Rator,Rand = list2} = dest_comb tm val {Rator,Rand = list1} = dest_comb Rator in if #Name(dest_const Rator) = "APPEND" then let val my_gravity = INFIX 600 fun parenth s = if (gravity_geq gravity my_gravity) then add_string ppstrm s else () val context' = {depth=depth-1,gravity=my_gravity, boundvars=boundvars} in begin_block ppstrm System.PrettyPrint.INCONSISTENT 3; parenth "("; recursor context' list1 ppstrm; System.PrettyPrint.add_break ppstrm (1,0); System.PrettyPrint.add_string ppstrm "@"; System.PrettyPrint.add_break ppstrm (1,0); recursor context' list2 ppstrm; parenth ")"; end_block ppstrm end else raise Fail "" end end;The following examples show how context is being tracked. The first shows that brackets are appropriately added when the APPEND occurs in a higher binding context; the second shows the opposite situation.
- Extend_hol_pp.extend_pp_term pp_append_extension'; - --`P (APPEND [1;2;3] [4;5;6]):bool`--; val it = (--`P ([1; 2; 3] @ [4; 5; 6])`--) : term - --`APPEND [1;2;3] [4;5;6] = APPEND [1] [7;8;9]`--; val it = (--`[1; 2; 3] @ [4; 5; 6] = [1] @ [7; 8; 9]`--) : termThe last examples show that depth is being monitored appropriately. Notice that the standard prettyprinter has a different notion of ellipsis!
- Globals.max_print_depth := 2; val it = () : unit - --`P (APPEND [1;2;3] [4;5;6]):bool`--; val it = (--`P (<term> @ <term>)`--) : term - --`[APPEND [1;2;3] [4;5;6];[1];[7;8;9]]`--; val it = (--`[<term> @ <term>; [ ... ]; [ ... ; ... ; ... ]]`--) : term