Re: [isabelle] make_string





On 06/24/2018 02:23 AM, Lars Hupel wrote:
 And just like @{make_string} combined with |> YXML.parse_body |>
XML.content_of seems to do, but you seem to be saying that I shouldn't
use this for production-quality output (why is this the case?)

I would be suprised if that worked for terms.

If you use this routine on the term "λx. x", you'll get:

   Abs ("x", "'a", Bound 0)

Note that the type there is pretty-printed as "'a". If you try to read that in in an ML block:

   ML‹Abs ("x", "'a", Bound 0)›

You'll get an error message that the type is supposed to be a "typ", not a "string". The correct ML input representation would instead be:

   Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0)

I would instead recommend dealing with non-human-readable terms in files instead (arguably, the above is not really human-readable anyway).

Cheers
Lars

Hi Lars,

Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0)

is exactly what I want, having learnt the lesson a very long time ago that human-readable is always better, for debugging and generally understanding what is going on. That's why internet protocols such as HTTP, SMTP etc, are human-readable.

And I can get Abs ("x", TFree ("'a", ["HOL.type"]), Bound 0) printed on
the screen, and by using @{make_string}, coupled with |> YXML.parse_body |> XML.content_of I can get it into a string value.

What I am asking is (1) why is @{make_string} unsuitable for production-quality code, and (2) if this is a reason for not using it, what should I use to achieve the same effect.

Thanks

Jeremy




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