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.matth...@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@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Reply via email to