Fixed Parameter Static Analyzer

inductive Lean.Compiler.LCNF.FixedParams.AbsValue : Type

Abstract value for the "fixed parameter" analysis.

• top: Lean.Compiler.LCNF.FixedParams.AbsValue
• erased: Lean.Compiler.LCNF.FixedParams.AbsValue
• val: Nat → Lean.Compiler.LCNF.FixedParams.AbsValue

Instances For

• Lean.Compiler.LCNF.FixedParams.instBEqAbsValue
• Lean.Compiler.LCNF.FixedParams.instHashableAbsValue
• Lean.Compiler.LCNF.FixedParams.instInhabitedAbsValue

instance Lean.Compiler.LCNF.FixedParams.instInhabitedAbsValue : Inhabited Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

• Lean.Compiler.LCNF.FixedParams.instInhabitedAbsValue = { default := Lean.Compiler.LCNF.FixedParams.AbsValue.top }

instance Lean.Compiler.LCNF.FixedParams.instBEqAbsValue : BEq Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

• Lean.Compiler.LCNF.FixedParams.instBEqAbsValue = { beq := Lean.Compiler.LCNF.FixedParams.beqAbsValue✝ }

instance Lean.Compiler.LCNF.FixedParams.instHashableAbsValue : Hashable Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

• Lean.Compiler.LCNF.FixedParams.instHashableAbsValue = { hash := Lean.Compiler.LCNF.FixedParams.hashAbsValue✝ }

structure Lean.Compiler.LCNF.FixedParams.Context : Type

• decls : Array Lean.Compiler.LCNF.Decl

  Declaration in the same mutual block.

• main : Lean.Compiler.LCNF.Decl

  Function being analyzed. We check every recursive call to this function. Remark: main is in decls.

• assignment : Lean.FVarIdMap Lean.Compiler.LCNF.FixedParams.AbsValue

  The assignment maps free variable ids in the current code being analyzed to abstract values. We only track the abstract value assigned to parameters.

structure Lean.Compiler.LCNF.FixedParams.State : Type

• visited : Std.HashSet (Lean.Name × Array Lean.Compiler.LCNF.FixedParams.AbsValue)

  Set of calls that have been already analyzed. Recall that we assume that only functions in decls may have recursive calls to the function being analyzed (i.e., main). Whenever there is function application f a₁ ... aₙ, where f is in decls, f is not main, and we visit with the abstract values assigned to aᵢ, but first we record the visit here.

• fixed : Array Bool

  Bitmask containing the result, i.e., which parameters of main are fixed. We initialize it with true everywhere.

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FixedParams.FixParamM (α : Type) : Type

Monad for the fixed parameter static analyzer. We use the unit-exception to interrupt the analysis.

Equations

• Lean.Compiler.LCNF.FixedParams.FixParamM = ReaderT Lean.Compiler.LCNF.FixedParams.Context (EStateM Unit Lean.Compiler.LCNF.FixedParams.State)

@[reducible, inline]

abbrev Lean.Compiler.LCNF.FixedParams.abort {α : Type} : Lean.Compiler.LCNF.FixedParams.FixParamM α

Stop the analysis and mark all parameters as non-fixed.

Equations

• Lean.Compiler.LCNF.FixedParams.abort = do modify fun (s : Lean.Compiler.LCNF.FixedParams.State) => { visited := s.visited, fixed := Array.map (fun (x : Bool) => false) s.fixed } throw ()

def Lean.Compiler.LCNF.FixedParams.evalFVar (fvarId : Lean.FVarId) : Lean.Compiler.LCNF.FixedParams.FixParamM Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

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

def Lean.Compiler.LCNF.FixedParams.evalArg (arg : Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.FixedParams.FixParamM Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

• Lean.Compiler.LCNF.FixedParams.evalArg Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.FixedParams.AbsValue.erased
• Lean.Compiler.LCNF.FixedParams.evalArg (Lean.Compiler.LCNF.Arg.type (Lean.Expr.fvar fvarId)) = Lean.Compiler.LCNF.FixedParams.evalFVar fvarId
• Lean.Compiler.LCNF.FixedParams.evalArg (Lean.Compiler.LCNF.Arg.type expr) = pure Lean.Compiler.LCNF.FixedParams.AbsValue.top
• Lean.Compiler.LCNF.FixedParams.evalArg (Lean.Compiler.LCNF.Arg.fvar fvarId) = Lean.Compiler.LCNF.FixedParams.evalFVar fvarId

def Lean.Compiler.LCNF.FixedParams.inMutualBlock (declName : Lean.Name) : Lean.Compiler.LCNF.FixedParams.FixParamM Bool

Equations

• Lean.Compiler.LCNF.FixedParams.inMutualBlock declName = do let __do_lift ← read pure (__do_lift.decls.any fun (x : Lean.Compiler.LCNF.Decl) => x.name == declName)

def Lean.Compiler.LCNF.FixedParams.mkAssignment (decl : Lean.Compiler.LCNF.Decl) (values : Array Lean.Compiler.LCNF.FixedParams.AbsValue) : Lean.FVarIdMap Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

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

partial def Lean.Compiler.LCNF.FixedParams.evalLetValue (e : Lean.Compiler.LCNF.LetValue) : Lean.Compiler.LCNF.FixedParams.FixParamM Unit

partial def Lean.Compiler.LCNF.FixedParams.evalCode (code : Lean.Compiler.LCNF.Code) : Lean.Compiler.LCNF.FixedParams.FixParamM Unit

partial def Lean.Compiler.LCNF.FixedParams.evalApp (declName : Lean.Name) (args : Array Lean.Compiler.LCNF.Arg) : Lean.Compiler.LCNF.FixedParams.FixParamM Unit

def Lean.Compiler.LCNF.FixedParams.mkInitialValues (numParams : Nat) : Array Lean.Compiler.LCNF.FixedParams.AbsValue

Equations

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

def Lean.Compiler.LCNF.mkFixedParamsMap (decls : Array Lean.Compiler.LCNF.Decl) : Lean.NameMap (Array Bool)

Given the (potentially mutually) recursive declarations decls, return a map from declaration name decl.name to a bit-mask m where m[i] is true iff the decl.params[i] is a fixed argument. That is, it does not change in recursive applications. The function assumes that if a function f was declared in a mutual block, then decls contains all (computationally relevant) functions in the mutual block.

Equations

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