Algebra of an import hierarchy

This file provides algebraic/compositional relationships between module system dependencies in an import hierarchy.

Notably, we provide transitive closure operators relative to an import hierarchy, which relies on the nontrivial composition of module system imports.

Future work

• Document this more thoroughly.
• Consider making the Hierarchy API more featureful.

class ImportGraph.Shake.HPostcomp (α : Sort u_1) (β : Sort u_2) (γ : outParam (Type u)) : Sort (max (max (u + 1) u_1) u_2)

• hpostcomp : α → β → γ

def ImportGraph.Shake.«term_≫_» : Lean.TrailingParserDescr

class ImportGraph.Shake.HTransClosure (α : Sort u_1) (β : Sort u_2) (γ : outParam (Type u)) : Sort (max (max (u + 1) u_1) u_2)

• htransClosure : α → β → γ

def ImportGraph.Shake.«term_⟦_⟧» : Lean.TrailingParserDescr

𝓘⟦n⟧ is the transitive closure of n with respect to the hierarchy 𝓘.

class ImportGraph.Shake.Hierarchy (α : Sort u_1) : Sort (max 1 u_1)

An import hierarchy, with a size and dependencies (Provides) for each index.

• size : α → Nat
• getDeps (a : α) (i : Nat) : i < size a → Provides
• getDeps? : α → Nat → Option Provides
• getDeps! : α → Nat → Provides

@[reducible, inline]

abbrev ImportGraph.Shake.ArrayHierarchy : Type

An Array Provides.

@[instance_reducible, inline]

instance ImportGraph.Shake.instHierarchyArrayHierarchy : Hierarchy ArrayHierarchy

@[instance_reducible]

instance ImportGraph.Shake.instGetElem?NatProvidesLtSize {H : Type u_1} [Hierarchy H] : GetElem? H Nat Provides fun (a : H) (i : Nat) => i < Hierarchy.size a

@[reducible, inline]

