Email Gateway (Aug 17 2022 at 06:29): Email Gateway (Aug 17 2022 at 06:29):From: Joachim Breitner <mail@joachim-breitner.de>
Hello,
one of the things that I really like with Isabelle is its flexible
syntax, and the ability to write things like I would do on paper, using
infix or even funny mixfix symbols, rather than all in ascii prefix
functions.
But when still developing a theory I often don’t want to think of
clever syntax yet, and just use plain function names. And sometimes I
have nice syntax, but the plain function is easier to type.
Is there a tool that I can run over my .thy files that replaces prefix
function syntax with the corresponding pretty syntax, for certain
functions? Or maybe a tool that pretty-prints every term the way
Isabelle would show it to me (e.g. in the goal state), and replace it
with that in the .thy file?
Thanks!
Joachim
Email Gateway (Sep 16 2022 at 10:30):From: Makarius <makarius@sketis.net>
By "is there a tool", do you mean constructive existence in reality, or
classic existence in the Platonic Heaven of Ideas? The latter should hold, but
we are far from making that work concretely.
Such a tool cannot be just an external program that operates on postulated
"Isabelle syntax trees" --- they don't exist. Instead, it needs to take
semantic information from the belly of the system into account. One approach
that might work eventually is to have PIDE markup on the source text that is
sufficiently rich to allow the pretty-printing that you have in mind.
The coming Isabelle2022 release will have again more detailed HTML
presentation, based on such semantic PIDE markup. But this is still not
sufficient for advanced pretty printing.
See
https://isabelle.sketis.net/website-Isabelle2022-RC1/dist/library/HOL/HOL/index.html
and hover e.g. on the conjunction symbol here
https://isabelle.sketis.net/website-Isabelle2022-RC1/dist/library/HOL/HOL/HOL.html
Makarius
Email Gateway (Sep 19 2022 at 09:01):From: Joachim Breitner <mail@joachim-breitner.de>
Hello,
Am Freitag, dem 16.09.2022 um 12:29 +0200 schrieb Makarius:
By "is there a tool", do you mean constructive existence in reality, or
classic existence in the Platonic Heaven of Ideas? The latter should hold, but
we are far from making that work concretely.Such a tool cannot be just an external program that operates on postulated
"Isabelle syntax trees" --- they don't exist. Instead, it needs to take
semantic information from the belly of the system into account. One approach
that might work eventually is to have PIDE markup on the source text that is
sufficiently rich to allow the pretty-printing that you have in mind.
Yes, something like that is what I had in my heavenly platonic mind
The coming Isabelle2022 release will have again more detailed HTML
presentation, based on such semantic PIDE markup. But this is still not
sufficient for advanced pretty printing.
That's already pretty nice indeed!
Out of curiosity, what is missing for a tool like this, which seems to
have access to the bellied semantic information, to use the (existing?)
pretty-printer to re-render the pieces of inner syntax, like the term
or prop commands would do?
Cheers,
Joachim
Last updated: Apr 27 2024 at 01:05 UTC