fix old syntax and wrong heuristic.

Author: wadoon

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/msetRules.key

@@ -31,7 +31,7 @@
             \then(msetEmpty)
             \else(msetRange{uSub;}(left, right, t)))
 
-        \heuristics(out_of_bounds)
+        \heuristics(simplify)
     };
 
     mset_Single {
@@ -230,15 +230,15 @@
         \schemaVar \term Heap h;
         \schemaVar \term Object array;
 
-        \find(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub))))
+        \find(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub))))
         \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right), \notFreeIn(uSub, h), \notFreeIn(uSub, array))
         \replacewith(\if(left <= middle & middle <= right)
-                     \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h, array, arr(uSub))),
-                                           msetSingle(beta::select(h, array, arr(middle)))),
-                                   msetRange{uSub;}(middle+1, right, beta::select(h, array, arr(uSub)))))
-                     \else(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub)))))
+                     \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, select<[beta]>(h, array, arr(uSub))),
+                                           msetSingle(select<[beta]>(h, array, arr(middle)))),
+                                   msetRange{uSub;}(middle+1, right, select<[beta]>(h, array, arr(uSub)))))
+                     \else(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub)))))
         \heuristics(comprehension_split, triggered)
-        \trigger {middle} msetSingle(beta::select(h, array, arr(middle)))
+        \trigger {middle} msetSingle(select<[beta]>(h, array, arr(middle)))
         \avoid middle <= -1 + left, right <= -1 + middle;
     };
 
@@ -250,13 +250,13 @@
         \schemaVar \variables int uSub;
         \schemaVar \term alpha x;
 
-        \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(middle), x), array, arr(uSub))))
+        \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(middle), x), array, arr(uSub))))
         \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, middle), \notFreeIn(uSub, right))
         \replacewith(\if(left <= middle & middle <= right)
-                     \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, beta::select(h, array, arr(uSub))),
+                     \then(msetSum(msetSum(msetRange{uSub;}(left, middle-1, select<[beta]>(h, array, arr(uSub))),
                                            msetSingle({\subst uSub; middle} x)),
-                                   msetRange{uSub;}(middle+1, right, beta::select(h, array, arr(uSub)))))
-                     \else(msetRange{uSub;}(left, right, beta::select(h, array, arr(uSub)))))
+                                   msetRange{uSub;}(middle+1, right, select<[beta]>(h, array, arr(uSub)))))
+                     \else(msetRange{uSub;}(left, right, select<[beta]>(h, array, arr(uSub)))))
         \heuristics(simplify_ENLARGING)
     };
 
@@ -267,10 +267,10 @@
         \schemaVar \term Object array;
         \schemaVar \term alpha x;
 
-        \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(left), x), array, arr(uSub))))
+        \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(left), x), array, arr(uSub))))
         \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right))
         \replacewith(msetSum(msetSingle({\subst uSub; left} x),
-                             msetRange{uSub;}(left+1, right, beta::select(h, array, arr(uSub)))))
+                             msetRange{uSub;}(left+1, right, select<[beta]>(h, array, arr(uSub)))))
         \heuristics(simplify_enlarging)
     };
 
@@ -281,9 +281,9 @@
         \schemaVar \term Object array;
         \schemaVar \term alpha x;
 
-        \find(msetRange{uSub;}(left, right, beta::select(store(h, array, arr(right), x), array, arr(uSub))))
+        \find(msetRange{uSub;}(left, right, select<[beta]>(store(h, array, arr(right), x), array, arr(uSub))))
         \varcond(\notFreeIn(uSub, left), \notFreeIn(uSub, right))
-        \replacewith(msetSum(msetRange{uSub;}(left, right-1, beta::select(h, array, arr(uSub))),
+        \replacewith(msetSum(msetRange{uSub;}(left, right-1, select<[beta]>(h, array, arr(uSub))),
                              msetSingle({\subst uSub; right} x)))
         \heuristics(simplify_enlarging)
     };
@@ -294,12 +294,12 @@
         \schemaVar \term Heap h;
         \schemaVar \term Object array;
 
-        \find(msetRange{uSub;}(low, high, beta::select(h, array, arr(uSub))))
+        \find(msetRange{uSub;}(low, high, select<[beta]>(h, array, arr(uSub))))
         \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array))
-        \replacewith(msetSum(msetSingle(beta::select(h, array, arr(low))),
-                             msetRange{uSub;}(low+1, high, beta::select(h, array, arr(uSub)))))
+        \replacewith(msetSum(msetSingle(select<[beta]>(h, array, arr(low))),
+                             msetRange{uSub;}(low+1, high, select<[beta]>(h, array, arr(uSub)))))
         \heuristics(comprehension_split, triggered)
-        \trigger {low} msetSingle(beta::select(h, array, arr(low)))
+        \trigger {low} msetSingle(select<[beta]>(h, array, arr(low)))
         \avoid low >= high, false;
     };
 
@@ -309,12 +309,12 @@
         \schemaVar \term Heap h;
         \schemaVar \term Object array;
 
-        \find(msetRange{uSub;}(low, high, beta::select(h, array, arr(uSub))))
+        \find(msetRange{uSub;}(low, high, select<[beta]>(h, array, arr(uSub))))
         \varcond(\notFreeIn(uSub, low), \notFreeIn(uSub, high), \notFreeIn(uSub, h), \notFreeIn(uSub, array))
-        \replacewith(msetSum(msetSingle(beta::select(h, array, arr(high))),
-                             msetRange{uSub;}(low, high-1, beta::select(h, array, arr(uSub)))))
+        \replacewith(msetSum(msetSingle(select<[beta]>(h, array, arr(high))),
+                             msetRange{uSub;}(low, high-1, select<[beta]>(h, array, arr(uSub)))))
         \heuristics(comprehension_split, triggered)
-        \trigger {high} msetSingle(beta::select(h, array, arr(high)))
+        \trigger {high} msetSingle(select<[beta]>(h, array, arr(high)))
         \avoid high <= low, false;
     };
 }