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