Skip to Content.
Sympa Menu

k-user - [K-user] a question about strictness annotation

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] a question about strictness annotation


Chronological Thread 
  • From: Ömer Sinan Ağacan <omeragacan AT gmail.com>
  • To: "k-user AT cs.uiuc.edu" <k-user AT cs.uiuc.edu>
  • Subject: [K-user] a question about strictness annotation
  • Date: Mon, 16 Sep 2013 06:37:08 +0300
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
  • List-id: <k-user.cs.uiuc.edu>

Hi,

I'm trying to figure out how exactly strictness annotation works. My
problem is that when I rely on strictness annotations in my program, I
have too much bugs. So I decided to not to use strictness annotations
in my programs but this time my program is full of HOLE variables and
I need to plug in evaluated values to HOLEs manually, which is very
boring and repetitive process.

Let's say I have this syntax:

syntax Exp ::= somePredicate(Exp, Exp) [strict]

syntax Val ::= ...

syntax KResult ::= Val

the problem with this definition is that when two Exps evaluated,
results will be in Val syntactic category, so cooling rules doesn't
apply(because can't plug Val values to somePredicate). So if I
understand this stuff correctly, for strictness annotations to work,
resulting values should be in same syntactic category.

And I don't want to do this because I want my programs to get stuck as
soon as possible. I want evaluation of every sub expression to result
with an value and get stuck otherwise.

But then I have to create new syntax for intermediate stages of
computation and manually plug every resulting value to that new
syntax. For instance, to evaluate somePredicate syntax, I need this
rules:

syntax K ::= somePredicate1(Val, Exp) | somePredicate2(Val, Val)
rule <k> somePredicate(E1:Exp, E2:Exp) ~> E1 ~>
somePredicate1(HOLE, E2) ... </k>
rule <k> V:Val ~> somePredicate1(HOLE, E:Exp) => somePredicate1(V,
E) ... </k>
rule <k> somePredicate1(V:Val, E:Exp) ~> E ~> somePredicate2(V,
HOLE) ... </k>
rule <k> V2:Val ~> somePredicate2(V1:Val, HOLE) =>
somePredicate2(V1, V2) ... </k>
rule <k> somePredicate2(V1, V2) => whatever I want to do with this </k>

and this is ridiculously long code for just to evaluate some
subexpressions. Think of this but for the whole language syntax.

I'm probably doing something wrong here, can anyone help me for what
I'm trying to do?

Thanks,


---
Ömer Sinan Ağacan
http://osa1.net





Archive powered by MHonArc 2.6.16.

Top of Page