chore: fix warnings (#734)

opencompl · Oct 28, 2024 · f808911 · f808911
1 parent b406498
commit f808911
Show file tree

Hide file tree

Showing 7 changed files with 70 additions and 70 deletions.
diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean
@@ -322,7 +322,7 @@ theorem Valuation.eq_nil (V : Valuation (empty : Ctxt Ty)) : V = Valuation.nil :
 
 @[simp]
 theorem Valuation.snoc_toSnoc_last {Γ : Ctxt Ty} {t : Ty} (V : Valuation (Γ.snoc t)) :
-    snoc (fun t v' => V v'.toSnoc) (V <|.last ..) = V := by
+    snoc (fun _ v' => V v'.toSnoc) (V <|.last ..) = V := by
   funext _ v
   cases v using Var.casesOn <;> rfl
 

diff --git a/SSA/Core/Framework.lean b/SSA/Core/Framework.lean
@@ -1823,14 +1823,14 @@ section SubsetEntries
 theorem subset_entries :
     (
      ∀ (Γ_in : Ctxt d.Ty) (eff : EffectKind) (Γ_out Δ_in Δ_out : Ctxt d.Ty)
-        (inst : DecidableEq d.Op)
+        (_ : DecidableEq d.Op)
         (lets : Lets d Γ_in eff Γ_out)
         (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (l : List d.Ty)
         (argsl : HVector Γ_out.Var l) (argsr : HVector Δ_out.Var l) (ma : Mapping Δ_in Γ_out),
       ∀ varMap ∈ matchArg lets matchLets argsl argsr ma, ma.entries ⊆ varMap.entries
     )
     ∧ (
-      ∀ (eff : EffectKind) (Γ_in Γ_out Δ_in Δ_out : Ctxt d.Ty) (t : d.Ty) (inst : DecidableEq d.Op)
+      ∀ (eff : EffectKind) (Γ_in Γ_out Δ_in Δ_out : Ctxt d.Ty) (t : d.Ty) (_ : DecidableEq d.Op)
         (lets : Lets d Γ_in eff Γ_out) (v : Γ_out.Var t)
         (matchLets : Lets d Δ_in EffectKind.pure Δ_out)
         (w : Var Δ_out t) (ma : Mapping Δ_in Γ_out),
@@ -2080,8 +2080,8 @@ theorem matchVar_var_last {lets : Lets d Γ_in eff Γ_out} {matchLets : Lets d
     {Γv : Valuation Γ} {Δv : Valuation Δ}
     (op_eq : e₁.op = e₂.op)
     (h_regArgs : HEq e₁.regArgs e₂.regArgs)
-    (h_args : HVector.map (fun x v => Γv v) (op_eq ▸ e₁.args)
-              = HVector.map (fun x v => Δv v) e₂.args) :
+    (h_args : HVector.map (fun _ v => Γv v) (op_eq ▸ e₁.args)
+              = HVector.map (fun _ v => Δv v) e₂.args) :
     e₁.denote Γv = e₂.denote Δv := by
   rcases e₁ with ⟨op₁, ty_eq, _, args₁, regArgs₁⟩
   rcases e₂ with ⟨_, _, _, args₂, _⟩

diff --git a/SSA/Core/MLIRSyntax/AST.lean b/SSA/Core/MLIRSyntax/AST.lean
@@ -37,12 +37,12 @@ inductive BBName
 
 /-- An ssa value is a variable name -/
 inductive SSAVal : Type where
-  | SSAVal : String -> SSAVal
+  | name : String -> SSAVal
 deriving DecidableEq, Repr
 
 def SSAValToString (s: SSAVal): String :=
   match s with
-  | SSAVal.SSAVal str => str
+  | SSAVal.name str => str
 
 instance : ToString SSAVal where
   toString := SSAValToString
@@ -181,7 +181,7 @@ def Op.attrs {φ} : Op φ -> (AttrDict φ)
 | Op.mk _ _ _ _ attrs => attrs
 
 instance : Coe String SSAVal where
-  coe (s: String) := SSAVal.SSAVal s
+  coe (s: String) := SSAVal.name s
 
 instance : Coe String (AttrValue φ) where
   coe (s: String) := AttrValue.str s
@@ -265,7 +265,7 @@ instance : Repr (AttrDefn φ) where
 
 instance : Repr SSAVal where
   reprPrec x _ := match x with
-    | SSAVal.SSAVal name => f!"%{name}"
+    | SSAVal.name name => f!"%{name}"
 
 instance : ToFormat SSAVal where
   format := repr

diff --git a/SSA/Core/MLIRSyntax/GenericParser.lean b/SSA/Core/MLIRSyntax/GenericParser.lean
@@ -237,29 +237,29 @@ syntax "%" ident : mlir_op_operand
 syntax "[mlir_op_operand|" mlir_op_operand "]" : term
 macro_rules
   | `([mlir_op_operand| $$($q)]) => return q
-  | `([mlir_op_operand| % $x:ident]) => `(SSAVal.SSAVal $(Lean.quote (x.getId.toString)))
-  | `([mlir_op_operand| % $n:num]) => `(SSAVal.SSAVal (IntToString $n))
+  | `([mlir_op_operand| % $x:ident]) => `(SSAVal.name $(Lean.quote (x.getId.toString)))
+  | `([mlir_op_operand| % $n:num]) => `(SSAVal.name (IntToString $n))
 
 section Test
 
 private def operand0 := [mlir_op_operand| %x]
 /--
 info: private def MLIR.EDSL.operand0 : SSAVal :=
-SSAVal.SSAVal "x"
+SSAVal.name "x"
 -/
 #guard_msgs in #print operand0
 
 private def operand1 := [mlir_op_operand| %x]
 /--
 info: private def MLIR.EDSL.operand1 : SSAVal :=
-SSAVal.SSAVal "x"
+SSAVal.name "x"
 -/
 #guard_msgs in #print operand1
 
 private def operand2 := [mlir_op_operand| %0]
 /--
 info: private def MLIR.EDSL.operand2 : SSAVal :=
-SSAVal.SSAVal (IntToString 0)
+SSAVal.name (IntToString 0)
 -/
 #guard_msgs in #print operand2
 
@@ -924,8 +924,8 @@ private def op1 : Op φ :=
 info: private def MLIR.EDSL.op1 : {φ : ℕ} → Op φ :=
 fun {φ} =>
   Op.mk "foo" []
-    [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32), (SSAVal.SSAVal "y", MLIRType.int Signedness.Signless 32)]
-    [] (AttrDict.mk [])
+    [(SSAVal.name "x", MLIRType.int Signedness.Signless 32), (SSAVal.name "y", MLIRType.int Signedness.Signless 32)] []
+    (AttrDict.mk [])
 -/
 #guard_msgs in #print op1
 
@@ -934,9 +934,9 @@ private def op2 : Op φ :=
 /--
 info: private def MLIR.EDSL.op2 : {φ : ℕ} → Op φ :=
 fun {φ} =>
-  Op.mk "foo" [(SSAVal.SSAVal "z", MLIRType.int Signedness.Signless 32)]
-    [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32), (SSAVal.SSAVal "y", MLIRType.int Signedness.Signless 32)]
-    [] (AttrDict.mk [])
+  Op.mk "foo" [(SSAVal.name "z", MLIRType.int Signedness.Signless 32)]
+    [(SSAVal.name "x", MLIRType.int Signedness.Signless 32), (SSAVal.name "y", MLIRType.int Signedness.Signless 32)] []
+    (AttrDict.mk [])
 -/
 #guard_msgs in #print op2
 
@@ -949,7 +949,7 @@ following example:
 private def bbop1 : SSAVal × MLIRTy φ := [mlir_bb_operand| %x : i32 ]
 /--
 info: private def MLIR.EDSL.bbop1 : {φ : ℕ} → SSAVal × MLIRTy φ :=
-fun {φ} => (SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)
+fun {φ} => (SSAVal.name "x", MLIRType.int Signedness.Signless 32)
 -/
 #guard_msgs in #print bbop1
 
@@ -965,12 +965,11 @@ info: private def MLIR.EDSL.bb1NoArgs : {φ : ℕ} → Region φ :=
 fun {φ} =>
   Region.mk "entry" []
     [Op.mk "foo" []
-        [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32),
-          (SSAVal.SSAVal "y", MLIRType.int Signedness.Signless 32)]
+        [(SSAVal.name "x", MLIRType.int Signedness.Signless 32), (SSAVal.name "y", MLIRType.int Signedness.Signless 32)]
         [] (AttrDict.mk []),
-      Op.mk "bar" [(SSAVal.SSAVal "z", MLIRType.int Signedness.Signless 32)]
-        [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk []),
-      Op.mk "std.return" [] [(SSAVal.SSAVal "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
+      Op.mk "bar" [(SSAVal.name "z", MLIRType.int Signedness.Signless 32)]
+        [(SSAVal.name "x", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk []),
+      Op.mk "std.return" [] [(SSAVal.name "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
 -/
 #guard_msgs in #print bb1NoArgs
 
@@ -991,14 +990,14 @@ private def bb2SingleArg : Region φ :=
 /--
 info: private def MLIR.EDSL.bb2SingleArg : {φ : ℕ} → Region φ :=
 fun {φ} =>
-  Region.mk "entry" [(SSAVal.SSAVal "argp", MLIRType.int Signedness.Signless 32)]
+  Region.mk "entry" [(SSAVal.name "argp", MLIRType.int Signedness.Signless 32)]
     [Op.mk "foo" []
-        [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32),
-          (SSAVal.SSAVal "y", MLIRType.int Signedness.Signless 32)]
+        [(SSAVal.name "x", MLIRType.int Signedness.Signless 32), (SSAVal.name "y", MLIRType.int Signedness.Signless 32)]
         [] (AttrDict.mk []),
-      Op.mk "bar" [(SSAVal.SSAVal "z", MLIRType.int Signedness.Signless 32)]
-        [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk []),
-      Op.mk "std.return" [] [(SSAVal.SSAVal "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]-/
+      Op.mk "bar" [(SSAVal.name "z", MLIRType.int Signedness.Signless 32)]
+        [(SSAVal.name "x", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk []),
+      Op.mk "std.return" [] [(SSAVal.name "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
+-/
 #guard_msgs in #print bb2SingleArg
 
 
@@ -1011,16 +1010,17 @@ private def bb3MultipleArgs : Region φ :=
   }]
 /--
 info: Region.mk "entry"
-  [(SSAVal.SSAVal "argp", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32)),
-    (SSAVal.SSAVal "argq", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 64))]
+  [(SSAVal.name "argp", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32)),
+    (SSAVal.name "argq", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 64))]
   [Op.mk "foo" []
-      [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32)),
-        (SSAVal.SSAVal "y", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32))]
+      [(SSAVal.name "x", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32)),
+        (SSAVal.name "y", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32))]
       [] (AttrDict.mk []),
-    Op.mk "bar" [(SSAVal.SSAVal "z", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32))]
-      [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32))] [] (AttrDict.mk []),
-    Op.mk "std.return" [] [(SSAVal.SSAVal "x0", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 42))] []
-      (AttrDict.mk [])]-/
+    Op.mk "bar" [(SSAVal.name "z", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32))]
+      [(SSAVal.name "x", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 32))] [] (AttrDict.mk []),
+    Op.mk "std.return" [] [(SSAVal.name "x0", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 42))] []
+      (AttrDict.mk [])]
+-/
 #guard_msgs in #reduce bb3MultipleArgs
 
 
@@ -1040,7 +1040,7 @@ private def rgn1 : Region φ :=
 info: private def MLIR.EDSL.rgn1 : {φ : ℕ} → Region φ :=
 fun {φ} =>
   Region.mk "entry" []
-    [Op.mk "std.return" [] [(SSAVal.SSAVal "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
+    [Op.mk "std.return" [] [(SSAVal.name "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
 -/
 #guard_msgs in #print rgn1
 
@@ -1053,7 +1053,7 @@ private def rgn2 : Region φ :=
 info: private def MLIR.EDSL.rgn2 : {φ : ℕ} → Region φ :=
 fun {φ} =>
   Region.mk "entry" []
-    [Op.mk "std.return" [] [(SSAVal.SSAVal "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
+    [Op.mk "std.return" [] [(SSAVal.name "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
 -/
 #guard_msgs in #print rgn2
 
@@ -1067,7 +1067,7 @@ private def rgn3 : Region φ :=
 info: private def MLIR.EDSL.rgn1 : {φ : ℕ} → Region φ :=
 fun {φ} =>
   Region.mk "entry" []
-    [Op.mk "std.return" [] [(SSAVal.SSAVal "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
+    [Op.mk "std.return" [] [(SSAVal.name "x0", MLIRType.int Signedness.Signless 42)] [] (AttrDict.mk [])]
 -/
 #guard_msgs in #print rgn1
 
@@ -1079,8 +1079,8 @@ private def opcall1 : Op φ := [mlir_op| "foo" (%x, %y) : (i32, i32) -> (i32) ]
 info: private def MLIR.EDSL.opcall1 : {φ : ℕ} → Op φ :=
 fun {φ} =>
   Op.mk "foo" []
-    [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32), (SSAVal.SSAVal "y", MLIRType.int Signedness.Signless 32)]
-    [] (AttrDict.mk [])
+    [(SSAVal.name "x", MLIRType.int Signedness.Signless 32), (SSAVal.name "y", MLIRType.int Signedness.Signless 32)] []
+    (AttrDict.mk [])
 -/
 #guard_msgs in #print opcall1
 
@@ -1092,7 +1092,7 @@ private def oprgn0 : Op φ := [mlir_op|
 /--
 info: Op.mk "func" [] []
   [Region.mk "entry" []
-      [Op.mk "foo.add" [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 64))] [] []
+      [Op.mk "foo.add" [(SSAVal.name "x", MLIRType.int Signedness.Signless (ConcreteOrMVar.concrete 64))] [] []
           (AttrDict.mk [])]]
   (AttrDict.mk [])
 -/
@@ -1117,13 +1117,13 @@ fun {φ} =>
     [Region.mk "entry" []
         [Op.mk "func" [] []
             [Region.mk "bb0"
-                [(SSAVal.SSAVal "arg0", MLIRType.int Signedness.Signless 32),
-                  (SSAVal.SSAVal "arg1", MLIRType.int Signedness.Signless 32)]
-                [Op.mk "std.addi" [(SSAVal.SSAVal "zero", MLIRType.int Signedness.Signless 64)]
-                    [(SSAVal.SSAVal "arg0", MLIRType.int Signedness.Signless 32),
-                      (SSAVal.SSAVal "arg1", MLIRType.int Signedness.Signless 16)]
+                [(SSAVal.name "arg0", MLIRType.int Signedness.Signless 32),
+                  (SSAVal.name "arg1", MLIRType.int Signedness.Signless 32)]
+                [Op.mk "std.addi" [(SSAVal.name "zero", MLIRType.int Signedness.Signless 64)]
+                    [(SSAVal.name "arg0", MLIRType.int Signedness.Signless 32),
+                      (SSAVal.name "arg1", MLIRType.int Signedness.Signless 16)]
                     [] (AttrDict.mk []),
-                  Op.mk "std.return" [] [(SSAVal.SSAVal "zero", MLIRType.int Signedness.Signless 32)] []
+                  Op.mk "std.return" [] [(SSAVal.name "zero", MLIRType.int Signedness.Signless 32)] []
                     (AttrDict.mk [])]]
             (AttrDict.mk [AttrEntry.mk "sym_name" (AttrValue.str "add")]),
           Op.mk "module_terminator" [] [] [] (AttrDict.mk [])]]

diff --git a/SSA/Core/MLIRSyntax/Transform.lean b/SSA/Core/MLIRSyntax/Transform.lean
@@ -116,13 +116,13 @@ def BuilderM.isErr {α : Type} (x : BuilderM d α) : Bool :=
   | Except.error _ => false
 
 def TypedSSAVal.mkTy [TransformTy d φ] : TypedSSAVal φ → ExceptM d d.Ty
-  | (.SSAVal _, ty) => TransformTy.mkTy ty
+  | (.name _, ty) => TransformTy.mkTy ty
 
 /-- Translate a `TypedSSAVal` (a name with an expected type), to a variable in the context.
     This expects the name to have already been declared before -/
 def TypedSSAVal.mkVal [instTransformTy : TransformTy d φ] (Γ : Ctxt d.Ty) : TypedSSAVal φ →
     ReaderM d (Σ (ty : d.Ty), Ctxt.Var Γ ty)
-| (.SSAVal valStx, tyStx) => do
+| (.name valStx, tyStx) => do
     let ty ← instTransformTy.mkTy tyStx
     let var ← getValFromCtxt Γ valStx ty
     return ⟨ty, var⟩
@@ -133,7 +133,7 @@ def TypedSSAVal.mkVal [instTransformTy : TransformTy d φ] (Γ : Ctxt d.Ty) : Ty
     to cut infinite regress. -/
 def TypedSSAVal.mkVal' [instTransformTy : TransformTy d φ] (Γ : Ctxt d.Ty) : TypedSSAVal φ →
     ReaderM d (Σ (ty : d.Ty), Ctxt.Var Γ ty)
-| (.SSAVal valStx, tyStx) => do
+| (.name valStx, tyStx) => do
     let ty ← instTransformTy.mkTy tyStx
     let var ← getValFromCtxt Γ valStx ty
     return ⟨ty, var⟩
@@ -142,7 +142,7 @@ def TypedSSAVal.mkVal' [instTransformTy : TransformTy d φ] (Γ : Ctxt d.Ty) : T
     by adding the passed name to the name mapping stored in the monad state -/
 def TypedSSAVal.newVal [instTransformTy : TransformTy d φ] (Γ : Ctxt d.Ty) : TypedSSAVal φ →
     BuilderM d (Σ (Γ' : DerivedCtxt Γ) (ty : d.Ty), Ctxt.Var Γ'.ctxt ty)
-| (.SSAVal valStx, tyStx) => do
+| (.name valStx, tyStx) => do
     let ty ← instTransformTy.mkTy tyStx
     let ⟨Γ, var⟩ ← addValToMapping Γ valStx ty
     return ⟨Γ, ty, var⟩

diff --git a/SSA/Projects/CSE/CSE.lean b/SSA/Projects/CSE/CSE.lean
@@ -130,8 +130,8 @@ def arglistRemapVar [DecidableEq d.Ty] [DecidableEq d.Op]
     ((lets.denote Vstart).comap hom) vnew)
   {ts : List d.Ty} (as' : HVector (Ctxt.Var Γ') <| ts) :
     { as : HVector (Ctxt.Var Γ) <| ts //
-      ∀ (Vstart : Γstart.Valuation), as.map (fun t v => (lets.denote Vstart) v) =
-        as'.map (fun t v' => ((lets.denote Vstart).comap hom) v') } :=
+      ∀ (Vstart : Γstart.Valuation), as.map (fun _ v => (lets.denote Vstart) v) =
+        as'.map (fun _ v' => ((lets.denote Vstart).comap hom) v') } :=
   match as' with
   | .nil => ⟨.nil, by simp [HVector.map]⟩
   | .cons a' as' =>

diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean
@@ -49,24 +49,24 @@ def bb0 : Region 0 := [mlir_region|
 
 /--
 info: def bb0 : Region 0 :=
-Region.mk "bb0" [(SSAVal.SSAVal "arg0", MLIRType.int Signedness.Signless 32)]
-  [Op.mk "llvm.mlir.constant" [(SSAVal.SSAVal (EDSL.IntToString 0), MLIRType.int Signedness.Signless 32)] [] []
+Region.mk "bb0" [(SSAVal.name "arg0", MLIRType.int Signedness.Signless 32)]
+  [Op.mk "llvm.mlir.constant" [(SSAVal.name (EDSL.IntToString 0), MLIRType.int Signedness.Signless 32)] [] []
       (AttrDict.mk [AttrEntry.mk "value" (AttrValue.int 8 (MLIRType.int Signedness.Signless 32))]),
-    Op.mk "llvm.mlir.constant" [(SSAVal.SSAVal (EDSL.IntToString 1), MLIRType.int Signedness.Signless 32)] [] []
+    Op.mk "llvm.mlir.constant" [(SSAVal.name (EDSL.IntToString 1), MLIRType.int Signedness.Signless 32)] [] []
       (AttrDict.mk [AttrEntry.mk "value" (AttrValue.int 31 (MLIRType.int Signedness.Signless 32))]),
-    Op.mk "llvm.ashr" [(SSAVal.SSAVal (EDSL.IntToString 2), MLIRType.int Signedness.Signless 32)]
-      [(SSAVal.SSAVal "arg0", MLIRType.int Signedness.Signless 32),
-        (SSAVal.SSAVal (EDSL.IntToString 1), MLIRType.int Signedness.Signless 32)]
+    Op.mk "llvm.ashr" [(SSAVal.name (EDSL.IntToString 2), MLIRType.int Signedness.Signless 32)]
+      [(SSAVal.name "arg0", MLIRType.int Signedness.Signless 32),
+        (SSAVal.name (EDSL.IntToString 1), MLIRType.int Signedness.Signless 32)]
       [] (AttrDict.mk []),
-    Op.mk "llvm.and" [(SSAVal.SSAVal (EDSL.IntToString 3), MLIRType.int Signedness.Signless 32)]
-      [(SSAVal.SSAVal (EDSL.IntToString 2), MLIRType.int Signedness.Signless 32),
-        (SSAVal.SSAVal (EDSL.IntToString 0), MLIRType.int Signedness.Signless 32)]
+    Op.mk "llvm.and" [(SSAVal.name (EDSL.IntToString 3), MLIRType.int Signedness.Signless 32)]
+      [(SSAVal.name (EDSL.IntToString 2), MLIRType.int Signedness.Signless 32),
+        (SSAVal.name (EDSL.IntToString 0), MLIRType.int Signedness.Signless 32)]
       [] (AttrDict.mk []),
-    Op.mk "llvm.add" [(SSAVal.SSAVal (EDSL.IntToString 4), MLIRType.int Signedness.Signless 32)]
-      [(SSAVal.SSAVal (EDSL.IntToString 3), MLIRType.int Signedness.Signless 32),
-        (SSAVal.SSAVal (EDSL.IntToString 2), MLIRType.int Signedness.Signless 32)]
+    Op.mk "llvm.add" [(SSAVal.name (EDSL.IntToString 4), MLIRType.int Signedness.Signless 32)]
+      [(SSAVal.name (EDSL.IntToString 3), MLIRType.int Signedness.Signless 32),
+        (SSAVal.name (EDSL.IntToString 2), MLIRType.int Signedness.Signless 32)]
       [] (AttrDict.mk []),
-    Op.mk "llvm.return" [] [(SSAVal.SSAVal (EDSL.IntToString 4), MLIRType.int Signedness.Signless 32)] []
+    Op.mk "llvm.return" [] [(SSAVal.name (EDSL.IntToString 4), MLIRType.int Signedness.Signless 32)] []
       (AttrDict.mk [])]
 -/
 #guard_msgs in #print bb0