Deterministic choice operator

prover/strategies/core.md

@@ -23,8 +23,15 @@ module PROVER-CORE-SYNTAX
   syntax SequenceStrategy ::= Strategy "." Strategy [right]
   syntax ResultStrategy ::= "noop"
                           | TerminalStrategy
+                          | IntroduceBranchStrategy
+                          | ResolveBranchStrategy
                           | Strategy "&" Strategy [right, format(%1%n%2  %3)]
                           | Strategy "|" Strategy [right, format(%1%n%2  %3)]
+
+  syntax IntroduceBranchStrategy ::= Strategy "&>" Strategy [right, format(%1%n%2  %3)]
+
+  syntax ResolveBranchStrategy ::= Strategy "<|" Strategy [right, format(%1%n%2  %3)]
+
   syntax Strategy ::= "or-split" | "and-split" | "or-split-rhs"
   syntax Strategy ::= "prune" "(" Patterns ")"
 
@@ -53,10 +60,6 @@ module PROVER-CORE
 
 `Strategy`s can be sequentially composed via the `.` operator.
 
-```k
-  rule <k> (S . T) . U => S . (T . U) ... </k>
-```
-
 Since strategies do not live in the K cell, we must manually heat and cool.
 `ResultStrategy`s are strategies that can only be simplified when they are
 cooled back into the sequence strategy.
@@ -65,7 +68,7 @@ cooled back into the sequence strategy.
   syntax ResultStrategy ::= "#hole"
   rule <k> S1 . S2 => S1 ~> #hole . S2 ... </k>
     requires notBool(isResultStrategy(S1))
-     andBool notBool(isSequenceStrategy(S1))
+
   rule <k> S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... </k>
 ```
 
@@ -185,6 +188,33 @@ approach succeeds:
      andBool notBool(isTerminalStrategy(S2))
 ```
 
+The `<|` strategy allows us to choose different strategies
+for different subgoals.
+
+```k
+
+  rule <k> S &> fail => fail ... </k>
+  rule <k> fail &> S => fail ... </k>
+  rule <k> S &> success => S ... </k>
+  rule <k> success &> S => S ... </k>
+
+  // we could achieve the same result using &> on RHS
+  rule ((I1 &> Is) . (O1 <| Os)) => ((I1 . O1) & (Is . Os))
+
+  rule (I1 &> Is) . S => (I1 . S) &> (Is . S)
+    requires notBool isResolveBranchStrategy(S)
+
+  rule <k> T:TerminalStrategy ~> #hole &> S2
+           => T &> S2
+           ...
+       </k>
+
+  rule <k> ((S1 &> S2) => subgoal(GOAL, S1) ~> #hole &> S2) </k>
+       <claim> GOAL:Pattern </claim>
+    requires notBool(isTerminalStrategy(S1))
+     andBool notBool(isTerminalStrategy(S2))
+```
+
 The S { N } construct allows us to repeat a strategy S N times
 
 ```k
@@ -262,7 +292,7 @@ Internal strategy used to implement `or-split` and `and-split`.
   syntax Strategy ::= "#andSplit" "(" Patterns ")" [function]
   rule #andSplit(.Patterns) => noop
   rule #andSplit(P:Pattern, .Patterns) => replace-goal(P)
-  rule #andSplit(P:Pattern, Ps) => replace-goal(P) & #andSplit(Ps) [owise]
+  rule #andSplit(P:Pattern, Ps) => replace-goal(P) &> #andSplit(Ps) [owise]
 ```
 
 If-then-else-fi strategy is useful for implementing other strategies:

prover/t/deterministic-choice.kore

@@ -0,0 +1,16 @@
+symbol P() : Bool
+symbol Q() : Bool
+symbol R() : Bool
+symbol S() : Bool
+
+axiom p: P()
+axiom q: \equals(Q(), P())
+axiom r: \equals(R(), P())
+axiom s: \equals(S(), P())
+
+claim \and(Q(), R(), S())
+strategy (and-split
+      .( apply-equation -> q at 0 by []
+      <| apply-equation -> r at 0 by []
+      <| apply-equation -> s at 0 by []
+       )) . apply(p, fail)

prover/t/deterministic-choice.kore.expected

@@ -0,0 +1,44 @@
+<prover>
+  <exit-code>
+    0
+  </exit-code>
+  <goals>
+    <goal>
+      id: ., parent: .
+      <claim>
+        \and ( .Patterns )
+      </claim>
+      <k>
+        .
+      </k>n<expected>
+        .
+      </expected>
+      <local-context>
+        .LocalDeclCellSet
+      </local-context>
+    <trace>
+      .
+    </trace>
+  </goals>
+  <declarations>
+    <declaration>
+      axiom ax0 : \and ( Q ( .Patterns ) , R ( .Patterns ) , S ( .Patterns ) , .Patterns )
+    </declaration> <declaration>
+      axiom p : P ( .Patterns )
+    </declaration> <declaration>
+      axiom q : \equals ( Q ( .Patterns ) , P ( .Patterns ) )
+    </declaration> <declaration>
+      axiom r : \equals ( R ( .Patterns ) , P ( .Patterns ) )
+    </declaration> <declaration>
+      axiom s : \equals ( S ( .Patterns ) , P ( .Patterns ) )
+    </declaration> <declaration>
+      symbol P ( .Sorts ) : Bool
+    </declaration> <declaration>
+      symbol Q ( .Sorts ) : Bool
+    </declaration> <declaration>
+      symbol R ( .Sorts ) : Bool
+    </declaration> <declaration>
+      symbol S ( .Sorts ) : Bool
+    </declaration>
+  </declarations>
+</prover>