Documentation

Lean.Meta.LazyDiscrTree

Lazy Discrimination Tree #

This file defines a new type of discrimination tree optimized for rapid population of imported modules for use in tactics. It uses a lazy initialization strategy.

The discrimination tree can be created through createImportedDiscrTree. This creates a discrimination tree from all public imported modules in an environment using a callback that provides the entries as InitEntry values.

The function getMatch can be used to get the values that match the expression as well as an updated lazy discrimination tree that has elaborated additional parts of the tree.

Discrimination tree key.

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

      Returns true iff the argument should be treated as a "wildcard" by the discrimination tree.

      This includes proofs, instance implicit arguments, implicit arguments, and terms of the form noIndexing t

      This is a clone of Lean.Meta.DiscrTree.ignoreArg and mainly added to avoid coupling between DiscrTree and LazyDiscrTree while both are potentially subject to independent changes.

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

        Returns true if e is one of the following

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

          Returns true if e is one of the following

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

            Eliminate loose bound variables via beta-reduction.

            This is primarily used to reduce pi-terms ∀(x : P), T into non-dependent functions P → T. The latter has a more specific discrimination tree key .arrow.. and this improves the accuracy of the discrimination tree.

            Clone of Lean.Meta.DiscrTree.elimLooseBVarsByBeta. See it for more discussion.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible, inline]

                An unprocessed entry in the lazy discrimination tree.

                Equations
                Instances For
                  @[reducible]

                  Index identifying trie in a discrimination tree.

                  Equations
                  Instances For

                    Discrimination tree trie. See LazyDiscrTree.

                    • node :: (
                    • )
                    Instances For
                      Equations

                      Push lazy entry to trie.

                      Equations
                      • { values := vs, star := star, children := cs, pending := p }.pushPending x✝ = { values := vs, star := star, children := cs, pending := p.push x✝ }
                      Instances For

                        LazyDiscrTree is a variant of the discriminator tree datatype DiscrTree in Lean core that is designed to be efficiently initializable with a large number of patterns. This is useful in contexts such as searching an entire Lean environment for expressions that match a pattern.

                        Lazy discriminator trees achieve good performance by minimizing the amount of work that is done up front to build the discriminator tree. When first adding patterns to the tree, only the root discriminator key is computed and processing the remaining terms is deferred until demanded by a match.

                        • tries : Array (Trie α)

                          Backing array of trie entries. Should be owned by this trie.

                        • Map from discriminator trie roots to the index.

                        Instances For

                          Specialization of Lean.Meta.DiscrTree.pushArgs

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

                            Initial capacity for key and todo vector.

                            Equations
                            Instances For

                              Get the root key and rest of terms of an expression using the specified config.

                              Equations
                              Instances For
                                partial def Lean.Meta.LazyDiscrTree.buildPath (op : BoolArray ExprExprMetaM (Key × Array Expr)) (root : Bool) (todo : Array Expr) (keys : Array Key) :

                                Create a key path from an expression using the function used for patterns.

                                This differs from Lean.Meta.DiscrTree.mkPath and targetPath in that the expression should uses free variables rather than meta-variables for holes.

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

                                  Create a key path from an expression we are matching against.

                                  This should have mvars instantiated where feasible.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lean.Meta.LazyDiscrTree.runMatch {α β : Type} (d : LazyDiscrTree α) (m : MatchM α β) :
                                    Equations
                                    Instances For
                                      def Lean.Meta.LazyDiscrTree.newTrie {m : TypeType u_1} {α : Type} [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α) :

                                      Create a new trie with the given lazy entry.

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

                                        Add a lazy entry to an existing trie.

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

                                            This evaluates all lazy entries in a trie and updates values, starIdx, and children accordingly.

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

                                                  This drops a specific key from the lazy discrimination tree so that all the entries matching that key exactly are removed.

                                                  Equations
                                                  Instances For

                                                    A match result contains the terms formed from matching a term against patterns in the discrimination tree.

                                                    • elts : Array (Array (Array α))

                                                      The elements in the match result.

                                                      The top-level array represents an array from score values to the results with that score. A score is the number of non-star matches in a pattern against the term, and thus bounded by the size of the term being matched against. The elements of this array are themselves arrays of non-empty arrays so that we can defer concatenating results until needed.

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

                                                        Number of elements in result

                                                        Equations
                                                        Instances For
                                                          @[specialize #[]]
                                                          def Lean.Meta.LazyDiscrTree.MatchResult.appendResultsAux {α : Type} {β : Type u_1} (mr : MatchResult α) (a : Array β) (f : Natαβ) :

                                                          Append results to array

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            Instances For
                                                              Instances For
                                                                partial def Lean.Meta.LazyDiscrTree.getMatchLoop {α : Type} (cases : Array PartialMatch) (result : MatchResult α) :

                                                                Evaluate all partial matches and add resulting matches to MatchResult.

                                                                The partial matches are stored in an array that is used as a stack. When adding multiple partial matches to explore next, to ensure the order of results matches user expectations, this code must add paths we want to prioritize and return results earlier are added last.

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

                                                                    Find values that match e in root.

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

                                                                      Find values that match e in d.

                                                                      The results are ordered so that the longest matches in terms of number of non-star keys are first with ties going to earlier operators first.

                                                                      Equations
                                                                      Instances For

                                                                        Structure for quickly initializing a lazy discrimination tree with a large number of elements using concurrent functions for generating entries.

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

                                                                            Add an entry to the pre-discrimination tree.

                                                                            Equations
                                                                            Instances For

                                                                              Convert a pre-discrimination tree to a lazy discrimination tree.

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

                                                                                Merge two discrimination trees.

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

                                                                                  Initial entry in lazy discrimination tree

                                                                                  • key : Key

                                                                                    Return root key for an entry.

                                                                                  • entry : LazyEntry α

                                                                                    Returns rest of entry for later insertion.

                                                                                  Instances For
                                                                                    def Lean.Meta.LazyDiscrTree.InitEntry.fromExpr {α : Type} (expr : Expr) (value : α) :

                                                                                    Constructs an initial entry from an expression and value.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      def Lean.Meta.LazyDiscrTree.InitEntry.mkSubEntry {α : Type} (e : InitEntry α) (idx : Nat) (value : α) :

                                                                                      Creates an entry for a subterm of an initial entry.

                                                                                      This is slightly more efficient than using fromExpr on subterms since it avoids a redundant call to whnf.

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

                                                                                        Information about a failed import.

                                                                                        • module : Name

                                                                                          Module with constant that import failed on.

                                                                                        • const : Name

                                                                                          Constant that import failed on.

                                                                                        • exception : Exception

                                                                                          Exception that triggers error.

                                                                                        Instances For

                                                                                          Information generation from imported modules.

                                                                                          Instances For
                                                                                            Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                              Instances For
                                                                                                def Lean.Meta.LazyDiscrTree.addConstImportData {α : Type} (cctx : Core.Context) (env : Environment) (modName : Name) (d : ImportData) (cacheRef : IO.Ref Cache) (tree : PreDiscrTree α) (act : NameConstantInfoMetaM (Array (InitEntry α))) (name : Name) (constInfo : ConstantInfo) :
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For

                                                                                                  Contains the pre discrimination tree and any errors occurring during initialization of the library search tree.

                                                                                                  Instances For

                                                                                                    Combine two initial results.

                                                                                                    Equations
                                                                                                    • { tree := yv, errors := ye }.append { tree := yv_1, errors := ye_1 } = { tree := yv ++ yv_1, errors := ye ++ ye_1 }
                                                                                                    Instances For
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        partial def Lean.Meta.LazyDiscrTree.loadImportedModule {α : Type} (cctx : Core.Context) (env : Environment) (act : NameConstantInfoMetaM (Array (InitEntry α))) (d : ImportData) (cacheRef : IO.Ref Cache) (tree : PreDiscrTree α) (mname : Name) (mdata : ModuleData) (i : Nat := 0) :
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          def Lean.Meta.LazyDiscrTree.combineGet {α : Type u_1} [Append α] (z : α) (tasks : Array (Task α)) :
                                                                                                          α

                                                                                                          Get the results of each task and merge using combining function

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    def Lean.Meta.LazyDiscrTree.createImportedDiscrTree {m : TypeType} {α : Type} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT BaseIO m] (cctx : Core.Context) (ngen : NameGenerator) (env : Environment) (act : NameConstantInfoMetaM (Array (InitEntry α))) (constantsPerTask : Nat := 1000) :

                                                                                                                    Create a discriminator tree for imported environment.

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

                                                                                                                      Creates the core context used for initializing a tree using the current context.

                                                                                                                      Equations
                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                      Instances For
                                                                                                                        def Lean.Meta.LazyDiscrTree.findImportMatches {α : Type} (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α)))) (addEntry : NameConstantInfoMetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (ty : Expr) :
                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For

                                                                                                                          A discriminator tree for the current module's declarations only.

                                                                                                                          Note. We use different discriminator trees for imported and current module declarations since imported declarations are typically much more numerous but not changed after the environment is created.

                                                                                                                          Instances For

                                                                                                                            Create a discriminator tree for current module declarations.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              def Lean.Meta.LazyDiscrTree.createModuleTreeRef {α : Type} (entriesForConst : NameConstantInfoMetaM (Array (InitEntry α))) (droppedKeys : List (List Key)) :

                                                                                                                              Creates reference for lazy discriminator tree that only contains this module's definitions.

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

                                                                                                                                Returns candidates from this module in this module that match the expression.

                                                                                                                                • moduleRef is a references to a lazy discriminator tree only containing this module's definitions.
                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  def Lean.Meta.LazyDiscrTree.findMatchesExt {α β : Type} (moduleTreeRef : ModuleDiscrTreeRef α) (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α)))) (addEntry : NameConstantInfoMetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (adjustResult : Natαβ) (ty : Expr) :

                                                                                                                                  findMatchesExt searches for entries in a lazily initialized discriminator tree.

                                                                                                                                  It provides some additional capabilities beyond findMatches to adjust results based on priority and cache module declarations

                                                                                                                                  • modulesTreeRef points to the discriminator tree for local environment. Used for caching and created by createLocalTree.
                                                                                                                                  • ext should be an environment extension with an IO.Ref for caching the import lazy discriminator tree.
                                                                                                                                  • addEntry is the function for creating discriminator tree entries from constants.
                                                                                                                                  • droppedKeys contains keys we do not want to consider when searching for matches. It is used for dropping very general keys.
                                                                                                                                  • constantsPerTask stores number of constants in imported modules used to decide when to create new task.
                                                                                                                                  • adjustResult takes the priority and value to produce a final result.
                                                                                                                                  • ty is the expression type.
                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    def Lean.Meta.LazyDiscrTree.findMatches {α : Type} (ext : EnvExtension (IO.Ref (Option (LazyDiscrTree α)))) (addEntry : NameConstantInfoMetaM (Array (InitEntry α))) (droppedKeys : List (List Key) := []) (constantsPerTask : Nat := 1000) (ty : Expr) :

                                                                                                                                    findMatches searches for entries in a lazily initialized discriminator tree.

                                                                                                                                    • ext should be an environment extension with an IO.Ref for caching the import lazy discriminator tree.
                                                                                                                                    • addEntry is the function for creating discriminator tree entries from constants.
                                                                                                                                    • droppedKeys contains keys we do not want to consider when searching for matches. It is used for dropping very general keys.
                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For