--- a/src/Tools/Metis/src/PP.sig Mon Sep 13 16:44:20 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-(* ========================================================================= *)
-(* PP -- pretty-printing -- from the SML/NJ library *)
-(* *)
-(* Modified for Moscow ML from SML/NJ Library version 0.2 *)
-(* *)
-(* COPYRIGHT (c) 1992 by AT&T Bell Laboratories. *)
-(* *)
-(* STANDARD ML OF NEW JERSEY COPYRIGHT NOTICE, LICENSE AND DISCLAIMER. *)
-(* *)
-(* Permission to use, copy, modify, and distribute this software and its *)
-(* documentation for any purpose and without fee is hereby granted, *)
-(* provided that the above copyright notice appear in all copies and that *)
-(* both the copyright notice and this permission notice and warranty *)
-(* disclaimer appear in supporting documentation, and that the name of *)
-(* AT&T Bell Laboratories or any AT&T entity not be used in advertising *)
-(* or publicity pertaining to distribution of the software without *)
-(* specific, written prior permission. *)
-(* *)
-(* AT&T disclaims all warranties with regard to this software, including *)
-(* all implied warranties of merchantability and fitness. In no event *)
-(* shall AT&T be liable for any special, indirect or consequential *)
-(* damages or any damages whatsoever resulting from loss of use, data or *)
-(* profits, whether in an action of contract, negligence or other *)
-(* tortious action, arising out of or in connection with the use or *)
-(* performance of this software. *)
-(* ========================================================================= *)
-
-signature PP =
-sig
-
- type ppstream
-
- type ppconsumer =
- {consumer : string -> unit,
- linewidth : int,
- flush : unit -> unit}
-
- datatype break_style =
- CONSISTENT
- | INCONSISTENT
-
- val mk_ppstream : ppconsumer -> ppstream
-
- val dest_ppstream : ppstream -> ppconsumer
-
- val add_break : ppstream -> int * int -> unit
-
- val add_newline : ppstream -> unit
-
- val add_string : ppstream -> string -> unit
-
- val begin_block : ppstream -> break_style -> int -> unit
-
- val end_block : ppstream -> unit
-
- val clear_ppstream : ppstream -> unit
-
- val flush_ppstream : ppstream -> unit
-
- val with_pp : ppconsumer -> (ppstream -> unit) -> unit
-
- val pp_to_string : int -> (ppstream -> 'a -> unit) -> 'a -> string
-
-end
-
-(*
- This structure provides tools for creating customized Oppen-style
- pretty-printers, based on the type ppstream. A ppstream is an
- output stream that contains prettyprinting commands. The commands
- are placed in the stream by various function calls listed below.
-
- There following primitives add commands to the stream:
- begin_block, end_block, add_string, add_break, and add_newline.
- All calls to add_string, add_break, and add_newline must happen
- between a pair of calls to begin_block and end_block must be
- properly nested dynamically. All calls to begin_block and
- end_block must be properly nested (dynamically).
-
- [ppconsumer] is the type of sinks for pretty-printing. A value of
- type ppconsumer is a record
- { consumer : string -> unit,
- linewidth : int,
- flush : unit -> unit }
- of a string consumer, a specified linewidth, and a flush function
- which is called whenever flush_ppstream is called.
-
- A prettyprinter can be called outright to print a value. In
- addition, a prettyprinter for a base type or nullary datatype ty
- can be installed in the top-level system. Then the installed
- prettyprinter will be invoked automatically whenever a value of
- type ty is to be printed.
-
- [break_style] is the type of line break styles for blocks:
-
- [CONSISTENT] specifies that if any line break occurs inside the
- block, then all indicated line breaks occur.
-
- [INCONSISTENT] specifies that breaks will be inserted to only to
- avoid overfull lines.
-
- [mk_ppstream {consumer, linewidth, flush}] creates a new ppstream
- which invokes the consumer to output text, putting at most
- linewidth characters on each line.
-
- [dest_ppstream ppstrm] extracts the linewidth, flush function, and
- consumer from a ppstream.
-
- [add_break ppstrm (size, offset)] notifies the pretty-printer that
- a line break is possible at this point.
- * When the current block style is CONSISTENT:
- ** if the entire block fits on the remainder of the line, then
- output size spaces; else
- ** increase the current indentation by the block offset;
- further indent every item of the block by offset, and add
- one newline at every add_break in the block.
- * When the current block style is INCONSISTENT:
- ** if the next component of the block fits on the remainder of
- the line, then output size spaces; else
- ** issue a newline and indent to the current indentation level
- plus the block offset plus the offset.
-
- [add_newline ppstrm] issues a newline.
-
- [add_string ppstrm str] outputs the string str to the ppstream.
-
- [begin_block ppstrm style blockoffset] begins a new block and
- level of indentation, with the given style and block offset.
-
- [end_block ppstrm] closes the current block.
-
- [clear_ppstream ppstrm] restarts the stream, without affecting the
- underlying consumer.
-
- [flush_ppstream ppstrm] executes any remaining commands in the
- ppstream (that is, flushes currently accumulated output to the
- consumer associated with ppstrm); executes the flush function
- associated with the consumer; and calls clear_ppstream.
-
- [with_pp consumer f] makes a new ppstream from the consumer and
- applies f (which can be thought of as a producer) to that
- ppstream, then flushed the ppstream and returns the value of f.
-
- [pp_to_string linewidth printit x] constructs a new ppstream
- ppstrm whose consumer accumulates the output in a string s. Then
- evaluates (printit ppstrm x) and finally returns the string s.
-
-
- Example 1: A simple prettyprinter for Booleans:
-
- load "PP";
- fun ppbool pps d =
- let open PP
- in
- begin_block pps INCONSISTENT 6;
- add_string pps (if d then "right" else "wrong");
- end_block pps
- end;
-
- Now one may define a ppstream to print to, and exercise it:
-
- val ppstrm = PP.mk_ppstream {consumer =
- fn s => TextIO.output(TextIO.stdOut, s),
- linewidth = 72,
- flush =
- fn () => TextIO.flushOut TextIO.stdOut};
-
- fun ppb b = (ppbool ppstrm b; PP.flush_ppstream ppstrm);
-
- - ppb false;
- wrong> val it = () : unit
-
- The prettyprinter may also be installed in the toplevel system;
- then it will be used to print all expressions of type bool
- subsequently computed:
-
- - installPP ppbool;
- > val it = () : unit
- - 1=0;
- > val it = wrong : bool
- - 1=1;
- > val it = right : bool
-
- See library Meta for a description of installPP.
-
-
- Example 2: Prettyprinting simple expressions (examples/pretty/ppexpr.sml):
-
- datatype expr =
- Cst of int
- | Neg of expr
- | Plus of expr * expr
-
- fun ppexpr pps e0 =
- let open PP
- fun ppe (Cst i) = add_string pps (Int.toString i)
- | ppe (Neg e) = (add_string pps "~"; ppe e)
- | ppe (Plus(e1, e2)) = (begin_block pps CONSISTENT 0;
- add_string pps "(";
- ppe e1;
- add_string pps " + ";
- add_break pps (0, 1);
- ppe e2;
- add_string pps ")";
- end_block pps)
- in
- begin_block pps INCONSISTENT 0;
- ppe e0;
- end_block pps
- end
-
- val _ = installPP ppexpr;
-
- (* Some example values: *)
-
- val e1 = Cst 1;
- val e2 = Cst 2;
- val e3 = Plus(e1, Neg e2);
- val e4 = Plus(Neg e3, e3);
- val e5 = Plus(Neg e4, e4);
- val e6 = Plus(e5, e5);
- val e7 = Plus(e6, e6);
- val e8 =
- Plus(e3, Plus(e3, Plus(e3, Plus(e3, Plus(e3, Plus(e3, e7))))));
-*)