shake core types

This file copies types and functions from Lake.CLI.Shake wholesale in order to make them public, with some modifications to Needs in order to suit our purposes (namely, we benefit from keeping track of private dependence in order to uniformly handle declarations from the same file, whereas shake can get away with handling import all specially.)

More utilities on these types are defined in ImportGraph.Shake.Basic.

Bitset

This section is copied without modification, and should be removed if Shake API becomes public.

structure ImportGraph.Shake.Bitset : Type

We use Nat as a bitset for doing efficient set operations. The bit indexes will usually be a module index.

• toNat : Nat

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedBitset : Inhabited Bitset

Equations

• ImportGraph.Shake.instInhabitedBitset = { default := ImportGraph.Shake.instInhabitedBitset.default }

@[instance_reducible]

instance ImportGraph.Shake.instDecidableEqBitset : DecidableEq Bitset

Equations

• ImportGraph.Shake.instDecidableEqBitset = ImportGraph.Shake.instDecidableEqBitset.decEq

def ImportGraph.Shake.instDecidableEqBitset.decEq (x✝ x✝¹ : Bitset) : Decidable (x✝ = x✝¹)

Equations

• ImportGraph.Shake.instDecidableEqBitset.decEq { toNat := a } { toNat := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ImportGraph.Shake.instReprBitset : Repr Bitset

Equations

• ImportGraph.Shake.instReprBitset = { reprPrec := ImportGraph.Shake.instReprBitset.repr }

def ImportGraph.Shake.instReprBitset.repr : Bitset → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instEmptyCollection : EmptyCollection Bitset

Equations

• ImportGraph.Shake.Bitset.instEmptyCollection = { emptyCollection := { toNat := 0 } }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInsertNat : Insert Nat Bitset

Equations

• ImportGraph.Shake.Bitset.instInsertNat = { insert := fun (i : Nat) (s : ImportGraph.Shake.Bitset) => { toNat := s.toNat ||| 1 <<< i } }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instSingletonNat : Singleton Nat Bitset

Equations

• ImportGraph.Shake.Bitset.instSingletonNat = { singleton := fun (i : Nat) => insert i ∅ }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInter : Inter Bitset

Equations

• ImportGraph.Shake.Bitset.instInter = { inter := fun (a b : ImportGraph.Shake.Bitset) => { toNat := a.toNat &&& b.toNat } }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instUnion : Union Bitset

Equations

• ImportGraph.Shake.Bitset.instUnion = { union := fun (a b : ImportGraph.Shake.Bitset) => { toNat := a.toNat ||| b.toNat } }

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instXorOp : XorOp Bitset

Equations

• ImportGraph.Shake.Bitset.instXorOp = { xor := fun (a b : ImportGraph.Shake.Bitset) => { toNat := a.toNat ^^^ b.toNat } }

def ImportGraph.Shake.Bitset.has (s : Bitset) (i : Nat) : Bool

Equations

• s.has i = s.toNat.testBit i

Needs and NeedsKind

This section is modified from shake's version to allow us to reason about import alls in the import hierarchy instead of dynamically.

structure ImportGraph.Shake.VisibilityKind : Type

An "atomic" visibility dependency. Note that we consider an inclusion of the public scope and an inclusion of the private scope to be two separate dependencies. Modules may be related by multiple VisibilityKinds; the presence of any VisibilityKind implies some dependency between the modules.

• isExported : Bool

  Represents a need for public (meta)? import: an import of the public scope of the source into the public scope of the target. false means that the public scope of the source is instead imported into the private scope of the target.

• isAll : Bool

  Represents a need for (meta)? import all: an import of the private scope into the private scope. false means the private scope of the source is not accessed.

• not_isExported_and_isAll : ¬(self.isExported = true ∧ self.isAll = true)

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedVisibilityKind : Inhabited VisibilityKind

Equations

• ImportGraph.Shake.instInhabitedVisibilityKind = { default := ImportGraph.Shake.instInhabitedVisibilityKind.default }

def ImportGraph.Shake.instBEqVisibilityKind.beq : VisibilityKind → VisibilityKind → Bool

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instBEqVisibilityKind : BEq VisibilityKind

Equations

• ImportGraph.Shake.instBEqVisibilityKind = { beq := ImportGraph.Shake.instBEqVisibilityKind.beq }

@[instance_reducible]

instance ImportGraph.Shake.instReprVisibilityKind : Repr VisibilityKind

Equations

• ImportGraph.Shake.instReprVisibilityKind = { reprPrec := ImportGraph.Shake.instReprVisibilityKind.repr }

def ImportGraph.Shake.instReprVisibilityKind.repr : VisibilityKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instHashableVisibilityKind : Hashable VisibilityKind

Equations

• ImportGraph.Shake.instHashableVisibilityKind = { hash := ImportGraph.Shake.instHashableVisibilityKind.hash }

def ImportGraph.Shake.instHashableVisibilityKind.hash : VisibilityKind → UInt64

Equations

• ImportGraph.Shake.instHashableVisibilityKind.hash { isExported := a, isAll := a_1, not_isExported_and_isAll := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

@[instance_reducible]

instance ImportGraph.Shake.instOrdVisibilityKind : Ord VisibilityKind

Equations

• ImportGraph.Shake.instOrdVisibilityKind = { compare := ImportGraph.Shake.instOrdVisibilityKind.ord }

def ImportGraph.Shake.instOrdVisibilityKind.ord : VisibilityKind → VisibilityKind → Ordering

Equations

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

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.VisibilityKind.priv : VisibilityKind

Equations

• ImportGraph.Shake.VisibilityKind.priv = { isExported := false, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.priv._proof_2 }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.VisibilityKind.pub : VisibilityKind

Equations

• ImportGraph.Shake.VisibilityKind.pub = { isExported := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.pub._proof_2 }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.VisibilityKind.privOfPriv : VisibilityKind

Equations

• ImportGraph.Shake.VisibilityKind.privOfPriv = { isExported := false, isAll := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.privOfPriv._proof_2 }

structure ImportGraph.Shake.NeedsKind extends ImportGraph.Shake.VisibilityKind : Type

An "atomic" module dependency. Note that we consider an inclusion of the public scope and an inclusion of the private scope to be two separate dependencies. Modules may be related by multiple NeedsKinds; the presence of any NeedsKind implies some dependency between the modules.

• isExported : Bool
• isAll : Bool
• not_isExported_and_isAll : ¬(self.isExported = true ∧ self.isAll = true)
• isMeta : Bool

  Represents (public)? meta import (all)?: a lifting of non-meta declarations to the meta phase.

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedNeedsKind : Inhabited NeedsKind

Equations

• ImportGraph.Shake.instInhabitedNeedsKind = { default := ImportGraph.Shake.instInhabitedNeedsKind.default }

@[instance_reducible]

instance ImportGraph.Shake.instBEqNeedsKind : BEq NeedsKind

Equations

• ImportGraph.Shake.instBEqNeedsKind = { beq := ImportGraph.Shake.instBEqNeedsKind.beq }

def ImportGraph.Shake.instBEqNeedsKind.beq : NeedsKind → NeedsKind → Bool

Equations

• ImportGraph.Shake.instBEqNeedsKind.beq { toVisibilityKind := a, isMeta := a_1 } { toVisibilityKind := b, isMeta := b_1 } = (a == b && a_1 == b_1)
• ImportGraph.Shake.instBEqNeedsKind.beq x✝¹ x✝ = false

def ImportGraph.Shake.instReprNeedsKind.repr : NeedsKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprNeedsKind : Repr NeedsKind

Equations

• ImportGraph.Shake.instReprNeedsKind = { reprPrec := ImportGraph.Shake.instReprNeedsKind.repr }

def ImportGraph.Shake.instHashableNeedsKind.hash : NeedsKind → UInt64

Equations

• ImportGraph.Shake.instHashableNeedsKind.hash { toVisibilityKind := a, isMeta := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

instance ImportGraph.Shake.instHashableNeedsKind : Hashable NeedsKind

Equations

• ImportGraph.Shake.instHashableNeedsKind = { hash := ImportGraph.Shake.instHashableNeedsKind.hash }

def ImportGraph.Shake.instOrdNeedsKind.ord : NeedsKind → NeedsKind → Ordering

Equations

• ImportGraph.Shake.instOrdNeedsKind.ord { toVisibilityKind := a, isMeta := a_1 } { toVisibilityKind := b, isMeta := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

@[instance_reducible]

instance ImportGraph.Shake.instOrdNeedsKind : Ord NeedsKind

Equations

• ImportGraph.Shake.instOrdNeedsKind = { compare := ImportGraph.Shake.instOrdNeedsKind.ord }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.priv : NeedsKind

Equations

• ImportGraph.Shake.NeedsKind.priv = { isExported := false, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.priv._proof_2, isMeta := false }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.pub : NeedsKind

Equations

• ImportGraph.Shake.NeedsKind.pub = { isExported := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.pub._proof_2, isMeta := false }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.metaPriv : NeedsKind

Equations

• ImportGraph.Shake.NeedsKind.metaPriv = { isExported := false, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.priv._proof_2, isMeta := true }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.metaPub : NeedsKind

Equations

• ImportGraph.Shake.NeedsKind.metaPub = { isExported := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.pub._proof_2, isMeta := true }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.privOfPriv : NeedsKind

Equations

• ImportGraph.Shake.NeedsKind.privOfPriv = { isExported := false, isAll := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.privOfPriv._proof_2, isMeta := false }

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.metaPrivOfPriv : NeedsKind

Equations

• ImportGraph.Shake.NeedsKind.metaPrivOfPriv = { isExported := false, isAll := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.privOfPriv._proof_2, isMeta := true }

def ImportGraph.Shake.NeedsKind.setIsAll (k : NeedsKind) : NeedsKind

Equations

• k.setIsAll = { isExported := false, isAll := true, not_isExported_and_isAll := ImportGraph.Shake.VisibilityKind.privOfPriv._proof_1✝, isMeta := k.isMeta }

def ImportGraph.Shake.NeedsKind.unsetIsAll (k : NeedsKind) : NeedsKind

Equations

• k.unsetIsAll = { isExported := k.isExported, not_isExported_and_isAll := ⋯, isMeta := k.isMeta }

def ImportGraph.Shake.NeedsKind.all : Array NeedsKind

Equations

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

def ImportGraph.Shake.NeedsKind.ofImport : Lean.Import → NeedsKind

Assumes that ¬(imp.isExported ∧ imp.importAll).

Equations

• ImportGraph.Shake.NeedsKind.ofImport { module := module, importAll := importAll, isMeta := true } = ImportGraph.Shake.NeedsKind.metaPub
• ImportGraph.Shake.NeedsKind.ofImport { module := module, importAll := importAll } = ImportGraph.Shake.NeedsKind.pub
• ImportGraph.Shake.NeedsKind.ofImport { module := module, isExported := false, isMeta := true } = ImportGraph.Shake.NeedsKind.metaPriv
• ImportGraph.Shake.NeedsKind.ofImport { module := module, isExported := false } = ImportGraph.Shake.NeedsKind.priv
• ImportGraph.Shake.NeedsKind.ofImport { module := module, importAll := true, isExported := false } = ImportGraph.Shake.NeedsKind.privOfPriv
• ImportGraph.Shake.NeedsKind.ofImport { module := module, importAll := true, isExported := false, isMeta := true } = ImportGraph.Shake.NeedsKind.metaPrivOfPriv

def ImportGraph.Shake.NeedsKind.toImport (module : Lean.Name) (k : NeedsKind) : Lean.Import

An import effecting a NeedsKind.

Equations

• ImportGraph.Shake.NeedsKind.toImport module k = { module := module, importAll := k.isAll, isExported := k.isExported, isMeta := k.isMeta }

structure ImportGraph.Shake.Needs : Type

Logically, a map NeedsKind → Set <modules>.

• pub : Bitset
• priv : Bitset
• metaPub : Bitset
• metaPriv : Bitset
• privOfPriv : Bitset
• metaPrivOfPriv : Bitset

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedNeeds : Inhabited Needs

Equations

• ImportGraph.Shake.instInhabitedNeeds = { default := ImportGraph.Shake.instInhabitedNeeds.default }

@[instance_reducible]

instance ImportGraph.Shake.instReprNeeds : Repr Needs

Equations

• ImportGraph.Shake.instReprNeeds = { reprPrec := ImportGraph.Shake.instReprNeeds.repr }

def ImportGraph.Shake.instReprNeeds.repr : Needs → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev ImportGraph.Shake.Provides : Type

An abbreviation for Needs, but intended to express what is provided to a given scope. Notably, we expect this to be both transitively closed and linearized (i.e., to have also taken public ⊆ private into account) but do not enforce this for ease of building up Provides.

Equations

• ImportGraph.Shake.Provides = ImportGraph.Shake.Needs

def ImportGraph.Shake.Needs.empty : Needs

Equations

• ImportGraph.Shake.Needs.empty = { pub := ∅, priv := ∅, metaPub := ∅, metaPriv := ∅, privOfPriv := ∅, metaPrivOfPriv := ∅ }

@[instance_reducible]

instance ImportGraph.Shake.instEmptyCollectionNeeds : EmptyCollection Needs

Equations

• ImportGraph.Shake.instEmptyCollectionNeeds = { emptyCollection := ImportGraph.Shake.Needs.empty }

@[inline]

def ImportGraph.Shake.Needs.get (needs : Needs) (k : NeedsKind) : Bitset

Equations

• needs.get { isExported := true, not_isExported_and_isAll := ⋯, isMeta := false } = needs.pub
• needs.get { isExported := false, not_isExported_and_isAll := ⋯, isMeta := false } = needs.priv
• needs.get { isExported := true, not_isExported_and_isAll := ⋯, isMeta := true } = needs.metaPub
• needs.get { isExported := false, not_isExported_and_isAll := ⋯, isMeta := true } = needs.metaPriv
• needs.get { isExported := false, isAll := true, not_isExported_and_isAll := ⋯, isMeta := false } = needs.privOfPriv
• needs.get { isExported := false, isAll := true, not_isExported_and_isAll := ⋯, isMeta := true } = needs.metaPrivOfPriv

@[inline]

def ImportGraph.Shake.Needs.has (needs : Needs) (k : NeedsKind) (i : Nat) : Bool

Equations

• needs.has k i = (needs.get k).has i

@[inline]

def ImportGraph.Shake.Needs.hasPhaseless (needs : Needs) (v : VisibilityKind) (i : Nat) : Bool

Whether needs has the given VisibilityKind at either phase.

Equations

• needs.hasPhaseless v i = ((needs.get { toVisibilityKind := v, isMeta := false }).has i || (needs.get { toVisibilityKind := v, isMeta := true }).has i)

@[inline]

def ImportGraph.Shake.Needs.set (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs

Equations

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

def ImportGraph.Shake.Needs.modify (needs : Needs) (k : NeedsKind) (f : Bitset → Bitset) : Needs

Equations

• needs.modify k f = needs.set k (f (needs.get k))

def ImportGraph.Shake.Needs.union (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs

Equations

• needs.union k s = needs.modify k fun (x : ImportGraph.Shake.Bitset) => x ∪ s

def ImportGraph.Shake.Needs.sub (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs

Equations

• needs.sub k s = needs.modify k fun (s' : ImportGraph.Shake.Bitset) => s' ^^^ s' ∩ s

@[instance_reducible]

instance ImportGraph.Shake.instUnionNeeds : Union Needs

Equations

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