k-user AT lists.cs.illinois.edu
Subject: K-user mailing list
List archive
- From: Soha H <husseinsoh AT gmail.com>
- To: Everett Hildenbrandt <hildenb2 AT illinois.edu>
- Cc: Eric Huber <echuber2 AT illinois.edu>, k-user AT lists.cs.illinois.edu
- Subject: Re: [[K-user] ] HOLE and ~> in new K
- Date: Fri, 19 May 2017 12:44:11 +0200
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
- [[K-user] ] HOLE and ~> in new K, Soha H, 05/18/2017
- Re: [[K-user] ] HOLE and ~> in new K, Eric Huber, 05/18/2017
- Re: [[K-user] ] HOLE and ~> in new K, Soha H, 05/18/2017
- Re: [[K-user] ] HOLE and ~> in new K, Everett Hildenbrandt, 05/18/2017
- Re: [[K-user] ] HOLE and ~> in new K, Soha H, 05/19/2017
- Re: [[K-user] ] HOLE and ~> in new K, Everett Hildenbrandt, 05/18/2017
- Re: [[K-user] ] HOLE and ~> in new K, Soha H, 05/18/2017
- Re: [[K-user] ] HOLE and ~> in new K, Eric Huber, 05/18/2017
Archive powered by MHonArc 2.6.19.