K-user mailing list

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

This is very, very confusing. Let's say I have this syntax:


    syntax Exps ::= List{Exp, ","}
    syntax K ::= printExps(Exps) [strict]


Now I want to write a rule about printExps syntax.


    rule <k> printExps(V1:Val , Rest) => . ... </k>


But this doesn't work because printExp argument should be Exps, which
means V1 should be Exp. Here's the error message:


    [Error] Critical: type error: unexpected term 'V1:Val ' of sort
'Val', expected sort 'Exp'.
            File: /home/omer/K/lua-semantics/lua.k
            Location: (29,17,29,23)


... this is so frustrating. After heating and cooling that Exps will
be rewritten to Vals, which is list of values with same syntax. I have
a hundred extra syntax rules because of manually handling HOLE
variables and heating/cooling because of this kind of weird problems.

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


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