Re: [isabelle] lexical matters



on 18/1/11 7:10 PM, Makarius <makarius at sketis.net> wrote:

> ....
>
> Dvid Matthews kindly provides ways in Poly/ML to manage the whole
> compilation process in user space, including printing and binding of the
> results.  One would merely have to protect agains shadowing of certain
> structure names, say.

Oh good.  This is excellent news.  How long has this been available for?

A related problem is overwriting a datatype's pretty printer.  Do you know
if Poly/ML can protect against this?

> When you've showed me an early version of HOL0 in Cambridge ITP 2009, I
> have already pointed out that OCaml is not the best platform for that (due
> to its mutable strings and silently overflowing machine words called
> "int").

Yes you did (was it Montreal ITP 2008?).  HOL Zero uses a technique to avoid
problems with mutable strings (unlike HOL Light) and doesn't use machine
words for its representation of natural number numerals (like HOL Light).

But you are right - OCaml is not the best language.  Larry convinced me a
few months ago that SML is simply more well-defined.  I plan to port it to
SML as a priority as soon version 1.0 is out.  But this port might not be
until next year.

Mark.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.