Rob, I've had a look at this and it does appear to be more complicated than I thought. The pretty type is embedded fairly deeply in the compiler.
The difference between PolyML.prettyPrint and PolyML.addPrettyPrinter is that PolyML.addPrettyPrinter is an infinitely overloaded function, like PolyML.print and PolyML.makestring, and the FixedInt.int argument here is the the depth of the printing before "..." is used. The compiler builds pretty printing functions for types as they are defined and the code decrements and tests the argument using fixed precision arithmetic. All pretty printers have to use fixed precision arithmetic for the depth for everything to be safe.
PolyML.prettyPrint is defined in the basis library and the int argument is the line width. It uses FixedInt.toInt and FixedInt.fromInt where necessary so works with either fixed or arbitrary precision int.
Regards, David
On 21/09/2016 11:46, Rob Arthan wrote:
David,
On 20 Sep 2016, at 19:00, David Matthews <David.Matthews at prolingua.co.uk> wrote:
Rob, The complication is that the pretty print datatype is essentially shared between the compiler and the compiled code. If the compiler has been compiled with a different length of int from the user code there's the potential for confusion. The compiler builds default print functions for types and I was trying to ensure that both sides had the same understanding.
It may be that it isn't a problem. I'll think about this some more.
I have now tried a ProofPower build with a work-around for this and everything is working. It would be nice not to have to work around this. As things stand, the PolyML structure contains a rather odd mixture of int and FixedInt.int when you compile with ?enable-intinf-as-int. E.g., compare prettyPrint with addPrettyPrinter.
The "datatype" definition in PRETTYSIG.sml is commented out. The "constructors" actually use FixedInt.int.
I didn?t notice that!
Regards,
Rob.
Regards, David
On 20/09/2016 16:40, Rob Arthan wrote:
David,
After using the patch in my last post to enable me to build poly, ProofPower now builds and behaves as I would expect it to when compiled without ?enable-intinf-as-int. When I compile with ?enable-intinf-as-int I get a problem because the type of PolyML.PrettyBlock has a FixedInt in it where it had just in in version 5.6.
PolyML.PrettyBlock;
val it = fn: FixedInt.int * bool * PolyML.context list * PolyML.pretty list -> PolyML.pretty
Is that intended? I can?t understand why it has happening because the datatype declaration in PRETTYSIG.sml uses int. If this is intended then I can work round it, but it would be nice not to have to.
Regards,
Rob.
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml