K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

That's not a good idea in general.  Even in purely syntactic definitions, you 
end up extending the syntax of expressions with new values.  For example, 
adding closures to an environment-based definition of lambda calculus, or 
adding "error" values to catch division-by-zero, etc.  While you could argue 
that you don't want to change the original syntax for semantic reasons, it is 
in fact acceptable and common practice.  But if you still don't want to, then 
so be it, let's try to find a solution your way.

BTW, I noticed in general that you write more than you should in your rules.  
For example,

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

is completely equivalent to 

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

You should be able to "shut up" the parser by doing this:

 rule printExps((V1:Val)::Exp , Rest) => .

This rule still performs the dynamic check that V1 is a Val, but for parsing 
reasons it tells K to treat it as an Exp (note the :: used for syntactic 
casting instead of :).  If this does not work (sorry, cannot try it now 
myself), then you should be able to replace it with

 rule printExps(V1::Exp , Rest) => . when isVal(V1)

Finally, don't forget that syntax in K is nothing but syntactic sugar :)  You 
can always work with KASTs:

  rule 'printExps`(_`)(V1:Val,, Rest) => .

This way you take the parser out of the picture completely.

Grigore



________________________________________
From: Ömer Sinan Ağacan 
[omeragacan AT gmail.com]
Sent: Thursday, September 19, 2013 10:26 AM
To: Rosu, Grigore
Cc: Moore, Brandon Michael; 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] how strictness annotations generate invalid terms

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