Re: [isabelle] lexical matters



On Sun, 16 Jan 2011, Matthias Schmalz wrote:

mark at proof-technologies.com schrieb:
On a related topic, what does Isabelle do for parsing/printing irregular variable/constant names? E.g. a variable with a space in its name. Is it possible to parse such a variable name,

No, as
term "a a"
is rejected.

By extending the syntax in user space, you can easily inject odd strings into the term language, e.g. via something like

  FREE ''foo bar''

with a grammar production for the "FREE" literal token and a suitable parse translations. See the existing CONST notation, although I do not really recommend to try this at home.


If you create variables with irregular names using the ML infrastructure, the printer justs prints them:

ML_val {*
cterm_of @{theory} (Free ("a a", @{typ bool}))
*}

... prints
val it = "a a" : cterm

This use of cterm_of reminds me of an old trick that has come out of use some years ago, because printing with the background theory certificate lacks local syntax of the foreground context (local theory or proof body).

Did you come up with idea yourself, or do we still have it in some old manual?


Here is the localized version:

ML_val {*
  writeln (Syntax.string_of_term @{context} (Free ("a a", @{typ bool})))
*}


	Makarius





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