David,
> On 20 Sep 2016, at 19:00, David Matthews <[email protected]> > 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 > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
