Re: [isabelle] definition vs const(def)s as targets for print_translation



Hi Brian,

On 26/10/10 00:50, Brian Huffman wrote:
From the Isabelle NEWS file (Isabelle 2007 section):

* Syntax: constants introduced by new-style packages ('definition',
'abbreviation' etc.) are passed through the syntax module in
``authentic mode''. This means that associated mixfix annotations
really stick to such constants, independently of potential name space
ambiguities introduced later on. INCOMPATIBILITY: constants in parse
trees are represented slightly differently, may need to adapt syntax
translations accordingly. Use CONST marker in 'translations' and
@{const_syntax} antiquotation in 'parse_translation' etc.

So you will need to change your print translation command like this:

print_translation {* [(@{const_syntax "iadd"}, rev_iadd_tr')] *}

After this change, the print translation worked fine for me. In case
you're wondering what string it actually generates:

ML_val {* @{const_syntax "iadd"} *}
val it = "\<^const>Scratch.iadd" : string

Having all names of actual constants tagged with "\<^const>" makes the
syntax mechanisms more robust, since constants will never be confused
with similarly-named variables or types. (Doing Isabelle>  Show me ...
inner syntax in Proof General should help give an idea of how the
scheme works.)

However, if I change "definition" to "constdefs", the print
translation works. Could someone help me understand why this is? To me, it
feels completely non-obvious and unintuitive.

"constdefs" was never upgraded to be a "new-style" package, so it
never participated in the syntax scheme using "\<^const>". (There will
never be a "new-style" constdefs package, since in the development
version "constdefs" has been discontinued.)

Thank you very much! That explains everything, and also improves future-compatibility of my code.

Incidentally I think that this simple reversed-add example would make a good addition to the Isabelle developer's manual. All the parse/print translation examples out there are rather complex (if they weren't, people would use notation instead) and the ones in HOL that I looked at all seem to use const or constdefs (maybe I'm just lucky).

Thanks again Brian!

Sincerely,

Rafal Kolanski.





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