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

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

@[instance_reducible]

instance ImportGraph.Shake.instDecidableEqBitset : DecidableEq Bitset

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

@[instance_reducible]

instance ImportGraph.Shake.instReprBitset : Repr Bitset

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instEmptyCollection : EmptyCollection Bitset

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instInter : Inter Bitset

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instUnion : Union Bitset

@[instance_reducible]

instance ImportGraph.Shake.Bitset.instXorOp : XorOp Bitset

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

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.NeedsKind : 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

  Represents 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.

• isMeta : Bool

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

• isAll : Bool

  Represents (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.instInhabitedNeedsKind : Inhabited NeedsKind

@[instance_reducible]

instance ImportGraph.Shake.instBEqNeedsKind : BEq NeedsKind

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

@[instance_reducible]

instance ImportGraph.Shake.instReprNeedsKind : Repr NeedsKind

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

@[instance_reducible]

instance ImportGraph.Shake.instHashableNeedsKind : Hashable NeedsKind

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

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

@[instance_reducible]

instance ImportGraph.Shake.instOrdNeedsKind : Ord NeedsKind

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.priv : NeedsKind

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.pub : NeedsKind

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.metaPriv : NeedsKind

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.metaPub : NeedsKind

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.privOfPriv : NeedsKind

@[reducible, match_pattern, inline]

abbrev ImportGraph.Shake.NeedsKind.metaPrivOfPriv : NeedsKind

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

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

def ImportGraph.Shake.NeedsKind.all : Array NeedsKind

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

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

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

An import effecting a NeedsKind.

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

@[instance_reducible]

instance ImportGraph.Shake.instReprNeeds : Repr Needs

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

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

def ImportGraph.Shake.Needs.empty : Needs

@[instance_reducible]

instance ImportGraph.Shake.instEmptyCollectionNeeds : EmptyCollection Needs

@[inline]

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

@[inline]

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

@[inline]

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

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

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

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

@[instance_reducible]

instance ImportGraph.Shake.instUnionNeeds : Union Needs