ae1ab94992
This PR reworks the `simp` set around the `Id` monad, to not elide or unfold `pure` and `Id.run` In particular, it stops encoding the "defeq abuse" of `Id X = X` in the statements of theorems, instead using `Id.run` and `pure` to pass back and forth between these two spellings. Often when writing these with `pure`, they generalize to other lawful monads; though such changes were split off to other PRs. This fixes the problem with the current simp set where `Id.run (pure x)` is simplified to `Id.run x`, instead of the desirable `x`. This is particularly bad because the` x` is sometimes inferred with type `Id X` instead of `X`, which prevents other `simp` lemmas about `X` from firing. Making `Id` reducible instead is not an option, as then the `Monad` instances would have nothing to key on. --------- Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
63 lines
2 KiB
Text
63 lines
2 KiB
Text
/-
|
||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Author: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import Lean.Data.PersistentHashMap
|
||
|
||
namespace Lean
|
||
universe u v
|
||
|
||
structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where
|
||
(set : PersistentHashMap α Unit)
|
||
|
||
abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
|
||
|
||
namespace PersistentHashSet
|
||
|
||
@[inline] def empty [BEq α] [Hashable α] : PersistentHashSet α :=
|
||
{ set := PersistentHashMap.empty }
|
||
|
||
instance [BEq α] [Hashable α] : Inhabited (PersistentHashSet α) where
|
||
default := empty
|
||
|
||
instance [BEq α] [Hashable α] : EmptyCollection (PersistentHashSet α) :=
|
||
⟨empty⟩
|
||
|
||
variable {_ : BEq α} {_ : Hashable α}
|
||
|
||
@[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
|
||
s.set.isEmpty
|
||
|
||
@[inline] def insert (s : PersistentHashSet α) (a : α) : PersistentHashSet α :=
|
||
{ set := s.set.insert a () }
|
||
|
||
@[inline] def erase (s : PersistentHashSet α) (a : α) : PersistentHashSet α :=
|
||
{ set := s.set.erase a }
|
||
|
||
@[inline] def find? (s : PersistentHashSet α) (a : α) : Option α :=
|
||
match s.set.findEntry? a with
|
||
| some (a, _) => some a
|
||
| none => none
|
||
|
||
@[inline] def contains (s : PersistentHashSet α) (a : α) : Bool :=
|
||
s.set.contains a
|
||
|
||
@[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
|
||
|
||
@[inline] def fold {β : Type v} (f : β → α → β) (init : β) (s : PersistentHashSet α) : β :=
|
||
Id.run $ s.foldM (pure <| f · ·) init
|
||
|
||
def toList (s : PersistentHashSet α) : List α :=
|
||
s.set.toList.map (·.1)
|
||
|
||
protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
|
||
(s : PersistentHashSet α) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ := do
|
||
PersistentHashMap.forIn s.set init fun p s => f p.1 s
|
||
|
||
instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashSet α) α where
|
||
forIn := PersistentHashSet.forIn
|
||
|
||
end PersistentHashSet
|