feat: print opt programs wrapped in func.func

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

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) "

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}"

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
 
 /--