Email Gateway (Aug 19 2022 at 13:53): Email Gateway (Aug 19 2022 at 13:53):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
exists a clean way for pretty printing terms disregarding all of the
more advanced syntax constructs? Basically the syntax provided by Pure?
Best regards, Lars
Email Gateway (Aug 19 2022 at 13:53):From: Makarius <makarius@sketis.net>
In principle you could use the syntax of Pure.thy and the name spaces of
the current context. This might require some tinkering, similar to
Proof_Syntax.pretty_proof, but in a non-monotonic way to take away
existing syntax.
The general question is where to draw the line for "more advanced syntax
constructs". On the one hand Pure has already quite advanced
abbreviations, and on the other hand main HOL has elementary things that
you probably don't want to miss, e.g. numeral syntax.
So we are back to the standard questions: What is the application behind
this? What do you actually need?
Makarius
Email Gateway (Aug 19 2022 at 13:54):From: Lars Noschinski <noschinl@in.tum.de>
Together with a student, I am currently looking at the flex-flex pairs
created by the unifier during resolution. For this it is quite useful to
see the terms in a compact form on can mentally connect to the raw term
structure. Unfamiliar syntax makes this hard -- for example, I was quite
confused that ZF prints the term "f a b" as "f(a,b)".
-- Lars
Email Gateway (Aug 19 2022 at 13:54):From: Makarius <makarius@sketis.net>
The latter is actually the standard notation of the Isabelle Logical
Framework from 25 years ago. Only later, due to the predominance of
Isabelle/HOL as main application of the same, there was a reform towards
something that people with HOL / ML / Haskell background would find
convenient (while loosing most other people out there).
Today, "f a b" is normal in Isabelle, and the old form is merely a special
feature in Pure: see Pure_Thy.old_appl_syntax_setup. In experiments one
could try to do some tinkering there to make it look more familiar, but it
might be helpful to become familiar with Isabelle in distant past. The HO
unification is from the same period.
Makarius
Email Gateway (Aug 19 2022 at 13:54):From: Stephan Merz <Stephan.Merz@loria.fr>
Please don't discontinue that syntax. As Lars noted, it is used in Isabelle/ZF. I am also happy that I can use standard first-order syntax for operator application in Isabelle/TLA+. The syntax is convenient in logics that do not have partial application (so in the above example, "f a" would be considered malformed). You might even want to consider renaming the attribute, say to Pure_Thy.first_order_appl_syntax_setup, to make it sound less pejorative.
Thanks,
Stephan
Email Gateway (Aug 19 2022 at 13:54):From: Makarius <makarius@sketis.net>
There were never any plans to remove this old syntax, althouth it
sometimes causes small inconveniences.
The old_appl_syntax_setup formalizes the distinction in a reasonably
robust way. Note that the notation is still higher-order, and admits
partial application. So you can write partial applications f(a) or
f(a)(b). This old form of Isabelle has become again popular in Scala,
although I am personally more in favour of notations without lots of
redundant parentheses, and sometimes get confused in the Odersky world.
"Old" in Isabelle jargon does not mean "bad", it just means old.
Otherwise the name of the ML function would have contained "legacy".
Makarius
Last updated: Apr 16 2024 at 04:18 UTC