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.

@[inline]

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

The number of set bits in a Bitset.

@[inline]

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

Whether the Bitset contains any elements.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

The set s without the element i.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instHasSubset : HasSubset Bitset

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instDecidableRelSubset : DecidableRel Subset

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instSDiff : SDiff Bitset

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

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

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.

@[inline]

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

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

@[inline]

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

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

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.

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instReprHighToLow : Repr HighToLow

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInhabitedHighToLow : Inhabited HighToLow

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

@[instance_reducible]

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

@[specialize #[]]

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

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

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInhabitedLowToHigh : Inhabited LowToHigh

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

@[instance_reducible]

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

@[specialize #[]]

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

Whether f returns true for all elements of the Bitset.

@[specialize #[]]

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

Whether f returns true for any elements of the Bitset.

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.

Representations

@[instance_reducible]

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

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

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

@[instance_reducible]

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

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.

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instToString : ToString Bitset

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.

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.

@[instance_reducible]

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

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

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.

@[instance_reducible]

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

Operations

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

@[instance_reducible]

instance ImportGraph.Shake.Needs.instBEq : BEq Needs

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

Includes i in the field of Needs corresponding to k.

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

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

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

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

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

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

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

@[specialize #[1]]

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

Applies f to all component Bitsets of the given Needs.

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

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

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

@[inline]

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

Whether all component bitsets are empty.

@[inline]

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

Whether the component bitset at k : NeedsKind is empty.

@[inline]

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

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

@[instance_reducible]

instance ImportGraph.Shake.Needs.instSDiff : SDiff Needs

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

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.

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

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.

@[instance_reducible]

instance ImportGraph.Shake.Needs.instToString : ToString Needs

@[instance_reducible]

instance ImportGraph.Shake.NeedsKind.instToString : ToString NeedsKind

@[inline]

def ImportGraph.Shake.NeedsKind.toPrivate : Array NeedsKind

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

@[inline]

def ImportGraph.Shake.NeedsKind.toPublic : Array NeedsKind

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

@[inline]

def ImportGraph.Shake.NeedsKind.fromPrivate : Array NeedsKind

The NeedsKinds which (directly) demand the private scope.

@[inline]

def ImportGraph.Shake.NeedsKind.fromPublic : Array NeedsKind

The NeedsKinds which (directly) demand the public scope.

@[inline]

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

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

@[inline]

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

The NeedsKinds which (directly) demand the given scope.

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

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

@[inline]

def ImportGraph.Shake.NeedsKind.fromPrivateTrans : Array NeedsKind

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

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

@[inline]

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

The scope (directly) demanded by the NeedsKind.

@[inline]

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

The scope targeted by the NeedsKind.

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

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.

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.

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

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

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.