abbrev ImportGraph.Shake.HierarchyT (H : Type u_1) [Hierarchy H] (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

Equips a monad with a Hierarchy state.

def ImportGraph.Shake.Needs.addAndThen (impTransDeps : Needs) (kImp : NeedsKind) (base : Needs := ∅) : Needs

Given an abstract NeedsKind [kImp⟩ and a collection of prearrows j [k⟩ · (Provides), add to base the composed prearrows j [k⟩[imp⟩ · where composition is possible. Does not account for public ⊆ private on the codomain side (see linearize).

Note that this does not add the original collection of prearrows to base.

@[inline]

def ImportGraph.Shake.Needs.andThen (impTransDeps : Needs) (kImp : NeedsKind) : Needs

@[instance_reducible]

def ImportGraph.Shake.instHPostcompNeedsNeedsKind : Shake.HPostcomp Needs NeedsKind Needs

@[inline]

def ImportGraph.Shake.Lean.Import.addAndThen (impTransDeps : Needs) (imp : Lean.Import) (base : Needs := ∅) : Needs

Given an abstract Import [kImp⟩ and a collection of prearrows j [k⟩ · (Provides), add to base the composed prearrows j [k⟩[imp⟩ · where composition is possible.

Note that this does not add the original collection of prearrows to base.

@[inline]

def ImportGraph.Shake.Lean.Import.andThen (impTransDeps : Needs) (imp : Lean.Import) : Needs

Given an abstract import [k⟩ and a collection of prearrows j [k⟩ · (Needs), forms the composed prearrows j [k'⟩[k⟩ · where composition is possible.

@[instance_reducible]

def ImportGraph.Shake.instHPostcompNeedsImport : Shake.HPostcomp Needs Lean.Import Needs

@[inline]

def ImportGraph.Shake.NeedsKind.transitiveClosureSingle {H : Type u_1} [Hierarchy H] (i : Nat) (k : NeedsKind) (transDeps : H) : Needs

Given an import hierarchy of arrows j' [_⟩ j and a preimport i [imp⟩ ·, forms the set of prearrows obtained by transitively closing i [imp⟩ · with respect to the import hierarchy. This is i [imp⟩ · together with compositions j [_⟩ i [imp⟩ ·. transDeps is assumed to be reflexified.

@[instance_reducible]

def ImportGraph.Shake.instHTransClosureProdNatNeedsKindNeedsOfHierarchy {H : Type u_1} [Hierarchy H] : Shake.HTransClosure H (Nat × NeedsKind) Needs

@[inline]

def ImportGraph.Shake.Lean.Import.transitiveClosureSingle {H : Type u_1} [Hierarchy H] (i : Nat) (imp : Lean.Import) (transDeps : H) : Needs

Given an import hierarchy of arrows j' [_⟩ j and a preimport i [imp⟩ ·, forms the set of prearrows obtained by transitively closing i [imp⟩ · with respect to the import hierarchy. This is i [imp⟩ · together with compositions j [_⟩ i [imp⟩ ·. transDeps is assumed to be reflexified.

@[instance_reducible, inline]

def ImportGraph.Shake.instHTransClosureProdNatImportNeedsOfHierarchy {H : Type u_1} [Hierarchy H] : Shake.HTransClosure H (Nat × Lean.Import) Needs

def ImportGraph.Shake.Hierarchy.addAndThen {H : Type u_1} [Hierarchy H] (transDeps : H) (n : Needs) (base : Needs := Needs.empty) : Needs

Given a set of prearrows i [k⟩ · and an import hierarchy, includes in base the compositions of arrows j [k'⟩ i [k⟩ · where composition is possible. Assumes every index is valid.

@[inline]

def ImportGraph.Shake.Hierarchy.andThen {H : Type u_1} [Hierarchy H] (transDeps : H) (n : Needs) : Needs

Given a set of prearrows i [k⟩ · and an import hierarchy, forms the compositions of arrows j [k'⟩ i [k⟩ · where composition is possible.

@[instance_reducible]

def ImportGraph.Shake.instHPostcompNeedsOfHierarchy {H : Type u_1} [Hierarchy H] : Shake.HPostcomp H Needs Needs

@[inline]

def ImportGraph.Shake.Needs.addTransitiveClosure {H : Type u_1} [Hierarchy H] (base n : Needs) (transDeps : H) : Needs

@[inline]

def ImportGraph.Shake.Needs.transitiveClosure {H : Type u_1} [Hierarchy H] (n : Needs) (transDeps : H) : Needs

n ∪ (transDeps ≫ n)

@[instance_reducible]

def ImportGraph.Shake.instHTransClosureNeedsOfHierarchy {H : Type u_1} [Hierarchy H] : Shake.HTransClosure H Needs Needs

@[inline]

def ImportGraph.Shake.Needs.linearize (a : Needs) : Needs

Includes the public visibilities in the corresponding private visibilities, to represent a "provides" relationship. A k : Needs is "linear" iff it accounts for public ⊆ private (and likewise for both being meta). Accounting for this on the target side means that k.pub ⊆ k.priv (public imports are available privately) and accounting for it on the source side means that k.privOfPriv ⊆ k.priv (importing the private scope privately implies importing the public scope privately).

@[inline]

def ImportGraph.Shake.Needs.isLinear (a : Needs) : Bool

Whether public ⊆ private for the given Needs, on both the meta and non-meta levels.

@[inline]

def ImportGraph.Shake.Needs.antilinearize (a : Needs) : Needs

Removes private needs which can be inferred by accounting for public ⊆ private on both the source and target side. See Needs.linearize for details.

@[inline]

def ImportGraph.Shake.Needs.isAntilinear (a : Needs) : Bool

@[inline]

def ImportGraph.Shake.Needs.reflOf (i : Nat) : Provides

A Provides providing to a module the aspects of that module which it provides to itself. Note that a module does not provide its own non-meta scopes as meta dependencies to itself. Linearized.

@[inline]

def ImportGraph.Shake.Needs.reflexify (i : Nat) (a : Needs) : Needs

Adds in the reflexive availabilities of a given module, which are just the public and private availabilities and not the meta lifted versions. This matches what is available within a given module. Equivalent to a ∪ .reflOf i.

Note that this operation does not necessarily commute with transitive closure.

@[inline]

def ImportGraph.Shake.Needs.clearAt (i : Nat) (a : Needs) : Needs

Clears all dependencies at the given index.

@[inline]

def ImportGraph.Shake.Needs.providedToBy {H : Type u_1} [Hierarchy H] (needs : Needs) (i : Nat) (transDeps : H) : Bool

Checks if the Provides hierarchy transDeps provides arrows j [k⟩ i for all (j [k⟩ ·) ∈ needs. Assumes transDeps is well-formed as a Provides hierarchy (i.e. linearized and reflexified).

@[inline]

def ImportGraph.Shake.Needs.subsumedBy {H : Type u_1} [Hierarchy H] (n₁ n₂ : Needs) (transDeps : H) : Bool

Checks if the prearrows j [k⟩ · in n₁ are included in the arrows provided by the transitive closure of n₂ with respect to the import hierarchy. Linearizes n₂ first, which ensures n₁ is not penalized for itself being linearized and respecting public ⊆ private. Assumes transDeps is a well-formed Provides hierarchy, i.e. linearized and reflexified.

def ImportGraph.Shake.Needs.reduce {H : Type u_1} [Hierarchy H] (a : Needs) (transDeps : H) : Needs

Returns an antilinearized reduced : Needs such that

a ≤ transDeps⟦reduced.linearize⟧

and reduced is minimal (perhaps non-uniquely) among such Needs.

The returned reduced is antilinearized, and thus suitable for converting to imports.

Does not assume a is linearized.

@[inline]

def ImportGraph.Shake.Array.incorporateBelow? {α : Type} (as : Array (Option α)) (a : α) (lt : α → α → Bool) : Array (Option α)

Attempts to insert a among the set as of minimal elements as a new minimal element according to lt. Clears elements of as that are above a, and ignores a if we already have an element lower than a.

@[inline]

def ImportGraph.Shake.Std.HashMap.incorporateBelowAt? {α : Type} {κ : Type u_1} [BEq κ] [Hashable κ] (map : Std.HashMap κ (Array (Option α))) (k : κ) (a : α) (lt : α → α → Bool) : Std.HashMap κ (Array (Option α))

At k, attempts to insert a among the set as of minimal elements as a new minimal element according to lt. Clears elements of as that are above a, and ignores a if we already have an element lower than a.

@[inline]

def ImportGraph.Shake.Array.minimals {α : Type} (xs : Array α) (lt : α → α → Bool) : Array α

The minimal elements of xs, according to lt.

@[inline]

def ImportGraph.Shake.Array.minimalValuesPer {α : Type u_1} {β : Type} {κ : Type u_2} [BEq κ] [Hashable κ] (xs : Array α) (key : α → κ) (val : α → β) (lt : β → β → Bool) : Std.HashMap κ (Array β)

The minimal values of xs under val according to lt, organized and compared per key value. See minimalsPer for a version without val; val is essentially an optimization.

@[inline]

def ImportGraph.Shake.Array.minimalsPer {α : Type} {κ : Type u_1} [BEq κ] [Hashable κ] (xs : Array α) (key : α → κ) (lt : α → α → Bool) : Std.HashMap κ (Array α)

The minimal elements of xs according to lt, organized and compared per key value.