Type inference for LCNF

@[reducible, inline]

abbrev Lean.Compiler.LCNF.InferType.Pure.InferTypeM (α : Type) : Type

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

Equations

• Lean.Compiler.LCNF.InferType.Pure.InferTypeM = ReaderT Lean.LocalContext Lean.Compiler.LCNF.CompilerM

def Lean.Compiler.LCNF.InferType.Pure.getBinderName (fvarId : FVarId) : InferTypeM Name

Equations

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

def Lean.Compiler.LCNF.InferType.Pure.getType (fvarId : FVarId) : InferTypeM Expr

Equations

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

def Lean.Compiler.LCNF.InferType.Pure.mkForallFVars (xs : Array Expr) (type : Expr) : InferTypeM Expr

Equations

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

def Lean.Compiler.LCNF.InferType.Pure.mkForallParams (params : Array (Param Purity.pure)) (type : Expr) : InferTypeM Expr

Equations

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

@[inline]

def Lean.Compiler.LCNF.InferType.Pure.withLocalDecl {α : Type} (binderName : Name) (type : Expr) (binderInfo : BinderInfo) (k : Expr → InferTypeM α) : InferTypeM α

Equations

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

def Lean.Compiler.LCNF.InferType.Pure.inferConstType (declName : Name) (us : List Level) : CompilerM Expr

Equations

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

def Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (value : LitValue) : Expr

Equations

• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.nat val) = Lean.mkConst `Nat
• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.str val) = Lean.mkConst `String
• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.uint8 val) = Lean.mkConst `UInt8
• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.uint16 val) = Lean.mkConst `UInt16
• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.uint32 val) = Lean.mkConst `UInt32
• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.uint64 val) = Lean.mkConst `UInt64
• Lean.Compiler.LCNF.InferType.Pure.inferLitValueType (Lean.Compiler.LCNF.LitValue.usize val) = Lean.mkConst `USize

def Lean.Compiler.LCNF.InferType.Pure.inferArgType (arg : Arg Purity.pure) : InferTypeM Expr

Equations

• Lean.Compiler.LCNF.InferType.Pure.inferArgType Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.erasedExpr
• Lean.Compiler.LCNF.InferType.Pure.inferArgType (Lean.Compiler.LCNF.Arg.type e ⋯) = Lean.Compiler.LCNF.InferType.Pure.inferType e
• Lean.Compiler.LCNF.InferType.Pure.inferArgType (Lean.Compiler.LCNF.Arg.fvar fvarId) = liftM (Lean.Compiler.LCNF.getType fvarId)

partial def Lean.Compiler.LCNF.InferType.Pure.inferType (e : Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.Pure.inferLetValueType (e : LetValue Purity.pure) : InferTypeM Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.InferType.Pure.inferLetValueType Lean.Compiler.LCNF.LetValue.erased = pure Lean.Compiler.LCNF.erasedExpr
• Lean.Compiler.LCNF.InferType.Pure.inferLetValueType (Lean.Compiler.LCNF.LetValue.lit v) = pure (Lean.Compiler.LCNF.InferType.Pure.inferLitValueType v)
• Lean.Compiler.LCNF.InferType.Pure.inferLetValueType (Lean.Compiler.LCNF.LetValue.proj structName idx fvarId ⋯) = Lean.Compiler.LCNF.InferType.Pure.inferProjType structName idx fvarId

def Lean.Compiler.LCNF.InferType.Pure.inferAppTypeCore (fType : Expr) (args : Array (Arg Purity.pure)) : InferTypeM Expr

Equations

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

partial def Lean.Compiler.LCNF.InferType.Pure.inferAppType (e : Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.InferType.Pure.inferProjType (structName : Name) (idx : Nat) (s : FVarId) : InferTypeM Expr

Equations

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

partial def Lean.Compiler.LCNF.InferType.Pure.getLevel? (type : Expr) : InferTypeM (Option Level)

partial def Lean.Compiler.LCNF.InferType.Pure.inferForallType (e : Expr) : InferTypeM Expr

partial def Lean.Compiler.LCNF.InferType.Pure.inferLambdaType (e : Expr) : InferTypeM Expr

def Lean.Compiler.LCNF.inferType (e : Expr) : CompilerM Expr

Equations

• Lean.Compiler.LCNF.inferType e = ReaderT.run (Lean.Compiler.LCNF.InferType.Pure.inferType e) { }

def Lean.Compiler.LCNF.inferAppType {pu : Purity} (fnType : Expr) (args : Array (Arg pu)) : CompilerM Expr

Equations

• Lean.Compiler.LCNF.inferAppType fnType args_2 = ReaderT.run (Lean.Compiler.LCNF.InferType.Pure.inferAppTypeCore fnType args_2) { }
• Lean.Compiler.LCNF.inferAppType fnType args_2 = panicWithPosWithDecl "Lean.Compiler.LCNF.InferType" "Lean.Compiler.LCNF.inferAppType" 258 15 "Infer type for impure unimplemented"

def Lean.Compiler.LCNF.Arg.inferType {pu : Purity} (arg : Arg pu) : CompilerM Expr

Equations

• arg_2.inferType = ReaderT.run (Lean.Compiler.LCNF.InferType.Pure.inferArgType arg_2) { }
• arg_2.inferType = panicWithPosWithDecl "Lean.Compiler.LCNF.InferType" "Lean.Compiler.LCNF.Arg.inferType" 263 15 "Infer type for impure unimplemented"

def Lean.Compiler.LCNF.LetValue.inferType {pu : Purity} (e : LetValue pu) : CompilerM Expr

Equations

• e_2.inferType = ReaderT.run (Lean.Compiler.LCNF.InferType.Pure.inferLetValueType e_2) { }
• e_2.inferType = panicWithPosWithDecl "Lean.Compiler.LCNF.InferType" "Lean.Compiler.LCNF.LetValue.inferType" 268 15 "Infer type for impure unimplemented"

@[irreducible]

def Lean.Compiler.LCNF.Code.inferType {pu : Purity} (code : Code pu) : CompilerM Expr

Equations

• (Lean.Compiler.LCNF.Code.let decl k).inferType = k.inferType
• (Lean.Compiler.LCNF.Code.fun decl k h).inferType = k.inferType
• (Lean.Compiler.LCNF.Code.jp decl k).inferType = k.inferType
• (Lean.Compiler.LCNF.Code.return fvarId).inferType = Lean.Compiler.LCNF.getType fvarId
• (Lean.Compiler.LCNF.Code.jmp fvarId args).inferType = do let __do_lift ← Lean.Compiler.LCNF.getType fvarId ReaderT.run (Lean.Compiler.LCNF.InferType.Pure.inferAppTypeCore __do_lift args) { }
• (Lean.Compiler.LCNF.Code.unreach type).inferType = pure type
• (Lean.Compiler.LCNF.Code.cases c).inferType = pure c.resultType
• code_2.inferType = panicWithPosWithDecl "Lean.Compiler.LCNF.InferType" "Lean.Compiler.LCNF.Code.inferType" 279 15 "Infer type for impure unimplemented"

def Lean.Compiler.LCNF.Code.inferParamType {pu : Purity} (params : Array (Param pu)) (code : Code pu) : CompilerM Expr

Equations

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

def Lean.Compiler.LCNF.Alt.inferType {pu : Purity} (alt : Alt pu) : CompilerM Expr

Equations

• alt.inferType = alt.getCode.inferType

def Lean.Compiler.LCNF.mkAuxLetDecl {pu : Purity} (e : LetValue pu) (prefixName : Name := `_x) : CompilerM (LetDecl pu)

