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.ImportNeedsKindextends ImportGraph.Shake.NeedsKind : 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.

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

  A flag for the case where the ambient declaration needs a meta declaration from the needed module. In that case, the import is allowed to be meta, but does not have to be. Note that ordinary expression uses also allowMeta; it is only usage in the computational content (LCNF) that will disallow meta and set this to false.

  However, to allow NeedsKinds constructors to not conflict with .allowMetaPub, we set this to isMeta by default.

• allowMeta_if_isMeta : (!self.isMeta || self.allowMeta) = true

  Needing a meta import implies allowMeta = true.

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.pubNoMeta : ImportNeedsKind

Equations

• ImportGraph.Shake.ImportNeedsKind.pubNoMeta = { toNeedsKind := ImportGraph.Shake.NeedsKind.pub, allowMeta := false, allowMeta_if_isMeta := ImportGraph.Shake.ImportNeedsKind.pubNoMeta._proof_2 }

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privNoMeta : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privOfPrivNoMeta : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.metaPub : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.metaPriv : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.metaPrivOfPriv : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.pubAllowMeta : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privAllowMeta : ImportNeedsKind

Equations

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

@[match_pattern]

def ImportGraph.Shake.ImportNeedsKind.privOfPrivAllowMeta : 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.

def ImportGraph.Shake.NeedsKind.toImportNeedsKind (k : NeedsKind) (allowMeta : Bool) : ImportNeedsKind

Equations

• k.toImportNeedsKind allowMeta = { toNeedsKind := k, allowMeta := k.isMeta || allowMeta, allowMeta_if_isMeta := ⋯ }

structure ImportGraph.Shake.ImportNeedsextends ImportGraph.Shake.Needs : Type

Like Needs, but preserves allowMeta. We interpret pub/priv/privOfPriv from NeedsKind as having allowMeta := false, i.e. as specifically disallowing a meta import.

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

  The modules which may be imported as meta or non-meta which are needed in the public scope.

• allowMetaPriv : Bitset

  The modules which may be imported as meta or non-meta whose public scopes must be available in the current private scope.

• allowMetaPrivOfPriv : Bitset

  The modules which may be imported as meta or non-meta whose private scopes must be available in the current private scope.

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

• ImportGraph.Shake.ImportNeeds.empty = { toSubNeeds := ImportGraph.Shake.Needs.empty, allowMetaPub := ∅, allowMetaPriv := ∅, allowMetaPrivOfPriv := ∅ }

@[instance_reducible]

instance ImportGraph.Shake.ImportNeeds.instEmptyCollection : EmptyCollection ImportNeeds

Equations

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

def ImportGraph.Shake.ImportNeeds.toNeeds (useMeta : Bool := false) (imp : ImportNeeds) : Needs

Turns ImportNeeds into a concrete Needs with an opinionated choice of whether allowMeta should revert to public imports (useMeta := false) or be regarded as meta imports (useMeta := true)

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, isMeta := false, not_isExported_and_isAll := ⋯, allowMeta_if_isMeta := ⋯ } = needs.pub
• needs.get { isExported := false, isMeta := false, not_isExported_and_isAll := ⋯, allowMeta_if_isMeta := ⋯ } = needs.priv
• needs.get { isExported := true, isMeta := true, not_isExported_and_isAll := ⋯, allowMeta_if_isMeta := ⋯ } = needs.metaPub
• needs.get { isExported := false, isMeta := true, not_isExported_and_isAll := ⋯, allowMeta_if_isMeta := ⋯ } = needs.metaPriv
• needs.get { isExported := false, isMeta := false, isAll := true, not_isExported_and_isAll := ⋯, allowMeta_if_isMeta := ⋯ } = needs.privOfPriv
• needs.get { isExported := false, isMeta := true, isAll := true, not_isExported_and_isAll := ⋯, allowMeta_if_isMeta := ⋯ } = needs.metaPrivOfPriv
• needs.get { isExported := true, isMeta := false, not_isExported_and_isAll := ⋯, allowMeta := true, allowMeta_if_isMeta := ⋯ } = needs.allowMetaPub
• needs.get { isExported := false, isMeta := false, not_isExported_and_isAll := ⋯, allowMeta := true, allowMeta_if_isMeta := ⋯ } = needs.allowMetaPriv
• needs.get { isExported := false, isMeta := false, isAll := true, not_isExported_and_isAll := ⋯, allowMeta := true, allowMeta_if_isMeta := ⋯ } = needs.allowMetaPrivOfPriv

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

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

