Re: [isabelle] lexical matters



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> 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?

Thanks,
Matthias

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFNMyWEczhznXSdWggRAvr3AJ0eRIp9uf9kgwKUp04ezV8mv5WNjgCghaiE
i8BbcS+Rrm35tdaKS05fAys=
=SKRs
-----END PGP SIGNATURE-----





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