Email Gateway (Oct 31 2024 at 08:47): Email Gateway (Oct 31 2024 at 08:47):From: Tobias Nipkow <nipkow@in.tum.de>
Dear List,
Is there a hook where one can modify the way that names of constants are printed?
Thanks
Tobias
Email Gateway (Oct 31 2024 at 11:31):From: Manuel Eberl <manuel@pruvisto.org>
One simple thing that you could do that allows you great freedom is to
just add an unchecking phase that tags all constants (or, probably
better, all the constants you care about) with something. Then you can
manipulate the printing of this tag in whatever way you want:
"notation", "syntax", "print_translation", "print_ast_translation", etc.
Here's an example that prints all constants of type "nat ⇒ nat ⇒ nat" in
angle brackets:
definition DUMMY :: "'a ⇒ 'a" where "DUMMY x = x"
ML ‹
local
val tag_consts_switch = Attrib.setup_config_bool
\<^binding>‹tag_consts› (K false)
fun tag_consts (t as Const (\<^const_name>‹DUMMY›, _) $ _) = t
| tag_consts (f $ x) = tag_consts f $ tag_consts x
| tag_consts (Abs (x, T, t)) = Abs (x, T, tag_consts t)
| tag_consts (t as Const (c, T)) =
if c = \<^const_name>‹DUMMY› orelse T <> \<^typ>‹nat ⇒ nat ⇒
nat› then t
else \<^instantiate>‹'a = ‹T› in term ‹DUMMY :: 'a ⇒ 'a›› $ t
| tag_consts t = t
in
val _ =
Context.>> (Syntax_Phases.term_uncheck 0 "foo"
(fn ctxt => fn ts => if Config.get ctxt tag_consts_switch then map
tag_consts ts else ts))
end
›
notation (output) DUMMY ("⟨_⟩")
lemma "(∑k≤n. k * k) = n * (n+1) * (2*n+1) div (6::nat)"
using [[tag_consts]]
(* Output: (∑k≤n. ⟨()⟩ k k) = ⟨(div)⟩ (⟨()⟩ (⟨(*)⟩ n (⟨(+)⟩ n 1))
(⟨(+)⟩ (⟨(*)⟩ 2 n) 1)) 6 *)
Since there's no way to remove unchecking phases (as far as I am aware)
I added an attribute to switch the special printing on and off. I'm a
bit unsure about adding this unchecking phase with priority 0 (like the
internal ones), but the abbreviation phase runs with priority 1 and
might interfere with the tagging. So I guess it depends on what
behaviour you want: if in the case of e.g. "x ^ 2" want to see the
underlying constant "^" and modify that, you want to use priority 0 like
I did. If you want to see the abbreviation "power2 x" instead, use
priority 2 or higher.
With something like a print translation or AST print translation you
could probably do much nastier things like reversing the names of
particular constants, or switching out one constant for another.
Manuel
On 31/10/2024 09:46, Tobias Nipkow wrote:
Dear List,
Is there a hook where one can modify the way that names of constants
are printed?Thanks
Tobias
Email Gateway (Nov 05 2024 at 21:11):From: Makarius <makarius@sketis.net>
On 31/10/2024 09:46, Tobias Nipkow wrote:
Is there a hook where one can modify the way that names of constants are printed?
You did not say much about the purpose of the exercise.
Here is another possible answer:
alias flatMap = List.map_filter
term List.map_filter
Makarius
Email Gateway (Nov 06 2024 at 10:31):From: Manuel Eberl <manuel@pruvisto.org>
I know a little bit about Tobias's use case: the idea is that he wants
to print some constants in different ways in the LaTeX output. For
example, constants like "T_foo" should be printed as something like
"\textsf{T}_{\textsf{foo}}" and other constants "bar" should be printed
as "\textsf{bar}".
Right now we do roughly what I outlined in my last email, i.e. tagging
the constants with a print_translation and then having a bunch of
"notation (latex)" commands to modify the way the tagged constants get
printed.
A better way to address this would probably be to somehow hook into
document preparation, but I don't know how to do that.
Manuel
On 05/11/2024 22:11, Makarius wrote:
On 31/10/2024 09:46, Tobias Nipkow wrote:
Is there a hook where one can modify the way that names of constants
are printed?You did not say much about the purpose of the exercise.
Here is another possible answer:
alias flatMap = List.map_filter
term List.map_filterMakarius
Email Gateway (Nov 07 2024 at 15:01):From: Manuel Eberl <manuel@pruvisto.org>
I guess the most robust option would be if the document system were to
output constant names as something like "\isaconst{length}" instead of
just "length", and perhaps similarly for free/bound variables, schematic
variables, etc. This is already done e.g. for \isadigit. Then one could
simply tweak the definition of the \isa* LaTeX macros to achieve
whatever effect one wants.
However, I don't know how this would work with more complex constant
names including e.g. Greek letters or subscripts.
Manuel
On 06/11/2024 11:00, Manuel Eberl wrote:
I know a little bit about Tobias's use case: the idea is that he wants
to print some constants in different ways in the LaTeX output. For
example, constants like "T_foo" should be printed as something like
"\textsf{T}_{\textsf{foo}}" and other constants "bar" should be
printed as "\textsf{bar}".Right now we do roughly what I outlined in my last email, i.e. tagging
the constants with a print_translation and then having a bunch of
"notation (latex)" commands to modify the way the tagged constants get
printed.A better way to address this would probably be to somehow hook into
document preparation, but I don't know how to do that.Manuel
On 05/11/2024 22:11, Makarius wrote:
On 31/10/2024 09:46, Tobias Nipkow wrote:
Is there a hook where one can modify the way that names of constants
are printed?You did not say much about the purpose of the exercise.
Here is another possible answer:
alias flatMap = List.map_filter
term List.map_filterMakarius
Email Gateway (Nov 08 2024 at 12:22):From: Makarius <makarius@sketis.net>
On 07/11/2024 15:52, Manuel Eberl wrote:
I guess the most robust option would be if the document system were to output
constant names as something like "\isaconst{length}" instead of just "length",
and perhaps similarly for free/bound variables, schematic variables, etc. This
is already done e.g. for \isadigit. Then one could simply tweak the definition
of the \isa* LaTeX macros to achieve whatever effect one wants.
Yes, this observation is correct. I will take a look before the Isabelle2025
process starts, to see if it can be done properly now --- after so many
changes of the inner-syntax engine.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC