Re: [isabelle] Syntax translation for types



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.