Utilities for Shake types

This file provides basic API for Needs, NeedsKind, and Bitset.

def ImportGraph.Nat.numSetBits (n : Nat) : Nat

Counts the number of set bits in the binary representation of n.

Equations

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

@[inline]

def ImportGraph.Shake.Bitset.size (s : Bitset) : Nat

The number of set bits in a Bitset.

Equations

• s.size = ImportGraph.Nat.numSetBits s.toNat

@[inline]

def ImportGraph.Shake.Bitset.isEmpty (s : Bitset) : Bool

Whether the Bitset contains any elements.

Equations

• s.isEmpty = (s.toNat == 0)

@[inline]

def ImportGraph.Shake.Bitset.univSize (s : Bitset) : Nat

The minimum size of the ambient index set necessary to hold Bitset.

Equations

• s.univSize = if s.isEmpty = true then 0 else s.toNat.log2 + 1

@[inline]

def ImportGraph.Shake.Bitset.univ (n : Nat) : Bitset

The full set {0, ..., n - 1}.

Equations

• ImportGraph.Shake.Bitset.univ n = { toNat := 1 <<< n - 1 }

@[inline]

def ImportGraph.Shake.Bitset.erase (s : Bitset) (i : Nat) : Bitset

The set s without the element i.

Equations

• s.erase i = if s.has i = true then s ^^^ {i} else s

@[inline]

def ImportGraph.Shake.Bitset.max? (s : Bitset) : Option Nat

The highest set bit of a Bitset, if there is one.

Equations

• s.max? = if s.isEmpty = true then none else some s.toNat.log2

@[inline]

def ImportGraph.Shake.Bitset.min? (s : Bitset) : Option Nat

The lowest set bit of a Bitset, if there is one.

Equations

• s.min? = if s.isEmpty = true then none else some (s.toNat ^^^ s.toNat &&& s.toNat - 1).log2

@[inline]

def ImportGraph.Shake.Bitset.le (a b : Bitset) : Bool

a.le b iff every bit set in a is also set in b.

Equations

• a.le b = (a.toNat &&& b.toNat == a.toNat)

@[inline]

def ImportGraph.Shake.Bitset.lt (a b : Bitset) : Bool

a.le b iff every bit set in a is also set in b, and b is not equal to a.

Equations

• a.lt b = (a.le b && a != b)

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instHasSubset : HasSubset Bitset

Equations

• ImportGraph.Shake.Bitset.instHasSubset = { Subset := fun (a b : ImportGraph.Shake.Bitset) => a.le b = true }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instDecidableRelSubset : DecidableRel Subset

Equations

• x✝¹.instDecidableRelSubset x✝ = if h : x✝¹.le x✝ = true then isTrue h else isFalse h

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instSDiff : SDiff Bitset

Equations

• ImportGraph.Shake.Bitset.instSDiff = { sdiff := fun (a b : ImportGraph.Shake.Bitset) => { toNat := a.toNat &&& (a.toNat ^^^ b.toNat) } }

