K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

First, I think that typing S1 to Stmt would force at least one
statement to be consumed each time rule 2 is applied, and thus avoid
non-termination (although it could be that rule 1 would not get to
apply).

Now, to return to your broader question, unfortunately we don't
currently support [owise] in K (although we plan for some limited
support).

There could be a "hacky" (undocumented, not guaranteed to be
maintained) way to achieve this now somehow similar to how Maude
explains that the owise is just "syntactic sugar".

Namely, what you could do would be to create a predicate for matching
the non-owise patterns, and then add its "negation" in the side
condition of the [owise] rule.

For your particular example, this would amount to:

syntax Bool ::= isBranchStmt(K)   [function]
rule isBranchStmt(I : S) => true

and modifying rule 2 to:
 rule <k> (Branch(I:Id) ~> S1:Stmt) => Branch(I) ...</k>
   when isBranchStmt(S1) =/=K true
   [owise]


or, if you like your rules looking cleaner, you can define
isBranchStmt totally with a different hack:
syntax Bool ::= #isBranchStmt(K)   [function]
                     | isBranchStmt(K) [function]
rule #isBranchStmt(I : S) => true
rule isBranchStmt(K) => #isBranchStmt(K) ==K true

and then use the more elegant version of rule 2:
 rule <k> (Branch(I:Id) ~> S1:Stmt) => Branch(I) ...</k>
   when notBool(isBranchStmt(S1))
   [owise]

2013/4/22 Abdul Dakkak 
<abduld AT wolfram.com>:
>
>
> What's the equivalent statement for maude's owise tag in K? I am trying to 
> implement branch jumps using:
>
>     syntax Stmt ::= Id ":" Stmt
>     syntax K ::= Branch(Id)
>     rule <k> (Branch(I:Id) ~> I : S) => S ...</k> // rule 1
>     rule <k> (Branch(I:Id) ~> S1) => Branch(I) ...</k> [owise] // rule 2
>
> currently the above goes in an infinite loop because rule 2 shadows rule 1. 
> Is there a way around that.
>
> thanks
>
> -adk-
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user