From 9096d6fc7180fe533c504f662bcb61550e4a2492 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Jun 2024 10:32:40 -0700 Subject: [PATCH] fix: remove `PersistentHashMap.size` It is buggy and was unnecessary overhead. closes #3029 --- src/Lean/Attributes.lean | 12 ++++---- src/Lean/Data/PersistentHashMap.lean | 41 ++++++++++++++++------------ src/Lean/Data/PersistentHashSet.lean | 3 -- src/Lean/Data/SMap.lean | 6 ---- src/Lean/Data/SSet.lean | 3 -- src/Lean/Elab/BuiltinCommand.lean | 2 ++ src/Lean/Elab/Tactic/Cache.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/Environment.lean | 3 -- src/Lean/Meta/Tactic/Simp/Types.lean | 21 ++++++++++---- stage0/src/stdlib_flags.h | 2 +- 11 files changed, 50 insertions(+), 47 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 1693cb558c1b..e36bc0deff33 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -53,7 +53,7 @@ structure AttributeImpl extends AttributeImplCore where erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased" deriving Inhabited -builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) ← IO.mkRef {} +builtin_initialize attributeMapRef : IO.Ref (HashMap Name AttributeImpl) ← IO.mkRef {} /-- Low level attribute registration function. -/ def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do @@ -317,7 +317,7 @@ inductive AttributeExtensionOLeanEntry where structure AttributeExtensionState where newEntries : List AttributeExtensionOLeanEntry := [] - map : PersistentHashMap Name AttributeImpl + map : HashMap Name AttributeImpl deriving Inhabited abbrev AttributeExtension := PersistentEnvExtension AttributeExtensionOLeanEntry (AttributeExtensionOLeanEntry × AttributeImpl) AttributeExtensionState @@ -348,7 +348,7 @@ private def AttributeExtension.addImported (es : Array (Array AttributeExtension let map ← es.foldlM (fun map entries => entries.foldlM - (fun (map : PersistentHashMap Name AttributeImpl) entry => do + (fun (map : HashMap Name AttributeImpl) entry => do let attrImpl ← mkAttributeImplOfEntry ctx.env ctx.opts entry return map.insert attrImpl.name attrImpl) map) @@ -374,7 +374,7 @@ def isBuiltinAttribute (n : Name) : IO Bool := do /-- Return the name of all registered attributes. -/ def getBuiltinAttributeNames : IO (List Name) := - return (← attributeMapRef.get).foldl (init := []) fun r n _ => n::r + return (← attributeMapRef.get).fold (init := []) fun r n _ => n::r def getBuiltinAttributeImpl (attrName : Name) : IO AttributeImpl := do let m ← attributeMapRef.get @@ -392,7 +392,7 @@ def isAttribute (env : Environment) (attrName : Name) : Bool := def getAttributeNames (env : Environment) : List Name := let m := (attributeExtension.getState env).map - m.foldl (fun r n _ => n::r) [] + m.fold (fun r n _ => n::r) [] def getAttributeImpl (env : Environment) (attrName : Name) : Except String AttributeImpl := let m := (attributeExtension.getState env).map @@ -427,7 +427,7 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do def updateEnvAttributesImpl (env : Environment) : IO Environment := do let map ← attributeMapRef.get let s := attributeExtension.getState env - let s := map.foldl (init := s) fun s attrName attrImpl => + let s := map.fold (init := s) fun s attrName attrImpl => if s.map.contains attrName then s else diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean index 737d6eb3d392..29c85f6f9334 100644 --- a/src/Lean/Data/PersistentHashMap.lean +++ b/src/Lean/Data/PersistentHashMap.lean @@ -23,6 +23,13 @@ inductive Node (α : Type u) (β : Type v) : Type (max u v) where | entries (es : Array (Entry α β (Node α β))) : Node α β | collision (ks : Array α) (vs : Array β) (h : ks.size = vs.size) : Node α β +partial def Node.isEmpty : Node α β → Bool + | .collision .. => false + | .entries es => es.all fun + | .entry .. => false + | .ref n => n.isEmpty + | .null => true + instance {α β} : Inhabited (Node α β) := ⟨Node.entries #[]⟩ abbrev shift : USize := 5 @@ -36,8 +43,7 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) := end PersistentHashMap structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where - root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray - size : Nat := 0 + root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β @@ -45,8 +51,8 @@ namespace PersistentHashMap def empty [BEq α] [Hashable α] : PersistentHashMap α β := {} -def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool := - m.size == 0 +def isEmpty {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → Bool + | { root } => root.isEmpty instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩ @@ -130,7 +136,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize else Entry.ref $ mkCollisionNode k' v' k v def insert {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → β → PersistentHashMap α β - | { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 1 k v, size := sz + 1 } + | { root := n }, k, v => { root := insertAux n (hash k |>.toUSize) 1 k v } partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β := if h : i < keys.size then @@ -225,7 +231,7 @@ def isUnaryNode : Node α β → Option (α × β) else none -partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bool +partial def eraseAux [BEq α] : Node α β → USize → α → Node α β | n@(Node.collision keys vals heq), _, k => match keys.indexOf? k with | some idx => @@ -234,28 +240,27 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo let vals' := vals.feraseIdx (Eq.ndrec idx heq) have veq := vals.size_feraseIdx (Eq.ndrec idx heq) have : keys.size - 1 = vals.size - 1 := by rw [heq] - (Node.collision keys' vals' (keq.trans (this.trans veq.symm)), true) - | none => (n, false) + Node.collision keys' vals' (keq.trans (this.trans veq.symm)) + | none => n | n@(Node.entries entries), h, k => let j := (mod2Shift h shift).toNat let entry := entries.get! j match entry with - | Entry.null => (n, false) + | Entry.null => n | Entry.entry k' _ => - if k == k' then (Node.entries (entries.set! j Entry.null), true) else (n, false) + if k == k' then Node.entries (entries.set! j Entry.null) else n | Entry.ref node => let entries := entries.set! j Entry.null - let (newNode, deleted) := eraseAux node (div2Shift h shift) k - if !deleted then (n, false) - else match isUnaryNode newNode with - | none => (Node.entries (entries.set! j (Entry.ref newNode)), true) - | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true) + let newNode := eraseAux node (div2Shift h shift) k + match isUnaryNode newNode with + | none => Node.entries (entries.set! j (Entry.ref newNode)) + | some (k, v) => Node.entries (entries.set! j (Entry.entry k v)) def erase {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → PersistentHashMap α β - | { root := n, size := sz }, k => + | { root := n }, k => let h := hash k |>.toUSize - let (n, del) := eraseAux n h k - { root := n, size := if del then sz - 1 else sz } + let n := eraseAux n h k + { root := n } section variable {m : Type w → Type w'} [Monad m] diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean index 63deda7b2bed..ec57ff612b65 100644 --- a/src/Lean/Data/PersistentHashSet.lean +++ b/src/Lean/Data/PersistentHashSet.lean @@ -44,9 +44,6 @@ variable {_ : BEq α} {_ : Hashable α} @[inline] def contains (s : PersistentHashSet α) (a : α) : Bool := s.set.contains a -@[inline] def size (s : PersistentHashSet α) : Nat := - s.set.size - @[inline] def foldM {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (init : β) (s : PersistentHashSet α) : m β := s.set.foldlM (init := init) fun d a _ => f d a diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index 3a0c06cb4570..bb429e12592a 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -90,12 +90,6 @@ def switch (m : SMap α β) : SMap α β := def fold {σ : Type w} (f : σ → α → β → σ) (init : σ) (m : SMap α β) : σ := m.map₂.foldl f $ m.map₁.fold f init -def size (m : SMap α β) : Nat := - m.map₁.size + m.map₂.size - -def stageSizes (m : SMap α β) : Nat × Nat := - (m.map₁.size, m.map₂.size) - def numBuckets (m : SMap α β) : Nat := m.map₁.numBuckets diff --git a/src/Lean/Data/SSet.lean b/src/Lean/Data/SSet.lean index 9a12c550a67e..dafbfe9b39c1 100644 --- a/src/Lean/Data/SSet.lean +++ b/src/Lean/Data/SSet.lean @@ -34,9 +34,6 @@ abbrev switch (s : SSet α) : SSet α := abbrev fold (f : σ → α → σ) (init : σ) (s : SSet α) : σ := SMap.fold (fun d a _ => f d a) init s -abbrev size (s : SSet α) : Nat := - SMap.size s - def toList (m : SSet α) : List α := m.fold (init := []) fun es a => a::es diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 3c12788db2cf..90dc1db8208b 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -262,6 +262,7 @@ def elabCheckCore (ignoreStuckTC : Bool) : CommandElab @[builtin_command_elab Lean.Parser.Command.check] def elabCheck : CommandElab := elabCheckCore (ignoreStuckTC := true) +/- @[builtin_command_elab Lean.reduceCmd] def elabReduce : CommandElab | `(#reduce%$tk $term) => go tk term | `(#reduce%$tk (proofs := true) $term) => go tk term (skipProofs := false) @@ -278,6 +279,7 @@ where withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `smartUnfolding false }) do let e ← withTransparency (mode := TransparencyMode.all) <| reduce e (skipProofs := skipProofs) (skipTypes := skipTypes) logInfoAt tk e +-/ def hasNoErrorMessages : CommandElabM Bool := do return !(← get).messages.hasErrors diff --git a/src/Lean/Elab/Tactic/Cache.lean b/src/Lean/Elab/Tactic/Cache.lean index 6655d8fa50fe..fb29d04f0da7 100644 --- a/src/Lean/Elab/Tactic/Cache.lean +++ b/src/Lean/Elab/Tactic/Cache.lean @@ -37,7 +37,7 @@ private def dbg_cache (msg : String) : TacticM Unit := do private def dbg_cache' (cacheRef : IO.Ref Cache) (pos : String.Pos) (mvarId : MVarId) (msg : String) : TacticM Unit := do if tactic.dbg_cache.get (← getOptions) then let {line, column} := (← getFileMap).toPosition pos - dbg_trace "{msg}, cache size: {(← cacheRef.get).pre.size}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}" + dbg_trace "{msg}, line: {line}, column: {column}, contains entry: {(← cacheRef.get).pre.find? { mvarId, pos } |>.isSome}" private def findCache? (cacheRef : IO.Ref Cache) (mvarId : MVarId) (stx : Syntax) (pos : String.Pos) : TacticM (Option Snapshot) := do let some s := (← cacheRef.get).pre.find? { mvarId, pos } | do dbg_cache "cache key not found"; return none diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 21f6653bcb99..59f558137217 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -341,7 +341,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do let mut localsOrStar := some #[] let lctx ← getLCtx let env ← getEnv - for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do + for thm in usedSimps.toArray do match thm with | .decl declName post inv => -- global definitions in the environment if env.contains declName diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 1ade563ad3a4..3a2865fb7c16 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -984,9 +984,6 @@ def displayStats (env : Environment) : IO Unit := do IO.println ("direct imports: " ++ toString env.header.imports); IO.println ("number of imported modules: " ++ toString env.header.regions.size); IO.println ("number of memory-mapped modules: " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size)); - IO.println ("number of consts: " ++ toString env.constants.size); - IO.println ("number of imported consts: " ++ toString env.constants.stageSizes.1); - IO.println ("number of local consts: " ++ toString env.constants.stageSizes.2); IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets); IO.println ("trust level: " ++ toString env.header.trustLevel); IO.println ("number of extensions: " ++ toString env.extensions.size); diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 642291712b4d..ad1a9b389284 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -106,8 +106,21 @@ structure Context where def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool := ctx.simpTheorems.isDeclToUnfold declName --- We should use `PHashMap` because we backtrack the contents of `UsedSimps` -abbrev UsedSimps := PHashMap Origin Nat +structure UsedSimps where + -- We should use `PHashMap` because we backtrack the contents of `UsedSimps` + -- The natural number tracks the insertion order + map : PHashMap Origin Nat := {} + size : Nat := 0 + deriving Inhabited + +def UsedSimps.insert (s : UsedSimps) (thmId : Origin) : UsedSimps := + if s.map.contains thmId then + s + else match s with + | { map, size } => { map := map.insert thmId size, size := size + 1 } + +def UsedSimps.toArray (s : UsedSimps) : Array Origin := + s.map.toArray.qsort (·.2 < ·.2) |>.map (·.1) structure Diagnostics where /-- Number of times each simp theorem has been used/applied. -/ @@ -367,9 +380,7 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do else pure thmId | _ => pure thmId - modify fun s => if s.usedTheorems.contains thmId then s else - let n := s.usedTheorems.size - { s with usedTheorems := s.usedTheorems.insert thmId n } + modify fun s => { s with usedTheorems := s.usedTheorems.insert thmId } def recordCongrTheorem (declName : Name) : SimpM Unit := do modifyDiag fun s => diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba452..cb8a954a4d16 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -6,7 +6,7 @@ options get_default_options() { // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications #if LEAN_IS_STAGE0 == 1 // switch to `true` for ABI-breaking changes affecting meta code - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `true` for changing built-in parsers used in quotations opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax