Documentation

Lean.Compiler.LCNF.Check

Note: Type compatibility checking for LCNF #

We used to have a type compatibility relation ≃ for LCNF types. It treated erased types/values as wildcards. Examples:

List Nat ≃ List ◾
(List ◾ → List ◾) ≃ (List Nat → List Bool)

We used this relation to sanity check compiler passes, and detect buggy transformations that broke type compatibility. For example, given an application f a, we would check whether as type as compatible with the type expected by f.

However, the type compatibility relation is not transitive. Example:

List Nat ≃ List ◾, List ◾ ≃ List String, but List Nat and List String are not compatible.

We tried address the issue above by adding casts, which required us to then add cast elimination simplifications, and generated a significant overhead in the code generator.

Here is an example of transformation that would require the insertion of a cast operation.

def foo (g : List A → List A) (a : List B) :=
  fun f (x : List ◾) :=
    let _x.1 := g x
    ...
  let _x.2 := f a
  ...

The code above would not trigger any type compatibility issue, but by inlining f without adding cast operations, we would get the following type incorrect code.

def foo (g : List A → List A) (a : List B) :=
let _x.2 := g a -- Type error
...

We have considered using a reflexive and transitive subtype relation ≺.

A ≺ A
(Nat × Nat) ≺ (Nat × ◾) ≺ (◾ × ◾) ≺ ◾
List Nat ≺ List ◾ ⊀ List String
(List ◾ → List Nat) ≺ (List Bool → List ◾) Note that A ≺ B implies A ≃ B

The subtype relation has better properties, but also has problems. First, when converting to LCNF we would have to add more casts. Example: the function takes a List ◾, but the value has type ◾. Moreover, recall that (List Nat → List Nat) ⊀ (◾ → ◾) forcing us to add many casts operations when moving to the mono phase where we erase type parameters.

Recall that type compatibility and subtype relationships do not help with memory layout. We have that (UInt32 × UInt32) ≺ (◾ × ◾) ≺ ◾ but elements of these types have different runtime representation.

Thus, we have decided to abandon the type compatibility checks and cast operations in LCNF. The only drawback is that we lose the capability of catching simple bugs at compiler passes.

In the future, we can try to add a sanity check flag that instructs the compiler to use the subtype relation in sanity checks and add the necessary casts.

structure Lean.Compiler.LCNF.Check.Context :

jps : Lean.FVarIdSet
Join points that are in scope.
vars : Lean.FVarIdSet
Variables and local functions in scope

Instances For

structure Lean.Compiler.LCNF.Check.State :

all : Lean.FVarIdHashSet
All free variables found

Instances For

@[inline, reducible]

abbrev Lean.Compiler.LCNF.Check.CheckM (α : Type) :

Equations

