EmitML prints types with reserved words

[xrchz]

Emitting something like

val _ = Hol_datatype `op = Foo`
val _ = Hol_datatype `bar = Bar of op`
emitLib.eSML "bug" [DATATYPE `op = Foo`, DATATYPE `bar = Bar of op`]

generates the inconsistent and invalid

signature bugML =
sig
  datatype op_ = Foo
  datatype bar = Bar of op
end

This is not trivial to fix because EmitML uses type_pp.pp_type for arguments on the right hand side of a datatype.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

The fix would probably be to link the type pretty-printer up to a backend that knew to munge particular tokens as they were emitted.

[konrad-slind]

Seems to me that futzing with the overload map when calling emitML would
do the trick, but I haven't thought it through. (Is there an overload
map for types?) If that doesn't work, then you could add a constant
"op_" to the type signature when calling emitML and when pp_type_as_ML
comes to prettyprint a type, recurse through the type, do the

op |-> op_

replacement. Ugly, I know, but it is prettyprinting after all.

Konrad.

On Mon, Apr 2, 2012 at 6:16 PM, Ramana Kumar
[email protected]
wrote:

Emitting something like

   val _ = Hol_datatype op = Foo
   val _ = Hol_datatype bar = Bar of op
   emitLib.eSML "bug" [DATATYPE op = Foo, DATATYPE bar = Bar of op]

generates the inconsistent and invalid

   signature bugML =
   sig
     datatype op_ = Foo
     datatype bar = Bar of op
   end

This is not trivial to fix because EmitML uses type_pp.pp_type for arguments on the right hand side of a datatype.

---

Reply to this email directly or view it on GitHub:
#56

[xrchz]

My workaround is

val _ = Parse.temp_type_abbrev("op_",``:op``)

That's what you mean, right Konrad?
It's an easy workaround, but probably EmitML should be better (doing as Michael suggested I think).

[konrad-slind]

Yes, that's it. Not very solid-feeling, as you say.

Konrad.

On Mon, Apr 2, 2012 at 7:13 PM, Ramana Kumar
[email protected]
wrote:

My workaround is

   val _ = Parse.temp_type_abbrev("op_",:op)

That's what you mean, right Konrad?
It's an easy workaround, but probably EmitML should be better (doing as Michael suggested I think).

---

Reply to this email directly or view it on GitHub:
#56 (comment)