Email Gateway (Aug 22 2022 at 17:22): Email Gateway (Aug 22 2022 at 17:22):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Well, obviously I don't want to create a print function for any new
datatype when there is one there already (now that I've been told how to
remove all the extra crap in the output from @{make_string}).
In what way is @{make_string} not suitable for production-quality output?
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 17:23):From: Makarius <makarius@sketis.net>
Before we continue this thread, can you just explain what you are trying
to do.
There is usually no need to abuse Isabelle/ML to get things done properly.
Makarius
Email Gateway (Aug 22 2022 at 17:25):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
Well, as you suggest, this gives only machine writable/readable data; I
want to get an ML value of type term (or, as in my case, a related
datatype, or more generally any ML value), as a string, that is, an ML
value of type string, which is readable, and could be used to construct
a theory file, by reading it in by
ML {* val t = ... *}
Just like PolyML.makestring, which I assume has been deliberately made
unavailable (why is this?)
And just like @{make_string} combined with |> YXML.parse_body |>
XML.content_of seems to do, but you seem to be saying that I shouldn't
use this for production-quality output (why is this the case?)
Regards,
Jeremy
Email Gateway (Aug 22 2022 at 17:25):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
How so? When I try
theory Scratch imports ZF Main begin
I get an error message
Jeremy
Email Gateway (Aug 22 2022 at 17:25):From: Lars Hupel <hupel@in.tum.de>
"In the same process" means that you can have an editor window open with
two theories, one of which imports "ZF", the other imports "Main". Both
theories can be edited simultaneously.
It doesn't mean that you can import both into the same theory, which
would be very hard indeed.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:25):From: Lars Hupel <hupel@in.tum.de>
I would be suprised if that worked for terms.
If you use this routine on the term "λx. x", you'll get:
Abs ("x", "'a", Bound 0)
Note that the type there is pretty-printed as "'a". If you try to read
that in in an ML block:
ML‹Abs ("x", "'a", Bound 0)›
You'll get an error message that the type is supposed to be a "typ", not
a "string". The correct ML input representation would instead be:
Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0)
I would instead recommend dealing with non-human-readable terms in files
instead (arguably, the above is not really human-readable anyway).
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:26):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,
Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0)
is exactly what I want, having learnt the lesson a very long time ago
that human-readable is always better, for debugging and generally
understanding what is going on. That's why internet protocols such as
HTTP, SMTP etc, are human-readable.
And I can get Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0) printed on
the screen, and by using @{make_string}, coupled with |> YXML.parse_body
|> XML.content_of I can get it into a string value.
What I am asking is (1) why is @{make_string} unsuitable for
production-quality code, and (2) if this is a reason for not using it,
what should I use to achieve the same effect.
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 17:26):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,
Thanks but how do I do this? Does the "editor window" mean the bit on
the top left, where I enter things like theory Scratch imports ZF begin?
And how do I do what you are referring to?
If I try
theory Scratch imports ZF begin
ML {* val t = 1 *}
end
theory Scratch imports Main begin
it gives one error message, if I delete the "end" it gives another error
message, changing Scratch to Scratch1 makes no difference.
What do I actually do to achieve "have an editor window open with
two theories, one of which imports "ZF", the other imports "Main""
Thanks.
Jeremy
Email Gateway (Aug 22 2022 at 17:26):From: Lars Hupel <hupel@in.tum.de>
What do I actually do to achieve "have an editor window open with
two theories, one of which imports "ZF", the other imports "Main""
One theory = one buffer. You have to open a new buffer by pressing
Ctrl-N (or Cmd-N on macOS). You can also have them open side-by-side, by
going to "View", "Splitting".
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:26):From: Lars Hupel <hupel@in.tum.de>
How, if I may ask? If you can get this printed on the screen, surely you
must have it as a string somehow? So why shoving this to @{make_string}
again?
Email Gateway (Aug 22 2022 at 17:26):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,
structure MyTerm = struct
datatype typ =
TFree of string * sort
| TVar of indexname * sort
| Type of string * typ list
datatype term =
$ of term * term
| Abs of string * typ * term
| Bound of int
| Const of string * typ
| Free of string * typ
| Var of indexname * typ
end ; (* structure MyTerm *)
fun ty_toMy (Term.Type (s, tys)) = MyTerm.Type (s, List.map ty_toMy tys)
| ty_toMy (Term.TVar (ixn, st)) = MyTerm.TVar (ixn, st)
| ty_toMy (Term.TFree (s, st)) = MyTerm.TFree (s, st) ;
fun tm_toMy (Term.$ (f, x)) = MyTerm.$ (tm_toMy f, tm_toMy x)
| tm_toMy (Term.Abs (s, ty, tm)) = MyTerm.Abs (s, ty_toMy ty, tm_toMy tm)
| tm_toMy (Term.Bound n) = MyTerm.Bound n
| tm_toMy (Term.Const (s, ty)) = MyTerm.Const (s, ty_toMy ty)
| tm_toMy (Term.Free (s, ty)) = MyTerm.Free (s, ty_toMy ty)
| tm_toMy (Term.Var (ixn, ty)) = MyTerm.Var (ixn, ty_toMy ty) ;
so tm_toMy t results in
val it = .... (ie, it gets printed out naturally, with no
pretty-printing of types). I don't know if that's the easiest way of
stopping types from being pretty-printed, but it is the way I found.
I maybe don't quite understand your remark, but since ML always prints a
newly defined value on the screen - which means it must work out how to
express it as a string (sometimes not very usefully, when it's a
function), but it doesn't actually give you an ML value of type string.
But to get this as a string ML value one would normally use
PolyML.makestring, or the "production-quality equivalent" of
@{make_string}, followed by |> YXML.parse_body |> XML.content_of.
My question is, what is that production-quality equivalent.
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:26):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
OK, thanks - I've done that (ie both those things), but the second
buffer is completely non-responsive (well, almost, since clicking in the
second buffer removes the output from the first buffer from the output
area, but there's no output from the second buffer. Is there a second
output area that's hidden away somewhere, that I need to do something to
make visible?
Thanks,
Jeremy
Email Gateway (Aug 22 2022 at 17:26):From: Makarius <makarius@sketis.net>
See the included ROOT file which defines a session that contains all
theories from HOL + ZF. You can copy that to your project DIRECTORY and
use the session in Isabelle/jEdit as follows:
isabelle jedit -d DIRECTORY -l "HOL+ZF"
Then you can work with theory ML values from unrelated contexts as
illustrated in the included Scratch.thy, but note that
Thy_Info.get_theory only works for theories loaded into the underlying
session image.
So there is no need to write out string representations of ML values at
all, and try to read them back again (that additional problem has not
even been touch on this thread so far).
Makarius
ROOT
Scratch.thy
Email Gateway (Aug 22 2022 at 17:27):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
Thanks - I tried the above and an extra window appeared containing the
following
Build started for Isabelle/HOL+ZF ...
Building HOL+ZF ...
(lots of output here)
*** Failed to load theory "ZF.InfDatatype" (unresolved "ZF.Cardinal_AC")
*** Failed to load theory "ZFC" (unresolved "ZF.InfDatatype")
*** Cannot merge theories with different application syntax
*** At command "theory" (line 10 of "~~/src/ZF/Cardinal_AC.thy")
Unfinished session(s): HOL+ZF
Return code: 2
Session build failed -- prover process remains inactive!
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:27):From: Makarius <makarius@sketis.net>
You actually need Isabelle2018-RC0 for that: it approximates the
Isabelle2018 release that is scheduled for August 2018, see
http://isabelle.in.tum.de/website-Isabelle2018-RC0
Makarius
Email Gateway (Aug 22 2022 at 17:28):From: Lars Hupel <hupel@in.tum.de>
You obviously have to enter something in the second buffer to see
something in the output. The output shows only the current state of
where your cursor is.
Email Gateway (Aug 22 2022 at 17:28):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Lars,
I did that - ie, entering stuff in the second buffer, but no response
Jeremy
Email Gateway (Aug 22 2022 at 17:28):From: Dominique Unruh <unruh@ut.ee>
Hi,
Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0)
You will not get this from @{make_string}, only something similar looking
but unparseable.
@{make_string} gives you somewhat human readable output, for debugging
(which, in case of term is relatively raw, I assume that is because it has
to work on non-wellformed terms, too).
So - independent of whether it is production-suitable or it - it does not
seem to be what you are looking for.
If I understand right, what you want is something that converts a term into
valid ML-code?
You find this here: ML_Syntax.print_term
I think the reason why @{make_string} is not production-suitable (besides
the fact that for terms, it is not very readable) is that it is a bit of a
hack: It does not have an argument "context", so it has to guess which
context is appropriate for the term at hand.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:28):From: Makarius <makarius@sketis.net>
This already summarizes the situation nicely: @{make_string} / @{print}
is for tracing and debugging while doing Isabelle/ML development. The
output is sometimes close to ML notation (e.g. term structure),
sometimes close to regular output (e.g. typ). In some situations there
might be no usable output at all: the exact side-conditions change over
time as the Poly/ML compiler evolves.
Thus it is suitable (and very useful) for adhoc tests, but not suitable
for another program reading the results. Even with perfect output, the
build-in print_depth prevents this. (The print_depth is very important
to avoid bombing the system when printing really big values.)
The default pretty printing with markup conforms to this overall idea of
@{make_string} / @{print} as adhoc diagnostic output. That was the start
of the thread: the <markup> that appears routinely when printing
structured values.
Makarius
Email Gateway (Aug 22 2022 at 17:28):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Dominique,
No, I want exactly Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0),
and it's what I get in the case of a value of type MyTerm.term (which I
use because the system doesn't know how to pretty print the type part of
it, because it is of type MyTerm.typ)
And I don't want a context involved (at least, not unless I can get two
contexts to co-exist together - which the latest messages in this thread
suggest may be possible). PolyML.makestring is of general
applicability, far beyond situations where there is an Isabelle context.
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:28):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
From the length of this email thread, and the absence in it of any
information giving an answer as to how I should be doing the equivalent
of PolyML.makestring, I infer that this function has been made
unavailable with nothing to take its place.
Is this so? And if so, I'm curious as to why it was removed?
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 17:29):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
OK, I've downloaded Isabelle 2018 RC0, and got your attached Scratch.thy
to work (which was as follows)
theory Scratch
imports Pure
begin
ML \<open>
val Main_thy = Thy_Info.get_theory "Main";
val ZF_thy = Thy_Info.get_theory "ZF";
\<close>
end
and it still works when I substitute imports ZF for imports Pure.
So no doubt I could grab a goal from the middle of a ZF proof and create
a HOL term/cterm out of it.
But how do I then start doing a proof in HOL involving that term? The
theory window won't let me put in another theory following the end of
the first one, and it won't let me do
theory Scratch
imports ZF Main
and if I back up to the beginning and replace imports ZF by imports Main
then it has forgotten the ML values which were declared.
So how does one transfer ML values from a ZF proof to a proof in Main?
Plus, there is the additional problem that
ML_prf {* @{Isar.goal} *} doesn't work (why?) and that
although ML_val {* @{Isar.goal} *} works,
ML_val {* ... *} seems to forget any ML value definitions anyway.
So that seems like an additional impediment to the idea of transferring
computed ML terms from a ZF proof to a HOL proof.
So, given that the problem is to take a goal from a ZF proof, compute a
goal to be proved in HOL, and start a HOL proof with that new goal, how
can I do that?
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 17:38):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,
I find that when I use @{make_string} to get a string from a value, it
produces something which is reported simply as
val str = "<markup>": string,
its length (String.size) is something enormous, and when exploded into
an enormous list of characters, seems to incorporate some sort of
pretty-printing information.
How do I get it simply as a string? There is a function writeln which
will print it on the screen as a sensible string, but how do I get this
string as an ML value?
thanks
Jeremy
Email Gateway (Aug 22 2022 at 17:39):From: "Nagashima, Yutaka" <Yutaka.Nagashima@uibk.ac.at>
Hi Jeremy,
Dose this function trm_to_string [1] do the job?
fun trm_to_string (ctxt:Proof.context) (trm:term) = Syntax.string_of_term ctxt trm
|> YXML.parse_body
|> XML.content_of : string;
davidg's comment here [2] might be useful as well.
[1] https://github.com/data61/PSL/blob/master/PGT/PGT.ML#L23
[2] https://stackoverflow.com/questions/26007442/how-do-i-convert-thm-conji-to-an-ascii-string-i-can-save-to-a-file
Regards,
Yutaka
Email Gateway (Aug 22 2022 at 17:39):From: Makarius <makarius@sketis.net>
See also section 0.2.4 Printing ML values in the "implementation"
manual, which is the first place to look for anything regarding
Isabelle/ML tool development.
In particular it says:
This is occasionally useful for diagnostic or demonstration purposes.
Note that production-quality tools require proper user-level error
messages, avoiding raw ML values in the output.
In other words, you use @{make_string} or more conveniently @{print} for
temporary output experiments, but use regular user-space print
operations for real output. The latter depends on what types of values
you want to print, and what is the purpose of it.
Makarius
Email Gateway (Aug 22 2022 at 17:39):From: Dominique Unruh <unruh@ut.ee>
One more explanation to clarify why you see "<markup>" here.
@{make_string} produces a string containing special markup instructions
(e.g., for supporting ctrl-click in jEdit, type-annotations when hovering,
and many more things).
And now the ML toplevel gives you the value of the ML-value "str".
However, since ML-value are not necessarily strings, but complex values,
those values are pretty printed.
So, the ML-toplevel applies the equivalent to @{make_string} to the content
of "str".
And what you end up with is the result of the attempt to pretty print a
string with markup (namely, @{make_string} (@{make_string} something)).
If you use, e.g., "tracing" or "warning" to output the result of
@{make_string} instead, then you will get proper readable output.
(And "tracing (@{make_string} (@{make_string} something))" will output
"<markup>" no matter what 'something' is.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 17:40):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Yutaka,
Thanks, that helps wonderfully.
Your function trm_to_string of course only works for terms, but
the following fixes the output of @{make_string}, exactly what I want
fun fix_markup str = str |> YXML.parse_body |> XML.content_of : string ;
Thanks again!
Jeremy
Email Gateway (Aug 22 2022 at 17:40):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Makarius,
Thanks for the information that I shouldn't be using @{make_string}.
This raises the obvious question of what I should be using. Would it be
possible for you to tell me that? Ie, what is the equivalent in the
managed ML environment called "Isabelle/ML" of the PolyML function
PolyML.makestring?
Thanks
Jeremy
Email Gateway (Aug 22 2022 at 17:40):From: Makarius <makarius@sketis.net>
There is none. For quick adhoc debugging and diagnistics, there is
@{print} and @{make_string}. For production-quality output, you do it
yourself specifically for your data types, potentially using existing
operations like Syntax.pretty_term -- generally it is better to print
Pretty.T than string.
Makarius
Last updated: Apr 24 2024 at 20:16 UTC