Email Gateway (Aug 18 2022 at 14:08): Email Gateway (Aug 18 2022 at 14:08):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hello,
I would like to have Isabelle print types using the type abbreviations I
have introduced with "types". To that end, I have come across
translations for types that work reasonably well if type variables occur
only once. However, I fail to make it work for type abbreviation like this:
types 'a my_type = "('a list × int × 'a list)"
translations
"my_type a" <= (type) "a list × int × a list"
Isabelle complains that variable a occurs twice in "a list × int × a
list". How can I set up an appropriate print translation for such a type
abbreviation? Do I need to write an ML translation function? If so, how
can I find out how to do that? Or is there any better support other than
translations (similar to abbreviation for constants)?
Regards,
Andreas
Email Gateway (Aug 18 2022 at 14:09):From: Norbert Schirmer <schirmer@in.tum.de>
Hi Andreas,
Email Gateway (Aug 18 2022 at 14:09):From: Norbert Schirmer <schirmer@in.tum.de>
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
Email Gateway (Aug 18 2022 at 14:09):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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
Last updated: Apr 19 2024 at 16:20 UTC