drivers/base: Merge <claim> and <k> cells

Author: nishantjr

prover/drivers/base.md

@@ -3,7 +3,7 @@ Configuration
 
 The configuration consists of a assoc-commutative bag of goals. Only goals
 marked `<active>` are executed to control the non-determinism in the system. The
-`<claim>` cell contains the Matching Logic Pattern for which we are searching for a
+`<k>` cell contains the Matching Logic Pattern for which we are searching for a
 proof. The `<strategy>` cell contains an imperative language that controls which
 (high-level) proof rules are used to complete the goal. The `<trace>` cell
 stores a log of the strategies used in the search of a proof and other debug
@@ -21,20 +21,18 @@ module PROVER-CONFIGURATION
 
   configuration
       <prover>
-        <k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
         <exit-code exit=""> 1 </exit-code>
         <goals>
           <goal multiplicity="*" type="Set" format="%1%i%n%2, %3, %4%n%5%n%6%n%7%n%8%n%d%9">
             <active format="active: %2"> true:Bool </active>
             <id format="id: %2"> .K </id>
             <parent format="parent: %2"> .K </parent>
-            <claim> .K </claim>
+            <k> $COMMANDLINE:CommandLine ~> $PGM:Pgm </k>
             <strategy> .K </strategy>
             <expected> .K </expected>
             <local-context>
               <local-decl multiplicity="*" type="Set">  .K </local-decl>
             </local-context>
-
             <trace> .K </trace>
           </goal>
         </goals>

prover/drivers/kore-driver.md

@@ -67,18 +67,18 @@ in the subgoal and the claim of the named goal remains intact.
            ...
        </k>
 
