From aba8b25061e342c8d4ee54e0237f2b5b6e411bb3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 12 Aug 2024 22:11:00 +1000 Subject: [PATCH] chore: adaptations for nightly-2024-08-11 (#912) Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: Wojciech Nawrocki Co-authored-by: L Co-authored-by: Joachim Breitner Co-authored-by: Kyle Miller --- Batteries.lean | 1 - Batteries/Data/ByteArray.lean | 2 +- Batteries/Data/LazyList.lean | 2 +- Batteries/Data/Thunk.lean | 10 ---------- Batteries/Data/UnionFind/Basic.lean | 1 + Batteries/Lean/AttributeExtra.lean | 4 +++- Batteries/Lean/HashMap.lean | 19 ++++--------------- Batteries/Lean/Meta/Inaccessible.lean | 2 +- Batteries/Linter/UnnecessarySeqFocus.lean | 2 +- Batteries/Linter/UnreachableTactic.lean | 4 ++-- lean-toolchain | 2 +- 11 files changed, 15 insertions(+), 34 deletions(-) delete mode 100644 Batteries/Data/Thunk.lean diff --git a/Batteries.lean b/Batteries.lean index 8e1e6f1828..73fc4efa9b 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -35,7 +35,6 @@ import Batteries.Data.Range import Batteries.Data.Rat import Batteries.Data.String import Batteries.Data.Sum -import Batteries.Data.Thunk import Batteries.Data.UInt import Batteries.Data.UnionFind import Batteries.Lean.AttributeExtra diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean index 585563ec5a..0b19bde7cb 100644 --- a/Batteries/Data/ByteArray.lean +++ b/Batteries/Data/ByteArray.lean @@ -131,7 +131,7 @@ private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where termination_by n - i @[csimp] private theorem ofFn_eq_ofFnAux : @ofFn = @ofFnAux := by - funext n f; ext; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty] + funext n f; ext1; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty] where ofFnAux_data {n} (f : Fin n → UInt8) (i) {acc} : (ofFnAux.go f i acc).data = Array.ofFn.go f i acc.data := by diff --git a/Batteries/Data/LazyList.lean b/Batteries/Data/LazyList.lean index 426cdd2248..a9100fcd48 100644 --- a/Batteries/Data/LazyList.lean +++ b/Batteries/Data/LazyList.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Simon Hudon -/ -import Batteries.Data.Thunk + /-! # Lazy lists diff --git a/Batteries/Data/Thunk.lean b/Batteries/Data/Thunk.lean deleted file mode 100644 index 88c92c3784..0000000000 --- a/Batteries/Data/Thunk.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- -Copyright (c) 2024 François G. Dorais. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE -Authors: François G. Dorais, et al. --/ - -namespace Thunk - -@[ext] protected theorem ext : {a b : Thunk α} → a.get = b.get → a = b - | {..}, {..}, heq => congrArg _ <| funext fun _ => heq diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean index 55798b0615..7d36a6b0cb 100644 --- a/Batteries/Data/UnionFind/Basic.lean +++ b/Batteries/Data/UnionFind/Basic.lean @@ -5,6 +5,7 @@ Authors: Mario Carneiro -/ import Batteries.Tactic.Lint.Misc import Batteries.Tactic.SeqFocus +import Batteries.Data.Array.Lemmas namespace Batteries diff --git a/Batteries/Lean/AttributeExtra.lean b/Batteries/Lean/AttributeExtra.lean index adb6c0ef1f..99eb7da612 100644 --- a/Batteries/Lean/AttributeExtra.lean +++ b/Batteries/Lean/AttributeExtra.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ import Batteries.Lean.TagAttribute +import Std.Data.HashMap.Basic + open Lean namespace Lean @@ -75,7 +77,7 @@ structure ParametricAttributeExtra (α : Type) where /-- The underlying `ParametricAttribute`. -/ attr : ParametricAttribute α /-- A list of pre-tagged declarations with their values. -/ - base : HashMap Name α + base : Std.HashMap Name α deriving Inhabited /-- diff --git a/Batteries/Lean/HashMap.lean b/Batteries/Lean/HashMap.lean index a8e963cf94..0cb3b0f87d 100644 --- a/Batteries/Lean/HashMap.lean +++ b/Batteries/Lean/HashMap.lean @@ -4,22 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jannis Limperg -/ -import Lean.Data.HashMap - -namespace Lean.HashMap +import Std.Data.HashMap.Basic +namespace Std.HashMap variable [BEq α] [Hashable α] -instance : ForIn m (HashMap α β) (α × β) where - forIn m init f := do - let mut acc := init - for buckets in m.val.buckets.val do - for d in buckets do - match ← f d acc with - | .done b => return b - | .yield b => acc := b - return acc - /-- `O(|other|)` amortized. Merge two `HashMap`s. The values of keys which appear in both maps are combined using the monadic function `f`. @@ -28,7 +17,7 @@ The values of keys which appear in both maps are combined using the monadic func def mergeWithM {m α β} [BEq α] [Hashable α] [Monad m] (f : α → β → β → m β) (self other : HashMap α β) : m (HashMap α β) := other.foldM (init := self) fun map k v₂ => - match map.find? k with + match map[k]? with | none => return map.insert k v₂ | some v₁ => return map.insert k (← f k v₁ v₂) @@ -41,6 +30,6 @@ def mergeWith (f : α → β → β → β) (self other : HashMap α β) : HashM -- Implementing this function directly, rather than via `mergeWithM`, gives -- us less constrained universes. other.fold (init := self) fun map k v₂ => - match map.find? k with + match map[k]? with | none => map.insert k v₂ | some v₁ => map.insert k <| f k v₁ v₂ diff --git a/Batteries/Lean/Meta/Inaccessible.lean b/Batteries/Lean/Meta/Inaccessible.lean index 5c465f5c52..55f203b252 100644 --- a/Batteries/Lean/Meta/Inaccessible.lean +++ b/Batteries/Lean/Meta/Inaccessible.lean @@ -15,7 +15,7 @@ later fvar with the same user name. def Lean.LocalContext.inaccessibleFVars (lctx : LocalContext) : Array LocalDecl := let (result, _) := - lctx.foldr (β := Array LocalDecl × HashSet Name) + lctx.foldr (β := Array LocalDecl × Std.HashSet Name) (init := (Array.mkEmpty lctx.numIndices, {})) fun ldecl (result, seen) => if ldecl.isImplementationDetail then diff --git a/Batteries/Linter/UnnecessarySeqFocus.lean b/Batteries/Linter/UnnecessarySeqFocus.lean index f53fd05f51..dca3aac1d7 100644 --- a/Batteries/Linter/UnnecessarySeqFocus.lean +++ b/Batteries/Linter/UnnecessarySeqFocus.lean @@ -83,7 +83,7 @@ structure Entry where used : Bool /-- The monad for collecting used tactic syntaxes. -/ -abbrev M (ω) := StateRefT (HashMap String.Range Entry) (ST ω) +abbrev M (ω) := StateRefT (Std.HashMap String.Range Entry) (ST ω) /-- True if this is a `<;>` node in either `tactic` or `conv` classes. -/ @[inline] def isSeqFocus (k : SyntaxNodeKind) : Bool := diff --git a/Batteries/Linter/UnreachableTactic.lean b/Batteries/Linter/UnreachableTactic.lean index cd73649969..1e55702674 100644 --- a/Batteries/Linter/UnreachableTactic.lean +++ b/Batteries/Linter/UnreachableTactic.lean @@ -29,14 +29,14 @@ namespace UnreachableTactic def getLinterUnreachableTactic (o : Options) : Bool := getLinterValue linter.unreachableTactic o /-- The monad for collecting used tactic syntaxes. -/ -abbrev M := StateRefT (HashMap String.Range Syntax) IO +abbrev M := StateRefT (Std.HashMap String.Range Syntax) IO /-- A list of blacklisted syntax kinds, which are expected to have subterms that contain unevaluated tactics. -/ initialize ignoreTacticKindsRef : IO.Ref NameHashSet ← - IO.mkRef <| HashSet.empty + IO.mkRef <| Std.HashSet.empty |>.insert ``Parser.Term.binderTactic |>.insert ``Lean.Parser.Term.dynamicQuot |>.insert ``Lean.Parser.Tactic.quotSeq diff --git a/lean-toolchain b/lean-toolchain index 9f6eaf7908..1645171233 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-08-08 +leanprover/lean4:nightly-2024-08-11