K-user mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Thanks. This explains everything.

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


2013/9/18 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