imp-simple: Use DOTVAR instead of dotk as second argument of kseq

kframework · Jul 3, 2019 · b5d8d9d · b5d8d9d
1 parent bee7247
commit b5d8d9d
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/t/imp-simple/expected.ekore b/t/imp-simple/expected.ekore
@@ -34,8 +34,8 @@ endmodule [  ]
 
 module IMP-SIMPLE
 
-  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( False {  } (  ) , VarB : BExp {  } ) ) , dotk {  } (  ) ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( False {  } (  ) ) , dotk {  } (  ) ) ) ) ) [  ]
-  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( True {  } (  ) , VarB : BExp {  } ) ) , dotk {  } (  ) ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( VarB : BExp {  } ) , dotk {  } (  ) ) ) ) ) [  ]
+  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( False {  } (  ) , VarB : BExp {  } ) ) , DOTVAR : K { } ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( False {  } (  ) ) , DOTVAR : K { } ) ) ) ) [  ]
+  axiom {  } \rewrites { KCell {  } } ( \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( And {  } ( True {  } (  ) , VarB : BExp {  } ) ) , DOTVAR : K { } ) ) ) , \and { KCell {  } } ( \top { KCell {  } } ( ) , kCell {  } ( kseq {  } ( inj { BExp {  } , KItem {  } } ( VarB : BExp {  } ) , DOTVAR : K { } ) ) ) ) [  ]
   import D-K [  ]
   sort BExp {  } [  ]
   sort KCell {  } [  ]

diff --git a/t/imp-simple/imp-simple.ekore b/t/imp-simple/imp-simple.ekore
@@ -46,8 +46,8 @@ module IMP-SIMPLE
                 | BExp "&&" BExp     [klabel(And)]
   syntax KCell ::= "kCell" "(" K ")" [klabel(kCell)]
 
-  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),dotk{}()))
-    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),dotk{}()))
-  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),dotk{}()))
-    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),dotk{}()))
+  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(True{}(),VarB:BExp{})),DOTVAR:K{}))
+    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),DOTVAR:K{}))
+  rule kCell{}(kseq{}(inj{BExp{}, KItem{}}(And{}(False{}(),VarB:BExp{})),DOTVAR:K{}))
+    => kCell{}(kseq{}(inj{BExp{}, KItem{}}(False{}()),DOTVAR:K{}))
 endmodule