From b6a326ca01027db2d4e00e351e57f873e4eb526f Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 23 Dec 2024 02:06:12 +0100 Subject: [PATCH] chore: update to nightly-testing-2024-12-20 (#906) --- SSA/Core/Util.lean | 6 +-- SSA/Core/Util/ConcreteOrMVar.lean | 6 +-- SSA/Experimental/Bits/AutoStructs/Defs.lean | 38 +++++++++---------- .../Bits/AutoStructs/ForLean.lean | 4 -- .../Bits/AutoStructs/ForMathlib.lean | 26 ++++++------- .../Bits/AutoStructs/FormulaToAuto.lean | 20 +++++----- SSA/Projects/InstCombine/Base.lean | 2 +- SSA/Projects/InstCombine/LLVM/CLITests.lean | 10 ++--- SSA/Projects/InstCombine/LLVM/EDSL.lean | 14 +++---- lake-manifest.json | 12 +++--- lakefile.toml | 2 +- lean-toolchain | 2 +- 12 files changed, 69 insertions(+), 73 deletions(-) diff --git a/SSA/Core/Util.lean b/SSA/Core/Util.lean index 9ad2512d2..050621a96 100644 --- a/SSA/Core/Util.lean +++ b/SSA/Core/Util.lean @@ -94,13 +94,13 @@ elab "print_goal_as_error " : tactic => do pure () -- TODO: should these go into Std? -def Vector.ofList {α : Type u} (l : List α) : Mathlib.Vector α l.length := +def Vector.ofList {α : Type u} (l : List α) : List.Vector α l.length := ⟨l, rfl⟩ -def Vector.ofArray {α : Type u} (a : Array α) : Mathlib.Vector α a.size := +def Vector.ofArray {α : Type u} (a : Array α) : List.Vector α a.size := Vector.ofList a.toList -instance [inst : Cli.ParseableType τ] {n : ℕ} : Cli.ParseableType (Mathlib.Vector τ n) where +instance [inst : Cli.ParseableType τ] {n : ℕ} : Cli.ParseableType (List.Vector τ n) where name := s!"Vector ({inst.name}) {n}" parse? str := do let arr : Array τ ← Cli.ParseableType.parse? str diff --git a/SSA/Core/Util/ConcreteOrMVar.lean b/SSA/Core/Util/ConcreteOrMVar.lean index dbcd712a4..d6f23f286 100644 --- a/SSA/Core/Util/ConcreteOrMVar.lean +++ b/SSA/Core/Util/ConcreteOrMVar.lean @@ -44,7 +44,7 @@ def instantiateOne (a : α) : ConcreteOrMVar α (φ+1) → ConcreteOrMVar α φ (fun j => .mvar j) -- `i = Fin.castSucc j` /-- Instantiate all meta-variables -/ -def instantiate (as : Mathlib.Vector α φ) : ConcreteOrMVar α φ → α +def instantiate (as : List.Vector α φ) : ConcreteOrMVar α φ → α | .concrete w => w | .mvar i => as.get i @@ -54,14 +54,14 @@ def ofNat_eq_concrete (x : Nat) : (OfNat.ofNat x) = (ConcreteOrMVar.concrete x : ConcreteOrMVar Nat φ) := rfl @[simp] -def instantiate_ofNat_eq (as : Mathlib.Vector Nat φ) (x : Nat) : +def instantiate_ofNat_eq (as : List.Vector Nat φ) (x : Nat) : ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x := rfl @[simp] lemma instantiate_mvar_zero {hφ : List.length (w :: ws) = φ} {h0 : 0 < φ} : ConcreteOrMVar.instantiate (Subtype.mk (w :: ws) hφ) (ConcreteOrMVar.mvar ⟨0, h0⟩) = w := by simp [instantiate] - simp [Mathlib.Vector.get] + simp [List.Vector.get] @[simp] lemma instantiate_mvar_zero' : diff --git a/SSA/Experimental/Bits/AutoStructs/Defs.lean b/SSA/Experimental/Bits/AutoStructs/Defs.lean index 7de8aa8fe..6ec54ffa2 100644 --- a/SSA/Experimental/Bits/AutoStructs/Defs.lean +++ b/SSA/Experimental/Bits/AutoStructs/Defs.lean @@ -328,7 +328,7 @@ def Formula.language (φ : Formula) : Set (BitVecs φ.arity) := l'.proj fun n => n.castLE (by simp [Formula.arity, FinEnum.card]) lemma helper1 : (k = 0) → (x ::ᵥ vs).get k = x := by rintro rfl; simp -lemma helper2 : (k = 1) → (x ::ᵥ y ::ᵥ vs).get k = y := by rintro rfl; simp [Mathlib.Vector.get] +lemma helper2 : (k = 1) → (x ::ᵥ y ::ᵥ vs).get k = y := by rintro rfl; simp [List.Vector.get] lemma msb_coe {x : BitVec w1} (heq : w1 = w2) : x.msb = (heq ▸ x).msb := by rcases heq; simp lemma formula_language_case_atom : @@ -356,7 +356,7 @@ lemma formula_language_case_atom : apply hrel have ht1 : bvsb.bvs.get n = t1.evalFin fun n => bvsb.bvs.get n := by unfold Term.language at h1 - simp [Mathlib.Vector.transport, liftMaxSucc1] at h1 + simp [List.Vector.transport, liftMaxSucc1] at h1 unfold n; simp +zetaDelta; rw [←h1] congr; ext1 k split_ifs with h @@ -367,7 +367,7 @@ lemma formula_language_case_atom : · congr; ext; simp; rw [Nat.mod_eq_of_lt]; omega have ht2 : bvsb.bvs.get (Fin.last (n+1)) = t2.evalFin fun n => bvsb.bvs.get n := by unfold Term.language at h2 - simp [Mathlib.Vector.transport, liftMaxSucc2] at h2 + simp [List.Vector.transport, liftMaxSucc2] at h2 unfold n; simp +zetaDelta only [Formula.arity, Fin.natCast_self]; rw [←h2] congr; ext1 k split_ifs with h @@ -382,14 +382,14 @@ lemma formula_language_case_atom : apply evalFin_eq hw; intros k rcases bvs with ⟨w, bvs⟩; rcases hw injection heqb with _ heqb; rw [←heqb] - simp [Mathlib.Vector.transport, liftExcept2] + simp [List.Vector.transport, liftExcept2] congr; ext; simp; omega have heq2 : (t2.evalFin fun n => bvsb.bvs.get n) = hw ▸ t2.evalFin fun n => bvs.bvs.get $ n.castLE (by simp) := by apply evalFin_eq hw; intros k rcases bvs with ⟨w, bvs⟩; rcases hw injection heqb with _ heqb; rw [←heqb] - simp [Mathlib.Vector.transport, liftExcept2] + simp [List.Vector.transport, liftExcept2] congr; ext; simp; omega rw [ht1, ht2, heq1, heq2, evalRelation_coe] at hrel dsimp only [Set.instMembership, Set.Mem] @@ -398,21 +398,21 @@ lemma formula_language_case_atom : simp let bv1 := t1.evalFin fun k => bvs.bvs.get $ k.castLE (by simp) let bv2 := t2.evalFin fun k => bvs.bvs.get $ k.castLE (by simp) - use ⟨bvs.w, bvs.bvs.append $ bv1 ::ᵥ bv2 ::ᵥ Mathlib.Vector.nil⟩ + use ⟨bvs.w, bvs.bvs.append $ bv1 ::ᵥ bv2 ::ᵥ List.Vector.nil⟩ rcases bvs with ⟨w, bvs⟩ simp constructor · unfold l; simp; split_ands · unfold lrel; simp only [Fin.isValue, BitVecs.transport_getElem, liftLast2, Set.mem_setOf_eq, Fin.val_last, le_add_iff_nonneg_right, zero_le, - Mathlib.Vector.append_get_ge] - rw [Mathlib.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)] + List.Vector.append_get_ge] + rw [List.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)] simp [Set.instMembership, Set.Mem] at h convert h using 2 · apply helper1; ext; simp; rw [Nat.mod_eq_of_lt] <;> omega · apply helper2; ext; simp - · unfold l1 Term.language; simp [Mathlib.Vector.transport, liftMaxSucc1] - rw [Mathlib.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)] + · unfold l1 Term.language; simp [List.Vector.transport, liftMaxSucc1] + rw [List.Vector.append_get_ge (by dsimp; rw [Nat.mod_eq_of_lt]; omega)] rw [helper1 (by ext; simp; rw [Nat.mod_eq_of_lt] <;> omega)] unfold bv1 congr; ext1 k; split_ifs @@ -421,7 +421,7 @@ lemma formula_language_case_atom : have _ : k = t1.arity := by rcases k with ⟨k, hk⟩; simp_all [Fin.last] omega · simp; congr 1 - · unfold l2 Term.language; simp [Mathlib.Vector.transport, liftMaxSucc2] + · unfold l2 Term.language; simp [List.Vector.transport, liftMaxSucc2] rw [helper2 (by ext; simp)] unfold bv2 congr; ext1 k; split_ifs @@ -432,8 +432,8 @@ lemma formula_language_case_atom : · simp; congr 1 · ext1; simp next i => - simp [Mathlib.Vector.transport, liftExcept2] - rw [Mathlib.Vector.append_get_lt i.isLt] + simp [List.Vector.transport, liftExcept2] + rw [List.Vector.append_get_lt i.isLt] congr 1 theorem formula_language (φ : Formula) : @@ -456,7 +456,7 @@ theorem formula_language (φ : Formula) : congr! rcases op <;> simp [evalBinop, langBinop, Set.compl, Set.instMembership, - Set.Mem, Mathlib.Vector.transport] <;> simp_all <;> tauto + Set.Mem, List.Vector.transport] <;> simp_all <;> tauto case msbSet t => ext1 bvs; simp only [Formula.arity, Formula.language, Set.proj, Set.lift, langMsb, Fin.isValue, Set.preimage_setOf_eq, Set.mem_image, Set.mem_inter_iff, @@ -466,19 +466,19 @@ theorem formula_language (φ : Formula) : · rintro ⟨bvsb, ⟨ht, hmsb⟩, heq⟩ simp only [Fin.isValue, Formula.arity] at ht hmsb ⊢ unfold Term.language at ht - simp only [BitVecs.transport, Mathlib.Vector.transport] at hmsb + simp only [BitVecs.transport, List.Vector.transport] at hmsb simp at ht; rw [←ht] at hmsb; rw [←hmsb] simp [BitVecs.transport] at heq obtain ⟨hw, hbvs⟩ := heq simp [hw]; congr 1; simp [hw] rcases hw; simp congr 1; ext1 k - simp at hbvs; simp [←hbvs, Mathlib.Vector.transport]; congr + simp at hbvs; simp [←hbvs, List.Vector.transport]; congr · intros heq use ⟨w, - bvs.append ((t.evalFin fun k => bvs.get $ k.castLE (by simp)) ::ᵥ Mathlib.Vector.nil)⟩ + bvs.append ((t.evalFin fun k => bvs.get $ k.castLE (by simp)) ::ᵥ List.Vector.nil)⟩ unfold Term.language - simp [BitVecs.transport, Mathlib.Vector.transport] at heq ⊢ + simp [BitVecs.transport, List.Vector.transport] at heq ⊢ constructor; assumption ext1 k; simp; congr 1 @@ -527,7 +527,7 @@ lemma sat_impl_sat' {φ : Formula} : simp [←evalFin_evalNat] lemma env_to_bvs (φ : Formula) (ρ : Fin φ.arity → BitVec w) : - let bvs : BitVecs φ.arity := ⟨w, Mathlib.Vector.ofFn fun k => ρ k⟩ + let bvs : BitVecs φ.arity := ⟨w, List.Vector.ofFn fun k => ρ k⟩ ρ = fun k => bvs.bvs.get k := by simp diff --git a/SSA/Experimental/Bits/AutoStructs/ForLean.lean b/SSA/Experimental/Bits/AutoStructs/ForLean.lean index 21bc79702..2104f6b66 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForLean.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForLean.lean @@ -39,10 +39,6 @@ theorem Array.take_ge_size {a : Array α} {n} (h : n ≥ a.size) : a.take n = a have heq : a.size - n = 0 := by omega rw [heq]; rfl -@[simp] -theorem Array.take_size {a : Array α} : a.take a.size = a := - a.take_ge_size (Nat.le_refl a.size) - @[simp] theorem Array.take_zero {a : Array α} : a.take 0 = #[] := eq_empty_of_size_eq_zero (by simp) diff --git a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean index 7d631596b..b6582fa81 100644 --- a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean +++ b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean @@ -11,17 +11,17 @@ open Set open Mathlib @[simp] -lemma Mathlib.Vector.append_get_lt {x : Mathlib.Vector α n} {y : Mathlib.Vector α m} {i : Fin (n+m)} (hlt: i < n) : +lemma List.Vector.append_get_lt {x : List.Vector α n} {y : List.Vector α m} {i : Fin (n+m)} (hlt: i < n) : (x.append y).get i = x.get (i.castLT hlt) := by rcases x with ⟨x, hx⟩; rcases y with ⟨y, hy⟩ - dsimp [Mathlib.Vector.append, Mathlib.Vector.get] + dsimp [List.Vector.append, List.Vector.get] apply List.getElem_append_left @[simp] -lemma Mathlib.Vector.append_get_ge {x : Mathlib.Vector α n} {y : Mathlib.Vector α m} {i : Fin (n+m)} (hlt: n ≤ i) : +lemma List.Vector.append_get_ge {x : List.Vector α n} {y : List.Vector α m} {i : Fin (n+m)} (hlt: n ≤ i) : (x.append y).get i = y.get ((i.cast (Nat.add_comm n m) |>.subNat n hlt)) := by rcases x with ⟨x, hx⟩; rcases y with ⟨y, hy⟩ - dsimp [Mathlib.Vector.append, Mathlib.Vector.get] + dsimp [List.Vector.append, List.Vector.get] rcases hx apply List.getElem_append_right hlt @@ -40,7 +40,7 @@ instance finenum_fin : FinEnum (Fin n) where instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩ instance (α : Type) : Union (Language α) := ⟨Set.union⟩ -def Mathlib.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n := +def List.Vector.transport (v : Vector α m) (f : Fin n → Fin m) : Vector α n := Vector.ofFn fun i => v.get (f i) def BitVec.transport (f : Fin n2 → Fin n1) (bv : BitVec n1) : BitVec n2 := @@ -63,14 +63,14 @@ The set of `n`-tuples of bit vectors of an arbitrary width. -/ structure BitVecs (n : Nat) where w : Nat - bvs : Mathlib.Vector (BitVec w) n + bvs : List.Vector (BitVec w) n -abbrev BitVecs.empty : BitVecs n := ⟨0, Mathlib.Vector.replicate n .nil⟩ +abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩ abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩ abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩ def BitVecs0 : Set (BitVecs n) := - {⟨0, Vector.replicate n (BitVec.zero 0)⟩} + {⟨0, List.Vector.replicate n (BitVec.zero 0)⟩} -- TODO: this ought to be way easier @[ext (iff := false)] @@ -100,7 +100,7 @@ def enc (bvs : BitVecs n) : BitVecs' n := def dec (bvs' : BitVecs' n) : BitVecs n where w := bvs'.length - bvs := Mathlib.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k + bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k @[simp] lemma dec_nil n : dec (n := n) [] = BitVecs.empty := by @@ -142,7 +142,7 @@ lemma dec_enc : Function.RightInverse (α := BitVecs' n) enc dec := by intros bvs; ext1; exact dec_enc_w bvs next i => simp only [enc, Fin.getElem_fin, dec, List.getElem_map, List.getElem_finRange, Fin.cast_mk, - Fin.is_lt, BitVec.ofFn_getLsbD', Fin.eta, Vector.get_ofFn] + Fin.is_lt, BitVec.ofFn_getLsbD', Fin.eta, List.Vector.get_ofFn] ext simp_all only [List.length_map, List.length_finRange, BitVec.ofFn_getLsbD', BitVec.getLsbD_cast'] @@ -177,9 +177,9 @@ def dec_inj {n : Nat} : Function.Injective (dec (n := n)) := by @[simp] lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) : dec (bvs' ++ [a]) = { w := bvs'.length + 1 - bvs := Mathlib.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } := by + bvs := List.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } := by ext k i <;> simp_all only [dec, Fin.getElem_fin, List.length_append, List.length_singleton, - Vector.get_ofFn, BitVec.ofFn_getLsbD', BitVec.getLsbD_cast'] + List.Vector.get_ofFn, BitVec.ofFn_getLsbD', BitVec.getLsbD_cast'] rw [BitVec.getLsbD_cons] split next heq => simp_all @@ -204,7 +204,7 @@ lemma BitVecs.transport_w {bvs : BitVecs n} : (BitVecs.transport f bvs).w = bvs. @[simp] lemma BitVecs.transport_getElem {bvs : BitVecs m} (f : Fin n → Fin m) (i : Fin n) : (bvs.transport f).bvs.get i = bvs.bvs.get (f i) := by - simp [transport, Mathlib.Vector.transport] + simp [transport, List.Vector.transport] def BitVecs'.transport (f : Fin n → Fin m) (bvs' : BitVecs' m): BitVecs' n := bvs'.map fun bv => bv.transport f diff --git a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean index 2635e6fcc..79d918eeb 100644 --- a/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean +++ b/SSA/Experimental/Bits/AutoStructs/FormulaToAuto.lean @@ -38,7 +38,7 @@ lemma NFA.correct_spec {M : NFA α σ} {ζ : M.sa} {L : Language α} : simp_all abbrev BVRel := ∀ ⦃w⦄, BitVec w → BitVec w → Prop -abbrev BVNRel n := ∀ ⦃w⦄, Mathlib.Vector (BitVec w) n → Prop +abbrev BVNRel n := ∀ ⦃w⦄, List.Vector (BitVec w) n → Prop def NFA'.sa (M : NFA' n) := M.σ → BVNRel n def NFA'.sa2 (M : NFA' 2) := M.σ → BVRel @@ -56,7 +56,7 @@ lemma in_enc : x ∈ enc '' S ↔ dec x ∈ S := by · rintro hS; use dec x; simp_all @[simp] -lemma Mathlib.Vector.ofFn_0 {f : Fin 0 → α} : ofFn f = .nil := by +lemma List.Vector.ofFn_0 {f : Fin 0 → α} : ofFn f = .nil := by simp [ofFn] @[simp] @@ -66,7 +66,7 @@ lemma BitVec.ofFn_0 {f : Fin 0 → Bool} : ofFn f = .nil := by @[simp] lemma dec_snoc_in_langRel {n} {R : BVNRel n} {w : BitVecs' n} {a : BitVec n} : dec (w ++ [a]) ∈ langRel R ↔ - R (Mathlib.Vector.ofFn fun k => .cons (a.getLsbD k) ((dec w).bvs.get k)) := by + R (List.Vector.ofFn fun k => .cons (a.getLsbD k) ((dec w).bvs.get k)) := by simp [langRel] @[simp] @@ -117,10 +117,10 @@ lemma BitVec.cons_inj : cons b1 bv1 = cons b2 bv2 ↔ (b1 = b2) ∧ bv1 = bv2 := @[simp] lemma BitVec.lk01 : (0#2 : BitVec 2)[1] = false := by rfl structure NFA'.correct (M : NFA' n) (ζ : M.sa) (L : BVNRel n) where - cond1 : ∀ ⦃w⦄ (bvn : Mathlib.Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn) - cond2 q : q ∈ M.M.start ↔ ζ q (Vector.replicate n .nil) - cond3 q a {w} (bvn : Mathlib.Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔ - ζ q (Mathlib.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k)) + cond1 : ∀ ⦃w⦄ (bvn : List.Vector (BitVec w) n), (L bvn ↔ ∃ q ∈ M.M.accept, ζ q bvn) + cond2 q : q ∈ M.M.start ↔ ζ q (List.Vector.replicate n .nil) + cond3 q a {w} (bvn : List.Vector (BitVec w) n) : q ∈ M.M.stepSet { q | ζ q bvn } a ↔ + ζ q (List.Vector.ofFn fun k => BitVec.cons (a.getLsbD k) (bvn.get k)) structure NFA'.correct2 (M : NFA' 2) (ζ : M.sa2) (L : BVRel) where cond1 : ∀ (bv1 bv2 : BitVec w), (L bv1 bv2 ↔ ∃ q ∈ M.M.accept, ζ q bv1 bv2) @@ -155,7 +155,7 @@ lemma NFA'.correct_spec {M : NFA' n} {ζ : M.sa} {L : BVNRel n} : lemma NFA'.correct2_spec {M : NFA' 2} {ζ : M.sa2} {L : BVRel} : M.correct2 ζ L → M.accepts = langRel2 L := by rintro ⟨h1, h2, h3⟩ - suffices hc : M.correct (fun q w (bvn : Mathlib.Vector (BitVec w) 2) => ζ q (bvn.get 0) (bvn.get 1)) + suffices hc : M.correct (fun q w (bvn : List.Vector (BitVec w) 2) => ζ q (bvn.get 0) (bvn.get 1)) (fun w bvn => L (bvn.get 0) (bvn.get 1)) by rw [M.correct_spec hc] simp [langRel2, langRel] @@ -188,7 +188,7 @@ def _root_.NFA'.ofFSM' (p : FSM arity) : NFA' (FinEnum.card arity + 1) where M := NFA.ofFSM p @[simp] -abbrev inFSMRel (p : FSM arity) {w} (bvn : Mathlib.Vector (BitVec w) _) := +abbrev inFSMRel (p : FSM arity) {w} (bvn : List.Vector (BitVec w) _) := bvn.get (Fin.last (FinEnum.card arity)) = p.evalBV (fun ar => bvn.get (FinEnum.equiv.toFun ar)) def NFA'.ofFSM_sa (p : FSM arity) : (NFA'.ofFSM' p).sa := fun q _ bvn => @@ -343,7 +343,7 @@ lemma evalFinStream_evalFin {t : Term} {k : Nat} (hlt : k < w) (vars : Fin t.ari symm; apply BitStream.neg_congr; simp_all @[simp] -lemma FSM.eval_bv (bvn : Mathlib.Vector (BitVec w) (t.arity + 1)) : +lemma FSM.eval_bv (bvn : List.Vector (BitVec w) (t.arity + 1)) : ((FSM.ofTerm t).evalBV fun ar => bvn.get ar.castSucc) = (t.evalFin fun ar => bvn.get ar.castSucc) := by simp [FSM.evalBV]; ext k hk diff --git a/SSA/Projects/InstCombine/Base.lean b/SSA/Projects/InstCombine/Base.lean index 1f02e5d0d..dfeaf329f 100644 --- a/SSA/Projects/InstCombine/Base.lean +++ b/SSA/Projects/InstCombine/Base.lean @@ -284,7 +284,7 @@ instance : ToString (MOp φ) where abbrev Op := MOp 0 -def MOp.UnaryOp.instantiate (as : Mathlib.Vector Nat φ) : MOp.UnaryOp φ → MOp.UnaryOp 0 +def MOp.UnaryOp.instantiate (as : List.Vector Nat φ) : MOp.UnaryOp φ → MOp.UnaryOp 0 | .trunc w' flags => .trunc (.concrete <| w'.instantiate as) flags | .zext w' flag => .zext (.concrete <| w'.instantiate as) flag | .sext w' => .sext (.concrete <| w'.instantiate as) diff --git a/SSA/Projects/InstCombine/LLVM/CLITests.lean b/SSA/Projects/InstCombine/LLVM/CLITests.lean index e14226070..e6dd95f68 100644 --- a/SSA/Projects/InstCombine/LLVM/CLITests.lean +++ b/SSA/Projects/InstCombine/LLVM/CLITests.lean @@ -201,11 +201,11 @@ def CliTest.eval (test : CliTest) (values : Vector ℤ test.context.length) -/ def InstCombine.mkValuation (ctxt : MContext 0) - (values : Mathlib.Vector (Option Int) ctxt.length): Ctxt.Valuation ctxt := + (values : List.Vector (Option Int) ctxt.length): Ctxt.Valuation ctxt := match ctxt, values with | [], ⟨[],_⟩ => Ctxt.Valuation.nil | ty::tys, ⟨val::vals,hlen⟩ => - let valsVec : Mathlib.Vector (Option Int) tys.length := ⟨vals,by aesop⟩ + let valsVec : List.Vector (Option Int) tys.length := ⟨vals,by aesop⟩ let valuation' := mkValuation tys valsVec match ty with | .bitvec (.concrete w) => @@ -214,7 +214,7 @@ match ctxt, values with Ctxt.Valuation.snoc valuation' newTy def ConcreteCliTest.eval (test : ConcreteCliTest) - (values : Mathlib.Vector (Option Int) test.context.length) : + (values : List.Vector (Option Int) test.context.length) : IO ⟦test.ty⟧ := do let valuesStack := values.reverse -- we reverse values since context is a stack let valuation := InstCombine.mkValuation test.context valuesStack @@ -223,14 +223,14 @@ def ConcreteCliTest.eval (test : ConcreteCliTest) def ConcreteCliTest.eval? (test : ConcreteCliTest) (values : Array (Option Int)) : IO (Except String ⟦test.ty⟧) := do if h : values.size = test.context.length then - let valuesVec : Mathlib.Vector (Option Int) test.context.length := h ▸ (Vector.ofArray values) + let valuesVec : List.Vector (Option Int) test.context.length := h ▸ (Vector.ofArray values) return Except.ok <| (← test.eval valuesVec) else return Except.error (s!"Invalid input length: {values} has length {values.size}, " ++ s!" required {test.context.length}") def ConcreteCliTest.parseableInputs (test : ConcreteCliTest) : - Cli.ParseableType (Mathlib.Vector Int test.context.length) + Cli.ParseableType (List.Vector Int test.context.length) := inferInstance def CocreteCliTest.signature (test : ConcreteCliTest) : diff --git a/SSA/Projects/InstCombine/LLVM/EDSL.lean b/SSA/Projects/InstCombine/LLVM/EDSL.lean index ee12d367d..b3cef4049 100644 --- a/SSA/Projects/InstCombine/LLVM/EDSL.lean +++ b/SSA/Projects/InstCombine/LLVM/EDSL.lean @@ -251,22 +251,22 @@ instance : AST.TransformReturn (MetaLLVM φ) φ where Finally, we show how to instantiate a family of programs to a concrete program -/ -def instantiateMTy (vals : Mathlib.Vector Nat φ) : (MetaLLVM φ).Ty → LLVM.Ty +def instantiateMTy (vals : List.Vector Nat φ) : (MetaLLVM φ).Ty → LLVM.Ty | .bitvec w => .bitvec <| w.instantiate vals -def instantiateMOp (vals : Mathlib.Vector Nat φ) : (MetaLLVM φ).Op → LLVM.Op +def instantiateMOp (vals : List.Vector Nat φ) : (MetaLLVM φ).Op → LLVM.Op | .binary w binOp => .binary (w.instantiate vals) binOp | .unary w unOp => .unary (w.instantiate vals) (unOp.instantiate vals) | .select w => .select (w.instantiate vals) | .icmp c w => .icmp c (w.instantiate vals) | .const w val => .const (w.instantiate vals) val -def instantiateCtxt (vals : Mathlib.Vector Nat φ) (Γ : Ctxt (MetaLLVM φ).Ty) : +def instantiateCtxt (vals : List.Vector Nat φ) (Γ : Ctxt (MetaLLVM φ).Ty) : Ctxt InstCombine.Ty := Γ.map (instantiateMTy vals) open InstCombine in -def MOp.instantiateCom (vals : Mathlib.Vector Nat φ) : DialectMorphism (MetaLLVM φ) LLVM where +def MOp.instantiateCom (vals : List.Vector Nat φ) : DialectMorphism (MetaLLVM φ) LLVM where mapOp := instantiateMOp vals mapTy := instantiateMTy vals preserves_signature op := by @@ -282,7 +282,7 @@ def MOp.instantiateCom (vals : Mathlib.Vector Nat φ) : DialectMorphism (MetaLLV open InstCombine in def mkComInstantiate (reg : MLIR.AST.Region φ) : - MLIR.AST.ExceptM (MetaLLVM φ) (Mathlib.Vector Nat φ → Σ Γ eff ty, Com LLVM Γ eff ty) := do + MLIR.AST.ExceptM (MetaLLVM φ) (List.Vector Nat φ → Σ Γ eff ty, Com LLVM Γ eff ty) := do let ⟨Γ, eff, ty, com⟩ ← MLIR.AST.mkCom reg return fun vals => let Γ' := instantiateCtxt vals Γ @@ -306,10 +306,10 @@ elab "[llvm(" mvars:term,* ")| " reg:mlir_region "]" : term => do let mcom ← withTraceNode `llvm (return m!"{exceptEmoji ·} elabIntoCom") <| SSA.elabIntoCom reg q(MetaLLVM $φ) - let mvalues : Q(Mathlib.Vector Nat $φ) ← + let mvalues : Q(List.Vector Nat $φ) ← withTraceNode `llvm (return m!"{exceptEmoji ·} elaborating mvalues") <| do let mvalues ← `(⟨[$mvars,*], by rfl⟩) - elabTermEnsuringType mvalues q(Mathlib.Vector Nat $φ) + elabTermEnsuringType mvalues q(List.Vector Nat $φ) let com ← withTraceNode `llvm (return m!"{exceptEmoji ·} building final Expr") <| do let instantiateFun ← mkAppM ``MOp.instantiateCom #[mvalues] diff --git a/lake-manifest.json b/lake-manifest.json index 152ce4a80..159482c91 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "13dbab738d85e172eaed1ba05012dd6b48c72039", + "rev": "8a4877456aa721f76724451be03284db54851891", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing-2024-12-15", + "inputRev": "nightly-testing-2024-12-20", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", @@ -65,17 +65,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "rev": "1f4ff06751a472de3b1525294cd4cb38a76fe93a", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "v0.0.49-pre1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6dd5eb5a3aeb43f710a35e7fe4fa3f85649ac9a4", + "rev": "c09b5d02362705b1e570962dd1b06fcfcf7ff90b", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f8fd42f689c0cd4bd1416685d65c1f7d8a003a2", + "rev": "2e82cd8e5d6462f20ffd810ea0e9460475e0b455", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", diff --git a/lakefile.toml b/lakefile.toml index 569cea07a..4ddae2c77 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,7 @@ defaultTargets = ["SSA"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "nightly-testing-2024-12-15" +rev = "nightly-testing-2024-12-20" [[require]] name = "Cli" diff --git a/lean-toolchain b/lean-toolchain index 856fab41e..bba519d51 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-12-15 +leanprover/lean4:nightly-2024-12-20