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 Lean.Expr) : Lean.MetaM Lean.Expr

def Lean.Meta.ArgsPacker.Unary.pack (type : Lean.Expr) (args : Array Lean.Expr) : Lean.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.

Equations

• Lean.Meta.ArgsPacker.Unary.pack type args = Lean.Meta.ArgsPacker.Unary.pack.go args 0 type

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

def Lean.Meta.ArgsPacker.Unary.unpack (arity : Nat) (e : Lean.Expr) : Lean.MetaM (Array Lean.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 Lean.Name) (type : Lean.Expr) : Lean.MetaM Lean.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 Lean.Name) (e : Lean.Expr) : Lean.MetaM Lean.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].

Equations

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

Helpers for iterated PSum.

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

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

def Lean.Meta.ArgsPacker.Mutual.pack (numFuncs : Nat) (domain : Lean.Expr) (fidx : Nat) (arg : Lean.Expr) : Lean.MetaM Lean.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 : Lean.Expr) (i : Nat) (type : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

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

def Lean.Meta.ArgsPacker.Mutual.unpack (numFuncs : Nat) (expr : Lean.Expr) : Lean.MetaM (Nat × Lean.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.

Equations

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

def Lean.Meta.ArgsPacker.Mutual.mkCodomain (types : Array Lean.Expr) (x : Lean.Expr) : Lean.MetaM Lean.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.

Equations

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

@[irreducible]

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

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

Equations

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

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

def Lean.Meta.ArgsPacker.Mutual.uncurry (es : Array Lean.Expr) : Lean.MetaM Lean.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.uncurryND (es : Array Lean.Expr) : Lean.MetaM Lean.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 : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Equations

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

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

The number of functions being packed

Equations

• argsPacker.numFuncs = argsPacker.varNamess.size

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

The arities of the functions being packed

Equations

• argsPacker.arities = Array.map (fun (x : Array Lean.Name) => x.size) argsPacker.varNamess

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

def Lean.Meta.ArgsPacker.unpack (argsPacker : Lean.Meta.ArgsPacker) (e : Lean.Expr) : Lean.MetaM (Nat × Array Lean.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 projectinos.

def Lean.Meta.ArgsPacker.uncurryType (argsPacker : Lean.Meta.ArgsPacker) (types : Array Lean.Expr) : Lean.MetaM Lean.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 : Lean.Meta.ArgsPacker) (es : Array Lean.Expr) : Lean.MetaM Lean.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]

Equations

• argsPacker.uncurry es = do let unary ← Array.mapM id (argsPacker.varNamess.zipWith es Lean.Meta.ArgsPacker.Unary.uncurry) Lean.Meta.ArgsPacker.Mutual.uncurry unary

def Lean.Meta.ArgsPacker.uncurryND (argsPacker : Lean.Meta.ArgsPacker) (es : Array Lean.Expr) : Lean.MetaM Lean.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 : Lean.Meta.ArgsPacker) (e : Lean.Expr) (i : Nat) : Lean.MetaM Lean.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 : Lean.Meta.ArgsPacker) (t : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

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

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

Equations

• argsPacker.curryType t = do let unary ← Lean.Meta.ArgsPacker.Mutual.curryType argsPacker.numFuncs t Array.mapM id (argsPacker.varNamess.zipWith unary Lean.Meta.ArgsPacker.Unary.curryType✝)

def Lean.Meta.ArgsPacker.curry (argsPacker : Lean.Meta.ArgsPacker) (e : Lean.Expr) : Lean.MetaM Lean.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)])

Equations

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

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

Given value : type where type is

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

brings m1 : a → b → s and m2 : c → d → s 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

Equations

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