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


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

  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] = @{const "iadd"} $ t2 $ t1
    | rev_iadd_tr ts = raise TERM ("rev_iadd_tr", ts);

parse_translation {* [("_rev_iadd", rev_iadd_tr)] *}

term "1 ri+ 2" -- "prints: iadd 2 1"

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"

There are no warnings or errors, yet the translation does not work. Using the fully qualified name of iadd to register the print translation doesn't help either. 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.

Using Isabelle 2009-1.


Rafal Kolanski.

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