From cb69c8458ae2e89ca01abf4547deedcdec77b03e Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 28 Oct 2024 04:03:54 -0700 Subject: [PATCH 1/2] chore: fix warnings --- SSA/Core/ErasedContext.lean | 2 +- SSA/Core/Framework.lean | 8 +- SSA/Core/MLIRSyntax/AST.lean | 8 +- SSA/Core/MLIRSyntax/GenericParser.lean | 84 +++++++++---------- SSA/Core/MLIRSyntax/Transform.lean | 8 +- SSA/Projects/CSE/CSE.lean | 4 +- SSA/Projects/InstCombine/AliveStatements.lean | 2 +- SSA/Projects/InstCombine/Test.lean | 26 +++--- 8 files changed, 71 insertions(+), 71 deletions(-) diff --git a/SSA/Core/ErasedContext.lean b/SSA/Core/ErasedContext.lean index 4db75b11f..85fe3c18e 100644 --- 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 index fe54913eb..e084f6b7b 100644 --- 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 index 0e5b22ed4..b21f6c42a 100644 --- 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 index b11f1bf19..a578d4317 100644 --- 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 index 8231fcafd..665901349 100644 --- 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 index 79e80b252..c50ed9917 100644 --- 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/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean index 6ee67f5a7..a6516c141 100644 --- a/SSA/Projects/InstCombine/AliveStatements.lean +++ b/SSA/Projects/InstCombine/AliveStatements.lean @@ -709,7 +709,7 @@ theorem bv_820' : all_goals sorry theorem bv_1030 : - ∀ (e : LLVM.IntW w), LLVM.sdiv e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e := by + ∀ (e : LLVM.IntW 16), LLVM.sdiv e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e := by simp_alive_undef simp_alive_ops simp_alive_case_bash diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean index d731f9900..80f199368 100644 --- 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 From d807cbf315a49a3bc784d0e23af80c1242b6b00c Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 28 Oct 2024 04:13:23 -0700 Subject: [PATCH 2/2] fix width change --- SSA/Projects/InstCombine/AliveStatements.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean index a6516c141..6ee67f5a7 100644 --- a/SSA/Projects/InstCombine/AliveStatements.lean +++ b/SSA/Projects/InstCombine/AliveStatements.lean @@ -709,7 +709,7 @@ theorem bv_820' : all_goals sorry theorem bv_1030 : - ∀ (e : LLVM.IntW 16), LLVM.sdiv e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e := by + ∀ (e : LLVM.IntW w), LLVM.sdiv e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e := by simp_alive_undef simp_alive_ops simp_alive_case_bash