Declaration needs

This file records the needs of declarations in a "non-baked-in" manner via DeclNeeds. We record in what manner one declaration needs another (e.g. in its type), and then postpone the calculation of what import needs this implies. This sets us up to provide finer explanations.

We also define ImportNeeds so that we can express when an import is allowed to be meta (or not).

Note that, crucially, DeclNeeds is agnostic to the source of our import hierarchy, as it uses module names instead of e.g. ModuleIdxs/ModIdxs. Hence these functions are compatible with both a WorkspaceModel approach and an Environment approach.

This file culminates in withElabCommandCapturingNeeds, which elaborates a command and captures the (transitive) DeclNeeds of declarations produced in that command, including e.g. the needs implied by the command's syntax.

Future Work

• Write up more thorough documentation when this settles down.
• Handle meta IR.
• Performance: many of the data structures here could be improved. There's a lot of pointer-chasing.
• Revamp indirect mod uses. Currently they are associated with the declaration indirectly requiring them and added to the decl import needs specially. Instead, we should split them out. Also, we currently spoof the kind.
• Split out extra mod uses into a special command needs. Also put the syntax needs there; these should not be decl needs.
• Handle autogenerated declarations more consistently.
• Give a closer look to things like @[csimp].

Shake declarations

This section (fromShake) is inlined verbatim from shake, modulo whitespace.

Copyright (c) 2023 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Sebastian Ullrich

def ImportGraph.Shake.isDeclMeta' (env : Lean.Environment) (declName : Lean.Name) : Bool

Equations

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

def ImportGraph.Shake.Lean.Environment.getDepConstName? (ref : Lean.Name) (env : Lean.Environment) : Option Lean.Name

Given an Expr reference, returns the declaration name that should be considered the reference, if any, but from the environment directly.

Equations

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

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

A way in which a declaration might demand an imported module. Note that there may be multiple demands on the same module from the same declaration, which thus may require multiple of these.

The fields overlap with NeedsKind, except for meta?, as import needs may not specify a phase.

• isExported : Bool
• isAll : Bool
• not_isExported_and_isAll : ¬(self.isExported = true ∧ self.isAll = true)
• meta? : Option Bool

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.pubRuntime : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.pubRuntime = { toVisibilityKind := ImportGraph.Shake.NeedsKind.pub.toVisibilityKind, meta? := some false }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privRuntime : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.privRuntime = { toVisibilityKind := ImportGraph.Shake.NeedsKind.priv.toVisibilityKind, meta? := some false }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privOfPrivRuntime : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.privOfPrivRuntime = { toVisibilityKind := ImportGraph.Shake.NeedsKind.privOfPriv.toVisibilityKind, meta? := some false }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.metaPub : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.metaPub = { toVisibilityKind := ImportGraph.Shake.NeedsKind.metaPub.toVisibilityKind, meta? := some true }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.metaPriv : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.metaPriv = { toVisibilityKind := ImportGraph.Shake.NeedsKind.metaPriv.toVisibilityKind, meta? := some true }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.metaPrivOfPriv : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.metaPrivOfPriv = { toVisibilityKind := ImportGraph.Shake.NeedsKind.metaPrivOfPriv.toVisibilityKind, meta? := some true }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.pubPhaseless : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.pubPhaseless = { toVisibilityKind := ImportGraph.Shake.NeedsKind.pub.toVisibilityKind, meta? := none }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privPhaseless : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.privPhaseless = { toVisibilityKind := ImportGraph.Shake.NeedsKind.priv.toVisibilityKind, meta? := none }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privOfPrivPhaseless : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.privOfPrivPhaseless = { toVisibilityKind := ImportGraph.Shake.NeedsKind.privOfPriv.toVisibilityKind, meta? := none }

@[inline]

def ImportGraph.Shake.ImportNeedsKind.all : Array ImportNeedsKind

Every possible ImportNeedsKind.

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.ImportNeedsKind.instToString : ToString ImportNeedsKind

Equations

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

@[inline]

def ImportGraph.Shake.NeedsKind.toPhasedImportNeedsKind (k : NeedsKind) : ImportNeedsKind

Turns a k : NeedsKind into a phased ImportNeeds, interpreting the isMeta flag as specifying a runtime need when false and a meta need when true. Note that while this makes sense under certain interpretations of a NeedsKind, it should be used with care, as shake's ExtraModUses may record isMeta := false even when the import needed may optionally be meta.

Equations

• k.toPhasedImportNeedsKind = { toVisibilityKind := k.toVisibilityKind, meta? := some k.isMeta }

@[inline]

def ImportGraph.Shake.VisibilityKind.toPhaselessImportNeedsKind (v : VisibilityKind) : ImportNeedsKind

