Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Print raw structure of terms


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 08:18 UTC