From cda4c7b9bf658fd13a3b9d3dfe58f899d4e4973b Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Wed, 22 May 2024 09:42:26 +0100 Subject: [PATCH] chore: add missing def to simp set and use full types (prepare for lean 4.9) (#326) These changes issues in the 4.9 update. As they are independent and should pass CI already, we factored these out. --- SSA/Projects/InstCombine/LLVM/CLITests.lean | 2 +- SSA/Projects/Scf/ScfFunctor.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/SSA/Projects/InstCombine/LLVM/CLITests.lean b/SSA/Projects/InstCombine/LLVM/CLITests.lean index 7122772f3..26a29a552 100644 --- a/SSA/Projects/InstCombine/LLVM/CLITests.lean +++ b/SSA/Projects/InstCombine/LLVM/CLITests.lean @@ -200,7 +200,7 @@ match ctxt, values with let valuation' := mkValuation tys valsVec match ty with | .bitvec (.concrete w) => - let newTy : toType (.bitvec (.concrete w)) := Option.map (BitVec.ofInt w) val + let newTy : toType (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)) := Option.map (BitVec.ofInt w) val Ctxt.Valuation.snoc valuation' newTy def ConcreteCliTest.eval (test : ConcreteCliTest) (values : Vector (Option Int) test.context.length) : diff --git a/SSA/Projects/Scf/ScfFunctor.lean b/SSA/Projects/Scf/ScfFunctor.lean index dd422adee..58a9cc10e 100644 --- a/SSA/Projects/Scf/ScfFunctor.lean +++ b/SSA/Projects/Scf/ScfFunctor.lean @@ -477,7 +477,7 @@ abbrev instHadd : HAdd ⟦ScfFunctor.Arith.Ty.int⟧ ⟦ScfFunctor.Arith.Ty.int open Scf in open Arith in theorem correct : Com.denote (lhs v0) Γv = Com.denote (rhs v0) Γv := by - simp only [lhs, rhs, for_, axpy, cst] + simp only [lhs, rhs, for_, axpy, cst, add] simp_peephole at Γv intros A B simp only [Ctxt.Valuation.snoc, Var.casesOn, Ctxt.get?, Var.zero_eq_last, cast_eq]