@[specialize #[]]

def ImportGraph.Shake.Bitset.foldr {α : Type} (s : Bitset) (init : α) (f : α → Nat → α) : α

Fold over the set bit indices in a Bitset from high to low. This is more efficient for large bitsets than Bitset.foldl.

Equations

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

@[specialize #[]]

def ImportGraph.Shake.Bitset.foldl {α : Type} (s : Bitset) (init : α) (f : α → Nat → α) : α

Fold over the set bit indices in a Bitset from low to high. This is less efficient for large bitsets than Bitset.foldr.

Equations

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

Array

@[inline]

def ImportGraph.Shake.Bitset.ofArray (idxs : Array Nat) : Bitset

Regarding idxs : Array Nat as a set of Bitset indices, create a bitset which contains each idx ∈ idxs.

Equations

• ImportGraph.Shake.Bitset.ofArray idxs = Array.foldl (flip insert) ∅ idxs

@[inline]

def ImportGraph.Shake.Bitset.toIdxs (s : Bitset) : Array Nat

The set bit indices of a Bitset in order from low to high.

Equations

• s.toIdxs = s.foldl #[] fun (x1 : Array Nat) (x2 : Nat) => x1.push x2

@[inline]

def ImportGraph.Shake.Bitset.toRevIdxs (s : Bitset) : Array Nat

The set bit indices of a Bitset in order from high to low.

Equations

• s.toRevIdxs = s.foldr #[] fun (x1 : Array Nat) (x2 : Nat) => x1.push x2

ForIn

@[specialize #[]]

def ImportGraph.Shake.Bitset.forInRev {m : Type → Type u_1} [Monad m] {β : Type} (s : Bitset) (init : β) (f : Nat → β → m (ForInStep β)) : m (ForInStep β)

Iterates through the set bit indices of a Bitset from high to low.

Equations

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

structure ImportGraph.Shake.Bitset.HighToLow : Type

A Bitset with a ForIn instance that traverses the bitset's indices from the highest index to the lowest. This is the most efficient traversal of a bitset for large bitsets.

• toBitset : Bitset

def ImportGraph.Shake.Bitset.instReprHighToLow.repr : HighToLow → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instReprHighToLow : Repr HighToLow

Equations

• ImportGraph.Shake.Bitset.instReprHighToLow = { reprPrec := ImportGraph.Shake.Bitset.instReprHighToLow.repr }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInhabitedHighToLow : Inhabited HighToLow

Equations

• ImportGraph.Shake.Bitset.instInhabitedHighToLow = { default := ImportGraph.Shake.Bitset.instInhabitedHighToLow.default }

@[inline]

def ImportGraph.Shake.Bitset.highToLow (b : Bitset) : HighToLow

A Bitset with a ForIn instance that traverses the bitset's indices from the highest index to the lowest. This is the most efficient traversal of a bitset for large bitsets.

Equations

• b.highToLow = { toBitset := b }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instForInHighToLowNatOfMonad {m : Type → Type u_1} [Monad m] : ForIn m HighToLow Nat

Equations

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

@[specialize #[]]

def ImportGraph.Shake.Bitset.forIn {m : Type → Type u_1} [Monad m] {β : Type} (s : Bitset) (init : β) (f : Nat → β → m (ForInStep β)) : m (ForInStep β)

Equations

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

structure ImportGraph.Shake.Bitset.LowToHigh : Type

A Bitset with a ForIn instance that traverses the bitset's indices from the highest index to the lowest. Bitset.HighToLow (Bitset.highToLow) is more efficient for large Bitsets.

• toBitset : Bitset

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instReprLowToHigh : Repr LowToHigh

Equations

• ImportGraph.Shake.Bitset.instReprLowToHigh = { reprPrec := ImportGraph.Shake.Bitset.instReprLowToHigh.repr }

def ImportGraph.Shake.Bitset.instReprLowToHigh.repr : LowToHigh → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInhabitedLowToHigh : Inhabited LowToHigh

Equations

• ImportGraph.Shake.Bitset.instInhabitedLowToHigh = { default := ImportGraph.Shake.Bitset.instInhabitedLowToHigh.default }

@[inline]

def ImportGraph.Shake.Bitset.lowToHigh (b : Bitset) : LowToHigh

A Bitset with a ForIn instance that traverses the bitset's indices from the highest index to the lowest. Bitset.HighToLow (Bitset.highToLow) is more efficient for large Bitsets.

Equations

• b.lowToHigh = { toBitset := b }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instForInLowToHighNatOfMonad {m : Type → Type u_1} [Monad m] : ForIn m LowToHigh Nat

Equations

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

@[specialize #[]]

def ImportGraph.Shake.Bitset.all (b : Bitset) (f : Nat → Bool) : Bool

Whether f returns true for all elements of the Bitset.

Equations

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

@[specialize #[]]

def ImportGraph.Shake.Bitset.any (b : Bitset) (f : Nat → Bool) : Bool

Whether f returns true for any elements of the Bitset.

Equations

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

def ImportGraph.Shake.Bitset.extractArray {α : Type} (a : Array α) (b : Bitset) : Array α

Extract the elements of a : Array α occurring at the indices specified in b : Bitset. Ignores elements of b that index outside the array.

Equations

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

Representations

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instToJson : Lean.ToJson Bitset

Equations

• ImportGraph.Shake.Bitset.instToJson = { toJson := ImportGraph.Shake.Bitset.instToJson.toJson }

def ImportGraph.Shake.Bitset.instToJson.toJson : Bitset → Lean.Json

Equations

• ImportGraph.Shake.Bitset.instToJson.toJson x✝ = Lean.Json.mkObj [[("toNat", Lean.toJson x✝.toNat)]].flatten

def ImportGraph.Shake.Bitset.instFromJson.fromJson : Lean.Json → Except String Bitset

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instFromJson : Lean.FromJson Bitset

Equations

• ImportGraph.Shake.Bitset.instFromJson = { fromJson? := ImportGraph.Shake.Bitset.instFromJson.fromJson }

def ImportGraph.Shake.Bitset.toString (b : Bitset) (univSize? : Option Nat := none) : String

Converts a Bitset to a string of the form "◻◼◻◻◻◼◻◼◼◻◻◼", where indices run left-to-right from 0 and ◻ represents absence at that index, while ◼ represents presence.

By default, this shows only as many squares as necessary (or "◻" for an empty bitset), and so in the nonempty case the last square will always be ◼. Instead, univSize? : Option Nat can be provided to set the total number of indices, and will either truncate (even if higher bits are set) or pad with ◻ as appropriate.

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instToString : ToString Bitset

Equations

• ImportGraph.Shake.Bitset.instToString = { toString := fun (b : ImportGraph.Shake.Bitset) => b.toString }

ForIn

@[specialize #[]]

def ImportGraph.Shake.Needs.forInRev {m : Type → Type u_1} [Monad m] {β : Type} (n : Needs) (init : β) (f : NeedsKind × Nat → β → m (ForInStep β)) : m (ForInStep β)

Iterates through NeedsKinds.all, and for each NeedsKind, iterates through the set bit indices of the corresponding Bitset from highest to lowest.

Equations

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

structure ImportGraph.Shake.Needs.HighToLow : Type

A Needs with a ForIn instance that traverses the component bitset's indices from the highest index to the lowest. This is the most efficient traversal of a bitset. Does not actually reverse the indices in the bitsets.

• toNeeds : Needs

def ImportGraph.Shake.Needs.highToLow (b : Needs) : HighToLow

A Needs with a ForIn instance that traverses the component bitset's indices from the highest index to the lowest. This is the most efficient traversal of a bitset. Does not actually reverse the indices in the bitsets.

Equations

• b.highToLow = { toNeeds := b }

@[instance_reducible]

instance ImportGraph.Shake.Needs.instForInHighToLowProdNeedsKindNatOfMonad {m : Type → Type u_1} [Monad m] : ForIn m HighToLow (NeedsKind × Nat)

Equations

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

@[specialize #[]]

def ImportGraph.Shake.Needs.forIn {m : Type → Type u_1} [Monad m] {β : Type} (n : Needs) (init : β) (f : NeedsKind × Nat → β → m (ForInStep β)) : m (ForInStep β)

Iterates through NeedsKinds.all, and for each NeedsKind, iterates through the set bit indices of the corresponding Bitset from lowest to highest.

Equations

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

structure ImportGraph.Shake.Needs.LowToHigh : Type

A Needs with a ForIn instance that traverses the component bitset's indices from the lowest index to the highest. b.highToLow is more efficient.

• toNeeds : Needs

def ImportGraph.Shake.Needs.lowToHigh (b : Needs) : LowToHigh

A Needs with a ForIn instance that traverses the component bitset's indices from the lowest index to the highest. b.highToLow is more efficient.

Equations

• b.lowToHigh = { toNeeds := b }

@[instance_reducible]

instance ImportGraph.Shake.Needs.instForInLowToHighProdNeedsKindNatOfMonad {m : Type → Type u_1} [Monad m] : ForIn m LowToHigh (NeedsKind × Nat)

Equations

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

Operations

def ImportGraph.Shake.Needs.instBEq.beq : Needs → Needs → Bool

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Shake.Needs.instBEq.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.Shake.Needs.instBEq : BEq Needs

Equations

• ImportGraph.Shake.Needs.instBEq = { beq := ImportGraph.Shake.Needs.instBEq.beq }

def ImportGraph.Shake.Needs.single (i : Nat) (k : NeedsKind) : Needs

Includes i in the field of Needs corresponding to k.

Equations

• ImportGraph.Shake.Needs.single i k = ImportGraph.Shake.Needs.empty.set k {i}

@[inline]

def ImportGraph.Shake.Needs.applyAt {β : Sort u_1} (n : Needs) (k : NeedsKind) (f : Bitset → β) : β

Apply f to the component bitset of n : Needs at the given NeedsKind. Rephrasing of f (n.get k) for readability.

Equations

• n.applyAt k f = f (n.get k)

@[inline]

def ImportGraph.Shake.Needs.any (n : Needs) (f : Bitset → Bool) : Bool

Whether f : Bitset → Bool is true for any of the component bitsets of the given Needs.

Equations

• n.any f = ImportGraph.Shake.NeedsKind.all.any fun (x : ImportGraph.Shake.NeedsKind) => n.applyAt x f

@[inline]

def ImportGraph.Shake.Needs.anyWithKind (n : Needs) (f : NeedsKind → Bitset → Bool) : Bool

Whether f : NeedsKind → Bitset → Bool is true for any of the component bitsets of the given Needs at the bitset's corresponding NeedsKind.

Equations

• n.anyWithKind f = ImportGraph.Shake.NeedsKind.all.any fun (k : ImportGraph.Shake.NeedsKind) => n.applyAt k (f k)

@[inline]

def ImportGraph.Shake.Needs.all (n : Needs) (f : Bitset → Bool) : Bool

Whether f : Bitset → Bool is true for all of the component bitsets of the given Needs.

Equations

• n.all f = ImportGraph.Shake.NeedsKind.all.all fun (x : ImportGraph.Shake.NeedsKind) => n.applyAt x f

@[inline]

def ImportGraph.Shake.Needs.allWithKind (n : Needs) (f : NeedsKind → Bitset → Bool) : Bool

Whether f : NeedsKind → Bitset → Bool is true for any of the component bitsets of the given Needs at the bitset's corresponding NeedsKind.

Equations

• n.allWithKind f = ImportGraph.Shake.NeedsKind.all.all fun (k : ImportGraph.Shake.NeedsKind) => n.applyAt k (f k)

@[inline]

def ImportGraph.Shake.Needs.fold {α : Type u_1} (n : Needs) (f : α → Bitset → α) (init : α) : α

Folds f over the bitsets in Needs (in the order of NeedsKind.all).

Equations

• n.fold f init = Array.foldl (fun (a : α) (k : ImportGraph.Shake.NeedsKind) => n.applyAt k (f a)) init ImportGraph.Shake.NeedsKind.all

@[inline]

def ImportGraph.Shake.Needs.foldWithKind {α : Type u_1} (n : Needs) (f : α → NeedsKind → Bitset → α) (init : α) : α

Folds f over the bitsets in Needs at their corresponding NeedsKinds (in the order of NeedsKind.all).

Equations

• n.foldWithKind f init = Array.foldl (fun (a : α) (k : ImportGraph.Shake.NeedsKind) => n.applyAt k (f a k)) init ImportGraph.Shake.NeedsKind.all

@[specialize #[1]]

def ImportGraph.Shake.Needs.map (n : Needs) (f : Bitset → Bitset) : Needs

Applies f to all component Bitsets of the given Needs.

Equations

• n.map f = { pub := f n.pub, priv := f n.priv, metaPub := f n.metaPub, metaPriv := f n.metaPriv, privOfPriv := f n.privOfPriv, metaPrivOfPriv := f n.metaPrivOfPriv }

@[specialize #[1]]

def ImportGraph.Shake.Needs.mapWithKind (n : Needs) (f : NeedsKind → Bitset → Bitset) : Needs

Applies f to all component Bitsets of the given Needs at their corresponding NeedsKinds.

Equations

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

@[specialize #[2]]

def ImportGraph.Shake.Needs.map₂ (n₁ n₂ : Needs) (f : Bitset → Bitset → Bitset) : Needs

Applies f "pointwise" to the pairs of bitsets at each given NeedsKind. f (n₁.get k) (n₂.get k) = (n₁.map₂ n₂ f).get k for all k : NeedsKind.

Equations

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

@[specialize #[2]]

def ImportGraph.Shake.Needs.mapWithKind₂ (n₁ n₂ : Needs) (f : NeedsKind → Bitset → Bitset → Bitset) : Needs

Applies f "pointwise" to the pairs of bitsets at each given NeedsKind. f k (n₁.get k) (n₂.get k) = (n₁.mapWithKind₂ n₂ f).get k for all k : NeedsKind.

Equations

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

@[inline]

def ImportGraph.Shake.Needs.isEmpty (n : Needs) : Bool

Whether all component bitsets are empty.

Equations

• n.isEmpty = n.all fun (x : ImportGraph.Shake.Bitset) => x.isEmpty

@[inline]

def ImportGraph.Shake.Needs.isEmptyAt (k : NeedsKind) (n : Needs) : Bool

Whether the component bitset at k : NeedsKind is empty.

Equations

• ImportGraph.Shake.Needs.isEmptyAt k n = (n.get k).isEmpty

@[inline]

def ImportGraph.Shake.Needs.univSize (n : Needs) : Nat

The minimum size of the ambient index set necessary to hold every component Bitset.

Equations

• n.univSize = n.fold (fun (size : Nat) (b : ImportGraph.Shake.Bitset) => max size b.univSize) 0

@[instance_reducible]

instance ImportGraph.Shake.Needs.instSDiff : SDiff Needs

Equations

• ImportGraph.Shake.Needs.instSDiff = { sdiff := fun (a b : ImportGraph.Shake.Needs) => a.map₂ b fun (x1 x2 : ImportGraph.Shake.Bitset) => x1 \ x2 }

@[inline]

def ImportGraph.Shake.Needs.directLe (n m : Needs) : Bool

Whether each field of the first Needs is contained within the corresponding field of the second. Use with caution: this does not necessarily indicate that one Needs subsumes another. See also Needs.coveredBy for testing against an import hierarchy.

Equations

• n.directLe m = (n.pub.le m.pub && n.priv.le m.priv && n.metaPub.le m.metaPub && n.metaPriv.le m.metaPriv && n.privOfPriv.le m.privOfPriv && n.metaPrivOfPriv.le m.metaPrivOfPriv)

theorem ImportGraph.Shake.Needs.directLe_eq_allWithKind_le : directLe = fun (n m : Needs) => n.allWithKind fun (k : NeedsKind) (nb : Bitset) => nb.le (m.get k)

Representations

def ImportGraph.Shake.Needs.brailleCellAt (i : Nat) (n : Needs) : Char

A braille cell depicting the set of NeedsKinds of n at index i. The left column holds non-meta needs, and the right column meta needs; the top row holds public needs, the middle row private, and the bottom row private-of-private.

Equations

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

@[inline]

def ImportGraph.Shake.Needs.toStringAt (i : Nat) (n : Needs) : String

A braille cell in brackets depicting the set of NeedsKinds of n at index i. The left column holds non-meta needs, and the right column meta needs; the top row holds public needs, the middle row private, and the bottom row private-of-private.

For the braille cell character without brackets, see Needs.brailleCellAt.

Equations

• ImportGraph.Shake.Needs.toStringAt i n = toString "[" ++ toString (ImportGraph.Shake.Needs.brailleCellAt i n) ++ toString "]"

def ImportGraph.Shake.Needs.toString (n : Needs) (univSize? : Option Nat := none) (dividers : Bool := true) : String

Represents a Needs as a string of the form e.g. │⠇│⠑│⠁│⠝│, where each braille cell represents the set of NeedsKinds expressed by a single "column" of the Needs (i.e. at a given index). The left column of each Braille cell are non-meta needs, and the right column holds meta needs; the top row holds public needs, the middle private, and the bottom private-of-private.

By default, shows dividers (│) between each braille cell; dividers := false omits dividers.

By default this shows only as many cells as necessary, or a single empty cell for an empty Needs. Instead, univSize? : Option Nat can be provided to set the total number of indices, and will either truncate (even if higher indices are set) or pad with empty cells as appropriate.

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.Needs.instToString : ToString Needs

Equations

• ImportGraph.Shake.Needs.instToString = { toString := fun (n : ImportGraph.Shake.Needs) => n.toString }

@[instance_reducible]

instance ImportGraph.Shake.NeedsKind.instToString : ToString NeedsKind

Equations

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

@[inline]

def ImportGraph.Shake.NeedsKind.toPrivate : Array NeedsKind

The NeedsKinds which land (directly) in the private scope.

Equations

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

@[inline]

def ImportGraph.Shake.NeedsKind.toPublic : Array NeedsKind

The NeedsKinds which land (directly) in the public scope.

Equations

• ImportGraph.Shake.NeedsKind.toPublic = #[ImportGraph.Shake.NeedsKind.pub, ImportGraph.Shake.NeedsKind.metaPub]

@[inline]

def ImportGraph.Shake.NeedsKind.fromPrivate : Array NeedsKind

The NeedsKinds which (directly) demand the private scope.

Equations

• ImportGraph.Shake.NeedsKind.fromPrivate = #[ImportGraph.Shake.NeedsKind.privOfPriv, ImportGraph.Shake.NeedsKind.metaPrivOfPriv]

@[inline]

def ImportGraph.Shake.NeedsKind.fromPublic : Array NeedsKind

The NeedsKinds which (directly) demand the public scope.

Equations

• ImportGraph.Shake.NeedsKind.fromPublic = #[ImportGraph.Shake.NeedsKind.priv, ImportGraph.Shake.NeedsKind.pub, ImportGraph.Shake.NeedsKind.metaPriv, ImportGraph.Shake.NeedsKind.metaPub]

@[inline]

def ImportGraph.Shake.NeedsKind.to (vis : Lean.Environment.Visibility) : Array NeedsKind

The NeedsKinds which land (directly) in the given scope.

Equations

• ImportGraph.Shake.NeedsKind.to Lean.Environment.Visibility.public = ImportGraph.Shake.NeedsKind.toPublic
• ImportGraph.Shake.NeedsKind.to Lean.Environment.Visibility.private = ImportGraph.Shake.NeedsKind.toPrivate

@[inline]

def ImportGraph.Shake.NeedsKind.from (vis : Lean.Environment.Visibility) : Array NeedsKind

The NeedsKinds which (directly) demand the given scope.

Equations

• ImportGraph.Shake.NeedsKind.from Lean.Environment.Visibility.public = ImportGraph.Shake.NeedsKind.fromPublic
• ImportGraph.Shake.NeedsKind.from Lean.Environment.Visibility.private = ImportGraph.Shake.NeedsKind.fromPrivate

@[inline]

def ImportGraph.Shake.NeedsKind.toPrivateTrans : Array NeedsKind

The NeedsKinds which land in the private scope after taking into account public ⊆ private on both ends. This is simply NeedsKind.all, but can help record why we're using it.

Equations

• ImportGraph.Shake.NeedsKind.toPrivateTrans = ImportGraph.Shake.NeedsKind.all

@[inline]

def ImportGraph.Shake.NeedsKind.toPublicTrans : Array NeedsKind

The NeedsKinds which land in the public scope after taking into account public ⊆ private on both ends. This is simply toPublic, but can help record why we're using it.

Equations

• ImportGraph.Shake.NeedsKind.toPublicTrans = ImportGraph.Shake.NeedsKind.toPublic

@[inline]

def ImportGraph.Shake.NeedsKind.fromPrivateTrans : Array NeedsKind

The NeedsKinds which demand the private scope after taking into account public ⊆ private on both ends.

Equations

• ImportGraph.Shake.NeedsKind.fromPrivateTrans = ImportGraph.Shake.NeedsKind.fromPrivate

@[inline]

def ImportGraph.Shake.NeedsKind.fromPublicTrans : Array NeedsKind

The NeedsKinds which demand the public scope after taking into account public ⊆ private on both ends. This is simply NeedsKind.all, but can help record why we're using it.

Equations

• ImportGraph.Shake.NeedsKind.fromPublicTrans = ImportGraph.Shake.NeedsKind.all

@[inline]

def ImportGraph.Shake.NeedsKind.source (k : NeedsKind) : Lean.Environment.Visibility

The scope (directly) demanded by the NeedsKind.

Equations

• k.source = if k.isAll = true then Lean.Environment.Visibility.private else Lean.Environment.Visibility.public

@[inline]

def ImportGraph.Shake.NeedsKind.target (k : NeedsKind) : Lean.Environment.Visibility

The scope targeted by the NeedsKind.

Equations

• k.target = if k.isExported = true then Lean.Environment.Visibility.public else Lean.Environment.Visibility.private

@[inline]

def ImportGraph.Shake.NeedsKind.connects (src tgt : Lean.Environment.Visibility) (k : NeedsKind) : Bool

Whether k places the src in the tgt visibility, after taking into account public ⊆ private on both ends. Note that we abstractly consider NeedsKind to be a single arrow between scopes (i.e. privOfPriv only relates the private scope to the private scope), but in this function we allow linearization (i.e. composition with public ↪ private)

Equations

• ImportGraph.Shake.NeedsKind.connects Lean.Environment.Visibility.public Lean.Environment.Visibility.private k = true
• ImportGraph.Shake.NeedsKind.connects Lean.Environment.Visibility.public Lean.Environment.Visibility.public k = k.isExported
• ImportGraph.Shake.NeedsKind.connects Lean.Environment.Visibility.private Lean.Environment.Visibility.private k = k.isAll
• ImportGraph.Shake.NeedsKind.connects Lean.Environment.Visibility.private Lean.Environment.Visibility.public k = false

def ImportGraph.Shake.NeedsKind.yields (tgt : Lean.Environment.Visibility) (k : NeedsKind) : Bool

Whether k yields something in the scope tgt. This is always true when tgt is .private thanks to public ⊆ private on the target side, and is k.isExported when .public.

Equations

• ImportGraph.Shake.NeedsKind.yields Lean.Environment.Visibility.public k = k.isExported
• ImportGraph.Shake.NeedsKind.yields Lean.Environment.Visibility.private k = true

def ImportGraph.Shake.NeedsKind.demands (src : Lean.Environment.Visibility) (k : NeedsKind) : Bool

Whether k demands something in the scope src. This is always true when src is .public thanks to public ⊆ private on the source side, and is k.isAll when .private.

Equations

• ImportGraph.Shake.NeedsKind.demands Lean.Environment.Visibility.public k = true
• ImportGraph.Shake.NeedsKind.demands Lean.Environment.Visibility.private k = k.isAll

def ImportGraph.Shake.NeedsKind.andThen (k₁ k₂ : NeedsKind) (connectable : k₁.target = k₂.source := by grind) : NeedsKind

Equations

• k₁.andThen k₂ connectable = { isExported := k₂.isExported, isMeta := k₁.isMeta || k₂.isMeta, isAll := k₁.isAll && k₂.isAll, not_isExported_and_isAll := ⋯ }

@[simp]

theorem ImportGraph.Shake.NeedsKind.target_andThen_eq_right_target (k₁ k₂ : NeedsKind) (connectable : k₁.target = k₂.source) : (k₁.andThen k₂ ⋯).target = k₂.target

@[simp]

theorem ImportGraph.Shake.NeedsKind.source_andThen_eq_left_source (k₁ k₂ : NeedsKind) (connectable : k₁.target = k₂.source) : (k₁.andThen k₂ ⋯).source = k₁.source

@[simp]

theorem ImportGraph.Shake.NeedsKind.andThen_assoc (k₁ k₂ k₃ : NeedsKind) (connectable₁₂ : k₁.target = k₂.source) (connectable₂₃ : k₂.target = k₃.source) : (k₁.andThen k₂ ⋯).andThen k₃ ⋯ = k₁.andThen (k₂.andThen k₃ ⋯) ⋯

@[instance_reducible]

instance ImportGraph.Shake.NeedsKind.instDecidableEqVisibility : DecidableEq Lean.Environment.Visibility

Equations

• ImportGraph.Shake.NeedsKind.instDecidableEqVisibility x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ImportGraph.Shake.NeedsKind.connecting? (src tgt : Lean.Environment.Visibility) (isMeta : Bool := false) : Option NeedsKind

The NeedsKind that represents a connection from src to tgt, with tgt the importing file. E.g., connecting? .public .private is the NeedsKind that imports a public scope into a private scope.

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Shake.NeedsKind.connecting? Lean.Environment.Visibility.private Lean.Environment.Visibility.public isMeta = none