PolyML Specific Coding Tricks

Sharing common data

Sharing common data can significantly decreases the size of the heap:

val p = ([1,2,3],[1,2,3]);
PolyML.shareCommonData p;
PolyML.pointerEq (#1 p,#2 p);

outputs: val it = true : bool

Functor Inlining

In PolyML, by default, functors are inlined. This can cause code sizes to blow up a bit. You can turn functor inlining off by:

PolyML.Compiler.inlineFunctors := false;

Pointer level Equality

PolyML.pointer_eq can be used for all sorts of tests on the compiler's optimisation techniques, as well as to write more efficient code (by avoiding extra memory allocation and for quicker equality checking - where you are willing to just check pointers)

Installing Pretty Printing Functions

PolyML.install_pp : :
   ((string -> unit) 
   * (int * bool -> unit) 
   * (int * int -> unit) 
   * (unit -> unit) 
   -> int -> 'a -> 'b -> unit) -> unit

PolyML.install_pp takes a pretty print function and installs it. The most general function looks like:

pretty (putString, beginBlock, spaceBlock, endBlock) limitDepth printElement

Most of these arguments are only required for pretty printing complex types such as list or Array.array where the size of the structure isn't known and there has to be a call back to print the element of the list. If all you want is to print a string just use putString.

The pretty printer is based on a paper by D.C. Oppen in ACM ToPLAS Vol. 2 No. 4 Oct 1980 so that's the place to go if you want the details. beginBlock and endBlock define a block of items and spaceBlock the spaces and possible line-breaks between them. The pretty printer will try to keep a block together on a line but if it has to break it will indent the block. The arguments to beginBlock affect the indentation and whether, if the block has to be split onto multiple lines each element should be consistently split. limitDepth is used to count the depth of complex structures and is ultimately controlled by PolyML.print_depth. Each level should decrement the count and when it reaches zero should print "..." and not go any deeper. printElement is used in polytypes to print the element of a list or array. It passes the value to be printed and the current depth.

There are various examples of the use of it in the prelude (mlsource/prelude/prelude.ML - at this stage in the bootstrap it's PolyML.Inner.install_pp) and the Basis library (e.g. basis/Array.sml).

(This is from a post to the [http://lists.inf.ed.ac.uk/mailman/listinfo/polyml PolyML mailing list] 27 Feb 2008)

If you are working within Isabelle, then there is a wrapper which allows you do this, see references to install_pp in the code, which uses Isabelle's Pretty library (Pure/General/pretty.ML).