Re: [isabelle] make_string





On 06/25/2018 07:02 PM, Dominique Unruh wrote:
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.


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









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.