Re: [isabelle] make_string





On 06/24/2018 07:16 PM, Lars Hupel wrote:
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.

How, if I may ask? If you can get this printed on the screen, surely you
must have it as a string somehow? So why shoving this to @{make_string}
again?


Hi Lars,

structure MyTerm = struct
datatype typ =
    TFree of string * sort
  | TVar of indexname * sort
  | Type of string * typ list

datatype term =
    $ of term * term
  | Abs of string * typ * term
  | Bound of int
  | Const of string * typ
  | Free of string * typ
  | Var of indexname * typ
end ; (* structure MyTerm *)

fun ty_toMy (Term.Type (s, tys)) = MyTerm.Type (s, List.map ty_toMy tys)
  | ty_toMy (Term.TVar (ixn, st)) = MyTerm.TVar (ixn, st)
  | ty_toMy (Term.TFree (s, st)) = MyTerm.TFree (s, st) ;

fun tm_toMy (Term.$ (f, x)) = MyTerm.$ (tm_toMy f, tm_toMy x)
  | tm_toMy (Term.Abs (s, ty, tm)) = MyTerm.Abs (s, ty_toMy ty, tm_toMy tm)
  | tm_toMy (Term.Bound n) = MyTerm.Bound n
  | tm_toMy (Term.Const (s, ty)) = MyTerm.Const (s, ty_toMy ty)
  | tm_toMy (Term.Free (s, ty)) = MyTerm.Free (s, ty_toMy ty)
  | tm_toMy (Term.Var (ixn, ty)) = MyTerm.Var (ixn, ty_toMy ty) ;

so tm_toMy t results in
val it = .... (ie, it gets printed out naturally, with no pretty-printing of types). I don't know if that's the easiest way of stopping types from being pretty-printed, but it is the way I found.

I maybe don't quite understand your remark, but since ML always prints a newly defined value on the screen - which means it must work out how to express it as a string (sometimes not very usefully, when it's a function), but it doesn't actually give you an ML value of type string.

But to get this as a string ML value one would normally use PolyML.makestring, or the "production-quality equivalent" of
@{make_string}, followed by |> YXML.parse_body |> XML.content_of.

My question is, what is that production-quality equivalent.

Cheers,

Jeremy




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