Inline *-RULES modules, make <k> frame explicit

src/kimp/kdist/imp-semantics/calc.k

@@ -15,26 +15,21 @@ module CALC-SYNTAX
 endmodule
 
 
-module CALC-RULES
-  imports CALC-SYNTAX
-
-  rule [step]: S1:Stmt S2:Stmt => S1 ~> S2
-endmodule
-
-
 module CALC
+  imports CALC-SYNTAX
   imports EXPR-RULES
-  imports CALC-RULES
 
   configuration
     <k   color="green">  $PGM:Stmt </k>
     <env color="yellow"> $ENV:Map  </env>
 
+  rule [step]: <k> S1:Stmt S2:Stmt => S1 ~> S2 ... </k>
+
   rule [var]:
-    <k> X:Id => V ...</k>
-    <env> X |-> V ...</env>
+    <k> X:Id => V ... </k>
+    <env> X |-> V ... </env>
 
   rule [assign]:
-    <k> X = V:Value ; => .K ...</k>
+    <k> X = V:Value ; => .K ... </k>
     <env> E => E [ X <- V ] </env>
 endmodule

src/kimp/kdist/imp-semantics/imp.k

@@ -12,29 +12,27 @@ module IMP-SYNTAX
 endmodule
 
 
-module IMP-RULES
+module IMP
   imports IMP-SYNTAX
+  imports CALC
 
-  rule [if-true]:  if ( true  ) E1 else _  => E1
-  rule [if-false]: if ( false ) _  else E2 => E2
+  rule [if-true]:  <k> if ( true  ) S1 else _  => S1 ... </k>
+  rule [if-false]: <k> if ( false ) _  else S2 => S2 ... </k>
 
-  rule [if-else]: if ( C ) E => if ( C ) E else {}
+  rule [if-else]: <k> if ( C ) S => if ( C ) S else {} ... </k>
 
   rule [while]:
-    while ( C ) E
-    =>
-    if ( C ) {
-      E
-      while ( C ) E
-    }
-
-  rule [block]: { E } => E ~> {}
-
-  rule [done]: {} => .K
-endmodule
-
-
-module IMP
-  imports IMP-RULES
-  imports CALC
+    <k>
+      while ( C ) S
+      =>
+      if ( C ) {
+        S
+        while ( C ) S
+      }
+      ...
+    </k>
+
+  rule [block]: <k> { S } => S ~> { } ... </k>
+
+  rule [done]: <k> { } => .K ... </k>
 endmodule

src/kimp/kimp.py

@@ -272,8 +272,8 @@ def prove(
             prover = APRProver(
                 kcfg_explore=kcfg_explore,
                 execute_depth=max_depth,
-                cut_point_rules=['IMP-RULES.while'],
-                terminal_rules=['IMP-RULES.done'],
+                cut_point_rules=['IMP.while'],
+                terminal_rules=['IMP.done'],
             )
             prover.advance_proof(proof, max_iterations=max_iterations)