This module implements the equivalence between the types

(x : a) → (y : b) → r1[x,y],  (x : c) → (y : d) → r2[x,y]

(the “curried form”) and

(p : (a ⊗' b) ⊕' (c ⊗' d)) → r'[p]

where

r'[p] = match p with | inl (x,y) => r1[x,y] | inr (x,y) => r2[x,y]

(the “packed form”).

The ArgsPacker data structure (defined in Lean.Meta.ArgsPacker.Basic for fewer module dependencies) contains necessary information to pack and unpack reliably. Care is taken that the code is not confused even if the user intentionally uses a PSigma or PSum type, e.g. as the ast parameter. Additionally, “good” variable names are stored here.

It is used in the translation of a possibly mutual, possibly n-ary recursive function to a single unary function, which can then be made non-recursive using WellFounded.fix. Additional users are the GuessLex and FunInd modules, which also have to deal with this encoding.

Ideally, only this module has to know the precise encoding using PSigma and PSigma; all other modules should only use the high-level functions at the bottom of this file. At the same time, this module should be independent of WF-specific data structures (like EqnInfos).

The subnamespaces Unary and Mutual take care of PSigma resp. PSum packing, and are intended to be local to this module.

Helpers for iterated PSigma.

def Lean.Meta.ArgsPacker.Unary.packType (xs : Array Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.Unary.pack (type : Expr) (args : Array Expr) : Expr

Create a unary application by packing the given arguments using PSigma.mk. The type should be the expected type of the packed argument, as created with packType.

partial def Lean.Meta.ArgsPacker.Unary.pack.go (args : Array Expr) (i : Nat) (type : Expr) : Expr

def Lean.Meta.ArgsPacker.Unary.unpack (arity : Nat) (e : Expr) : Option (Array Expr)

Unpacks a unary packed argument created with Unary.pack.

Throws an error if the expression is not of that form.

def Lean.Meta.ArgsPacker.Unary.uncurryType (varNames : Array Name) (type : Expr) : MetaM Expr

Given a type t of the form (x : A) → (y : B[x]) → … → (z : D[x,y]) → R[x,y,z] returns the curried type (x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2].

def Lean.Meta.ArgsPacker.Unary.uncurry (varNames : Array Name) (e : Expr) : MetaM Expr

Given expression e of type (x : A) → (y : B[x]) → … → (z : D[x,y]) → R[x,y,z] returns an expression of type (x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2].

Helpers for iterated PSum.

def Lean.Meta.ArgsPacker.Mutual.packType (ds : Array Expr) : MetaM Expr

Given types #[t₁, t₂,…], returns the type t₁ ⊕' t₂ ….

def Lean.Meta.ArgsPacker.Mutual.pack (numFuncs : Nat) (domain : Expr) (fidx : Nat) (arg : Expr) : MetaM Expr

If arg is the argument to the fidxth of the argsPacker.numFuncs in the recursive group, then mk packs that argument in PSum.inl and PSum.inr constructors to create the mutual-packed argument of type domain.

@[irreducible]

def Lean.Meta.ArgsPacker.Mutual.pack.go (numFuncs fidx : Nat) (arg : Expr) (i : Nat) (type : Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.Mutual.unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr)

Unpacks a mutually packed argument created with Mutual.mk returning the argument and function index.

Throws an error if the expression is not of that form.

def Lean.Meta.ArgsPacker.Mutual.mkCodomain (types : Array Expr) (x : Expr) : MetaM Expr

Given unary types (x : Aᵢ) → Rᵢ[x], and (x : A₁ ⊕ A₂ …), calculate the packed codomain

match x with | inl x₁ => R₁[x₁] | inr x₂ => R₂[x₂] | …

This function assumes (and does not check) that Rᵢ all have the same level.

@[irreducible]

def Lean.Meta.ArgsPacker.Mutual.mkCodomain.go (types : Array Expr) (u : Level) (x : Expr) (i : Nat) : MetaM Expr

def Lean.Meta.ArgsPacker.Mutual.uncurryType (types : Array Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.Mutual.uncurryTypeND (types : Array Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.Mutual.uncurryWithType (resultType : Expr) (es : Array Expr) : MetaM Expr

Given unary expressions e₁, e₂ with types (x : A) → R₁[x] and (z : C) → R₂[z], returns an expression of type

(x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z])

def Lean.Meta.ArgsPacker.Mutual.uncurry (es : Array Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.Mutual.uncurryND (es : Array Expr) : MetaM Expr

Given unary expressions e₁, e₂ with types (x : A) → R and (z : C) → R, returns an expression of type

(x : A ⊕' C) → R

def Lean.Meta.ArgsPacker.Mutual.curryType (n : Nat) (type : Expr) : MetaM (Array Expr)

def Lean.Meta.ArgsPacker.numFuncs (argsPacker : ArgsPacker) : Nat

The number of functions being packed

def Lean.Meta.ArgsPacker.arities (argsPacker : ArgsPacker) : Array Nat

The arities of the functions being packed

def Lean.Meta.ArgsPacker.onlyOneUnary (argsPacker : ArgsPacker) : Bool

def Lean.Meta.ArgsPacker.pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.unpack (argsPacker : ArgsPacker) (e : Expr) : Option (Nat × Array Expr)

Given the packed argument of a (possibly) mutual and (possibly) nary call, return the function index that is called and the arguments individually.

We expect precisely the expressions produced by pack, with manifest PSum.inr, PSum.inl and PSigma.mk constructors, and thus take them apart rather than using projections.

def Lean.Meta.ArgsPacker.uncurryType (argsPacker : ArgsPacker) (types : Array Expr) : MetaM Expr

Given types (x : A) → (y : B[x]) → R₁[x,y] and (z : C) → R₂[z], returns the type uncurried type

(x : (A ⊗ B) ⊕ C) → (match x with | .inl (x, y) => R₁[x,y] | .inr R₂[z]

def Lean.Meta.ArgsPacker.uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr

Given expressions e₁, e₂ with types (x : A) → (y : B[x]) → R₁[x,y] and (z : C) → R₂[z], returns an expression of type

(x : (A ⊗ B) ⊕ C) → (match x with | .inl (x, y) => R₁[x,y] | .inr R₂[z]

def Lean.Meta.ArgsPacker.uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr

def Lean.Meta.ArgsPacker.uncurryND (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr

Given expressions e₁, e₂ with types (x : A) → (y : B[x]) → R and (z : C) → R, returns an expression of type

(x : (A ⊗ B) ⊕ C) → R

def Lean.Meta.ArgsPacker.curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr

Given expression e of type (x : a₁ ⊗' b₁ ⊕' a₂ ⊗' d₂ …) → e[x], uncurries the expression and projects to the ith function of type,

((x : aᵢ) → (y : bᵢ) → e[.inr….inl (x,y)])

def Lean.Meta.ArgsPacker.curryType (argsPacker : ArgsPacker) (t : Expr) : MetaM (Array Expr)

Given type (x : a ⊗' b ⊕' c ⊗' d) → R (dependent), return types

#[(x: a) → (y : b) → R, (x : c) → (y : d) → R]

def Lean.Meta.ArgsPacker.curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr

Given expression e of type (x : a ⊗' b ⊕' c ⊗' d) → e[x], wraps that expression to produce an expression of the isomorphic type

((x: a) → (y : b) → e[.inl (x,y)]) ∧ ((x : c) → (y : d) → e[.inr (x,y)])

def Lean.Meta.ArgsPacker.curryParam {α : Type} (argsPacker : ArgsPacker) (value type : Expr) (k : Array Expr → Expr → Expr → MetaM α) : MetaM α

Given value : type where type is

(m : (x : a ⊗' b ⊕' c ⊗' d) → s[x]) → r[m]

brings m1 : (x : a) → (y : b) → s[.inl ⟨x,y⟩] and m2 : (x : c) → (y : d) → s[.inr ⟨x,y⟩] into scope. The continuation receives

• FVars for m1…
• e[m]
• t[m]

where m : a ⊗' b ⊕' c ⊗' d → s is the uncurried form of m1 and m2.

The variable names m1 and m2 are taken from the parameter name in t, with numbers added unless numFuns = 1