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
