[isabelle-dev] fun : term -> string
makarius at sketis.net
Thu Sep 23 19:58:42 CEST 2010
On Thu, 23 Sep 2010, Jasmin Christian Blanchette wrote:
>>> The business with filter is there to respect the user's "xsymbols"
>>> preference. You probably don't need it.
>> There might be more user preferences that are getting lost here.
>> Under normal circumstances the default print mode should not be
> But something has to be filtered away, otherwise one gets YXML.
> For the record: What I'm trying to do is to take a nameless fact and
> produce a `foo` string out of it, hoping that this might work (and if it
> doesn't, hoping the user is smart enough to find out which fact
> Sledgehammer was trying to refer to and repair or name it).
Yes this is difficult in general. It is an instance of the "syntax
round-trip problem": a term should be printed in a way such that the
system agrees on it after reading it again.
I would say it is OK to print with only the "xsymbols" mode left and hope
for the best.
You can also try some explicit checks with Syntax.read_prop on the result,
but this is not bullet proof. (In HOL-Import Sebastian Skalberg had a load
of workarounds to approximate a full round trip, but this is not
necessarily for end-user consumption, only for the system reading slightly
odd generated theories again.)
More information about the isabelle-dev