K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

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