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

Equations

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

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.

Equations

• Lean.Meta.ArgsPacker.Unary.pack type args = if args.isEmpty = true then Lean.mkConst `Unit.unit else Lean.Meta.ArgsPacker.Unary.pack.go args 0 type

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.

Equations

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

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

Equations

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

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

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

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

Equations

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

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.

Equations

• Lean.Meta.ArgsPacker.Mutual.pack numFuncs domain fidx arg = Lean.Meta.ArgsPacker.Mutual.pack.go numFuncs fidx arg 0 domain

@[irreducible]

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

Equations

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

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.

Equations

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

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.

Equations

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

@[irreducible]

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

Equations

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

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

Equations

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

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

Equations

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

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])

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

The number of functions being packed

Equations

• argsPacker.numFuncs = argsPacker.varNamess.size

def Lean.Meta.ArgsPacker.arities (argsPacker : 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.onlyOneUnary (argsPacker : ArgsPacker) : Bool

Equations

• argsPacker.onlyOneUnary = (decide (argsPacker.varNamess.size = 1) && decide (argsPacker.varNamess[0]!.size = 1))

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

Equations

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

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.

Equations

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

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]

Equations

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

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]

Equations

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

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

Equations

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

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

Equations

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

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)])

Equations

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

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]

Equations

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

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)])

Equations

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

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

Equations

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