K-user mailing list

[Chris Hathhorn <chathhorn AT gmail.com>]

On Wed, Dec 11, 2013 at 4:01 PM, Traian Florin Șerbănuță
<traian.serbanuta AT info.uaic.ro>
 wrote:
> What could work is some hooked code which Dwight wrote (and used in the
> Python semantics), which can be found at the end of uris.k
> more precisely, you probably want to use:
>   syntax K ::= String2K(String) [function, hook(#K-PARSER:string2k)]
>   syntax String ::= K2String(K) [function, hook(#K-PRINTER:k2string)]
>
> These should probably work regardless of changes in K, because Dwight uses
> reflection in Maude to implement them.

See lines 28-50 of python-semantics-builtin-modules.k[1] and lines
32-34 of Makefile[2] (per Dwight's email from a few months ago) for
examples of this.

FWIW, I tried that method with the C semantics and found the overhead
(in terms of saving/loading time) to be pretty atrocious. It's
probably practical for smaller configurations, though. Currently I'm
using the "--load-cfg" option I added to krun in order to load
configurations saved with the "binary" output mode. It just loads the
deserialized configuration into the $PGM configuration variable
instead of a program. It's pretty hackish, though -- I'd certainly
appreciate it were you to rework this into some more general
mechanism.

[1] - 
https://github.com/kframework/python-semantics/blob/master/python-semantics-builtin-modules.k
[2] - https://github.com/kframework/python-semantics/blob/master/Makefile

Chris