Lean.Compiler.LCNF.Check.CheckM = ReaderT Lean.Compiler.LCNF.Check.Context (StateRefT' IO.RealWorld Lean.Compiler.LCNF.Check.State Lean.Compiler.LCNF.InferType.InferTypeM)

Instances For

def Lean.Compiler.LCNF.Check.checkTypes :

Lean.Compiler.LCNF.Check.CheckM Bool

Equations

Lean.Compiler.LCNF.Check.checkTypes = do let __do_lift ← liftM Lean.Compiler.LCNF.getConfig pure __do_lift.checkTypes

Instances For

def Lean.Compiler.LCNF.Check.checkFVar (fvarId : Lean.FVarId) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.isCtorParam (f : Lean.Expr) (i : Nat) :

Lean.CoreM Bool

Return true f is a constructor and i is less than its number of parameters.

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.checkAppArgs (f : Lean.Expr) (args : Array Lean.Compiler.LCNF.Arg) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.checkLetValue (e : Lean.Compiler.LCNF.LetValue) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.checkJpInScope (jp : Lean.FVarId) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.checkParam (param : Lean.Compiler.LCNF.Param) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.checkParams (params : Array Lean.Compiler.LCNF.Param) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

Lean.Compiler.LCNF.Check.checkParams params = Array.forM Lean.Compiler.LCNF.Check.checkParam params 0 (Array.size params)

Instances For

def Lean.Compiler.LCNF.Check.checkLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

def Lean.Compiler.LCNF.Check.addFVarId (fvarId : Lean.FVarId) :

Lean.Compiler.LCNF.Check.CheckM Unit

Equations

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

Instances For

@[inline]

def Lean.Compiler.LCNF.Check.withFVarId {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Check.CheckM α) :

Lean.Compiler.LCNF.Check.CheckM α

Equations

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

Instances For

@[inline]

def Lean.Compiler.LCNF.Check.withJp {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.Check.CheckM α) :

Lean.Compiler.LCNF.Check.CheckM α

Equations

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

Instances For

@[inline]

def Lean.Compiler.LCNF.Check.withParams {α : Type} (params : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.Check.CheckM α) :

Lean.Compiler.LCNF.Check.CheckM α

Equations

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

Instances For

partial def Lean.Compiler.LCNF.Check.checkFunDeclCore (declName : Lake.Name) (params : Array Lean.Compiler.LCNF.Param) (type : Lean.Expr) (value : Lean.Compiler.LCNF.Code) :

Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.checkFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) :

Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.checkCases (c : Lean.Compiler.LCNF.Cases) :

Lean.Compiler.LCNF.Check.CheckM Unit

partial def Lean.Compiler.LCNF.Check.check (code : Lean.Compiler.LCNF.Code) :

Lean.Compiler.LCNF.Check.CheckM Unit

def Lean.Compiler.LCNF.Check.run {α : Type} (x : Lean.Compiler.LCNF.Check.CheckM α) :

Lean.Compiler.LCNF.CompilerM α

Equations

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

Instances For

def Lean.Compiler.LCNF.Decl.check (decl : Lean.Compiler.LCNF.Decl) :

Lean.Compiler.LCNF.CompilerM Unit

Equations

Lean.Compiler.LCNF.Decl.check decl = Lean.Compiler.LCNF.Check.run (Lean.Compiler.LCNF.Check.checkFunDeclCore decl.name decl.params decl.type decl.value)

Instances For

def Lean.Compiler.LCNF.checkDeadLocalDecls (decls : Array Lean.Compiler.LCNF.Decl) :

Lean.Compiler.LCNF.CompilerM Unit

Check whether every local declaration in the local context is used in one of given decls.

Equations

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

Instances For

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar (fvarId : Lean.FVarId) :

StateM Lean.FVarIdHashSet Unit

Equations

Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar fvarId = modify fun (x : Lean.FVarIdHashSet) => Lean.HashSet.insert x fvarId

Instances For

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam (param : Lean.Compiler.LCNF.Param) :

StateM Lean.FVarIdHashSet Unit

Equations

Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam param = Lean.Compiler.LCNF.checkDeadLocalDecls.visitFVar param.fvarId

Instances For

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams (params : Array Lean.Compiler.LCNF.Param) :

StateM Lean.FVarIdHashSet Unit

Equations

Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams params = Array.forM Lean.Compiler.LCNF.checkDeadLocalDecls.visitParam params 0 (Array.size params)

Instances For

partial def Lean.Compiler.LCNF.checkDeadLocalDecls.visitCode (code : Lean.Compiler.LCNF.Code) :

StateM Lean.FVarIdHashSet Unit

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl (decl : Lean.Compiler.LCNF.Decl) :

StateM Lean.FVarIdHashSet Unit

Equations

Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl decl = do Lean.Compiler.LCNF.checkDeadLocalDecls.visitParams decl.params Lean.Compiler.LCNF.checkDeadLocalDecls.visitCode decl.value

Instances For

def Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecls (decls : Array Lean.Compiler.LCNF.Decl) :

StateM Lean.FVarIdHashSet Unit

Equations

Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecls decls = Array.forM Lean.Compiler.LCNF.checkDeadLocalDecls.visitDecl decls 0 (Array.size decls)

Instances For