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
end
Considering 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 -> unit
If 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 -> unit
which (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 term
instead of as
term => term | term
is 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]`--) : term
Now, 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.ppstream
Now, 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 = () : unit
Nothing 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 = () : unit
To 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 = () : unit
The custom prettyprinter must fail on non-conforming terms:
- display pp_append (--`1 + 3`--);
uncaught exception Fail ""
- display pp_append (--`T`--);
uncaught exception HOL_ERR
In 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 -> unit
Let'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 -> unit
At 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]`--) : term
The 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