Re: [isabelle] Syntax translation for types



Hi Andreas,

According to the old Isabelle reference manual (Sect. 7.6.1):

http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf

print translations are applied top-down. So from this you cannot expect that your inner translation of my_type was already applied before you get to translate foo. A straightforward solution is to put the modularity you want into your ML code. The foo translation matches on plain pairs, and then calls the my-type translation on its elements (if they fail they will raise a match, so thats fine).
Skeleton:

print_translation {*
let
fun my_type_tr' [Const ("list",_)$a1,Const ("*",_)$Const ("int",_)$ (Const ("list",_)$a2)] =
    if a1=a2 then Syntax.const "my_type"$a1
    else raise Match;
  fun foo_tr' [a,b] =
   let
     val Const("my_type",_)$a1 = my_type_tr' (snd (strip_comb a));
     val Const("my_type",_)$a2 = my_type_tr' (snd (strip_comb b));
   in if a1=a2 then Syntax.const "foo"$a1 else raise Match
   end
in [("*",my_type_tr'),
    ("*",foo_tr')]
end

   Cheers,

    Norbert

On 08.10.2009, at 10:58, Andreas Lochbihler wrote:

Hi Norbert,

thank you very much for the print translation. It works great - also for my more elaborate type abbreviations. However, with a hierarchy of types abbreviations and appropriate translatons, I seem to have to do pattern matching down to the real types in every translation. Is there any possibility to avoid this and reuse the previous translations? Here is a trivial example:

types 'a my_type = "('a list × int × 'a list)"
print_translation {*
let
fun tr' [Const ("list",_)$a1, Const ("*",_)$Const ("int",_)$(Const ("list",_)$a2)] =
   if a1=a2 then Syntax.const "my_type"$a1
   else raise Match;
in [("*",tr')]
end
*}

types 'a foo = "('a my_type * 'a my_type)"
print_translation {*
let
fun tr' [Const ("*", _) $ (Const ("list",_)$a1) $ (Const ("*",_) $Const ("int",_)$(Const ("list",_)$a2)), Const ("*", _) $ (Const ("list",_)$a3) $ (Const ("*",_) $Const ("int",_)$(Const ("list",_)$a4))] =
   if a1=a2 andalso a2=a3 andalso a3=a4 then Syntax.const "foo"$a1
   else raise Match;
in [("*",tr')]
end
*}

In the print translation for foo, I currently copy the pattern for my_type twice (and add the outermost "*" again), but it would be great to have the translation for my_type applied first (i.e. bottom- up) and then in tr' for foo, I would only have to check for my_type.

In particular, if I change my_type later on, I only have to change the translation for my_type, but not for all those that build on my_type.

Thanks in advance,
Andreas






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