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



On Sun, Oct 24, 2010 at 8:32 PM, Rafal Kolanski <rafalk at cse.unsw.edu.au> wrote:
> Greetings,
>
> After hours of trying to figure out what was wrong with my print translation
> code (no errors, no warnings, did nothing) while my parse translation was
> working perfectly, I discovered what was causing the mental blockage.
>
> Suppose I have the following example to have a "reversed add operator"
> (pointless, but good start for learning print/parse translations):
>
> definition
>  iadd :: "int ⇒ int ⇒ int" where
>  "iadd x y ≡ x + y"
>
> syntax "_rev_iadd" :: "int ⇒ int ⇒ int" ("_ ri+ _ " [50,50] 50)
[...]
> ML {*
>  fun rev_iadd_tr' [t1, t2] = Syntax.const "_rev_iadd" $ t2 $ t1
>    | rev_iadd_tr' _ = raise Match;
> *}
>
> print_translation {* [("iadd", rev_iadd_tr')] *}
>
> term "iadd 1 2" -- "this prints: iadd 1 2, should print: 2 ri+ 1"

Hi Rafal,

>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.)

- Brian





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