Documentation

Lean.Compiler.Util

def Lean.Compiler.neutralExpr :

Equations

Lean.Compiler.neutralExpr = Lean.mkConst `_neutral

def Lean.Compiler.unreachableExpr :

Equations

Lean.Compiler.unreachableExpr = Lean.mkConst `_unreachable

def Lean.Compiler.objectType :

Equations

Lean.Compiler.objectType = Lean.mkConst `_obj

def Lean.Compiler.voidType :

Equations

Lean.Compiler.voidType = Lean.mkConst `_void

def Lean.Compiler.mkLcProof (pred : Lean.Expr) :

Equations

Lean.Compiler.mkLcProof pred = Lean.mkApp (Lean.mkConst `lcProof) pred

structure Lean.Compiler.atMostOnce.AtMostOnceData :

Type

found : Bool
result : Bool

noncomputable def Lean.Compiler.atMostOnce.Visitor :

Type

Equations

Lean.Compiler.atMostOnce.Visitor = (Lean.Compiler.atMostOnce.AtMostOnceData → Lean.Compiler.atMostOnce.AtMostOnceData)

@[inline]

def Lean.Compiler.atMostOnce.seq (f : Lean.Compiler.atMostOnce.Visitor) (g : Lean.Compiler.atMostOnce.Visitor) :

Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.seq f g d = match f d with | { found := found, result := false } => { found := found, result := false } | other => g other

instance Lean.Compiler.atMostOnce.instAndThenVisitor :

AndThen Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.instAndThenVisitor = { andThen := fun a b => Lean.Compiler.atMostOnce.seq a (b ()) }

@[inline]

def Lean.Compiler.atMostOnce.skip :

Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.skip = id

@[inline]

def Lean.Compiler.atMostOnce.visitFVar (x : Lean.FVarId) (y : Lean.FVarId) :

Lean.Compiler.atMostOnce.Visitor

Equations

Lean.Compiler.atMostOnce.visitFVar x y x = match x with | d@h:{ found := x, result := false } => d | { found := false, result := true } => { found := x == y, result := true } | { found := true, result := true } => { found := true, result := x != y }

def Lean.Compiler.atMostOnce.visit (x : Lean.FVarId) :

Lean.Expr → Lean.Compiler.atMostOnce.Visitor

def Lean.Compiler.atMostOnce (e : Lean.Expr) (x : Lean.FVarId) :

Equations

Lean.Compiler.atMostOnce e x = let x := Lean.Compiler.atMostOnce.visit x e { found := false, result := true }; match x with | { found := x, result := result } => result

def Lean.Compiler.mkEagerLambdaLiftingName (n : Lean.Name) (idx : Nat) :

Equations

Lean.Compiler.mkEagerLambdaLiftingName n idx = Lean.Name.mkStr n ("_elambda_" ++ toString idx)

def Lean.Compiler.isEagerLambdaLiftingName :

Lean.Name → Bool

def Lean.Compiler.checkIsDefinition (env : Lean.Environment) (n : Lean.Name) :

Except String Unit

Equations

Lean.Compiler.checkIsDefinition env n = match Lean.Environment.find? env n with | some (Lean.ConstantInfo.defnInfo x) => Except.ok () | some (Lean.ConstantInfo.opaqueInfo x) => Except.ok () | none => Except.error (toString "unknow declaration '" ++ toString n ++ toString "'") | x => Except.error (toString "declaration is not a definition '" ++ toString n ++ toString "'")

def Lean.Compiler.mkUnsafeRecName (declName : Lean.Name) :

Equations

Lean.Compiler.mkUnsafeRecName declName = Lean.Name.mkStr declName "_unsafe_rec"

def Lean.Compiler.isUnsafeRecName? :

Lean.Name → Option Lean.Name

Equations

Lean.Compiler.isUnsafeRecName? x = match x with | Lean.Name.str n "_unsafe_rec" x => some n | x => none