Turns a visibility kind into the corresponding ImportNeedsKind that accepts either phase.

Equations

• v.toPhaselessImportNeedsKind = { toVisibilityKind := v, meta? := none }

structure ImportGraph.Shake.ImportNeeds : Type

Like Needs, but splits apart by phase in order to express an actual import requirement (which may or may not need a certain phase) instead of expressing an import specification per se:

• <vis>Runtime: needs a non-meta import
• meta<vis>: needs a meta import
• <vis>Phaseless: either a non-meta or meta import will do

• pubRuntime : Bitset

  The modules whose public scopes are needed publicly at specifically the non-meta phase.

• privRuntime : Bitset

  The modules whose public scopes are needed privately at specifically the non-meta phase.

• privOfPrivRuntime : Bitset

  The modules whose private scopes are needed at specifically the non-meta phase.

• metaPub : Bitset

  The modules whose public scopes are needed publicly at the meta phase.

• metaPriv : Bitset

  The modules whose public scopes are needed privately at the meta phase.

• metaPrivOfPriv : Bitset

  The modules whose private scopes are needed at the meta phase.

• pubPhaseless : Bitset

  The modules whose public scopes are needed publicly at either the meta or non-meta phase.

• privPhaseless : Bitset

  The modules whose public scopes are needed privately at either the meta or non-meta phase.

• privOfPrivPhaseless : Bitset

  The modules whose private scopes are needed at either the meta or non-meta phase.

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedImportNeeds : Inhabited ImportNeeds

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instBEqImportNeeds : BEq ImportNeeds

Equations

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

def ImportGraph.Shake.instBEqImportNeeds.beq : ImportNeeds → ImportNeeds → Bool

Equations

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

def ImportGraph.Shake.instReprImportNeeds.repr : ImportNeeds → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprImportNeeds : Repr ImportNeeds

Equations

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

def ImportGraph.Shake.ImportNeeds.empty : ImportNeeds

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.ImportNeeds.instEmptyCollection : EmptyCollection ImportNeeds

Equations

• ImportGraph.Shake.ImportNeeds.instEmptyCollection = { emptyCollection := ImportGraph.Shake.ImportNeeds.empty }

def ImportGraph.Shake.ImportNeeds.linearizePhased (needs : ImportNeeds) : ImportNeeds

Takes into account public ⊆ private for unambiguous phase specifications.

Equations

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

def ImportGraph.Shake.ImportNeeds.antilinearizePhased (needs : ImportNeeds) : ImportNeeds

Removes private when implied by public or all for unambiguous phase specifications.

Equations

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

def ImportGraph.Shake.ImportNeeds.narrowPhase (needs : ImportNeeds) : ImportNeeds

Ensures that we only keep phaseless entries when no other phase is specified for that index. Does not take into account phase specifications due to linearization. Depending on the application, consider linearizing the phased needs first.

Equations

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

def ImportGraph.Shake.ImportNeeds.toPhasedNeeds (needs : ImportNeeds) : Needs

The phased needs of an ImportNeeds. Completely ignores the phaseless needs.

Equations

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

@[inline]

def ImportGraph.Shake.ImportNeeds.isProvidedBy (n : ImportNeeds) (p : Provides) : Bool

Assumes that Provides is well-formed, i.e. is linearized and transitively closed.

Equations

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

@[inline]

def ImportGraph.Shake.ImportNeeds.get (needs : ImportNeeds) (k : ImportNeedsKind) : Bitset

Equations

• needs.get { isExported := true, not_isExported_and_isAll := ⋯, meta? := some false } = needs.pubRuntime
• needs.get { isExported := false, not_isExported_and_isAll := ⋯, meta? := some false } = needs.privRuntime
• needs.get { isExported := false, isAll := true, not_isExported_and_isAll := ⋯, meta? := some false } = needs.privOfPrivRuntime
• needs.get { isExported := true, not_isExported_and_isAll := ⋯, meta? := some true } = needs.metaPub
• needs.get { isExported := false, not_isExported_and_isAll := ⋯, meta? := some true } = needs.metaPriv
• needs.get { isExported := false, isAll := true, not_isExported_and_isAll := ⋯, meta? := some true } = needs.metaPrivOfPriv
• needs.get { isExported := true, not_isExported_and_isAll := ⋯, meta? := none } = needs.pubPhaseless
• needs.get { isExported := false, not_isExported_and_isAll := ⋯, meta? := none } = needs.privPhaseless
• needs.get { isExported := false, isAll := true, not_isExported_and_isAll := ⋯, meta? := none } = needs.privOfPrivPhaseless

@[inline]

def ImportGraph.Shake.ImportNeeds.has (needs : ImportNeeds) (k : ImportNeedsKind) (i : Lean.ModuleIdx) : Bool

