From 72545bf16a010e0f67751a0f666f19894c0690d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Tue, 3 Dec 2024 13:09:15 +0000
Subject: [PATCH] Inline `*-RULES` modules, make `<k>` frame explicit

---
 src/kimp/kdist/imp-semantics/calc.k | 17 +++++--------
 src/kimp/kdist/imp-semantics/imp.k  | 38 ++++++++++++++---------------
 src/kimp/kimp.py                    |  4 +--
 3 files changed, 26 insertions(+), 33 deletions(-)

diff --git a/src/kimp/kdist/imp-semantics/calc.k b/src/kimp/kdist/imp-semantics/calc.k
index 8d0128b..7c3cde2 100644
--- a/src/kimp/kdist/imp-semantics/calc.k
+++ b/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
diff --git a/src/kimp/kdist/imp-semantics/imp.k b/src/kimp/kdist/imp-semantics/imp.k
index 6efff49..be74363 100644
--- a/src/kimp/kdist/imp-semantics/imp.k
+++ b/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
diff --git a/src/kimp/kimp.py b/src/kimp/kimp.py
index 1ca75ec..ef1441a 100644
--- a/src/kimp/kimp.py
+++ b/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)