[isabelle-dev] numeral type translations

[Brian Huffman]

Hi Gerwin,

I'm responding also to the development list.

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"
>
> term "7 :: 10 word"
>
> (shows as 10 word)
>
> In Isabelle2012, it shows as "word8", i.e. all lengths fire the translation. Changing the "8 word" on the rhs to word_length8 or something like "num1 bit0 bit0 bit0" won't fire the translation at all.

As you suspected, this has nothing to do with the change in numeral
representation. It has only to do with Isabelle's parser.

I tested the following example in Isabelle/Pure, using the parse/print
translations copied from Library/Numeral_Type.thy:

type_synonym eight = 8
translations (type) "eight" <= (type) "8"
typ "10"
(shows as "eight" in Isabelle2012)

If you do "Isabelle > Show Me > Internal Syntax" in PG, then you can
see a difference in the "print_rules" section:

Isabelle2011-1:
  ("_NumeralType" "8")  ->  "\<^type>Temp.eight"

Isabelle2012:
  ("_NumeralType" 8)  ->  "\<^type>Temp.eight"

Note the difference in the quotation marks, which indicate that
something is a constant. In Isabelle2012, the rule has a free variable
called "8", which matches anything, as you observed.

I did a bisection to find the origin of the problem:

The first bad revision is:
changeset:   46236:ae79f2978a67
user:        wenzelm
date:        Mon Jan 16 21:50:15 2012 +0100
summary:     position constraints for numerals enable PIDE markup;

Unfortunately I don't know of any workaround to get your syntax
translations working again.

- Brian