Email Gateway (Aug 19 2022 at 16:54): Email Gateway (Aug 19 2022 at 16:54):From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle/ML experts,
In Isabelle/ML, by typing
@{term "1 + 1"}
I got
val it = Const ("Groups.plus_class.plus", "'a ⇒ 'a ⇒ 'a")
$ Const ("Groups.one_class.one", "'a")
$ Const ("Groups.one_class.one", "'a")
: term
which nicely shows the raw structure of @{term "1 + 1"}. When debugging
a tactic, I want to view the raw structure of some intermediate term. My
idea is to convert it into a string or Pretty.T, and then print it out
as a side effect of a tactic. However, with
Pretty.writeln (Syntax.pretty_term @{context} @{term "1+1"});
the output is
1 + 1
and with
writeln (ML_Syntax.print_term @{term "1+1"});
the output is
Term.$ (Term.$ (Term.Const ("Groups.plus_class.plus", Term.Type
("fun", [Term.TFree ("'a", ["Groups.one", "Groups.plus"]), Term.Type
("fun", [Term.TFree ("'a", ["Groups.one", "Groups.plus"]), Term.TFree
("'a", ["Groups.one", "Groups.plus"])])])), Term.Const
("Groups.one_class.one", Term.TFree ("'a", ["Groups.one",
"Groups.plus"]))), Term.Const ("Groups.one_class.one", Term.TFree ("'a",
["Groups.one", "Groups.plus"])))
None of these two outputs show the raw structure of @{term "1+1"} as
well as by typing @{term "1+1"} directly. Therefore, I was wondering if
there is any other built-in ways to do the job, or shall I implement it
on my own?
Any help is greatly appreciated.
Thanks,
Wenda
Email Gateway (Aug 19 2022 at 16:54):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Wenda,
the antiquotation @{make_string} (which should work for most types)
inlines a function that turns an arbitrary value into a string. If the
only reason for doing so is to print the resulting string, the
antiquotation @{print} is useful.
However, note that this should only be done for debugging.
The following all yield the same output
ML ‹
@{term "1 + 1"};
@{print} @{term "1 + 1"};
writeln (@{make_string} @{term "1 + 1"})
›
cheers
chris
Last updated: Nov 21 2024 at 12:39 UTC