[isabelle-dev] numeral type translations

[Gerwin Klein]

On 30/05/2012, at 6:50 PM, Makarius wrote:
>> On Wed, May 30, 2012 at 3:36 AM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
>>> Hi Brian,
>>> 
>>> not sure if this has anything to do with your change in numerals, but the following used to work as expected in Isabelle2011-1:
>>> 
>>> type_synonym word_length8 = 8
>>> type_synonym word8 = "word_length8 word"
>>> translations (type) "word8" <= (type) "8 word"
> 
> Such backward translations of the "type" category have always been fragile and and the risk of the user, ever since David von Oheimb started these things in Bali, from where Gerwin has probably picked it up many years ago.
> 
> To ensure that "8" is treated as a syntax constant in Isabelle2012, the usual way is this:
> 
>  syntax "8" :: _
> 
> I can't say on the spot if it has dire effects on other syntax, though.

Hm, subtle side effects is exactly what I was trying to avoid. In this case, it won't hurt to just not have the translation.


> If it does not work, one can use the ML function for translations (Syntax.update_trrules) to make an Ast pattern where the desired numerals are Ast.Constant, not Ast.Variable as guessed by the concrete syntax parser.

That'll work. Not worth the investment for this one, though.

Gerwin