K-user mailing list

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

No. In my program I deliberately want to avoid doing such a thing (for
debugging purposes, correctness, etc.)

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


2013/9/19 Rosu, Grigore 
<grosu AT illinois.edu>:
> Do you have syntax Exp ::= Val somewhere?
>
> Grigore
>
>
>
> ________________________________________
> 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: Thursday, September 19, 2013 10:18 AM
> To: Moore, Brandon Michael
> Cc: 
> k-user AT cs.uiuc.edu
> Subject: Re: [K-user] how strictness annotations generate invalid terms
>
> 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
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user