Re: [isabelle] lexical matters



On Sun, 16 Jan 2011, Matthias Schmalz wrote:

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

This depends on various fine points of what you really need, i.e. just detect lexical identifiers or ensure that certain generated names are resolved as free variables, not constants.

The following example does the lexical check only, quite reliably in the sense that I've studied the relevant Isabelle/Pure sources for 15min.

ML {*

fun is_syntax_ident ctxt s =
  Syntax.is_identifier s andalso
    not (can Name.dest_internal s) andalso
    not (Syntax.is_keyword (ProofContext.syn_of ctxt) s);

*}

locale test =
  fixes xxx ("FOO")
begin

lemma True
proof

  fix yyy ("BAR")

  ML_val {* is_syntax_ident @{context} "FOO" *}
  ML_val {* is_syntax_ident @{context} "BAR" *}
  ML_val {* is_syntax_ident @{context} "True" *}
  ML_val {* is_syntax_ident @{context} "x" *}
  ML_val {* is_syntax_ident @{context} "x_" *}

qed

end


It is important to work with the proper local context. In particular, a background @{theory} is generally not sufficient.


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?

Not yet, but this will come at some point. There are some raw technical issues, and some more profound questions concerning the formal context on the Isabelle/Scala side. Some concrete applications will make this emerge more quickly :-)


	Makarius





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