K-user mailing list

[Andrei Arusoaie <andrei.arusoaie AT gmail.com>]

Hi Omer,

I'm not sure I really understand what you're trying to do with those rules but I'm sure you can solve everything in a simple way.

First, let us reconsider what you have:

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

    syntax Val ::= ...

    syntax KResult ::= Val

If you have [strict] for somePredicate then the tool automatically *heats* (by generating some *heating* rewrite rules) your computation for all the expressions  somePredicate(E1, E2) into:

E1 ~> somePredicate(HOLE, E2)

E2 ~> somePredicate(E1, HOLE)

Then it evaluates E1 and E2 according to your rules --those for evaluating expressions from your semantics, not the ones you mentioned in the previous mail-- (make sure Exp is not subsorted to Val) and then when E1(E2) is evaluated to V1(V2) which is of sort Val the tool *cools* the computation, that is, your final evaluated _expression_ for somePredicate will be

somePredicate(V1, V2)

Now, when you write your rule for somePredicate you have to specify the sort of your variables:

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

Otherwise, if you write:

rule somePredicat(V1, V2) => something else 

the tool will sort V1 and V2 to K and this is not what you want because Exp may be a subsort of K and the tool may apply this rule instead of heating/cooling rules.

Hope this helps. Maybe if you attach your definition we can look at it and give more feedback.

K developer,

Andrei A.

2013/9/16 Ömer Sinan Ağacan <omeragacan AT gmail.com>

A correction:

>     rule <k> somePredicate(E1:Exp, E2:Exp) ~> E1 ~>
> somePredicate1(HOLE, E2) ... </k>

should be

    rule <k> somePredicate(E1:Exp, E2:Exp) => E1 ~>
somePredicate1(HOLE, E2) ... </k>

---
Ö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