k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] how strictness annotations generate invalid terms

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] how strictness annotations generate invalid terms
Date: Tue, 17 Sep 2013 23:57:56 +0300
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

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] how strictness annotations generate invalid terms, Ömer Sinan Ağacan, 09/17/2013
- Re: [K-user] how strictness annotations generate invalid terms, Moore, Brandon Michael, 09/17/2013
  - Re: [K-user] how strictness annotations generate invalid terms, Ömer Sinan Ağacan, 09/17/2013
    - Re: [K-user] how strictness annotations generate invalid terms, Ömer Sinan Ağacan, 09/19/2013
      - Re: [K-user] how strictness annotations generate invalid terms, Rosu, Grigore, 09/19/2013
        
        Re: [K-user] how strictness annotations generate invalid terms, Ömer Sinan Ağacan, 09/19/2013
        
        Re: [K-user] how strictness annotations generate invalid terms, Rosu, Grigore, 09/19/2013
        
        Re: [K-user] how strictness annotations generate invalid terms, Ömer Sinan Ağacan, 09/19/2013