search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Do we have KORE support for pretty-printing? #1940

Open grosu opened 8 years ago

grosu commented 8 years ago

Do we? If we do, then wouldn't it be nice to use it when defining the Id2String function? That is, instead of using a hook, like we do now,

syntax String ::= "Id2String" "(" Id ")"    [function, hook(STRING.token2string), klabel(Id2String)]

to have something like this

syntax String ::= Id2String(Id)  [function]
rule Id2String(X:Id) => #prettyPrint(X)
cos commented 8 years ago

Yes, we could. Should #prettyPrint be hooked to the meta or ground-level unparsing? I.e., should it print #token("foo", Id) or foo? From the example, it seems it should be the latter.

grosu commented 8 years ago

Yes, I think the latter. And this should be the naive prettyPrinter, not the smart unparser. We will probably have an unparser hook, too, but no need to worry about it right now. Thanks.

dwightguth commented 8 years ago

I will say I have no objection to having a #prettyPrint function but I am strongly opposed to using it to implement more basic conversions between types. This is both a performance issue and an issue with compatibility because supporting the pretty-printer from within the OCAML backend would be highly nontrivial.