K-user mailing list

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

Thanks for your help,

> 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

I don't understand this argument. My implementation also has
environments and closures. Here's how I implemented functions without
having `syntax Exp ::= Val`:

(only relevant parts are pasted below)


    syntax Val ::= Function(Map, Names, Block)

    syntax Block ::= ... // think a list of statements

    syntax Names ::= ... // think a list of identifiers for formal
parameters of function

    rule <k> functiondef(funcbody(novararg(Names), Block)) =>
Function(ClosureEnv, Names, Block) ... </k>
         <env> ClosureEnv </env>


function application is kinda long(because of manually handling
heating/cooling etc) so I'll won't paste here but it works great.

Solutions with :: and directly coding in KAST didn't work(I got same
errors). So instead I ended up with adding `syntax Exp ::= Val` for
now.


(rest of this email contains my random ideas on this topic while I had
while debugging my programs with strictness annotations and replacing
strictness annotations with rules)

This is how I'd design strictness annotations(but I'm probably wrong
since I'm just a beginner in K).

Let's say I have this syntax:


    syntax Exp ::= P(Exp, Exp, Exp) [strict]


for intermediate steps while fully evaluating this expression, I'd
design the K framework so that these syntax and rules would be
automatically generated:


    syntax K ::= P__rw_1(Val, Exp, Exp) [strict]
               | P__rw_2(Exp, Val, Exp) [strict]
               | P__rw_3(Exp, Exp, Val) [strict]

    rule P(E1, E2, E3) => E1 ~> P__rw_1(HOLE, E2, E3)
    rule P(E1, E2, E3) => E2 ~> P__rw_1(E1, HOLE, E3)
    rule P(E1, E2, E3) => E3 ~> P__rw_1(E1, E2, HOLE)

    rule V:Val ~> P__rw_1(HOLE, E2, E3) => P__rw_1(V, E2, E3)
    rule V:Val ~> P__rw_2(E1, HOLE, E3) => P__rw_2(E1, V, E3)
    rule V:Val ~> P__rw_3(E1, E2, HOLE) => P__rw_3(E1, E2, V)


and then same rule generation scheme applies to P__rw_1, P__rw_2,
P__rw_3 too. In the end we'll end up with:


    syntax K ::= P__rw(Val, Val, Val)


and this would give the user full control of evaluation with strongly
typed manner. (ie. without fighting with K framework parser)

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


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