Converting terms to string?

[LaifsV1]

For instance, if I have a term fun ( x : int ) : ( unit ) -> assert( x ) which is written in some syntax Term I defined, is there a way to convert it into the string "fun ( x : int ) : ( unit ) -> assert( x )"? i.e. some function Term -> String that just outputs the term as a String.

[nishantjr]

That functionality is not available unfortunately. For tokens (productions marked with the [token] attribute) you may use the token2String hook like so:

syntax String ::= XToString(X) [function, functional, hook(STRING.token2string)]

[dwightguth]

There are a number of reasons why this is probably not going to be implemented anytime soon, most importantly that unparsing is part of the K frontend and implements a postprocessing stage after the semantics has reached its final state. It breaks a lot of abstraction boundaries to try to make this available to backends, because suddenly the backend depends on an important component of the frontend. Furthermore, there is no clear semantics for such a function. Should I return "fun ( x : int ) : ( unit ) -> assert( x )" or "fun ( x : int ) : ( unit ) -> ( assert( x ) )" or "fun(x:int):(unit)->assert(x)"? It's not really appropriate for the formal reasoning about the behavior of your program to depend on a particular convention adopted by a particular piece of code written in Java that doesn't have clear semantics.

With that being said, if you want to have a semantics of something like this in your language you can and are encouraged to write a function like syntax String ::= Term2String(Term) [function] and give it whatever explicit semantics you want. This is a much more formal solution because your function actually has a clear and unambiguous formally specified behavior, which is not true in the former case.

[LaifsV1]

Thanks for the replies!

So I should define a procedure that recursively rewrites my term into a string. What happens if I reach something like a Bool or KVar? Do these have a to-string function?

Edit: Bool is not a good example since I can do true -> "true". But what about integers or variables?

[nishantjr]

The token2string thing above will work for Int KVar and other tokens

[LaifsV1]

Thanks!

Somewhat unrelated, how does one use #system in a function? I have a function:

syntax Bool ::= System(KItem)     [function]
rule System(#systemResult( 0, _  , _ )) => true
rule System(#systemResult( 1, _, _ )) => false

the intention is to do System(#system(CMD)) to run some command CMD. However, I get:

[Error] Inner Parser: Parse error: unexpected token '#system'.
[Error] Inner Parser: Parse error: unexpected token '#systemResult'.

EDIT: fixed the error. It seems I can't place #system on SYNTAX modules.

[dwightguth]

You are trying to put #system in your initial program? there are some peculiarities to the parser that make it not necessarily advisable to try to use non-user-defined syntax in the input program you parse with kast and krun. You are better off having a rule that has #system on the rhs.

[LaifsV1]

Ah, no, I was trying to use #system to call z3 to prune paths in my symbolic execution, and the idea was to write a function that makes the external call.

To give some context, I had two modules, Z3-SYNTAX and Z3. In Z3-SYNTAX, I had originally defined a function System(KItem) which performs external calls. This function has #system rules on the RHS.

  syntax Bool ::= CheckSAT(SMTLib)  [function]
  syntax Bool ::= SystemSAT(KItem)  [function,strict(1)]

  rule CheckSAT(P) => SystemSAT(#system("echo \"" +String SMTLibToString(P) +String "(check-sat)\" | z3 -in"))
  rule SystemSAT(#systemResult ( 0, "sat\n" ,   _)) => true
  rule SystemSAT(#systemResult ( 0, "unsat\n" , _)) => false

When trying to kompile the z3.k file, the parser was failing when I had the CheckSAT and SystemSAT functions in the Z3-SYNTAX module. But this was fixed when I moved the functions down to the Z3 module. So I concluded I'm either not allowed to have #system tokens in -SYNTAX modules, or I missed importing something needed to perform #system calls.