K-user mailing list

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

Hi Andrei, thanks for your response.

What I don't understand is;

    > rule somePredicate(V1:Val, V2:Val) => something else

To me this rule should give an error at compilation, because in the
syntax definition arguments of somePredicate is specified as Exp, but
here arguments is not Exp but Val.

I also tried that and it worked like I expected:


    ➜  test git:(master) ✗ cat test.k
    module TEST

      syntax Exp ::= "nilExp" | return(Exp) [strict]

      syntax Val ::= "nil"

      syntax KReuslt ::=  Val

      rule <k> nilExp => nil ... </k>

    endmodule
    ➜  test git:(master) ✗ cat test
    return(nilExp)
    ➜  test git:(master) ✗ krun test
    <k>
        nil ~> return ( HOLE )
    </k>
    ➜  test git:(master) ✗


Cooling rule can't apply here because return's parameter type is Exp,
not Val or some super-sort(if such a thing exists) of Val.

Am I missing something?

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