-  rule <k> claim NAME : PATTERN
-           strategy STRAT
-        => .K
-           ...
-       </k>
-       <goals>
+  rule <goals>
+         <k> claim NAME : PATTERN
+             strategy STRAT
+          => .K
+             ...
+         </k>
          ( .Bag =>
            <goal>
              <id> NAME </id>
              <active> true:Bool </active>
              <parent> .K </parent>
-             <claim> PATTERN </claim>
+             <k> PATTERN </k>
              <strategy> subgoal(PATTERN, STRAT) </strategy>
              <expected> success </expected>
              <local-context> .Bag </local-context>

prover/drivers/smt-driver.md

@@ -318,18 +318,18 @@ module DRIVER-SMT
   rule #containsSpatialPatterns(.Patterns, _) => false
   rule #containsSpatialPatterns((P, Ps), S) => #containsSpatial(P, S) orBool #containsSpatialPatterns(Ps, S)
 
-  rule <k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
-        ~> (check-sat)
-        => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
-           ...
-       </k>
-       <goals>
+  rule <goals>
+         <k> #goal( goal: (\exists{Vs} \and(Ps)) #as PATTERN, strategy: STRAT, expected: EXPECTED)
+          ~> (check-sat)
+          => #goal( goal: PATTERN, strategy: STRAT, expected: EXPECTED)
+             ...
+         </k>
          ( .Bag =>
            <goal>
              <id> !N:ClaimName </id>
              <active> true:Bool </active>
              <parent> .K </parent>
-             <claim> \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) </claim>
+             <k> \implies(\and(#filterPositive(Ps)), \and(\or(#filterNegative(Ps)))) </k>
              <strategy> STRAT </strategy>
              <expected> EXPECTED </expected>
              <local-context> .Bag </local-context>

prover/strategies/apply-equation.md

@@ -119,7 +119,7 @@ module STRATEGY-APPLY-EQUATION
         )
         ...
       </strategy>
-      <claim> T </claim>
+      <k> T </k>
 
   syntax KItem ::= "#apply-equation3"
                    "(" "hypothesis:" Pattern
@@ -138,9 +138,9 @@ module STRATEGY-APPLY-EQUATION
          => instantiateAssumptions(Subst, P)
          ~> createSubgoalsWithStrategies(strats: Ss, result: noop)
        ...</strategy>
-       <claim>
+       <k>
          _ => cool(heated: Heated, term: substMap(R, Subst))
-       </claim>
+       </k>
 
   syntax KItem ::= "createSubgoalsWithStrategies"
                    "(" "strats:" Strategies

prover/strategies/apply.md

@@ -37,7 +37,7 @@ module STRATEGY-APPLY
                Strat
              )
          ...</strategy>
-         <claim> G </claim>
+         <k> G </k>
 
 
   syntax KItem ::= #apply1(Pattern, MatchResult, Strategy)

prover/strategies/core.md

@@ -116,7 +116,7 @@ Proving a goal may involve proving other subgoals:
                <active> true </active>
                <parent> PARENT </parent>
                <strategy> SUBSTRAT </strategy>
-               <claim> SUBGOAL </claim>
+               <k> SUBGOAL </k>
                <local-context> LC </local-context>
                <trace> TRACE </trace>
                ...
@@ -151,7 +151,7 @@ all succeed, it succeeds:
   rule <prover>
          <goal>
            <strategy> ((S1 & S2) => subgoal(GOAL, S1) ~> #hole & S2) </strategy>
-           <claim> GOAL:Pattern </claim>
+           <k> GOAL:Pattern </k>
            ...
          </goal>
          ...
@@ -177,7 +177,7 @@ approach succeeds:
   rule <prover>
          <goal>
            <strategy> ((S1 | S2) => subgoal(GOAL, S1) ~> #hole | S2 ) </strategy>
-           <claim> GOAL:Pattern </claim>
+           <k> GOAL:Pattern </k>
            ...
          </goal>
          ...
@@ -199,7 +199,7 @@ Internal strategy used to implement `or-split` and `and-split`.
 
 ```k
   syntax Strategy ::= "replace-goal" "(" Pattern ")"
-  rule <claim> _ => NEWGOAL </claim>
+  rule <k> _ => NEWGOAL </k>
        <strategy> replace-goal(NEWGOAL) => noop ... </strategy>
 ```
 
@@ -212,7 +212,7 @@ Internal strategy used to implement `or-split` and `and-split`.
 ```
 
 ```k
-  rule <claim> \or(GOALS) </claim>
+  rule <k> \or(GOALS) </k>
        <strategy> or-split => #orSplit(GOALS) ... </strategy>
 
   syntax Strategy ::= "#orSplit" "(" Patterns ")" [function]
@@ -230,16 +230,16 @@ Internal strategy used to implement `or-split` and `and-split`.
 ```
 
 ```k
-  rule <claim> \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) </claim>
+  rule <k> \implies(LHS, \exists { Vs } \and(\or(RHSs), REST)) </k>
        <strategy> or-split-rhs => #orSplitImplication(LHS, Vs, RHSs, REST) ... </strategy>
 
-  rule <claim> \implies(LHS, \exists { Vs } \and(RHSs, REST)) </claim>
+  rule <k> \implies(LHS, \exists { Vs } \and(RHSs, REST)) </k>
        <strategy> or-split-rhs => noop ... </strategy>
     requires notBool isDisjunction(RHSs)
-  rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
+  rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
        <strategy> or-split-rhs => noop ... </strategy>
 
-  rule <claim> \implies(LHS, \exists { Vs } \and(.Patterns)) </claim>
+  rule <k> \implies(LHS, \exists { Vs } \and(.Patterns)) </k>
        <strategy> or-split-rhs => noop ... </strategy>
 
   syntax Strategy ::= "#orSplitImplication" "(" Pattern "," Patterns "," Patterns "," Patterns ")" [function]
@@ -257,7 +257,7 @@ Internal strategy used to implement `or-split` and `and-split`.
 ```
 
 ```k
-  rule <claim> \and(GOALS) </claim>
+  rule <k> \and(GOALS) </k>
        <strategy> and-split => #andSplit(GOALS) ... </strategy>
 
   syntax Strategy ::= "#andSplit" "(" Patterns ")" [function]

prover/strategies/inst-exists.md

@@ -16,9 +16,9 @@ module STRATEGY-INST-EXISTS
          inst-exists(V, T, Strat)
          => subgoal(\functionalPattern(T), Strat) & noop
        ...</strategy>
-       <claim>
+       <k>
          P => instExists(P, V, T)
-       </claim>
+       </k>
 
   syntax Pattern ::= instExists(Pattern, Variable, Pattern) [function]
 

prover/strategies/intros.md

@@ -11,7 +11,7 @@ module STRATEGY-INTROS
   imports KORE-HELPERS
 
   rule <strategy> intros Name => noop ...</strategy>
-       <claim> \implies(H, G) => G </claim>
+       <k> \implies(H, G) => G </k>
        <local-context> (.Bag =>
          <local-decl> axiom Name : H </local-decl>
          ) ...