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 paramters, 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

Equations

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

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

Equations

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

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

Is this parameter still plausibly a fixed parameter?

Equations

• Lean.Elab.FixedParams.Info.mayBeFixed callerIdx paramIdx info = info.graph[callerIdx]![paramIdx]!.isSome

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

Equations

• Lean.Elab.FixedParams.Info.getCallerParam? calleeIdx argIdx callerIdx info = info.graph[calleeIdx]![argIdx]!.bind fun (x : Array (Option Nat)) => x[callerIdx]!

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

Equations

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

instance Lean.Elab.FixedParams.instToFormatInfo : ToFormat Info

Equations

• Lean.Elab.FixedParams.instToFormatInfo = { format := Lean.Elab.FixedParams.Info.format }

def Lean.Elab.getParamRevDeps (preDefs : Array PreDefinition) : MetaM (Array (Array (Array Nat)))

Equations

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

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

Equations

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

@[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.

Equations

• Lean.Elab.FixedParamPerm = Array (Option Nat)

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

Equations

• Lean.Elab.instInhabitedFixedParamPerms = { default := { numFixed := default, perms := default, revDeps := default } }

instance Lean.Elab.instReprFixedParamPerms : Repr FixedParamPerms

Equations

• Lean.Elab.instReprFixedParamPerms = { reprPrec := Lean.Elab.reprFixedParamPerms✝ }

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

Equations

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

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

Equations

• perm.numFixed = Array.countP Option.isSome perm

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

Equations

• perm.isFixed i = perm[i]?.join.isSome

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 α

Equations

• perm.forallTelescope type k = Lean.Meta.map1MetaM (fun {α : Type} (k : Array Lean.Expr → Lean.MetaM α) => Lean.Elab.FixedParamPerm.forallTelescopeImpl✝ perm type k) k

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 paramters.

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.FixedParamPerm.instantiateForall.go xs [] x✝ = pure x✝

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 paramters. Expects enough manifest lambdas to instantiate all fixed parameters, but can handle eta-contracted definitions beyond that.

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.FixedParamPerm.instantiateLambda.go xs [] x✝ = pure x✝

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.

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.FixedParamPerm.pickFixed.go [] x✝ = pure x✝
• Lean.Elab.FixedParamPerm.pickFixed.go ((none, snd) :: perm) x✝ = Lean.Elab.FixedParamPerm.pickFixed.go perm x✝

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.

Equations

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

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 woudn't be fixed parameters.)

Equations

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

partial def Lean.Elab.FixedParamPerm.buildArgs.go {α : Type u_1} (perm : FixedParamPerm) (fixedArgs varyingArgs : Array α) (i j : Nat) (xs : Array α) : Array α

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

Are all fixed parameters a non-reordered prefix?

Equations

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

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.

Equations

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