Skip to Content.
Sympa Menu

k-user - Re: [K-user] Passing a K object between two different K definitions

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [K-user] Passing a K object between two different K definitions


Chronological Thread 
  • From: Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>
  • To: "Park, Daejun" <dpark69 AT illinois.edu>
  • Cc: Jiho Choi <jray319 AT gmail.com>, "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>, "Shull, Thomas Edward" <shull1 AT illinois.edu>
  • Subject: Re: [K-user] Passing a K object between two different K definitions
  • Date: Thu, 12 Dec 2013 00:01:12 +0200
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

Look in the reference manual :-D (just joking) 

I wrote at some point the include/modules/k-parser.k
which could print a K as an S-_expression_ and read it at a later stage.  This is fully in K.
Not sure if this is still working, though, as this was before the token representation of constants was added.

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.

best wishes,
Traian


2013/12/11 Park, Daejun <dpark69 AT illinois.edu>
Hi all,

What would be an easy (and safe, not need to be elegant) way to pass a K object between two different K definitions?
For example, is it possible that a K definition prints out something in an AST form and another K definition reads it?
I think it seems to have something to do with a combination of kast and krun --parser option, but I cannot find a concrete example.

Let me explain my initial problem:
Suppose that a K definition has two phases:
The first phase just transforms a given original program to a simpler one (with the same syntax.)
And the second phase has an actual semantics based on the simpler syntax (i.e., a subset of the original syntax).

In this case, I want to clearly separate two phases: each phase has its own K definition and they are executed at different processes.
This is partly because two phases use the almost same syntax but different annotations such as "strict". Of course, there would be an way to manage such cases, but I just want to make it simple and make my life easier.

In that case, my first trial was to simply print out the transformed program and read it later. However, it does not work due to the limitation of pretty-printing. Of course, pretty-printing will be improved, but I think it is not an ultimate way to do my job, because of the tricky problem of parentheses. So, I think it would be better to use the AST form as a medium to pass such an information.

Thanks in advance.

Best,
Daejun
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user




Archive powered by MHonArc 2.6.16.

Top of Page