Email Gateway (Aug 18 2022 at 17:22): Email Gateway (Aug 18 2022 at 17:22):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Users,
I'm on Isabelle 2009-2, and I'm stuck with the following problem. I have
a structure whose constructor name is the same as its type. For
presentation in LaTeX I'm using a notation hack which makes constants a
different font than normal isabelle text.
Here's the problem. I define notation as:
notation (output)
blah_C ("moo")
then:
typ "('a, 'p, blah_C) ptr_t"
prints:
('a,'p,moo) ptr_t
and: term "blah_C x y z" prints: "moo x y z" :: moo
Why does output notation pick up on the type, when I'm not using a type
translation? How do I specify I want the constant blah_C as the target
of my notation and not the type?
I realise that the same constructor and type name is not ideal, but the
output does not come from a tool written by me.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 17:22):From: Makarius <makarius@sketis.net>
That is a feature of all Isabelle versions until Isabelle2009-1. In
Isabelle2009-2 the syntax becaume fully "authentic" after many years of
reforming the system (see also the NEWS for Isabelle2009-2).
So the above should work properly, if this is really Isabelle2009-2.
Makarius
Email Gateway (Aug 18 2022 at 17:22):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Actually, I apologise, that was a typo due to being tired and stressed.
I meant Isabelle 2009-1. Do you know of any way of brute-forcing the
issue on this version? I'm low on time and I don't care about elegance,
especially if the problem no longer exists on 2009-2 and afterwards.
Hats off to whoever solved this in subsequent versions. I didn't even
notice the problem was there until it hit me over the head.
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 17:23):From: Makarius <makarius@sketis.net>
On Wed, 16 Mar 2011, Rafal Kolanski wrote:
I meant Isabelle 2009-1. Do you know of any way of brute-forcing the
issue on this version?
Isabelle2009-1 does provide authentic syntax, but not for certain older
packages. So it depends what you mean by the following:
I have a structure whose constructor name is the same as its type.
Is this a HOL datatype? This is probably the most delicate situation.
For output of plain constructor terms, you can use 'abbreviation' with its
own notation (the const is authentic here). It does not work for
patterns, though. For example:
datatype blah_C = blah_C
abbreviation (output)
blah_C_syntax ("moo")
where "blah_C_syntax == blah_C"
typ blah_C -- "blah_C"
term blah_C -- "moo"
term "case x of blah_C => y" -- "blah_C (!)"
Makarius
Email Gateway (Aug 18 2022 at 17:23):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
On 17/03/11 00:57, Makarius wrote:
On Wed, 16 Mar 2011, Rafal Kolanski wrote:
I meant Isabelle 2009-1. Do you know of any way of brute-forcing the
issue on this version?Isabelle2009-1 does provide authentic syntax, but not for certain older
packages. So it depends what you mean by the following:I have a structure whose constructor name is the same as its type.
Is this a HOL datatype? This is probably the most delicate situation.
I'm assuming it's something developed based on datatype code. It tries
to mimic a non-extensible recursive record.
For output of plain constructor terms, you can use 'abbreviation' with
its own notation (the const is authentic here). It does not work for
patterns, though. For example:datatype blah_C = blah_C
abbreviation (output)
blah_C_syntax ("moo")
where "blah_C_syntax == blah_C"typ blah_C -- "blah_C"
term blah_C -- "moo"
term "case x of blah_C => y" -- "blah_C (!)"
This is perfect for the problem at hand. I don't really care what's
inside the type itself, only its record-like capabilities, so I will
never see a case statement like that, and certainly won't present it in
the document.
The authentic syntax in later versions sounds great too, it means my
"show constant names in a different font" notation hack (you have to
specify a list of them manually, but still) will work in future versions.
Thank you Makarius!
Rafal Kolanski.
Last updated: Apr 20 2024 at 08:16 UTC