scope : Lean.FVarIdSet
Set of free variables in scope. The "collector" uses this information when collecting dependencies for code specialization.
ground : Lean.FVarIdSet
Set of let-declarations in scope that do not depend on parameters.
declName : Lake.Name
Name of the declaration being processed

Instances For

source

structure Lean.Compiler.LCNF.Specialize.State :

Type

decls : Array Lean.Compiler.LCNF.Decl

Instances For

source

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Specialize.SpecializeM (α : Type) :

Type

Equations

Lean.Compiler.LCNF.Specialize.SpecializeM = ReaderT Lean.Compiler.LCNF.Specialize.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Specialize.State Lean.Compiler.LCNF.CompilerM)

Instances For

source

instance Lean.Compiler.LCNF.Specialize.instMonadScopeSpecializeM :

Lean.Compiler.LCNF.MonadScope Lean.Compiler.LCNF.Specialize.SpecializeM

Equations

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

source

def Lean.Compiler.LCNF.Specialize.isGround {α : Type} [Lean.Compiler.LCNF.TraverseFVar α] (e : α) :

Lean.Compiler.LCNF.Specialize.SpecializeM Bool

Return true if e is a ground term. That is, it contains only free variables tagged as ground

Equations

Lean.Compiler.LCNF.Specialize.isGround e = do let __do_lift ← read let s : Lean.FVarIdSet := __do_lift.ground pure (Lean.Compiler.LCNF.allFVar (fun x => Lean.RBTree.contains s x) e)

Instances For

source

@[inline]

def Lean.Compiler.LCNF.Specialize.withLetDecl {α : Type} (decl : Lean.Compiler.LCNF.LetDecl) (x : Lean.Compiler.LCNF.Specialize.SpecializeM α) :

Lean.Compiler.LCNF.Specialize.SpecializeM α

Equations

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

Instances For

Dependency collector for the code specialization function. #

During code specialization, we select which arguments are going to be used during the specialization. Then, we have to collect their dependencies. For example, suppose are trying to specialize the following IO.println and List.forM applications in the following example:

    def f xs a.1 :=
      let _x.2 := @instMonadEIO IO.Error
      let _x.5 := instToStringString
      let _x.9 := instToStringNat
      let _x.6 := "hello"
      let _x.61 := @IO.println String _x.5 _x.6 a.1 -- (*)
      cases _x.61
      | EStateM.Result.ok a.6 a.7 =>
        fun _f.72 _y.69 _y.70 :=
          let _x.71 := @IO.println Nat _x.9 _y.69 _y.70 -- (*)
          _x.71
        let _x.65 := @List.forM (fun α => PUnit → EStateM.Result IO.Error PUnit α) _x.2 Nat xs _f.72 a.7 -- (*)
        ...
      ...

For IO.println the SpecArgInfo is [N, I, O, O], i.e., only the first two arguments are considered for code specialization. The first one is computationally neutral, and the second one is an instance. For List.forM, we have [N, I, N, O, H]. In this case, the fifth argument (tagged as H) is a function. Note that the actual List.forM application has 6 arguments, the extra argument comes from the IO monad.

For the first IO.println application, the collector collects _x.5. For the List.forM, it collects _x.2, _x.9, and _f.72. The collected values are used to construct a key to identify the specialization. Arguments that were not considered are replaced with lcErased. The key is used to make sure we don't keep generating the same specialization over and over again. This is not an optimization, it is essential to prevent the code specializer from looping while specializing recursive functions. The keys for these two applications are the terms.

@IO.println Nat instToStringNat lcErased lcErased

and

@List.forM
  (fun α => PUnit → EStateM.Result IO.Error PUnit α)
  (@instMonadEIO IO.Error) Nat lcErased
  (fun _y.69 _y.70 =>
   let _x.71 := @IO.println Nat instToStringNat _y.69 _y.70;
  _x.71)

The keys never contain free variables or loose bound variables.

source

def Lean.Compiler.LCNF.Specialize.Collector.collect (paramsInfo : Array Lean.Compiler.LCNF.SpecParamInfo) (args : Array Lean.Compiler.LCNF.Arg) :

Lean.Compiler.LCNF.Specialize.SpecializeM (Array (Option Lean.Compiler.LCNF.Arg) × Array Lean.Compiler.LCNF.Param × Array Lean.Compiler.LCNF.CodeDecl)

Given the specialization mask paramsInfo and the arguments args, collect their dependencies, and return an array mask of size paramsInfo.size s.t.

mask[i] = some args[i] if paramsInfo[i] != .other
mask[i] = none, otherwise. That is, mask contains only the arguments that are contributing to the code specialization. We use this information to compute a "key" to uniquely identify the code specialization, and creating the specialized code.

Equations

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

Instances For

source

def Lean.Compiler.LCNF.Specialize.shouldSpecialize (paramsInfo : Array Lean.Compiler.LCNF.SpecParamInfo) (args : Array Lean.Compiler.LCNF.Arg) :

Lean.Compiler.LCNF.Specialize.SpecializeM Bool

Return true if it is worth using arguments args for specialization given the parameter specialization information.

Equations

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

Instances For

source

def Lean.Compiler.LCNF.Specialize.expandCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) (body : Lean.Compiler.LCNF.LetValue) :

Lean.Compiler.LCNF.CompilerM Lean.Expr

Convert the given declarations into Expr, and "zeta-reduce" them into body. This function is used to compute the key that uniquely identifies an code specialization.

Equations

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

Instances For

source

def Lean.Compiler.LCNF.Specialize.expandCodeDecls.go (body : Lean.Compiler.LCNF.LetValue) (xs : Array Lean.Expr) (values : Array Lean.Expr) (i : Nat) (subst : Array Lean.Expr) :

Lean.Expr

Equations

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

Instances For

source

def Lean.Compiler.LCNF.Specialize.mkKey (params : Array Lean.Compiler.LCNF.Param) (decls : Array Lean.Compiler.LCNF.CodeDecl) (body : Lean.Compiler.LCNF.LetValue) :

Lean.Compiler.LCNF.CompilerM (Lean.Expr × List Lake.Name)

Create the "key" that uniquely identifies a code specialization. params and decls are the declarations collected by the collect function above. The result contains the list of universe level parameter names the key that params, decls, and body depends on. We use this information to create the new auxiliary declaration and resulting application.

Equations