K-user mailing list

[Eric Huber <echuber2 AT illinois.edu>]

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