@[reducible, inline]

abbrev ShareCommon.Object : Type

Equations

• ShareCommon.Object = NonScalar

unsafe def ShareCommon.Object.ptrEq (a b : Object) : Bool

Equations

• a.ptrEq b = (ptrAddrUnsafe a == ptrAddrUnsafe b)

@[reducible, inline]

unsafe abbrev ShareCommon.Object.ptrHash (a : Object) : UInt64

Equations

• a.ptrHash = (ptrAddrUnsafe a).toUInt64

structure ShareCommon.StateFactoryImpl : Type 1

• Map : Type
• Set : Type
• mkState : Unit → self.Map × self.Set
• mapFind? (m : self.Map) (k : Object) : Option Object
• mapInsert (m : self.Map) (k v : Object) : self.Map
• setFind? (m : self.Set) (k : Object) : Option Object
• setInsert (m : self.Set) (o : Object) : self.Set

opaque ShareCommon.StateFactoryPointed : NonemptyType

@[reducible, inline]

abbrev ShareCommon.StateFactory : Type

Equations

• ShareCommon.StateFactory = ShareCommon.StateFactoryPointed.type

Instances For

• ShareCommon.instNonemptyStateFactory

instance ShareCommon.instNonemptyStateFactory : Nonempty StateFactory

@[extern lean_sharecommon_eq]

unsafe opaque ShareCommon.Object.eq (a b : Object) : Bool

@[extern lean_sharecommon_hash]

unsafe opaque ShareCommon.Object.hash (a : Object) : UInt64

structure ShareCommon.StateFactoryBuilder : Type 1

• Map (α _β : Type) [BEq α] [Hashable α] : Type
• mkMap {α β : Type} [BEq α] [Hashable α] (capacity : Nat) : self.Map α β
• mapFind? {α β : Type} [BEq α] [Hashable α] : self.Map α β → α → Option β
• mapInsert {α β : Type} [BEq α] [Hashable α] : self.Map α β → α → β → self.Map α β
• Set (α : Type) [BEq α] [Hashable α] : Type
• mkSet {α : Type} [BEq α] [Hashable α] (capacity : Nat) : self.Set α
• setFind? {α : Type} [BEq α] [Hashable α] : self.Set α → α → Option α
• setInsert {α : Type} [BEq α] [Hashable α] : self.Set α → α → self.Set α

unsafe def ShareCommon.StateFactory.mkImpl : StateFactoryBuilder → StateFactory

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by ShareCommon.StateFactory.mkImpl]

opaque ShareCommon.StateFactory.mk : StateFactoryBuilder → StateFactory

unsafe def ShareCommon.StateFactory.get : StateFactory → StateFactoryImpl

Equations

• ShareCommon.StateFactory.get = unsafeCast

opaque ShareCommon.StatePointed (σ : StateFactory) : NonemptyType

Internally State is implemented as a pair ObjectMap and ObjectSet

@[reducible, inline]

abbrev ShareCommon.State (σ : StateFactory) : Type u

Equations

• ShareCommon.State σ = (ShareCommon.StatePointed σ).type

Instances For

• ShareCommon.instInhabitedState
• ShareCommon.instNonemptyState

instance ShareCommon.instNonemptyState {σ : StateFactory} : Nonempty (State σ)

unsafe def ShareCommon.mkStateImpl (σ : StateFactory) : State σ

Equations

• ShareCommon.mkStateImpl σ = unsafeCast (σ.get.mkState ())

@[implemented_by ShareCommon.mkStateImpl]

opaque ShareCommon.State.mk (σ : StateFactory) : State σ

instance ShareCommon.instInhabitedState {σ : StateFactory} : Inhabited (State σ)

Equations

• ShareCommon.instInhabitedState = { default := ShareCommon.State.mk σ }

@[extern lean_state_sharecommon]

def ShareCommon.State.shareCommon {α : Type u_1} {σ : StateFactory} (s : State σ) (a : α) : α × State σ

Equations

• s.shareCommon a = (a, s)

class MonadShareCommon (m : Type u → Type v) : Type (max (u + 1) v)

• withShareCommon {α : Type u} : α → m α

Instances

• Lean.ShareCommon.PShareCommonT.monadShareCommon
• Lean.ShareCommon.ShareCommonT.monadShareCommon
• ShareCommonT.monadShareCommon

@[reducible, inline]

abbrev withShareCommon {m : Type u_1 → Type u_2} [self : MonadShareCommon m] {α : Type u_1} : α → m α

Equations

• @withShareCommon = @MonadShareCommon.withShareCommon

@[reducible, inline]

abbrev shareCommonM {m : Type u_1 → Type u_2} {α : Type u_1} [MonadShareCommon m] (a : α) : m α

Equations

• shareCommonM a = withShareCommon a

@[reducible, inline]

abbrev ShareCommonT (σ : ShareCommon.StateFactory) (m : Type u → Type v) (α : Type u) : Type (max u v)

Equations

• ShareCommonT σ m = StateT (ShareCommon.State σ) m

Instances For

• ShareCommonT.monadShareCommon

@[reducible, inline]

abbrev ShareCommonM (σ : ShareCommon.StateFactory) (α : Type u_1) : Type u_1

Equations

• ShareCommonM σ = ShareCommonT σ Id

@[specialize #[]]

def ShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} {σ : ShareCommon.StateFactory} [Monad m] (a : α) : ShareCommonT σ m α

Equations

• ShareCommonT.withShareCommon a = modifyGet fun (s : ShareCommon.State σ) => s.shareCommon a

instance ShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} [Monad m] : MonadShareCommon (ShareCommonT σ m)

Equations

• ShareCommonT.monadShareCommon = { withShareCommon := fun {α : Type ?u.18} => ShareCommonT.withShareCommon }

@[inline]

def ShareCommonT.run {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} {α : Type u_1} [Monad m] (x : ShareCommonT σ m α) : m α

Equations

• x.run = StateT.run' x default

@[inline]

def ShareCommonM.run {σ : ShareCommon.StateFactory} {α : Type u_1} (x : ShareCommonM σ α) : α

Equations

• x.run = ShareCommonT.run x

@[extern lean_sharecommon_quick]

def ShareCommon.shareCommon' {α : Sort u_1} (a : α) : α

A more restrictive but efficient max sharing primitive.

Remark: it optimizes the number of RC operations, and the strategy for caching results.

Equations

• ShareCommon.shareCommon' a = a