K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Hi Charlie,

and thanks for your message.
You are right, the "fresh" mechanism is an exception for binding variables occurring in the right-hand side of a rule.

A more general mechanism, similar to that from Maude, was discussed several times in our group but the current implementation does not support it (yet).

Best regards,
Dorel

On 6/24/13 8:35 PM, Charles Jacobsen wrote:

Hello again,

This module kompiles:

module TEST

  syntax Expr ::= Int "+" Int

  rule I1:Int + I2:Int => S
       when fresh(S:Int)

endmodule

but this one does not:

module TEST

  syntax Expr ::= Int "+" Int

  rule I1:Int + I2:Int => S
       when S:Int ==Int 5

endmodule

Is it not possible to bind a variable in the "when", in general? fresh is just an exception? Perhaps S:Int ==Int 5 is improper.

Thanks, Charlie

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user