Documentation

Lean.Compiler.LCNF.InferType

Type inference for LCNF #

source
@[inline]
abbrev Lean.Compiler.LCNF.InferType.InferTypeM (α : Type) :
Type

We use a regular local context to store temporary local declarations created during type inference.

Equations
source
def Lean.Compiler.LCNF.InferType.getBinderName (fvarId : Lean.FVarId) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Name
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.InferType.getType (fvarId : Lean.FVarId) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.InferType.mkForallFVars (xs : Array Lean.Expr) (type : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.InferType.mkForallParams (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Compiler.LCNF.InferType.withLocalDecl {α : Type} (binderName : Lean.Name) (type : Lean.Expr) (binderInfo : Lean.BinderInfo) (k : Lean.Expr → Lean.Compiler.LCNF.InferType.InferTypeM α) :
Lean.Compiler.LCNF.InferType.InferTypeM α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.InferType.inferConstType (declName : Lean.Name) (us : List Lean.Level) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Compiler.LCNF.InferType.inferType (e : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.inferAppTypeCore (f : Lean.Expr) (args : Array Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.inferAppType (e : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.inferProjType (structName : Lean.Name) (idx : Nat) (s : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.getLevel? (type : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM (Option Lean.Level)
source
partial def Lean.Compiler.LCNF.InferType.inferForallType (e : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.inferForallType.go (e : Lean.Expr) (fvars : Array Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.inferLambdaType (e : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
partial def Lean.Compiler.LCNF.InferType.inferLambdaType.go (e : Lean.Expr) (fvars : Array Lean.Expr) (all : Array Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Lean.Expr
source
def Lean.Compiler.LCNF.inferType (e : Lean.Expr) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.getLevel (type : Lean.Expr) :
Lean.Compiler.LCNF.CompilerM Lean.Level
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkLcCast (e : Lean.Expr) (expectedType : Lean.Expr) :
Lean.Compiler.LCNF.CompilerM Lean.Expr

Create lcCast expectedType e : expectedType

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.Code.inferType (code : Lean.Compiler.LCNF.Code) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
source
def Lean.Compiler.LCNF.Code.inferParamType (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.AltCore.inferType (alt : Lean.Compiler.LCNF.Alt) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
source
def Lean.Compiler.LCNF.mkAuxLetDecl (e : Lean.Expr) (prefixName : optParam Lean.Name (Lean.Name.mkStr1 "_x")) :
Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl
Equations
source
def Lean.Compiler.LCNF.mkForallParams (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkAuxFunDecl (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : optParam Lean.Name (Lean.Name.mkStr1 "_f")) :
Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkAuxJpDecl (params : Array Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : optParam Lean.Name (Lean.Name.mkStr1 "_jp")) :
Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
Equations
source
def Lean.Compiler.LCNF.mkAuxJpDecl' (param : Lean.Compiler.LCNF.Param) (code : Lean.Compiler.LCNF.Code) (prefixName : optParam Lean.Name (Lean.Name.mkStr1 "_jp")) :
Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
Equations
source
def Lean.Compiler.LCNF.instantiateForall (type : Lean.Expr) (params : Array Lean.Compiler.LCNF.Param) :
Lean.CoreM Lean.Expr
Equations
source
def Lean.Compiler.LCNF.instantiateForall.go (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) (i : Nat) :
Lean.CoreM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.mkCasesResultType (alts : Array Lean.Compiler.LCNF.Alt) :
Lean.Compiler.LCNF.CompilerM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.isErasedCompatible (type : Lean.Expr) (predVars : optParam (Array Bool) #[]) :
Lean.Compiler.LCNF.CompilerM Bool

Return true if type should be erased. See item 1 in the note above where x ◾ ◾ is a proposition and should be erased when the universe level parameter is set to 0.

Remark: predVars is a bitmask that indicates whether de-bruijn variables are predicates or not. That is, #i is a predicate if predVars[predVars.size - i - 1] = true

Equations
source
partial def Lean.Compiler.LCNF.isErasedCompatible.go (type : Lean.Expr) (predVars : Array Bool) :
Lean.Compiler.LCNF.CompilerM Bool
source
partial def Lean.Compiler.LCNF.compatibleTypesQuick (a : Lean.Expr) (b : Lean.Expr) :
Bool

Quick check for compatibleTypes. It is not monadic, but it is incomplete because it does not eta-expand type formers. See comment at compatibleTypes.

Remark: if the result is true, then a and b are indeed compatible. If it is false, we must use the full-check.

source
partial def Lean.Compiler.LCNF.InferType.compatibleTypesFull (a : Lean.Expr) (b : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Bool

Complete check for compatibleTypes. It eta-expands type formers. See comment at compatibleTypes.

source
def Lean.Compiler.LCNF.InferType.compatibleTypesFull.etaExpand? (e : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM (Option Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Compiler.LCNF.InferType.compatibleTypes (a : Lean.Expr) (b : Lean.Expr) :
Lean.Compiler.LCNF.InferType.InferTypeM Bool

Return true if the LCNF types a and b are compatible.

Remark: a and b can be type formers (e.g., List, or fun (α : Type) => Nat → Nat × α)

Remark: We may need to eta-expand type formers to establish whether they are compatible or not. For example, suppose we have

fun (x : B) => Id B ◾ ◾
Id B ◾

We must eta-expand Id B ◾ to fun (x : B) => Id B ◾ x. Note that, we use x instead of ◾ to make the implementation simpler and skip the check whether B is a type former type. However, this simplification should not affect correctness since ◾ is compatible with everything.

Remark: see comment at isErasedCompatible.

Remark: because of "erasure confusion" see note above, we assume ◾ (aka lcErasure) is compatible with everything. This is a simplification. We used to use isErasedCompatible, but this only address item 1. For item 2, we would have to modify the toLCNFType function and make sure a type former is erased if the expected type is not always a type former (see S.mk type and example in the note above).

Equations
source
def Lean.Compiler.LCNF.compatibleTypes (a : Lean.Expr) (b : Lean.Expr) :
Lean.Compiler.LCNF.CompilerM Bool

Return true if the LCNF types a and b are compatible.

Remark: a and b can be type formers (e.g., List, or fun (α : Type) => Nat → Nat × α)

Remark: We may need to eta-expand type formers to establish whether they are compatible or not. For example, suppose we have

fun (x : B) => Id B ◾ ◾
Id B ◾

We must eta-expand Id B ◾ to fun (x : B) => Id B ◾ x. Note that, we use x instead of ◾ to make the implementation simpler and skip the check whether B is a type former type. However, this simplification should not affect correctness since ◾ is compatible with everything.

Remark: see comment at isErasedCompatible.

Remark: because of "erasure confusion" see note above, we assume ◾ (aka lcErasure) is compatible with everything. This is a simplification. We used to use isErasedCompatible, but this only address item 1. For item 2, we would have to modify the toLCNFType function and make sure a type former is erased if the expected type is not always a type former (see S.mk type and example in the note above).

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