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

Equations

• ImportGraph.Shake.«term_≫_» = Lean.ParserDescr.trailingNode `ImportGraph.Shake.«term_≫_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 81))

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

Equations

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

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.

Equations

• ImportGraph.Shake.ArrayHierarchy = Array ImportGraph.Shake.Provides

@[instance_reducible, inline]

instance ImportGraph.Shake.instHierarchyArrayHierarchy : Hierarchy ArrayHierarchy

Equations

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

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

Equations

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

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

Equations

• ImportGraph.Shake.HierarchyT H = StateT H

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.

Equations

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

@[inline]

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

Equations

• impTransDeps.andThen kImp = impTransDeps.addAndThen kImp

@[instance_reducible]

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

Equations

• ImportGraph.Shake.instHPostcompNeedsNeedsKind = { hpostcomp := fun (n : ImportGraph.Shake.Needs) (k : ImportGraph.Shake.NeedsKind) => n.andThen k }

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

Equations

• ImportGraph.Shake.Lean.Import.addAndThen impTransDeps imp base = Id.run (impTransDeps.addAndThen (ImportGraph.Shake.NeedsKind.ofImport imp) 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.

Equations

• ImportGraph.Shake.Lean.Import.andThen impTransDeps imp = ImportGraph.Shake.Lean.Import.addAndThen impTransDeps imp ImportGraph.Shake.Needs.empty

@[instance_reducible]

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

Equations

• ImportGraph.Shake.instHPostcompNeedsImport = { hpostcomp := fun (n : ImportGraph.Shake.Needs) (imp : Lean.Import) => ImportGraph.Shake.Lean.Import.andThen n imp }

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

Equations

• ImportGraph.Shake.NeedsKind.transitiveClosureSingle i k transDeps = ImportGraph.Shake.HPostcomp.hpostcomp transDeps[i]! k

@[instance_reducible]

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

Equations

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

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

Equations

• ImportGraph.Shake.Lean.Import.transitiveClosureSingle i imp transDeps = ImportGraph.Shake.HPostcomp.hpostcomp transDeps[i]! imp

@[instance_reducible, inline]

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

Equations

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

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.

Equations

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

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

Equations

• ImportGraph.Shake.Hierarchy.andThen transDeps n = ImportGraph.Shake.Hierarchy.addAndThen transDeps n

@[instance_reducible]

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

Equations

• ImportGraph.Shake.instHPostcompNeedsOfHierarchy = { hpostcomp := fun (transDeps : H) (n : ImportGraph.Shake.Needs) => ImportGraph.Shake.Hierarchy.andThen transDeps n }

@[inline]

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

Equations

• base.addTransitiveClosure n transDeps = ImportGraph.Shake.Hierarchy.addAndThen transDeps n (base ∪ n)

@[inline]

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

n ∪ (transDeps ≫ n)

Equations

• n.transitiveClosure transDeps = ImportGraph.Shake.Hierarchy.addAndThen transDeps n n

@[instance_reducible]

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

Equations

• ImportGraph.Shake.instHTransClosureNeedsOfHierarchy = { htransClosure := fun (transDeps : H) (n : ImportGraph.Shake.Needs) => n.transitiveClosure transDeps }

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

Equations

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

@[inline]

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

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

Equations

• a.isLinear = (decide (a.pub ∪ a.privOfPriv ⊆ a.priv) && decide (a.metaPub ∪ a.metaPrivOfPriv ⊆ a.metaPriv))

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

Equations

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

@[inline]

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

Equations

• a.isAntilinear = ((a.pub ∪ a.privOfPriv) ∩ a.priv == ∅ && (a.metaPub ∪ a.metaPrivOfPriv) ∩ a.metaPriv == ∅)

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

Equations

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

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

Equations

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

@[inline]

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

Clears all dependencies at the given index.

Equations

• ImportGraph.Shake.Needs.clearAt i a = a.map fun (x : ImportGraph.Shake.Bitset) => x \ {i}

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

Equations

• needs.providedToBy i transDeps = needs.directLe transDeps[i]!

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

Equations

• n₁.subsumedBy n₂ transDeps = n₁.directLe (ImportGraph.Shake.HTransClosure.htransClosure transDeps n₂.linearize)

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.

Equations

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

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

Equations

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

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

Equations

• ImportGraph.Shake.Std.HashMap.incorporateBelowAt? map k a lt = map.alter k fun (arr? : Option (Array (Option α))) => some (ImportGraph.Shake.Array.incorporateBelow? (arr?.getD #[]) a lt)

@[inline]

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

The minimal elements of xs, according to lt.

Equations

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

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

Equations

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

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

Equations

• ImportGraph.Shake.Array.minimalsPer xs key lt = ImportGraph.Shake.Array.minimalValuesPer xs key id lt