@[instance_reducible]

instance ImportGraph.Shake.instBEqComptimeDependency : BEq ComptimeDependency

Equations

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

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

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)

@[instance_reducible]

instance ImportGraph.Shake.instHashableComptimeDependency : Hashable ComptimeDependency

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instOrdComptimeDependency : Ord ComptimeDependency

Equations

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

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

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 }

@[instance_reducible]

instance ImportGraph.Shake.instBEqConstLocation : BEq ConstLocation

Equations

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

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

Equations

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

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.instReprConstLocation : Repr ConstLocation

Equations

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

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

@[instance_reducible]

instance ImportGraph.Shake.instHashableConstLocation : Hashable ConstLocation

Equations

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

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 }

@[instance_reducible]

instance ImportGraph.Shake.instBEqDeclDeclNeedsKind : BEq DeclDeclNeedsKind

Equations

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

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

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)

@[instance_reducible]

instance ImportGraph.Shake.instHashableDeclDeclNeedsKind : Hashable DeclDeclNeedsKind

Equations

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

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.pretty : DeclDeclNeedsKind → String

An English-language description of a DeclDeclNeedsKind.

Equations

• (ImportGraph.Shake.DeclDeclNeedsKind.expr down (some true) up).pretty = toString "uses " ++ toString up ++ toString " in " ++ toString down ++ toString " (public)"
• (ImportGraph.Shake.DeclDeclNeedsKind.expr down (some false) up).pretty = toString "uses " ++ toString up ++ toString " in " ++ toString down ++ toString " (private)"
• (ImportGraph.Shake.DeclDeclNeedsKind.expr down none up).pretty = toString "uses " ++ toString up ++ toString " in " ++ toString down ++ toString ""
• ImportGraph.Shake.DeclDeclNeedsKind.runtimeIR.pretty = "used in runtime IR"
• (ImportGraph.Shake.DeclDeclNeedsKind.metaIR isReExported through).pretty = "used in meta IR"
• (ImportGraph.Shake.DeclDeclNeedsKind.comptime source).pretty = "comptime dependency"

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

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

• freeDecls : Lean.NameMap DeclDeclNeedsKindSet

  Declarations whose location may be altered.

• fixedDecls : Std.TreeMap Lean.Name (Lean.NameMap DeclDeclNeedsKindSet) compare

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

• extraModUses : Lean.NameMap (Std.TreeSet NeedsKind compare)

  Extra module uses recorded in shake extensions during the command. Note that if several declarations were created during the command, the extra mod uses are the same among all of them.

• 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 }

@[instance_reducible]

instance ImportGraph.Shake.instReprDeclNeed : Repr DeclNeed

Equations

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

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

Equations

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

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

def ImportGraph.Shake.DeclNeed.insertExtraModUses (extraModUses : List Lean.ExtraModUse) (declNeed : DeclNeed) : DeclNeed

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

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

@[inline]

def ImportGraph.Shake.DeclNeeds.insertExtraModUsesFor (decl : Lean.Name) (extraModUses : List Lean.ExtraModUse) (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

Calcualte 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.withElabCommandCapturingNeeds (cmd : Lean.Command) : Lean.Elab.Command.CommandElabM (DeclNeeds × Array Lean.Name)

Elaborates the command and captures the DeclNeeds of all new declarations. Attaches the needs implied by the command's syntax to each new declaration. 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.