@[reducible, inline]

abbrev ShareCommon.Object : Type

Equations

• ShareCommon.Object = NonScalar

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

@[reducible, inline]

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

structure ShareCommon.StateFactoryImpl : Type 1

• Map : Type
• Set : Type
• mkState : Unit → self.Map × self.Set
• mapFind? : self.Map → ShareCommon.Object → Option ShareCommon.Object
• mapInsert : self.Map → ShareCommon.Object → ShareCommon.Object → self.Map
• setFind? : self.Set → ShareCommon.Object → Option ShareCommon.Object
• setInsert : self.Set → ShareCommon.Object → self.Set

opaque ShareCommon.StateFactoryPointed : NonemptyType

@[reducible, inline]

abbrev ShareCommon.StateFactory : Type

theorem ShareCommon.instNonemptyStateFactory : Nonempty ShareCommon.StateFactory

@[extern lean_sharecommon_eq]

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

@[extern lean_sharecommon_hash]

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

structure ShareCommon.StateFactoryBuilder : Type 1

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

unsafe def ShareCommon.StateFactory.mkImpl : ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory

@[implemented_by ShareCommon.StateFactory.mkImpl]

opaque ShareCommon.StateFactory.mk : ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory

unsafe def ShareCommon.StateFactory.get : ShareCommon.StateFactory → ShareCommon.StateFactoryImpl

opaque ShareCommon.StatePointed (σ : ShareCommon.StateFactory) : NonemptyType

Internally State is implemented as a pair ObjectMap and ObjectSet

@[reducible, inline]

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

Equations

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

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

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

@[implemented_by ShareCommon.mkStateImpl]

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

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

Equations

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

@[extern lean_state_sharecommon]

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

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

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

@[reducible, inline]

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

@[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)

@[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 α

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

@[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