[isabelle-dev] fun : term -> string

[Makarius]

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 
>> filtered.
>
> 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.)


 	Makarius