This module contains the logic for figuring out, given mutually recursive predefinitions, which parameters are “fixed”. This used to be a simple task when we only considered a fixed prefix, but becomes a quite involved task if we allow fixed parameters also later in the parameter list, and possibly in a different order in different modules.

The main components of this module are

• The pure Info data type for the bookkeeping during analysis
• The FixedParamPerm type, with the analysis result for one function (effectively a mask and a permutation)
• The FixedParamPerms data type, with the data for a whole recursive group.
• The getFixedParamPerms function that calculates the fixed parameters
• Various MetaM functions for bringing into scope fixed and varying parameters, assembling argument lists etc.

structure Lean.Elab.FixedParams.Info : Type

To determine which parameters in mutually recursive predefinitions are fixed, and how they correspond to each other, we run an analysis that aggregates information in the Info data type.

Abstractly, this represents

• a set varying of (funIdx × paramIdx) pairs known to be varying, initially empty
• a directed graph whose nodes are (funIdx × paramIdx) pairs, initially empty

We find the largest set and graph that satisfies these rules:

• Every parameter has to be related to itself: (funIdx, paramIdx) → (funIdx, paramIdx).
• whenever the function with index caller calls callee and the argIdx's argument is reducibly defeq to paramIdx, then we have an edge (caller, paramIdx) → (callee, argIdx).
• whenever the function with index caller calls callee and the argIdx's argument is not reducibly defeq to any of the caller's parameters, then (callee, argIdx) ∈ varying.
• If we have (caller, paramIdx₁) → (callee, argIdx) and (caller, paramIdx₂) → (callee, argIdx) with paramIdx₁ ≠ paramIdx₂, then (callee, argIdx) ∈ varying.
• The graph is transitive
• If we have (caller, paramIdx) → (callee, argIdx) and (caller, paramIdx) ∈ varying, then (callee, argIdx) ∈ varying
• If the type of funIdx’s parameter paramIdx₂ depends on the paramIdx₁and `(funIdx, paramIdx₁) ∈ varying, then (funIdx, paramIdx₁) ∈ varying`
• For structural recursion: The target and all its indices are varying. (This is taking into account post-hoc, using FixedParamPerms.erase)

Under the assumption that the predefintions indeed are mutually recursive, then the resulting graph, restricted to the non-varying nodes, should partition into cliques that have one member from each function. Every such clique becomes a fixed parameter.

• graph : Array (Array (Option (Array (Option Nat))))
• revDeps : Array (Array (Array Nat))

  The dependency structure of the function parameter. If paramIdx₂ ∈ revDeps[funIdx][paraIdx₁], then the type of paramIdx₂ depends on parmaIdx₁

def Lean.Elab.FixedParams.Info.init (revDeps : Array (Array (Array Nat))) : Info

def Lean.Elab.FixedParams.Info.addSelfCalls (info : Info) : Info

def Lean.Elab.FixedParams.Info.mayBeFixed (callerIdx paramIdx : Nat) (info : Info) : Bool

Is this parameter still plausibly a fixed parameter?

partial def Lean.Elab.FixedParams.Info.setVarying (funIdx paramIdx : Nat) (info : Info) : Info

This parameter is varying. Set and propagate that information.

def Lean.Elab.FixedParams.Info.getCallerParam? (calleeIdx argIdx callerIdx : Nat) (info : Info) : Option Nat

partial def Lean.Elab.FixedParams.Info.setCallerParam (calleeIdx argIdx callerIdx paramIdx : Nat) (info : Info) : Info

We observe a possibly valid edge.

def Lean.Elab.FixedParams.Info.format (info : Info) : Format

instance Lean.Elab.FixedParams.instToFormatInfo : ToFormat Info

def Lean.Elab.getParamRevDeps (value : Expr) : MetaM (Array (Array Nat))

def Lean.Elab.getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info

@[reducible, inline]

abbrev Lean.Elab.FixedParamPerm : Type

For a given function, a mapping from its parameters to the (indices of the) fixed parameters of the recursive group. The length of the array is the arity of the function, as determined from its body, consistent with the arity used by well-founded recursion. For the first function, they appear in order; for other functions they may be reordered.

structure Lean.Elab.FixedParamPerms : Type

