K-user mailing list

[Soha H <husseinsoh AT gmail.com>]

I don’t think strictness attribute is going to be helpful in my case. What I am doing is given a program, written in say C like language, I generate a new program that is non oblivious by changing the control flow of the program. The way I do it is by wrapping the whole program around a construct “obliv” and change its AST according to some rules. The result is the modified e program. So my values are _expression_, but then I want to reduce expressions that have obiv around them. That is, i.e., obliv (X := e) => X := obliv(e). I can’t make obliv a function because I want it to access the environment. This is why I though of controlling the evaluation through HOLE.

Would going back to an older version of K help me?

Soha

On May 18, 2017, at 10:54 AM, Eric Huber <echuber2 AT illinois.edu> wrote:

I believe that by specifying the [strict]ness rules on your syntax, you can avoid having to manually declare these intermediate stages.

On May 18, 2017 3:36 AM, "Soha H" <husseinsoh AT gmail.com> wrote:

Hello,

It looks like HOLE is not recognizable by K anymore, are there any alternatives? Can someone give an example on how to write something like this in new K

E1:Exp + E2:Exp => E1 ~> HOLE + E2 (A)

V:Val ~> HOLE + E2 => V + E2

I found #freezer in kool_typed_dynamic, is it used for that purpose? Code is below

  rule (A:Exp(B:Exps))(C:Exps) => A(B) ~> #freezerFunCall(C) (B)

  rule (A:Exp[B:Exps])(C:Exps) => A[B] ~> #freezerFunCall(C)

  rule V:Val ~> #freezerFunCall(C:Exps) => V(C)

  syntax KItem ::= "#freezerFunCall" "(" K ")"

 

Rules like in (A) above are very flexible, because HOLE resides in the spot where where computation should resume, while in (B) I would need to defined multiple freezers for different contexts. 

Did I get it right? Is there anything I am missing? 

Much appreciated! 

Soha