K-user mailing list

[Soha H <husseinsoh AT gmail.com>]

I will give it a try. Thanks Everett.

Soha

On May 18, 2017, at 4:57 PM, Everett Hildenbrandt <hildenb2 AT illinois.edu> wrote:

Can you just declare your own `HOLE`? Name it however you like, or even have it
parametric. `#freezerFunCall` is an example of a parametric hole because it
needs to remember the argument to the function-call when it's done evaluating
the function _expression_.

```k
   syntax K ::= "HOLE" | parametricHole ( Exp )
```

Will that work?

Everett H.

On Thu, May 18, 2017 at 01:07:53PM +0200, Soha H wrote:

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