This data structure stores the result of the fixed parameter analysis. See FixedParams.Info for details on the analysis.

• numFixed : Nat

  Number of fixed parameters

• perms : Array FixedParamPerm

  For each function in the clique, a mapping from its parameters to the fixed parameters. For the first function, they appear in order; for other functions they may be reordered.

• revDeps : Array (Array (Array Nat))

  The dependencies among the parameters. See FixedParams.Info.revDeps. We need this for the FixedParamsPerm.erase operation.

instance Lean.Elab.instInhabitedFixedParamPerms : Inhabited FixedParamPerms

instance Lean.Elab.instReprFixedParamPerms : Repr FixedParamPerms

def Lean.Elab.getFixedParamPerms (preDefs : Array PreDefinition) : MetaM FixedParamPerms

def Lean.Elab.FixedParamPerm.numFixed (perm : FixedParamPerm) : Nat

def Lean.Elab.FixedParamPerm.isFixed (perm : FixedParamPerm) (i : Nat) : Bool

def Lean.Elab.FixedParamPerm.forallTelescope {n : Type → Type u_1} {α : Type} [MonadControlT MetaM n] [Monad n] (perm : FixedParamPerm) (type : Expr) (k : Array Expr → n α) : n α

def Lean.Elab.FixedParamPerm.instantiateForall (perm : FixedParamPerm) (type₀ : Expr) (xs : Array Expr) : MetaM Expr

If type is the type of the funIdx's function, instantiate the fixed parameters.

def Lean.Elab.FixedParamPerm.instantiateForall.go (xs : Array Expr) : List (Option Nat) → Expr → MetaM Expr

def Lean.Elab.FixedParamPerm.instantiateLambda (perm : FixedParamPerm) (value₀ : Expr) (xs : Array Expr) : MetaM Expr

If value is the body of the funIdx's function, instantiate the fixed parameters. Expects enough manifest lambdas to instantiate all fixed parameters, but can handle eta-contracted definitions beyond that.

def Lean.Elab.FixedParamPerm.instantiateLambda.go (xs : Array Expr) : List (Option Nat) → Expr → MetaM Expr

def Lean.Elab.FixedParamPerm.pickFixed {α : Type u_1} (perm : FixedParamPerm) (xs : Array α) : Array α

If xs are arguments to the funIdx's function, pick only the fixed ones, and reorder appropriately. Expects xs to match the arity of the function.

def Lean.Elab.FixedParamPerm.pickFixed.go {α : Type u_1} : List (Option Nat × α) → Array α → Id (Array α)

def Lean.Elab.FixedParamPerm.pickVarying {α : Type u_1} (perm : FixedParamPerm) (xs : Array α) : Array α

If xs are arguments to the funIdx's function, pick only the varying ones. Unlike pickFixed, this function can handle over- or under-application.

def Lean.Elab.FixedParamPerm.buildArgs {α : Type u_1} (perm : FixedParamPerm) (fixedArgs varyingArgs : Array α) : Array α

Intersperses the fixed and varying parameters to be in the original parameter order. Can handle over- or und-application (extra or missing varying args), as long as there are all varying parameters that go before fixed parameters. (We expect to always find all fixed parameters, else they wouldn't be fixed parameters.)

partial def Lean.Elab.FixedParamPerm.buildArgs.go {α : Type u_1} (perm : FixedParamPerm) (fixedArgs varyingArgs : Array α) (i : Nat) (j : Std.PRange.Bound { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.unbounded }.lower Nat) (xs : Array α) : Array α

def Lean.Elab.FixedParamPerms.fixedArePrefix (fixedParamPerms : FixedParamPerms) : Bool

Are all fixed parameters a non-reordered prefix?

def Lean.Elab.FixedParamPerms.erase (fixedParamPerms : FixedParamPerms) (xs : Array Expr) (toErase : Array (Array Nat)) : FixedParamPerms × Array Expr × Array FVarId

If xs are the fixed parameters that are in scope, and toErase are, for each function, the positions of arguments that must no longer be fixed parameters, then this function splits partitions xs into those to keep and those to erase, and updates FixedParams accordingly.

This is used in structural recursion, where we may discover that some fixed parameters are actually indices and need to be treated as varying, including all parameters that depend on them.