Equations

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

@[inline]

def ImportGraph.Shake.ImportNeeds.set (needs : ImportNeeds) (k : ImportNeedsKind) (s : Bitset) : ImportNeeds

Equations

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

@[specialize #[]]

def ImportGraph.Shake.ImportNeeds.modify (needs : ImportNeeds) (k : ImportNeedsKind) (f : Bitset → Bitset) : ImportNeeds

Equations

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

def ImportGraph.Shake.ImportNeeds.union (needs : ImportNeeds) (k : ImportNeedsKind) (s : Bitset) : ImportNeeds

Equations

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

@[inline]

def ImportGraph.Shake.ImportNeeds.any (needs : ImportNeeds) (f : Bitset → Bool) : Bool

Equations

• needs.any f = ImportGraph.Shake.ImportNeedsKind.all.any fun (x : ImportGraph.Shake.ImportNeedsKind) => f (needs.get x)

@[inline]

def ImportGraph.Shake.ImportNeeds.all (needs : ImportNeeds) (f : Bitset → Bool) : Bool

Equations

• needs.all f = ImportGraph.Shake.ImportNeedsKind.all.all fun (x : ImportGraph.Shake.ImportNeedsKind) => f (needs.get x)

def ImportGraph.Shake.ImportNeeds.flatten (needs : ImportNeeds) : Bitset

Equations

• needs.flatten = Array.foldl (fun (x1 : ImportGraph.Shake.Bitset) (x2 : ImportGraph.Shake.ImportNeedsKind) => x1 ∪ needs.get x2) ∅ ImportGraph.Shake.ImportNeedsKind.all

@[specialize #[]]

def ImportGraph.Shake.ImportNeeds.reduceBy {H : Type u_1} [Hierarchy H] (needs : ImportNeeds) (transDeps : H) (metaBy : Nat → VisibilityKind → Needs → Bool) : Needs

Returns an antilinearized reduced : Needs such that

needs.isProvidedBy transDeps⟦reduced.linearize⟧

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

metaBy modIdx v reducedSoFar : Bool specifies how to turn phaseless needs into phased needs. This may be useful if we want to try preserving some phases from existing externally-provided imports, for instance.

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

Does not assume needs is linearized or narrowed.

Equations

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

def ImportGraph.Shake.ImportNeeds.reduceSimple {H : Type u_1} [Hierarchy H] (needs : ImportNeeds) (transDeps : H) (useMeta : Bool := false) : Needs

Returns an antilinearized reduced : Needs such that

needs.isProvidedBy transDeps⟦reduced.linearize⟧

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

If useMeta is false, then any phaseless needs not covered by phased needs are interpreted as run time needs, and otherwise as meta needs.

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

Does not assume needs is linearized or narrowed.

Equations

• needs.reduceSimple transDeps useMeta = needs.reduceBy transDeps fun (x : Nat) (x_1 : ImportGraph.Shake.VisibilityKind) (x_2 : ImportGraph.Shake.Needs) => useMeta

def ImportGraph.Shake.ImportNeeds.brailleCellAt (i : Nat) (n : ImportNeeds) : Char × Char

A pair of braille cells depicting the import needs at index i.

In the left cell, the left column denotes definite non-meta needs (due to runtime IR). The right column denotes meta or non-meta needs.

The left column of the right cell denotes definitely meta needs. The right column of the right cell is unused.

The top row denotes public needs, the middle row private needs, and the bottom row private-of-private needs.

We call this brailleCellAt instead of brailleCellsAt so that dot notation does not accidentally resolve to Needs.brailleCellAt.

Equations

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

@[inline]

def ImportGraph.Shake.ImportNeeds.toStringAt (i : Nat) (n : ImportNeeds) : String

A pair of braille cells depicting the import needs at index i.

In the left cell, the left column denotes definite non-meta needs (due to runtime IR). The right column denotes meta or non-meta needs.

The left column of the right cell denotes definitely meta needs. The right column of the right cell is unused.

The top row denotes public needs, the middle row private needs, and the bottom row private-of-private needs.

For the braille cell characters without brackets, see ImportNeeds.brailleCellAt.

Equations

• ImportGraph.Shake.ImportNeeds.toStringAt i n = match ImportGraph.Shake.ImportNeeds.brailleCellAt i n with | (l, r) => toString "[" ++ toString l ++ toString r ++ toString "]"

def ImportGraph.Shake.ImportNeeds.toString (n : ImportNeeds) (univSize? : Option Nat := none) (dividers : Bool := true) : String

Represents an ImportNeeds as a string of the form e.g. │⠇⠁│⠑⠁│⠁│⠝⠁│, where each braille cell represents the set of ImportNeedsKinds expressed by a single "column" of the ImportNeeds (i.e. at a given index). The left column of the left cell is non-meta-only needs; the next column is meta-or-non-meta needs; the next column is meta-only needs; and the final column is unused. 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 ImportNeeds. 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.

Equations

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

@[instance_reducible]

def ImportGraph.Shake.instOrdName_importGraph : Ord Lean.Name

Equations

• ImportGraph.Shake.instOrdName_importGraph = { compare := Lean.Name.quickCmp }

inductive ImportGraph.Shake.ComptimeDependency : Type

Information about the source of a compile-time dependency.

• indirect (use : Lean.IndirectModUse) (imposingModules : Array Lean.Name) : ComptimeDependency

  A potential compile-time dependency due to an indirect mod use. imposingModule records the module that imposed the indirect mod use (not the source module of the declaration).

• stx (kind : Lean.SyntaxNodeKind) (pos? : Option Lean.Syntax.Range) : ComptimeDependency

  A compile-time dependency due to parsing.

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedComptimeDependency : Inhabited ComptimeDependency

Equations

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

def ImportGraph.Shake.instBEqComptimeDependency.beq : ComptimeDependency → ComptimeDependency → Bool

Equations

• ImportGraph.Shake.instBEqComptimeDependency.beq (ImportGraph.Shake.ComptimeDependency.indirect a a_1) (ImportGraph.Shake.ComptimeDependency.indirect b b_1) = (a == b && a_1 == b_1)
• ImportGraph.Shake.instBEqComptimeDependency.beq (ImportGraph.Shake.ComptimeDependency.stx a a_1) (ImportGraph.Shake.ComptimeDependency.stx b b_1) = (a == b && a_1 == b_1)
• ImportGraph.Shake.instBEqComptimeDependency.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.Shake.instBEqComptimeDependency : BEq ComptimeDependency

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprComptimeDependency : Repr ComptimeDependency

Equations

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

def ImportGraph.Shake.instReprComptimeDependency.repr : ComptimeDependency → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instHashableComptimeDependency : Hashable ComptimeDependency

Equations

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

def ImportGraph.Shake.instHashableComptimeDependency.hash : ComptimeDependency → UInt64

Equations

• ImportGraph.Shake.instHashableComptimeDependency.hash (ImportGraph.Shake.ComptimeDependency.indirect a a_1) = mixHash (mixHash 0 (hash a)) (hash a_1)
• ImportGraph.Shake.instHashableComptimeDependency.hash (ImportGraph.Shake.ComptimeDependency.stx a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)

def ImportGraph.Shake.instOrdComptimeDependency.ord : ComptimeDependency → ComptimeDependency → Ordering

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Shake.instOrdComptimeDependency.ord (ImportGraph.Shake.ComptimeDependency.indirect a a_1) x✝ = Ordering.lt
• ImportGraph.Shake.instOrdComptimeDependency.ord x✝ (ImportGraph.Shake.ComptimeDependency.indirect a a_1) = Ordering.gt

@[instance_reducible]

instance ImportGraph.Shake.instOrdComptimeDependency : Ord ComptimeDependency

Equations

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

def ImportGraph.Shake.ComptimeDependency.toMessageData : ComptimeDependency → Lean.MessageData

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instToMessageDataComptimeDependency : Lean.ToMessageData ComptimeDependency

Equations

• ImportGraph.Shake.instToMessageDataComptimeDependency = { toMessageData := fun (x : ImportGraph.Shake.ComptimeDependency) => x.toMessageData }

inductive ImportGraph.Shake.ConstLocation : Type

A location at which a ConstantInfo can reference another.

• type : ConstLocation
• value : ConstLocation

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedConstLocation : Inhabited ConstLocation

Equations

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

def ImportGraph.Shake.instBEqConstLocation.beq : ConstLocation → ConstLocation → Bool

Equations

• ImportGraph.Shake.instBEqConstLocation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance ImportGraph.Shake.instBEqConstLocation : BEq ConstLocation

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprConstLocation : Repr ConstLocation

Equations

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

def ImportGraph.Shake.instReprConstLocation.repr : ConstLocation → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instHashableConstLocation : Hashable ConstLocation

Equations

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

def ImportGraph.Shake.instHashableConstLocation.hash : ConstLocation → UInt64

Equations

• ImportGraph.Shake.instHashableConstLocation.hash ImportGraph.Shake.ConstLocation.type = 0
• ImportGraph.Shake.instHashableConstLocation.hash ImportGraph.Shake.ConstLocation.value = 1

def ImportGraph.Shake.instOrdConstLocation.ord : ConstLocation → ConstLocation → Ordering

Equations

• ImportGraph.Shake.instOrdConstLocation.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

@[instance_reducible]

instance ImportGraph.Shake.instOrdConstLocation : Ord ConstLocation

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instToStringConstLocation : ToString ConstLocation

Equations

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

inductive ImportGraph.Shake.DeclDeclNeedsKind : Type

A way in which a declaration tgt might need another declaration src. In general, the same src and tgt may be related by multiple DeclDeclNeedsKinds.

• expr (downstream : ConstLocation) (isReExported : Option Bool := none) (upstream : ConstLocation := ConstLocation.type) : DeclDeclNeedsKind

  Expresses a dependency of tgt's location given by downstream on src's location given by upstream. isReExported := none indicates that the exported value is inherited from tgt's isPublic or isExposed stance, as appropriate. (Occasionally this will be some false if, for example, a proof is abstracted, since we count the dependencies of autogenerated declarations as part of the parent declaration.)

• metaIR (isReExported : Option Bool := none) (through : List Lean.Name := []) : DeclDeclNeedsKind

  Expresses a dependency of tgt on src due to the IR of tgt, which is meta-available. When isReExported := none, this is inherited from the tgt's isPublic stance (the same as its type, not its value.)

  Meta IR is unusual in that while a private meta def may not re-export its references, a public meta def that uses that private meta def will re-export that private meta def's references. Note, also, that this dependency is determined by Lean from the initial LCNF (unless a same-module transitive dependency, in which case it is determined from that declaration's base LCNF), but is intended to capture IR dependency.

• runtimeIR : DeclDeclNeedsKind

  Expresses a dependency of tgt on src in the IR of tgt, which is only available at runtime. This does not have the complicated reference semantics of IR used for meta declarations. We assume, for now, that we do not need to think about changing runtime defs to meta defs, and thus do not need to record the same information. As such, checkMetas recursive check for non-aux decls is irrelevant, as the runtime IR constraints such a recursive check puts on a reference are redundant with the runtime IR constraints that already exist on that reference. However, note that, like meta declarations, this dependency is determined by Lean from the initial LCNF, though is intended to capture IR dependency.

• comptime (source : ComptimeDependency) : DeclDeclNeedsKind

  A compile-time dependency of tgt (e.g. a parser used for notation in the command for tgt).

  If this arises due to an indirect mod use, we record the declaration that demanded it (if we can). Note that shake extensions do not expose this; this is known during the expression traversal. So some indirect mod uses will end up in extraModUses without any indication as to the declaration that drew them (at least, not in a way that's accessible to us, though this information is traced by shake).

  We record this separately mainly for reporting.

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedDeclDeclNeedsKind : Inhabited DeclDeclNeedsKind

Equations

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

def ImportGraph.Shake.instBEqDeclDeclNeedsKind.beq : DeclDeclNeedsKind → DeclDeclNeedsKind → Bool

Equations

• ImportGraph.Shake.instBEqDeclDeclNeedsKind.beq (ImportGraph.Shake.DeclDeclNeedsKind.expr a a_1 a_2) (ImportGraph.Shake.DeclDeclNeedsKind.expr b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• ImportGraph.Shake.instBEqDeclDeclNeedsKind.beq (ImportGraph.Shake.DeclDeclNeedsKind.metaIR a a_1) (ImportGraph.Shake.DeclDeclNeedsKind.metaIR b b_1) = (a == b && a_1 == b_1)
• ImportGraph.Shake.instBEqDeclDeclNeedsKind.beq ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR = true
• ImportGraph.Shake.instBEqDeclDeclNeedsKind.beq (ImportGraph.Shake.DeclDeclNeedsKind.comptime a) (ImportGraph.Shake.DeclDeclNeedsKind.comptime b) = (a == b)
• ImportGraph.Shake.instBEqDeclDeclNeedsKind.beq x✝¹ x✝ = false

@[instance_reducible]

instance ImportGraph.Shake.instBEqDeclDeclNeedsKind : BEq DeclDeclNeedsKind

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprDeclDeclNeedsKind : Repr DeclDeclNeedsKind

Equations

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

def ImportGraph.Shake.instReprDeclDeclNeedsKind.repr : DeclDeclNeedsKind → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instHashableDeclDeclNeedsKind : Hashable DeclDeclNeedsKind

Equations

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

def ImportGraph.Shake.instHashableDeclDeclNeedsKind.hash : DeclDeclNeedsKind → UInt64

Equations

• ImportGraph.Shake.instHashableDeclDeclNeedsKind.hash (ImportGraph.Shake.DeclDeclNeedsKind.expr a a_1 a_2) = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)
• ImportGraph.Shake.instHashableDeclDeclNeedsKind.hash (ImportGraph.Shake.DeclDeclNeedsKind.metaIR a a_1) = mixHash (mixHash 1 (hash a)) (hash a_1)
• ImportGraph.Shake.instHashableDeclDeclNeedsKind.hash ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR = 2
• ImportGraph.Shake.instHashableDeclDeclNeedsKind.hash (ImportGraph.Shake.DeclDeclNeedsKind.comptime a) = mixHash 3 (hash a)

def ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord : DeclDeclNeedsKind → DeclDeclNeedsKind → Ordering

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord (ImportGraph.Shake.DeclDeclNeedsKind.expr a a_1 a_2) x✝ = Ordering.lt
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord x✝ (ImportGraph.Shake.DeclDeclNeedsKind.expr a a_1 a_2) = Ordering.gt
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord (ImportGraph.Shake.DeclDeclNeedsKind.metaIR a a_1) x✝ = Ordering.lt
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord x✝ (ImportGraph.Shake.DeclDeclNeedsKind.metaIR a a_1) = Ordering.gt
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR = Ordering.eq
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR x✝ = Ordering.lt
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord x✝ ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR = Ordering.gt
• ImportGraph.Shake.instOrdDeclDeclNeedsKind.ord (ImportGraph.Shake.DeclDeclNeedsKind.comptime a) (ImportGraph.Shake.DeclDeclNeedsKind.comptime b) = (compare a b).then Ordering.eq

@[instance_reducible]

instance ImportGraph.Shake.instOrdDeclDeclNeedsKind : Ord DeclDeclNeedsKind

Equations

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

def ImportGraph.Shake.DeclDeclNeedsKind.toMessageData : DeclDeclNeedsKind → Lean.MessageData

An English-language description of a DeclDeclNeedsKind.

Equations

• One or more equations did not get rendered due to their size.
• ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR.toMessageData = (Lean.MessageData.ofFormat ∘ Std.format) "used in runtime IR"
• (ImportGraph.Shake.DeclDeclNeedsKind.metaIR isReExported through).toMessageData = (Lean.MessageData.ofFormat ∘ Std.format) "used in meta IR"
• (ImportGraph.Shake.DeclDeclNeedsKind.comptime source).toMessageData = Lean.toMessageData source

@[instance_reducible]

instance ImportGraph.Shake.DeclDeclNeedsKind.instToMessageData : Lean.ToMessageData DeclDeclNeedsKind

Equations

• ImportGraph.Shake.DeclDeclNeedsKind.instToMessageData = { toMessageData := fun (x : ImportGraph.Shake.DeclDeclNeedsKind) => x.toMessageData }

@[inline]

def ImportGraph.Shake.DeclDeclNeedsKind.irPhaseNeeds? : DeclDeclNeedsKind → Option Lean.IRPhases

some .comptime if this demands the source declaration's IRPhases includes .comptime; some .runtime if this demands the source declaration's IRPhases includes .runtime. (.all includes both.) none if there is no demand either way (as is the case for expressions).

Equations

• (ImportGraph.Shake.DeclDeclNeedsKind.expr downstream isReExported upstream).irPhaseNeeds? = none
• (ImportGraph.Shake.DeclDeclNeedsKind.metaIR isReExported through).irPhaseNeeds? = some Lean.IRPhases.comptime
• (ImportGraph.Shake.DeclDeclNeedsKind.comptime source).irPhaseNeeds? = some Lean.IRPhases.comptime
• ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR.irPhaseNeeds? = some Lean.IRPhases.runtime

structure ImportGraph.Shake.Stance : Type

The intrinsic information that determines subsequent placement under different manners of import.

• isPublic : Bool

  Whether the declaration is public or not. We assume we are only discussing declarations that appear in the environment. (If we want to relax this in the future, this might become Option Bool.)

• isExposed : Option Bool

  Whether the declaration is exposed. none if the notion of exposure does not apply (e.g. a theorem).

• isPublic_if_isExposed : (self.isExposed != some true || self.isPublic) = true

  Only public declarations can be exposed.

• isMeta : Option Bool

  Whether the declaration is meta, i.e. has exported IR. none if there is no IR to be exported. If some false, the declaration has runtime IR.

• isExact : Bool

  A flag indicating whether this is the exact stance (determined within the same module) or a lower bound.

@[macro_inline]

def ImportGraph.Shake.Stance.isPrivate (s : Stance) : Bool

Whether a Stance is not isPublic.

Equations

• s.isPrivate = !s.isPublic

def ImportGraph.Shake.Stance.toString : Stance → String

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instToStringStance : ToString Stance

Equations

• ImportGraph.Shake.instToStringStance = { toString := fun (x : ImportGraph.Shake.Stance) => x.toString }

@[reducible, inline]

abbrev ImportGraph.Shake.DeclDeclNeedsKindSet : Type

A set of declaration needs.

Equations

• ImportGraph.Shake.DeclDeclNeedsKindSet = Std.TreeSet ImportGraph.Shake.DeclDeclNeedsKind compare

structure ImportGraph.Shake.DeclNeed : Type

The demands of a single declaration, organized to facilitate movement. Free declarations are those whose modules may change; fixed ones must remain in the same module. Does not record extra mod uses.

• freeDecls : Lean.NameMap DeclDeclNeedsKindSet

  Declarations whose location may be altered.

• fixedDecls : Lean.NameMap (Lean.NameMap DeclDeclNeedsKindSet)

  Declarations whose location may not be altered. A map [module name] ↦ [needs of declarations from that module].

• parentDecls : List Lean.Name

  The parent declaration, if the ambient declaration is autogenerated.

• childDecls : List Lean.Name

  Any autogenerated declarations used by this declaration.

@[instance_reducible]

instance ImportGraph.Shake.instInhabitedDeclNeed : Inhabited DeclNeed

Equations

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

def ImportGraph.Shake.instReprDeclNeed.repr : DeclNeed → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprDeclNeed : Repr DeclNeed

Equations

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

def ImportGraph.Shake.DeclNeed.toMessageData : DeclNeed → Lean.MessageData

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instToMessageDataDeclNeed : Lean.ToMessageData DeclNeed

Equations

• ImportGraph.Shake.instToMessageDataDeclNeed = { toMessageData := fun (x : ImportGraph.Shake.DeclNeed) => x.toMessageData }

@[inline]

def ImportGraph.Shake.DeclNeed.insertFreeDecl (k : DeclDeclNeedsKind) (decl : Lean.Name) (declNeed : DeclNeed) : DeclNeed

Records that the ambient declaration needs the declaration decl at availability k, where the module of decl is left free.

Equations

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

def ImportGraph.Shake.DeclNeed.insertFixedDecl (k : DeclDeclNeedsKind) (mod decl : Lean.Name) (declNeed : DeclNeed) : DeclNeed

Records that the ambient declaration needs the imported declaration decl from module i at availability k, where decl is expected to stay in i.

Equations

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

@[inline]

def ImportGraph.Shake.DeclNeed.isAutoDecl (declNeed : DeclNeed) : Bool

Equations

• declNeed.isAutoDecl = !declNeed.parentDecls.isEmpty

@[reducible, inline]

abbrev ImportGraph.Shake.DeclNeeds : Type

A collection of needs per declaration.

Equations

• ImportGraph.Shake.DeclNeeds = Lean.NameMap ImportGraph.Shake.DeclNeed

def ImportGraph.Shake.DeclNeeds.toMessageData (needs : DeclNeeds) : Lean.MessageData

Equations

• needs.toMessageData = ImportGraph.Shake.NameMap.toMessageData✝ needs (fun (x : ImportGraph.Shake.DeclNeed) => x.toMessageData) true

@[instance_reducible]

instance ImportGraph.Shake.instToMessageDataDeclNeeds : Lean.ToMessageData DeclNeeds

Equations

• ImportGraph.Shake.instToMessageDataDeclNeeds = { toMessageData := fun (x : ImportGraph.Shake.DeclNeeds) => x.toMessageData }

@[inline]

def ImportGraph.Shake.DeclNeeds.insertAutoDeclLink (autoDecl parentDecl : Lean.Name) (declNeeds : DeclNeeds) : DeclNeeds

Equations

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

@[inline]

def ImportGraph.Shake.DeclNeeds.insertFreeDeclFor (currentDecl : Lean.Name) (k : DeclDeclNeedsKind) (usedDecl : Lean.Name) (declNeeds : DeclNeeds) : DeclNeeds

Equations

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

@[inline]

def ImportGraph.Shake.DeclNeeds.insertFixedDeclFor (currentDecl : Lean.Name) (k : DeclDeclNeedsKind) (mod usedDecl : Lean.Name) (declNeeds : DeclNeeds) : DeclNeeds

Equations

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

def ImportGraph.Shake.Stance.isPublicAt (s : Stance) : ConstLocation → Bool

Returns false if s.isExposed = none. Because of that, this is not necessarily equivalent to !(s.isPrivateAt loc).

Equations

• s.isPublicAt ImportGraph.Shake.ConstLocation.type = s.isPublic
• s.isPublicAt ImportGraph.Shake.ConstLocation.value = s.isExposed.getD false

def ImportGraph.Shake.Stance.isPrivateAt (s : Stance) : ConstLocation → Bool

Returns false if s.isExposed = none. Because of that, this is not necessarily equivalent to !(s.isPublicAt loc).

Equations

• s.isPrivateAt ImportGraph.Shake.ConstLocation.type = !s.isPublic
• s.isPrivateAt ImportGraph.Shake.ConstLocation.value = !s.isExposed.getD true

def ImportGraph.Shake.findStanceOfNonImported? (decl : Lean.Name) : Lean.CoreM (Option Stance)

Finds the stance of the given declaration, assuming decl is not imported. Returns none if decl is either not in the environment or is imported.

Equations

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

def ImportGraph.Shake.shouldHaveGeneratedCode (declName : Lean.Name) : Lean.CoreM Bool

Like shouldGenerateCode, but for imported constants.

Equations

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

def ImportGraph.Shake.findLowerBoundStanceOfImported? (decl : Lean.Name) : Lean.CoreM (Option Stance)

Approximates the stance of the imported declaration decl by a "lower bound". This means that we assume that any "extra information" is due to provisioning rather than the stance. For example, an import all will provide the body of every definition regardless of whether it is exposed or not. We therefore assume it is not exposed and that import all is doing the work. This allows us to ensure we have the imports we need. In most cases, however, this lower bound is sharp and matches the actual stance.

Equations

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

def ImportGraph.Shake.Stance.toImportNeedsKind (downstreamStance : Stance) (demand : DeclDeclNeedsKind) (upstreamStance : Stance) : ImportNeedsKind

The ImportNeedsKind implied by a downstream constant with stance downstreamStance demanding a declaration with stance upstreamStance via demand : DeclDeclNeedsKind. Assumes that the demand is satisfiable by the upstream declaration (e.g. that we are not trying to use an intrinsically private declaration in a public position).

Note that this does not account for indirect module uses.

Equations

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

@[reducible, inline]

abbrev ImportGraph.Shake.StanceM (α : Type) : Type

CoreM together with a cache for Stances.

Equations

• ImportGraph.Shake.StanceM = Lean.MonadCacheT Lean.Name (Option ImportGraph.Shake.Stance) Lean.CoreM

@[reducible, inline]

abbrev ImportGraph.Shake.StanceM.run {α : Type} (x : StanceM α) (s : Std.HashMap Lean.Name (Option Stance) := ∅) : Lean.CoreM (α × Std.HashMap Lean.Name (Option Stance))

Equations

• x.run s = StateRefT'.run x s

@[reducible, inline]

abbrev ImportGraph.Shake.StanceM.run' {α : Type} (x : StanceM α) (s : Std.HashMap Lean.Name (Option Stance) := ∅) : Lean.CoreM α

Equations

• x.run' s = StateRefT'.run' x s

def ImportGraph.Shake.getStance? (decl : Lean.Name) : StanceM (Option Stance)

Gets the stance of the given declaration. Records none if no stance could be found. This is insensitive to the isExporting flag on the ambient environment.

Equations

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

@[inline]

def ImportGraph.Shake.isDeclNeedsAutoDecl (env : Lean.Environment) (c : Lean.Name) : Bool

An approximation to whether something is an autogenerated declaration whose base decl is its prefix. This should be improved.

Equations

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

partial def ImportGraph.Shake.calcDeclConstInfoNeeds (decl : Lean.Name) (env : Lean.Environment) (currentDecls : DeclNeeds := ∅) (isReExported : Option Bool := none) : DeclNeeds

Calculate the needs of the given declaration based on its ConstInfo (type and value).

def ImportGraph.Shake.DeclNeeds.calcSyntaxNeeds (env : Lean.Environment) (decls : Array Lean.Name) (cmd : Lean.Syntax) (declNeeds : DeclNeeds) : Lean.Elab.Command.CommandElabM DeclNeeds

Calculate the syntax needs of some syntax, and attaches it as a comptime need for all decls. This design will likely change in the future, and command needs will have a dedicated location instead of being duplicated across different declarations.

Equations

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

def ImportGraph.Shake.DeclNeeds.calcIRNeeds (declNeeds : DeclNeeds) : StanceM DeclNeeds

Calculates the IR needs of a declaration. Currently ignores meta IR.

Equations

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

def ImportGraph.Shake.DeclNeeds.metaWarning? (env : Lean.Environment) (declNeeds : DeclNeeds) (cmd : String) : Option Lean.MessageData

A warning to display if any new declarations are meta, since meta declarations are not handled properly yet.

Equations

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

def ImportGraph.Shake.withElabCommandCapturingNeeds (cmd : Lean.Command) : Lean.Elab.Command.CommandElabM (DeclNeeds × Array Lean.Name × List Lean.ExtraModUse)

Elaborates the command and captures the DeclNeeds of all new declarations. Attaches the needs implied by the command's syntax to each new declaration. Also returns the new ExtraModUses produced during the command. Note: does not capture extra rev mod uses influencing the file as a whole.

Equations

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