K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

Your grammar is only enforced during parsing.

After the definition is compiled, return is just a label that may be applied 
to a list of children.

In particular, the automatically generated cooling rule only puts a side 
condition that enforces IsKResult, which nil passes.

Brandon

________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Ömer Sinan Ağacan 
[omeragacan AT gmail.com]
Sent: Tuesday, September 17, 2013 3:57 PM
To: 
k-user AT cs.uiuc.edu
Subject: [K-user] how strictness annotations generate invalid terms

Hi,

I already asked this question two days ago but still couldn't get an
answer, sorry for repeating but I'm still confused about this.

What I don't understand is when I have this syntax of expressions and values:


    module TEST

      syntax Exp ::= "nilExp" | return(Exp) [strict]

      syntax Val ::= "nil"

      syntax KResult ::=  Val

      rule <k> nilExp => nil ... </k>

    endmodule


I don't understand how can heating/cooling rules generate the term
`return(nil)` because according to this syntax rules this term should
not be possible. (return takes Exp as argument, not Val).

This rule

    rule <k> weird => return(nil) ... </k>

is rejected by kompiler (but `weird => return(nilExp) ... ` works)

Can anyone explain me how does that work?


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

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user