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.