Stream: Isabelle/ML

Topic: bstring & xstring


view this post on Zulip Qiyuan Xu (May 20 2022 at 01:23):

I know they are both strings but of different semantics, but, what the semantics exactly is? Thanks!

view this post on Zulip Manuel Eberl (May 20 2022 at 08:38):

FYI while it is entirely possible that you will get answers to such ML questions here on Zulip, the best source for such explanations is always Makarius, and he does not read Zulip, so you might want to try the isabelle-users mailing list as well. (important: NOT isabelle-dev)

view this post on Zulip Manuel Eberl (May 20 2022 at 08:39):

He doesn't always reply in a very timely manner though…

view this post on Zulip Manuel Eberl (May 20 2022 at 08:39):

(since he's obviously very busy)

view this post on Zulip Manuel Eberl (May 20 2022 at 08:39):

But not very many people other than him do lots of Isabelle/ML programming these days, especially not concerning such internal things like bstring and xstring

view this post on Zulip Manuel Eberl (May 20 2022 at 08:43):

From skimming the source code it seems to me that bstring is for bindings, i.e. things like fully qualified theorem names, constant names, type class names etc.

view this post on Zulip Manuel Eberl (May 20 2022 at 08:44):

xstring on the other hand looks more like that kind of string that the user will see in the end, where unnecessary information has been stripped

view this post on Zulip Manuel Eberl (May 20 2022 at 08:44):

for instance, if you do something like

ML_val Proof_Context.extern_const @{context} "HOL.True"

you will see that you get the output True (which according to the type signature is an xstring). In the other direction,

ML_val Proof_Context.intern_const @{context} "True"

gives you HOL.True, which is a bstring.

view this post on Zulip Qiyuan Xu (May 22 2022 at 11:40):

oh, these are really interesting! very thank you!


Last updated: Jul 15 2022 at 23:21 UTC