Folding through the environment efficiently

This file defines foldImportedDecls, a function for efficiently folding through the environment. It splits the environment into parts, each of which is folded over in a separate thread.

We also provide foldCurrFileDecls which loops through the declarations of the current module, without any parallellism.

@[reducible, inline]

abbrev Lean.Meta.FoldDeclErrorRef : Type

An IO.Ref that keeps track of any errors that could have been thrown by act when folding over the constants in the environment.

Equations

• Lean.Meta.FoldDeclErrorRef = IO.Ref (List Lean.MessageData)

@[specialize #[]]

def Lean.Meta.foldImportedDecls {α : Type} (init : α) (cfg : Config) (act : α → Name → ConstantInfo → MetaM α) (constantsPerTask : Nat := 5000) : CoreM (Array (Task (Except Exception α)) × FoldDeclErrorRef)

Fold through all imported constants using act. This uses paralellism, with each thread independently folding over a subset of modules. The array of tasks is returned, so this function typically returns before all tasks have finished. The results can then be combined using Array.foldl.

Equations

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

@[specialize #[]]

def Lean.Meta.foldCurrFileDecls {α : Type} (init : α) (cfg : Config) (act : α → Name → ConstantInfo → MetaM α) : CoreM (α × FoldDeclErrorRef)

Fold through all constants of the current file using act.

Equations

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