K-user mailing list

["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