Rules for clearing the store in the case of dcs (for #10)

kframework · Jun 20, 2017 · b2cb2b1 · b2cb2b1
1 parent cbac693
commit b2cb2b1
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/haskell-core-execution.k b/src/haskell-core-execution.k
@@ -305,5 +305,11 @@ module HASKELL-CORE-EXECUTION
     <k> val(L) => O </k>
     <store> Sto:Map (L |-> O) => .Map </store>
     <env> _ => .Map </env>
+  rule
+    <k> dc(R) </k>
+    <store> M:Map (_ |-> _) => .Map </store>
+  rule
+    <k> dc(R) </k>
+    <env> M:Map (_ |-> _) => .Map </env>
 
 endmodule