Documentation

Lean.Meta.ArgsPacker

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.

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

    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
    Instances For

      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.
      Instances For

        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.
        Instances For

          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.
          Instances For

            Helpers for iterated PSum.

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.Meta.ArgsPacker.Mutual.pack (numFuncs : Nat) (domain : Lean.Expr) (fidx : Nat) (arg : 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.

              Equations
              Instances For
                @[irreducible]
                def Lean.Meta.ArgsPacker.Mutual.pack.go (numFuncs : Nat) (fidx : Nat) (arg : Lean.Expr) (i : Nat) (type : Lean.Expr) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  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.
                  Instances For

                    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.
                    Instances For
                      @[irreducible]
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            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.
                            Instances For

                              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.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  The number of functions being packed

                                  Equations
                                  • argsPacker.numFuncs = argsPacker.varNamess.size
                                  Instances For

                                    The arities of the functions being packed

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

                                        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.

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

                                          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
                                          Instances For

                                            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
                                            Instances For

                                              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
                                              Instances For

                                                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.
                                                Instances For

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

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

                                                    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.
                                                    Instances For

                                                      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.
                                                      Instances For