I'm playing with porting HOL4 from Moscow ML to PolyML, and have found it a reasonably pleasant task so far (Moscow ML's out-of-date Basis Library is the major annoyance).
However, there are a couple of things I don't quite see how to do:
* how do I install a pretty-printer in my top-level loop so that my special data-types get printed nicely? Moscow ML offers Meta.installPP, and my scouring of the mailing list suggests I might use RunCall.Inner.install_pp. This is of type
((string -> unit) * (int * bool -> unit) * (int * int -> unit) * (unit -> unit) -> int -> 'a -> 'b -> unit) -> unit
What do the various parameters given to the printing function mean? The first emits actual text, and the int is perhaps the linewidth, but what about the others?
* Is there a way of doing a pointer-equality comparison on arbitrary values in order to give an efficient approximation of normal equality? In MoscowML there's an Obj.magic that can be used to turn 'a into an int (the underlying pointer I think). Is there something similar I can use in Poly?
Many thanks, Michael.
Michael Norrish wrote:
However, there are a couple of things I don't quite see how to do:
how do I install a pretty-printer in my top-level loop so that my special data-types get printed nicely? Moscow ML offers Meta.installPP, and my scouring of the mailing list suggests I might use RunCall.Inner.install_pp. This is of type
((string -> unit) * (int * bool -> unit) * (int * int -> unit) * (unit -> unit) -> int -> 'a -> 'b -> unit) -> unit
What do the various parameters given to the printing function mean? The first emits actual text, and the int is perhaps the linewidth, but what about the others?
I thought there was some documentation on this somewhere but I can't find it on the website. The function is actually in PolyML.install_pp and it's probably better to use that rather than RunCall.Inner despite the various occurrences in the code.
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).
- Is there a way of doing a pointer-equality comparison on arbitrary values in order to give an efficient approximation of normal equality? In MoscowML there's an Obj.magic that can be used to turn 'a into an int (the underlying pointer I think). Is there something similar I can use in Poly?
I see you've found PolyML.pointerEq.
David.