From 7bd25792f3c737f9e567118f6209cf7ee81a97bd Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 28 Oct 2025 11:31:34 +0000
Subject: [PATCH 1/2] feat: print opt programs wrapped in func.func

---
 SSA/Projects/InstCombine/LLVM/Opt.lean        | 2 +-
 SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean      | 6 ++++++
 SSA/Projects/LLVMRiscV/ParseAndTransform.lean | 4 ++--
 SSA/Projects/RISCV64/ParseAndTransform.lean   | 2 +-
 4 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/SSA/Projects/InstCombine/LLVM/Opt.lean b/SSA/Projects/InstCombine/LLVM/Opt.lean
index 10733b28ca..42effd9442 100644
--- a/SSA/Projects/InstCombine/LLVM/Opt.lean
+++ b/SSA/Projects/InstCombine/LLVM/Opt.lean
@@ -23,7 +23,7 @@ def wellformed (fileName : String ) : IO UInt32 := do
     match icom? with
     | none => return 1
     | some (Sigma.mk _Γ ⟨_eff, ⟨_retTy, c⟩⟩) => do
-      IO.println s!"{Com.printModule c}"
+      IO.println s!"{Com.printFunc c}"
       return 0
 
 def runMainCmd (args : Cli.Parsed) : IO UInt32 := do
diff --git a/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean b/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean
index fdd267fd98..6092b8133a 100644
--- a/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean
+++ b/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean
@@ -324,4 +324,10 @@ instance : DialectToExpr LLVMPlusRiscV where
 elab "[LV|" reg:mlir_region "]" : term => do
   SSA.elabIntoCom' reg LLVMPlusRiscV
 
+/--
+Print a `Com` in generic MLIR syntax, wrapped in a `func.func`.
+-/
+partial def Com.printFunc (com : Com LLVMPlusRiscV Γ eff ts) : Std.Format :=
+  f!"func.func {com.print}"
+
 end LLVMRiscV
diff --git a/SSA/Projects/LLVMRiscV/ParseAndTransform.lean b/SSA/Projects/LLVMRiscV/ParseAndTransform.lean
index 4c3adabee7..0029f12d28 100644
--- a/SSA/Projects/LLVMRiscV/ParseAndTransform.lean
+++ b/SSA/Projects/LLVMRiscV/ParseAndTransform.lean
@@ -28,7 +28,7 @@ def passriscv64 (fileName : String) : IO UInt32 := do
             `true` indicates pseudo variable lowering, `fuel` is 150-/
           let lowered := selectionPipeFuelWithCSE 150 c true
 
-          IO.println <| lowered.printModule
+          IO.println <| lowered.printFunc
           return 0
         | _ =>
         IO.println s!" debug: WRONG RETURN TYPE : expected Ty.llvm (Ty.bitvec 64) "
@@ -54,7 +54,7 @@ def passriscv64_optimized (fileName : String) : IO UInt32 := do
           /- calls to the optimized instruction selector defined in `InstructionLowering`,
           `true` indicates pseudo variable lowering, `fuel` is 150 -/
           let lowered := selectionPipeFuelWithCSEWithOpt 150 c true
-          IO.println <| lowered.printModule
+          IO.println <| lowered.printFunc
           return 0
         | _ =>
         IO.println s!" debug: WRONG RETURN TYPE : expected Ty.llvm (Ty.bitvec 64) "
diff --git a/SSA/Projects/RISCV64/ParseAndTransform.lean b/SSA/Projects/RISCV64/ParseAndTransform.lean
index cfb2a72a49..90e11c687c 100644
--- a/SSA/Projects/RISCV64/ParseAndTransform.lean
+++ b/SSA/Projects/RISCV64/ParseAndTransform.lean
@@ -20,7 +20,7 @@ def parseAsRiscv (fileName : String ) : IO UInt32 := do
   match icom? with
   | none => return 1
   | some (Sigma.mk _Γ ⟨_eff, ⟨_retTy, c⟩⟩) => do
-    IO.println c.printModule
+    IO.println c.printFunc
     return 0
 
 /--

From 073990dede56ca96259c6ca62cb6c675741e47f1 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 28 Oct 2025 13:07:27 +0000
Subject: [PATCH 2/2] fix: generalize printFunc

---
 SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean | 6 ------
 SSA/Projects/RISCV64/Base.lean           | 8 ++++++++
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean b/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean
index 6092b8133a..fdd267fd98 100644
--- a/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean
+++ b/SSA/Projects/LLVMRiscV/LLVMAndRiscv.lean
@@ -324,10 +324,4 @@ instance : DialectToExpr LLVMPlusRiscV where
 elab "[LV|" reg:mlir_region "]" : term => do
   SSA.elabIntoCom' reg LLVMPlusRiscV
 
-/--
-Print a `Com` in generic MLIR syntax, wrapped in a `func.func`.
--/
-partial def Com.printFunc (com : Com LLVMPlusRiscV Γ eff ts) : Std.Format :=
-  f!"func.func {com.print}"
-
 end LLVMRiscV
diff --git a/SSA/Projects/RISCV64/Base.lean b/SSA/Projects/RISCV64/Base.lean
index f38582ff0d..88101c4bcf 100644
--- a/SSA/Projects/RISCV64/Base.lean
+++ b/SSA/Projects/RISCV64/Base.lean
@@ -654,3 +654,11 @@ instance : DialectDenote RV64 where
   denote o args _ := [o.denote args]ₕ
 
 end RISCV64
+
+
+variable {d} [DialectSignature d] [DialectPrint d] in
+/--
+Print a `Com` in generic MLIR syntax, wrapped in a `func.func`.
+-/
+def Com.printFunc (com : Com d Γ eff ts) : Std.Format :=
+  f!"func.func {com.print}"