Re: [isabelle] make_string

On 06/25/2018 07:02 PM, Dominique Unruh wrote:

 > 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,

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.



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