Re: [isabelle] lexical matters
-----BEGIN PGP SIGNED MESSAGE-----
> It depends what you want to do in the end. Generating sources that are
> fed back into the system is inherently hard. I have occasionally seen
> people doing it empirically, e.g. trying Syntax.read_term on some
> identifier and checking if they get a "Free" term -- but this does not
> really take the scoping rules of const vs. free vs. bound into account.
For the moment, I need to generate sources. Heuristic solutions are
fine. Are you aware of other pitfalls than hitting reserved keywords,
predefined constants, and capturing?
> Unless your output needs to be inspected directly by users it is easier
> to avoid generating sources altogether, and use the Isabelle/ML
> interfaces to get logical content into the system. This is the norml
> way in LCF-style provers. Concrete syntax is just a superficial add-on
> for end-users.
On the long run, I indeed intend to bypass the parser. I implement my
tool in Scala and would like to avoid writing my own Scala/ML linkup.
Is there a way of accessing the term datatype via the the Isabelle/Scala
interface? Can I use Isabelle/Scala to access the Syntax.read_term function?
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
-----END PGP SIGNATURE-----
This archive was generated by a fusion of
Pipermail (Mailman edition) and