Discussion:
[isabelle] Printing full ML output in Isabelle/jEdit
(too old to reply)
Victor Dumitrescu
2016-07-24 09:40:53 UTC
Permalink
Raw Message
I am struggling with printing the full output of ML code in Isabelle/jEdit.

Specifically, I cannot figure out how to print the full contents of a
list (the default is 10). I have tried increasing PolyML.print_depth,
with no effect.

Also, when using Thm.proof_body_of, for example, the output seems to be
elided in many places (output in Isabelle/jEdit attached below). Is
there a way to retrieve the full output of the function?
PBody {oracles = [], proof =
PThm (1062004,
(("Tree.invert_inv", Const ("HOL.Trueprop",
"bool ⇒ prop") $ (Const ("...", "(tree ⇒ bool) ⇒ bool") $ ...), NONE),
PBody {oracles = [], proof = MinProof, thms =
[(1062003, ("", ... $ ..., PBody
{oracles = [...], ...})), (284, ("...", ..., ...)), (280, ("...",
...))]})),
thms = [(1062004,
("Tree.invert_inv",
Const ("HOL.Trueprop", "bool ⇒ prop") $
(Const ("HOL.All", "(tree ⇒ bool) ⇒ bool") $ Abs ("p", "tree", ...)),
PBody {oracles = [], proof = MinProof, thms =
[(1062003, ("", Const ("...", "bool ⇒
prop") $ ..., PBody {oracles = [...], proof = ..., thms = [...]})),
(284, ("Pure.protectD", ... $ ... $
..., PBody {oracles = [...], ...})), (280, ("...", ..., ...))]}))]}
Thank you,
Victor Dumitrescu
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Makarius
2016-07-24 09:50:14 UTC
Permalink
Raw Message
Post by Victor Dumitrescu
I am struggling with printing the full output of ML code in Isabelle/jEdit.
Specifically, I cannot figure out how to print the full contents of a
list (the default is 10). I have tried increasing PolyML.print_depth,
with no effect.
See ML_print_depth as explained in the Isabelle/Isar implementation
manual. It is actually about Isabelle/ML. Maybe this should be made more
clear somewhere.
Post by Victor Dumitrescu
Also, when using Thm.proof_body_of, for example, the output seems to be
elided in many places (output in Isabelle/jEdit attached below). Is
there a way to retrieve the full output of the function?
You get the full output as a value in ML. The text representation is
only an approximation in semi human-readable form.

If you want to do anything specific with the printed text, there are
usually operations with names like string_of_FOO or pretty_FOO. This
representation of the output can then be displayed via the functions
"writeln" or "Pretty.writeln".


Makarius
Lars Hupel
2016-07-24 09:56:00 UTC
Permalink
Raw Message
Hi Victor,
Post by Victor Dumitrescu
Specifically, I cannot figure out how to print the full contents of a
list (the default is 10). I have tried increasing PolyML.print_depth,
with no effect.
as far as I know, the canonical way of setting the print depth is via an
Isar attribute:

declare [[ML_print_depth=1000]]

Setting this to a sufficiently high value should also solve your problem
below. Beware that proof terms can be very big and pretty printing them
in full will produce a lot of output.

Cheers
Lars

Loading...