In this short rant I’ll demonstrate how K Framework is broken and how you can avoid the problem. If you don’t know what is K Framework or don’t use it, you probably want to ignore this post.
Let’s think this completely useless K module:
module TEST syntax Exp ::= "nilExp" | return(Exp) [strict] syntax Val ::= "nil" syntax KResult ::= Val rule nilExp => nil ... [nil] endmodule
and this TEST program:
what do you think this program has in K cell when it gets stuck? It’s not really hard to guess. Since we annotate
return(Exp) syntax with
strict, it’s argument gets evaluated according to our
nil rule and then it gets stuck. At this point K cell will be:
<k> return ( nil ) </k>
which may not be very surprising for you, but there’s something wrong going on here. In our syntax declaration we defined argument or
return to be an
Exp, but in the term in our K cell it’s
At this point you can say that this is how heating/cooling works an there’s nothing wrong here but then we have another problem: there’s no way for the user to write rules that does exactly what heating/cooling rules do. In our example above you’d expect from strictness annotation to generate rules like this:
rule return(E:Exp) => E ~> return(HOLE) rule V:Val ~> return(HOLE) => return(V)
but this is not a valid rule and it fails with the this error message:
[Error] Critical: type error: unexpected term 'V:Val ' of sort 'Val', expected sort 'Exp'. File: /home/omer/K/lua-semantics/test/test.k Location: (11,35,11,36)
and what’s more confusing is that even though K generated rule somehow generates the term
return(Val), you cannot match it in your rules because this term is actually ill-typed:
rule return(V:Val) => . ... [Error] Critical: type error: unexpected term 'V:Val ' of sort 'Val', expected sort 'Exp'. File: /home/omer/K/lua-semantics/test/test.k Location: (11,10,11,15)
which means there’s no way for you to work on this term. This time you’re stuck :-p
We discussed this on k-user mailing list a bit but there isn’t really a solution – we only have a workaround. Here’s the reason of this problem(quoted from mailing list discussion):
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.
Wow, this sounds like really broken to me. Anyway, only solution I could find to this is to add
Val syntactic category to a member of
Exp syntactic category. This is an obvious solution, but very bad one also. Because by having distinguished
Exp syntactic categories what I’m trying to do is to force my program to get stuck as soon as possible when something went wrong, instead of continuing evaluation and get stuck at a point where very very far from where the error actually occured.
Rest of this post is also sent to k-list mailing list and contains my ideas on implementing strictness annotations. These ideas may be wrong – I’m only a beginner K user.
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_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)
seqstrict etc. rules are specialized cases of this general strictness rule generation scheme)