Extend Cmds.toGotoTransform to handle all Stmt types

Strata/DL/Imperative/ToCProverGOTO.lean

@@ -15,6 +15,8 @@ open Std (ToFormat Format format)
 
 namespace Imperative
 
+open CProverGOTO
+
 class ToGoto (P : PureExpr) where
   -- NOTE: `lookupType` and `updateType` correspond to the functions `lookup`
   -- and `update` in the `Imperative.TypeContext` class.
@@ -129,3 +131,212 @@ def Cmds.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv)
   go { instructions := #[], nextLoc := loc, T := T } cs
 
 -------------------------------------------------------------------------------
+
+/-! ## Imperative's Statements to CProverGOTO's Instructions -/
+
+/-
+Mutual recursion between Stmt.toGotoInstructions and Block.toGotoInstructions:
+Statements can contain blocks (e.g., in .ite and .loop), and blocks contain statements.
+This mutual dependency requires both functions to be defined in a mutual block.
+-/
+mutual
+
+/--
+Convert an `Imperative.Stmt` to one or more `CProverGOTO.Instruction`s.
+
+This function handles all statement types including control flow constructs like
+blocks, conditionals, and loops.
+-/
+def Stmt.toGotoInstructions {P} [G: ToGoto P]
+    (T : P.TyEnv) (functionName : String) (s : Stmt P (Cmd P)) (trans : GotoTransform P.TyEnv) :
+    Except Format (GotoTransform P.TyEnv) := do
+  match s with
+  | .cmd c =>
+    -- Atomic command - delegate to existing Cmd transformation
+    Cmd.toGotoInstructions trans.T functionName c trans
+
+  | .block label body _md =>
+    -- Block with label - emit a LOCATION instruction with the label, then process body
+    let label_inst : Instruction :=
+      { type := .LOCATION,
+        locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [label],
+        code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push label_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    Block.toGotoInstructions trans.T functionName body trans
+
+  | .ite cond thenb elseb _md =>
+    /-
+    Conditional: if cond then thenb else elseb
+    Structure:
+      GOTO [!cond] else_label    ; jump to else branch if condition is false
+      <then branch instructions>
+      GOTO end_label             ; skip else branch
+      LOCATION else_label        ; else branch starts here
+      <else branch instructions>
+      LOCATION end_label         ; after conditional
+    -/
+    let else_label := s!"else_{trans.nextLoc}"
+    let end_label := s!"end_if_{trans.nextLoc}"
+
+    -- Emit conditional GOTO to else branch
+    let cond_expr ← G.toGotoExpr cond
+    let neg_cond := Expr.not cond_expr
+    let goto_else_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := neg_cond, target := .none }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_else_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    let goto_else_loc := trans.nextLoc - 1
+
+    -- Process then branch
+    let trans ← Block.toGotoInstructions trans.T functionName thenb trans
+
+    -- Emit unconditional GOTO to end
+    let goto_end_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := Expr.true, target := .none }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_end_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    let goto_end_loc := trans.nextLoc - 1
+
+    -- Emit else branch label
+    let else_loc := trans.nextLoc
+    let else_label_inst : Instruction :=
+      { type := .LOCATION, locationNum := else_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [else_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push else_label_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Process else branch
+    let trans ← Block.toGotoInstructions trans.T functionName elseb trans
+
+    -- Emit end label
+    let end_loc := trans.nextLoc
+    let end_label_inst : Instruction :=
+      { type := .LOCATION, locationNum := end_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [end_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push end_label_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Patch GOTO targets
+    let insts := trans.instructions
+    let insts := insts.set! goto_else_loc
+      { insts[goto_else_loc]! with target := .some else_loc }
+    let insts := insts.set! goto_end_loc
+      { insts[goto_end_loc]! with target := .some end_loc }
+    return { trans with instructions := insts }
+
+  | .loop guard _measure _invariant body _md =>
+    /-
+    Loop: while guard do body
+    Structure:
+      LOCATION loop_start        ; loop entry point
+      GOTO [!guard] loop_end     ; exit loop if guard false
+      <body instructions>
+      GOTO loop_start            ; back edge
+      LOCATION loop_end          ; after loop
+    -/
+    let loop_start_label := s!"loop_start_{trans.nextLoc}"
+    let loop_end_label := s!"loop_end_{trans.nextLoc}"
+
+    -- Emit loop start label
+    let loop_start_loc := trans.nextLoc
+    let loop_start_inst : Instruction :=
+      { type := .LOCATION, locationNum := loop_start_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [loop_start_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push loop_start_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Emit conditional GOTO to exit loop
+    let guard_expr ← G.toGotoExpr guard
+    let neg_guard := Expr.not guard_expr
+    let goto_end_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := neg_guard, target := .none }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_end_inst,
+                    nextLoc := trans.nextLoc + 1 }
+    let goto_end_loc := trans.nextLoc - 1
+
+    -- Process loop body
+    let trans ← Block.toGotoInstructions trans.T functionName body trans
+
+    -- Emit unconditional GOTO back to loop start
+    let goto_start_inst : Instruction :=
+      { type := .GOTO, locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        guard := Expr.true, target := .some loop_start_loc }
+    let trans := { trans with
+                    instructions := trans.instructions.push goto_start_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Emit loop end label
+    let loop_end_loc := trans.nextLoc
+    let loop_end_inst : Instruction :=
+      { type := .LOCATION, locationNum := loop_end_loc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        labels := [loop_end_label], code := Code.skip }
+    let trans := { trans with
+                    instructions := trans.instructions.push loop_end_inst,
+                    nextLoc := trans.nextLoc + 1 }
+
+    -- Patch GOTO to loop end
+    let insts := trans.instructions
+    let insts := insts.set! goto_end_loc
+      { insts[goto_end_loc]! with target := .some loop_end_loc }
+    return { trans with instructions := insts }
+
+  | .goto label _md =>
+    -- Goto statement - creates an incomplete GOTO (target will be resolved later)
+    -- Note: In a full implementation, we would need a second pass to resolve labels
+    let goto_inst : Instruction :=
+      { type := .INCOMPLETE_GOTO,
+        locationNum := trans.nextLoc,
+        sourceLoc := { SourceLocation.nil with function := functionName },
+        code := Code.goto label }
+    return { trans with
+              instructions := trans.instructions.push goto_inst,
+              nextLoc := trans.nextLoc + 1 }
+termination_by Stmt.sizeOf s
+decreasing_by all_goals simp [*] at * <;> omega
+
+/--
+Convert a block (list of statements) to GOTO instructions.
+-/
+def Block.toGotoInstructions {P} [G: ToGoto P]
+    (T : P.TyEnv) (functionName : String) (stmts : Block P (Cmd P)) (trans : GotoTransform P.TyEnv) :
+    Except Format (GotoTransform P.TyEnv) := do
+  match stmts with
+  | [] => return trans
+  | s :: rest => do
+    let new_trans ← Stmt.toGotoInstructions T functionName s trans
+    Block.toGotoInstructions T functionName rest new_trans
+termination_by Block.sizeOf stmts
+decreasing_by all_goals simp [*] at * <;> omega
+end
+
+/--
+Transform a block of statements to a GotoTransform structure.
+This is the main entry point for statement transformation.
+-/
+def Stmts.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv)
+    (functionName : String) (stmts : List (Stmt P (Cmd P))) (loc : Nat := 0) :
+    Except Format (GotoTransform P.TyEnv) := do
+  Block.toGotoInstructions T functionName stmts { instructions := #[], nextLoc := loc, T := T }
+
+-------------------------------------------------------------------------------