Fixed Parameter Static Analyzer #
Declaration in the same mutual block.
- main : Lean.Compiler.LCNF.Decl
The assignment maps free variable ids in the current code being analyzed to abstract values. We only track the abstract value assigned to parameters.
Set of calls that have been already analyzed. Recall that we assume that only functions in
declsmay have recursive calls to the function being analyzed (i.e.,
main). Whenever there is function application
f a₁ ... aₙ, where
main, and we visit with the abstract values assigned to
aᵢ, but first we record the visit here.
Bitmask containing the result, i.e., which parameters of
mainare fixed. We initialize it with
Given the (potentially mutually) recursive declarations
return a map from declaration name
decl.name to a bit-mask
m[i] is true
decl.params[i] is a fixed argument. That is, it does not change in recursive
The function assumes that if a function
f was declared in a mutual block, then
contains all (computationally relevant) functions in the mutual block.