Equations

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

def Lean.Compiler.LCNF.mkForallParams {pu : Purity} (params : Array (Param pu)) (type : Expr) : CompilerM Expr

Equations

• Lean.Compiler.LCNF.mkForallParams params_2 type = ReaderT.run (Lean.Compiler.LCNF.InferType.Pure.mkForallParams params_2 type) { }
• Lean.Compiler.LCNF.mkForallParams params_2 type = panicWithPosWithDecl "Lean.Compiler.LCNF.InferType" "Lean.Compiler.LCNF.mkForallParams" 295 15 "Infer type for impure unimplemented"

def Lean.Compiler.LCNF.mkAuxFunDecl (params : Array (Param Purity.pure)) (code : Code Purity.pure) (prefixName : Name := `_f) : CompilerM (FunDecl Purity.pure)

Equations

• Lean.Compiler.LCNF.mkAuxFunDecl params code prefixName = Lean.Compiler.LCNF.mkAuxFunDeclAux✝ params code prefixName

def Lean.Compiler.LCNF.mkAuxJpDecl {pu : Purity} (params : Array (Param pu)) (code : Code pu) (prefixName : Name := `_jp) : CompilerM (FunDecl pu)

Equations

• Lean.Compiler.LCNF.mkAuxJpDecl params code prefixName = Lean.Compiler.LCNF.mkAuxFunDeclAux✝ params code prefixName

def Lean.Compiler.LCNF.mkAuxJpDecl' {pu : Purity} (param : Param pu) (code : Code pu) (prefixName : Name := `_jp) : CompilerM (FunDecl pu)

Equations

• Lean.Compiler.LCNF.mkAuxJpDecl' param code prefixName = Lean.Compiler.LCNF.mkAuxFunDeclAux✝ #[param] code prefixName

def Lean.Compiler.LCNF.mkCasesResultType {pu : Purity} (alts : Array (Alt pu)) : CompilerM Expr

Equations

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

def Lean.Compiler.LCNF.isErasedCompatible (type : Expr) (predVars : Array Bool := #[]) : 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

• Lean.Compiler.LCNF.isErasedCompatible type predVars = Lean.Compiler.LCNF.isErasedCompatible.go✝ type predVars

partial def Lean.Compiler.LCNF.eqvTypes (a b : Expr) : Bool

Return true if the given LCNF are equivalent. List Nat and (fun x => List x) Nat are both equivalent.