Documentation

Lean.Compiler.LCNF.Basic

Lean Compiler Normal Form (LCNF) #

It is based on the A-normal form, and the approach described in the paper Compiling without continuations.

inductive Lean.Compiler.LCNF.Purity :

This type is used to index the fundamental LCNF IR data structures. Depending on its value different constructors are available for the different semantic phases of LCNF.

Notably in order to save memory we never index the IR types over Purity. Instead the type is parametrized by the phase and the individual constructors might carry a proof (that will be erased) that they are only allowed in a certain phase.

pure : Purity
The code we are acting on is still pure, things like reordering up to value dependencies are acceptable.
impure : Purity
The code we are acting on is to be considered generally impure, doing reorderings is potentially no longer legal.

Instances For

def Lean.Compiler.LCNF.instInhabitedPurity.default :

Equations

Lean.Compiler.LCNF.instInhabitedPurity.default = Lean.Compiler.LCNF.Purity.pure

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedPurity :

Inhabited Purity

Equations

Lean.Compiler.LCNF.instInhabitedPurity = { default := Lean.Compiler.LCNF.instInhabitedPurity.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instDecidableEqPurity :

DecidableEq Purity

Equations

Lean.Compiler.LCNF.instDecidableEqPurity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Compiler.LCNF.instHashablePurity.hash :

Purity → UInt64

Equations

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instHashablePurity :

Hashable Purity

Equations

Lean.Compiler.LCNF.instHashablePurity = { hash := Lean.Compiler.LCNF.instHashablePurity.hash }

@[instance_reducible]

instance Lean.Compiler.LCNF.instToStringPurity :

ToString Purity

Equations

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

@[inline]

def Lean.Compiler.LCNF.Purity.withAssertPurity {α : Sort u_1} [Inhabited α] (is should : Purity) (k : is = should → α) :

α

Equations

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

Instances For

def Lean.Compiler.LCNF.tacticPurity_tac :

Equations

Lean.Compiler.LCNF.tacticPurity_tac = Lean.ParserDescr.node `Lean.Compiler.LCNF.tacticPurity_tac 1024 (Lean.ParserDescr.nonReservedSymbol "purity_tac" false)

Instances For

structure Lean.Compiler.LCNF.Param (pu : Purity) :

fvarId : FVarId
binderName : Name
type : Expr
borrow : Bool

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedParam {a✝ : Purity} :

Inhabited (Param a✝)

Equations

Lean.Compiler.LCNF.instInhabitedParam = { default := Lean.Compiler.LCNF.instInhabitedParam.default }

def Lean.Compiler.LCNF.instInhabitedParam.default {a✝ : Purity} :

Param a✝

Equations

Lean.Compiler.LCNF.instInhabitedParam.default = { fvarId := default, binderName := default, type := default, borrow := default }

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqParam {pu✝ : Purity} :

BEq (Param pu✝)

Equations

Lean.Compiler.LCNF.instBEqParam = { beq := Lean.Compiler.LCNF.instBEqParam.beq }

def Lean.Compiler.LCNF.instBEqParam.beq {pu✝ : Purity} :

Param pu✝ → Param pu✝ → Bool

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.instBEqParam.beq x✝¹ x✝ = false

Instances For

def Lean.Compiler.LCNF.Param.toExpr {pu : Purity} (p : Param pu) :

Equations

p.toExpr = Lean.Expr.fvar p.fvarId

Instances For

inductive Lean.Compiler.LCNF.LitValue :

nat (val : Nat) : LitValue
str (val : String) : LitValue
uint8 (val : UInt8) : LitValue
uint16 (val : UInt16) : LitValue
uint32 (val : UInt32) : LitValue
uint64 (val : UInt64) : LitValue
usize (val : UInt64) : LitValue

Instances For

def Lean.Compiler.LCNF.instInhabitedLitValue.default :

Equations

Lean.Compiler.LCNF.instInhabitedLitValue.default = Lean.Compiler.LCNF.LitValue.nat default

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedLitValue :

Inhabited LitValue

Equations

Lean.Compiler.LCNF.instInhabitedLitValue = { default := Lean.Compiler.LCNF.instInhabitedLitValue.default }

def Lean.Compiler.LCNF.instBEqLitValue.beq :

LitValue → LitValue → Bool

Equations

Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.nat a) (Lean.Compiler.LCNF.LitValue.nat b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.str a) (Lean.Compiler.LCNF.LitValue.str b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.uint8 a) (Lean.Compiler.LCNF.LitValue.uint8 b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.uint16 a) (Lean.Compiler.LCNF.LitValue.uint16 b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.uint32 a) (Lean.Compiler.LCNF.LitValue.uint32 b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.uint64 a) (Lean.Compiler.LCNF.LitValue.uint64 b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq (Lean.Compiler.LCNF.LitValue.usize a) (Lean.Compiler.LCNF.LitValue.usize b) = (a == b)
Lean.Compiler.LCNF.instBEqLitValue.beq x✝¹ x✝ = false

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqLitValue :

Equations

Lean.Compiler.LCNF.instBEqLitValue = { beq := Lean.Compiler.LCNF.instBEqLitValue.beq }

@[instance_reducible]

instance Lean.Compiler.LCNF.instHashableLitValue :

Hashable LitValue

Equations

Lean.Compiler.LCNF.instHashableLitValue = { hash := Lean.Compiler.LCNF.instHashableLitValue.hash }

def Lean.Compiler.LCNF.LitValue.toExpr :

LitValue → Expr

Equations

(Lean.Compiler.LCNF.LitValue.nat a).toExpr = Lean.Expr.lit (Lean.Literal.natVal a)
(Lean.Compiler.LCNF.LitValue.str a).toExpr = Lean.Expr.lit (Lean.Literal.strVal a)
(Lean.Compiler.LCNF.LitValue.uint8 a).toExpr = (Lean.Expr.const `UInt8.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal a.toNat))
(Lean.Compiler.LCNF.LitValue.uint16 a).toExpr = (Lean.Expr.const `UInt16.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal a.toNat))
(Lean.Compiler.LCNF.LitValue.uint32 a).toExpr = (Lean.Expr.const `UInt32.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal a.toNat))
(Lean.Compiler.LCNF.LitValue.uint64 a).toExpr = (Lean.Expr.const `UInt64.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal a.toNat))
(Lean.Compiler.LCNF.LitValue.usize a).toExpr = (Lean.Expr.const `USize.ofNat []).app (Lean.Expr.lit (Lean.Literal.natVal a.toNat))

Instances For

def Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit (e : Expr) (n : Nat) :

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit (Lean.Expr.const `UInt8 []) n = Lean.Compiler.LCNF.LitValue.uint8 n.toUInt8
Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit (Lean.Expr.const `UInt16 []) n = Lean.Compiler.LCNF.LitValue.uint16 n.toUInt16
Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit (Lean.Expr.const `UInt32 []) n = Lean.Compiler.LCNF.LitValue.uint32 n.toUInt32
Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit (Lean.Expr.const `UInt64 []) n = Lean.Compiler.LCNF.LitValue.uint64 n.toUInt64
Lean.Compiler.LCNF.LitValue.impureTypeScalarNumLit (Lean.Expr.const `USize []) n = Lean.Compiler.LCNF.LitValue.usize n.toUInt64

Instances For

inductive Lean.Compiler.LCNF.Arg (pu : Purity) :

erased {pu : Purity} : Arg pu
fvar {pu : Purity} (fvarId : FVarId) : Arg pu
type {pu : Purity} (expr : Expr) (h : pu = Purity.pure := by purity_tac) : Arg pu

Instances For

def Lean.Compiler.LCNF.instInhabitedArg.default {a✝ : Purity} :

Arg a✝

Equations

Lean.Compiler.LCNF.instInhabitedArg.default = Lean.Compiler.LCNF.Arg.erased

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedArg {a✝ : Purity} :

Inhabited (Arg a✝)

Equations

Lean.Compiler.LCNF.instInhabitedArg = { default := Lean.Compiler.LCNF.instInhabitedArg.default }

def Lean.Compiler.LCNF.instBEqArg.beq {pu✝ : Purity} :

Arg pu✝ → Arg pu✝ → Bool

Equations

Lean.Compiler.LCNF.instBEqArg.beq Lean.Compiler.LCNF.Arg.erased Lean.Compiler.LCNF.Arg.erased = true
Lean.Compiler.LCNF.instBEqArg.beq (Lean.Compiler.LCNF.Arg.fvar a) (Lean.Compiler.LCNF.Arg.fvar b) = (a == b)
Lean.Compiler.LCNF.instBEqArg.beq (Lean.Compiler.LCNF.Arg.type a a_1) (Lean.Compiler.LCNF.Arg.type b b_1) = (a == b)
Lean.Compiler.LCNF.instBEqArg.beq x✝¹ x✝ = false

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqArg {pu✝ : Purity} :

BEq (Arg pu✝)

Equations

Lean.Compiler.LCNF.instBEqArg = { beq := Lean.Compiler.LCNF.instBEqArg.beq }

def Lean.Compiler.LCNF.instHashableArg.hash {pu✝ : Purity} :

Arg pu✝ → UInt64

Equations

Lean.Compiler.LCNF.instHashableArg.hash Lean.Compiler.LCNF.Arg.erased = 0
Lean.Compiler.LCNF.instHashableArg.hash (Lean.Compiler.LCNF.Arg.fvar a) = mixHash 1 (hash a)
Lean.Compiler.LCNF.instHashableArg.hash (Lean.Compiler.LCNF.Arg.type a a_1) = mixHash (mixHash 2 (hash a)) (hash a_1)

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instHashableArg {pu✝ : Purity} :

Hashable (Arg pu✝)

Equations

Lean.Compiler.LCNF.instHashableArg = { hash := Lean.Compiler.LCNF.instHashableArg.hash }

def Lean.Compiler.LCNF.Param.toArg {pu : Purity} (p : Param pu) :

Arg pu

Equations

p.toArg = Lean.Compiler.LCNF.Arg.fvar p.fvarId

Instances For

def Lean.Compiler.LCNF.Arg.toExpr {pu : Purity} (arg : Arg pu) :

Equations

Lean.Compiler.LCNF.Arg.erased.toExpr = Lean.Compiler.LCNF.erasedExpr
(Lean.Compiler.LCNF.Arg.fvar a).toExpr = Lean.Expr.fvar a
(Lean.Compiler.LCNF.Arg.type a a_1).toExpr = a

Instances For

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateTypeImp]

opaque Lean.Compiler.LCNF.Arg.updateType! {pu : Purity} (arg : Arg pu) (type : Expr) :

Arg pu

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateFVarImp]

opaque Lean.Compiler.LCNF.Arg.updateFVar! {pu : Purity} (arg : Arg pu) (fvarId' : FVarId) :

Arg pu

structure Lean.Compiler.LCNF.CtorInfo :

Constructor information.

name is the Name of the Constructor in Lean.
cidx is the Constructor index (aka tag).
size is the number of arguments of type object/tobject.
usize is the number of arguments of type usize.
ssize is the number of bytes used to store scalar values.

Recall that a Constructor object contains a header, then a sequence of pointers to other Lean objects, a sequence of USize (i.e., size_t) scalar values, and a sequence of other scalar values.

name : Name
cidx : Nat
size : Nat
usize : Nat
ssize : Nat

Instances For

def Lean.Compiler.LCNF.instInhabitedCtorInfo.default :

Equations

Lean.Compiler.LCNF.instInhabitedCtorInfo.default = { name := default, cidx := default, size := default, usize := default, ssize := default }

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCtorInfo :

Inhabited CtorInfo

Equations

Lean.Compiler.LCNF.instInhabitedCtorInfo = { default := Lean.Compiler.LCNF.instInhabitedCtorInfo.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqCtorInfo :

Equations

Lean.Compiler.LCNF.instBEqCtorInfo = { beq := Lean.Compiler.LCNF.instBEqCtorInfo.beq }

def Lean.Compiler.LCNF.instBEqCtorInfo.beq :

CtorInfo → CtorInfo → Bool

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.instBEqCtorInfo.beq x✝¹ x✝ = false

Instances For

def Lean.Compiler.LCNF.instReprCtorInfo.repr :

CtorInfo → Nat → Format

Equations

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

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instReprCtorInfo :

Equations

Lean.Compiler.LCNF.instReprCtorInfo = { reprPrec := Lean.Compiler.LCNF.instReprCtorInfo.repr }

def Lean.Compiler.LCNF.instHashableCtorInfo.hash :

CtorInfo → UInt64

Equations

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

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instHashableCtorInfo :

Hashable CtorInfo

Equations

Lean.Compiler.LCNF.instHashableCtorInfo = { hash := Lean.Compiler.LCNF.instHashableCtorInfo.hash }

def Lean.Compiler.LCNF.CtorInfo.isRef (info : CtorInfo) :

Equations

info.isRef = (decide (info.size > 0) || decide (info.usize > 0) || decide (info.ssize > 0))

Instances For

def Lean.Compiler.LCNF.CtorInfo.isScalar (info : CtorInfo) :

Equations

info.isScalar = !info.isRef

Instances For

def Lean.Compiler.LCNF.CtorInfo.type (info : CtorInfo) :

Equations

info.type = if info.isRef = true then Lean.Compiler.LCNF.ImpureType.object else Lean.Compiler.LCNF.ImpureType.tagged

Instances For

inductive Lean.Compiler.LCNF.LetValue (pu : Purity) :

lit {pu : Purity} (value : LitValue) : LetValue pu
A literal value.
erased {pu : Purity} : LetValue pu
An erased value that is irrelevant for computation.
proj {pu : Purity} (typeName : Name) (idx : Nat) (struct : FVarId) (h : pu = Purity.pure := by purity_tac) : LetValue pu
A projection from a pure LCNF value.
const {pu : Purity} (declName : Name) (us : List Level) (args : Array (Arg pu)) (h : pu = Purity.pure := by purity_tac) : LetValue pu
A pure application of a constant.
fvar {pu : Purity} (fvarId : FVarId) (args : Array (Arg pu)) : LetValue pu
An application of a free variable
ctor {pu : Purity} (i : CtorInfo) (args : Array (Arg pu)) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Allocating a constructor.
oproj {pu : Purity} (i : Nat) (var : FVarId) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Projecting objects out of a value.
uproj {pu : Purity} (i : Nat) (var : FVarId) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Projecting USize scalars out of a value.
sproj {pu : Purity} (n offset : Nat) (var : FVarId) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Projecting non-USize scalars out of a value
fap {pu : Purity} (fn : Name) (args : Array (Arg pu)) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Full, impure, application of a function.
pap {pu : Purity} (fn : Name) (args : Array (Arg pu)) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Partial application of a function.
reset {pu : Purity} (n : Nat) (var : FVarId) (h : pu = Purity.impure := by purity_tac) : LetValue pu
The reset instruction from Counting Immutable Beans. n is the amount of object fields stored in the constructor in var.
reuse {pu : Purity} (var : FVarId) (i : CtorInfo) (updateHeader : Bool) (args : Array (Arg pu)) (h : pu = Purity.impure := by purity_tac) : LetValue pu
reuse x in ctor_i ys instruction in the paper. updateHeader is set if the tag in the new ctor differs from the one in the old ctor and thus needs to be updated.
box {pu : Purity} (ty : Expr) (fvarId : FVarId) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Given a scalar type ty and a value fvarId : ty, this operation returns a value of type tobject. For small scalar values the result is a tagged pointer, and no memory allocation is performed.
unbox {pu : Purity} (fvarId : FVarId) (h : pu = Purity.impure := by purity_tac) : LetValue pu
Given fvarId : [t]object, obtain the underlying scalar value.

Instances For

def Lean.Compiler.LCNF.instInhabitedLetValue.default {a✝ : Purity} :

Equations

Lean.Compiler.LCNF.instInhabitedLetValue.default = Lean.Compiler.LCNF.LetValue.lit default

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedLetValue {a✝ : Purity} :

Inhabited (LetValue a✝)

Equations

Lean.Compiler.LCNF.instInhabitedLetValue = { default := Lean.Compiler.LCNF.instInhabitedLetValue.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqLetValue {pu✝ : Purity} :

BEq (LetValue pu✝)

Equations

Lean.Compiler.LCNF.instBEqLetValue = { beq := Lean.Compiler.LCNF.instBEqLetValue.beq }

def Lean.Compiler.LCNF.instBEqLetValue.beq {pu✝ : Purity} :

LetValue pu✝ → LetValue pu✝ → Bool

Equations

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

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instHashableLetValue {pu✝ : Purity} :

Hashable (LetValue pu✝)

Equations

Lean.Compiler.LCNF.instHashableLetValue = { hash := Lean.Compiler.LCNF.instHashableLetValue.hash }

def Lean.Compiler.LCNF.instHashableLetValue.hash {pu✝ : Purity} :

LetValue pu✝ → UInt64

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.lit a) = mixHash 0 (hash a)
Lean.Compiler.LCNF.instHashableLetValue.hash Lean.Compiler.LCNF.LetValue.erased = 1
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.proj a a_1 a_2 a_3) = mixHash (mixHash (mixHash (mixHash 2 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.const a a_1 a_2 a_3) = mixHash (mixHash (mixHash (mixHash 3 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.fvar a a_1) = mixHash (mixHash 4 (hash a)) (hash a_1)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.ctor a a_1 a_2) = mixHash (mixHash (mixHash 5 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.oproj a a_1 a_2) = mixHash (mixHash (mixHash 6 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.uproj a a_1 a_2) = mixHash (mixHash (mixHash 7 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.sproj a a_1 a_2 a_3) = mixHash (mixHash (mixHash (mixHash 8 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.fap a a_1 a_2) = mixHash (mixHash (mixHash 9 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.pap a a_1 a_2) = mixHash (mixHash (mixHash 10 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.reset a a_1 a_2) = mixHash (mixHash (mixHash 11 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.box a a_1 a_2) = mixHash (mixHash (mixHash 13 (hash a)) (hash a_1)) (hash a_2)
Lean.Compiler.LCNF.instHashableLetValue.hash (Lean.Compiler.LCNF.LetValue.unbox a a_1) = mixHash (mixHash 14 (hash a)) (hash a_1)

Instances For

def Lean.Compiler.LCNF.Arg.toLetValue {pu : Purity} (arg : Arg pu) :

Equations

Instances For

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateProjImp]

opaque Lean.Compiler.LCNF.LetValue.updateProj! {pu : Purity} (e : LetValue pu) (fvarId' : FVarId) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateConstImp]

opaque Lean.Compiler.LCNF.LetValue.updateConst! {pu : Purity} (e : LetValue pu) (declName' : Name) (us' : List Level) (args' : Array (Arg pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFVarImp]

opaque Lean.Compiler.LCNF.LetValue.updateFVar! {pu : Purity} (e : LetValue pu) (fvarId' : FVarId) (args' : Array (Arg pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateResetImp]

opaque Lean.Compiler.LCNF.LetValue.updateReset! {pu : Purity} (e : LetValue pu) (n' : Nat) (fvarId' : FVarId) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateReuseImp]

opaque Lean.Compiler.LCNF.LetValue.updateReuse! {pu : Purity} (e : LetValue pu) (var' : FVarId) (i' : CtorInfo) (updateHeader' : Bool) (args' : Array (Arg pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateFapImp]

opaque Lean.Compiler.LCNF.LetValue.updateFap! {pu : Purity} (e : LetValue pu) (declName' : Name) (args' : Array (Arg pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updatePapImp]

opaque Lean.Compiler.LCNF.LetValue.updatePap! {pu : Purity} (e : LetValue pu) (declName' : Name) (args' : Array (Arg pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateBoxImp]

opaque Lean.Compiler.LCNF.LetValue.updateBox! {pu : Purity} (e : LetValue pu) (ty' : Expr) (fvarId' : FVarId) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateUnboxImp]

opaque Lean.Compiler.LCNF.LetValue.updateUnbox! {pu : Purity} (e : LetValue pu) (fvarId' : FVarId) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateArgsImp]

opaque Lean.Compiler.LCNF.LetValue.updateArgs! {pu : Purity} (e : LetValue pu) (args' : Array (Arg pu)) :

def Lean.Compiler.LCNF.LetValue.toExpr {pu : Purity} (e : LetValue pu) :

Equations

One or more equations did not get rendered due to their size.
(Lean.Compiler.LCNF.LetValue.lit v).toExpr = v.toExpr
Lean.Compiler.LCNF.LetValue.erased.toExpr = Lean.Compiler.LCNF.erasedExpr
(Lean.Compiler.LCNF.LetValue.proj n i s h).toExpr = Lean.Expr.proj n i (Lean.Expr.fvar s)
(Lean.Compiler.LCNF.LetValue.const n us as h).toExpr = Lean.mkAppN (Lean.Expr.const n us) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)
(Lean.Compiler.LCNF.LetValue.fvar fvarId as).toExpr = Lean.mkAppN (Lean.Expr.fvar fvarId) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)
(Lean.Compiler.LCNF.LetValue.ctor i as h).toExpr = Lean.mkAppN (Lean.Expr.const i.name []) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)
(Lean.Compiler.LCNF.LetValue.fap fn as h).toExpr = Lean.mkAppN (Lean.Expr.const fn []) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)
(Lean.Compiler.LCNF.LetValue.pap fn as h).toExpr = Lean.mkAppN (Lean.Expr.const fn []) (Array.map Lean.Compiler.LCNF.Arg.toExpr as)
(Lean.Compiler.LCNF.LetValue.oproj i var h).toExpr = Lean.mkApp2 (Lean.Expr.const `oproj []) (Lean.toExpr i) (Lean.Expr.fvar var)
(Lean.Compiler.LCNF.LetValue.uproj i var h).toExpr = Lean.mkApp2 (Lean.Expr.const `uproj []) (Lean.toExpr i) (Lean.Expr.fvar var)
(Lean.Compiler.LCNF.LetValue.sproj i offset var h).toExpr = Lean.mkApp3 (Lean.Expr.const `sproj []) (Lean.toExpr i) (Lean.toExpr offset) (Lean.Expr.fvar var)
(Lean.Compiler.LCNF.LetValue.reset n var h).toExpr = Lean.mkApp2 (Lean.Expr.const `reset []) (Lean.toExpr n) (Lean.Expr.fvar var)
(Lean.Compiler.LCNF.LetValue.box ty var h).toExpr = Lean.mkApp2 (Lean.Expr.const `box []) ty (Lean.Expr.fvar var)
(Lean.Compiler.LCNF.LetValue.unbox var h).toExpr = Lean.mkApp (Lean.Expr.const `unbox []) (Lean.Expr.fvar var)

Instances For

structure Lean.Compiler.LCNF.LetDecl (pu : Purity) :

fvarId : FVarId
binderName : Name
type : Expr
value : LetValue pu

Instances For

def Lean.Compiler.LCNF.instInhabitedLetDecl.default {a✝ : Purity} :

Equations

Lean.Compiler.LCNF.instInhabitedLetDecl.default = { fvarId := default, binderName := default, type := default, value := default }

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedLetDecl {a✝ : Purity} :

Inhabited (LetDecl a✝)

Equations

Lean.Compiler.LCNF.instInhabitedLetDecl = { default := Lean.Compiler.LCNF.instInhabitedLetDecl.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqLetDecl {pu✝ : Purity} :

BEq (LetDecl pu✝)

Equations

Lean.Compiler.LCNF.instBEqLetDecl = { beq := Lean.Compiler.LCNF.instBEqLetDecl.beq }

def Lean.Compiler.LCNF.instBEqLetDecl.beq {pu✝ : Purity} :

LetDecl pu✝ → LetDecl pu✝ → Bool

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.instBEqLetDecl.beq x✝¹ x✝ = false

Instances For

inductive Lean.Compiler.LCNF.Alt (pu : Purity) :

alt {pu : Purity} (ctorName : Name) (params : Array (Param pu)) (code : Code pu) (h : pu = Purity.pure := by purity_tac) : Alt pu
ctorAlt {pu : Purity} (info : CtorInfo) (code : Code pu) (h : pu = Purity.impure := by purity_tac) : Alt pu
default {pu : Purity} (code : Code pu) : Alt pu

Instances For

inductive Lean.Compiler.LCNF.FunDecl (pu : Purity) :

mk {pu : Purity} (fvarId : FVarId) (binderName : Name) (params : Array (Param pu)) (type : Expr) (value : Code pu) : FunDecl pu

Instances For

inductive Lean.Compiler.LCNF.Cases (pu : Purity) :

mk {pu : Purity} (typeName : Name) (resultType : Expr) (discr : FVarId) (alts : Array (Alt pu)) : Cases pu

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCases {a✝ : Purity} :

Inhabited (Cases a✝)

Equations

Lean.Compiler.LCNF.instInhabitedCases = { default := Lean.Compiler.LCNF.instInhabitedCases.default_1 }

def Lean.Compiler.LCNF.instInhabitedCases.default_1 {a✝ : Purity} :

Cases a✝

Equations

Lean.Compiler.LCNF.instInhabitedCases.default_1 = Lean.Compiler.LCNF.Cases.mk default default default default

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCode {a✝ : Purity} :

Inhabited (Code a✝)

Equations

Lean.Compiler.LCNF.instInhabitedCode = { default := Lean.Compiler.LCNF.instInhabitedCode.default_1 }

def Lean.Compiler.LCNF.instInhabitedCode.default_1 {a✝ : Purity} :

Code a✝

Equations

Lean.Compiler.LCNF.instInhabitedCode.default_1 = Lean.Compiler.LCNF.Code.jmp default default

Instances For

inductive Lean.Compiler.LCNF.Code (pu : Purity) :

let {pu : Purity} (decl : LetDecl pu) (k : Code pu) : Code pu
fun {pu : Purity} (decl : FunDecl pu) (k : Code pu) (h : pu = Purity.pure := by purity_tac) : Code pu
jp {pu : Purity} (decl : FunDecl pu) (k : Code pu) : Code pu
jmp {pu : Purity} (fvarId : FVarId) (args : Array (Arg pu)) : Code pu
cases {pu : Purity} (cases : Cases pu) : Code pu
return {pu : Purity} (fvarId : FVarId) : Code pu
unreach {pu : Purity} (type : Expr) : Code pu
uset {pu : Purity} (var : FVarId) (i : Nat) (y : FVarId) (k : Code pu) (h : pu = Purity.impure := by purity_tac) : Code pu
sset {pu : Purity} (var : FVarId) (i offset : Nat) (y : FVarId) (ty : Expr) (k : Code pu) (h : pu = Purity.impure := by purity_tac) : Code pu

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.fvarId {pu : Purity} :

FunDecl pu → FVarId

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).fvarId = fvarId

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.binderName {pu : Purity} :

FunDecl pu → Name

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).binderName = binderName

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.params {pu : Purity} :

FunDecl pu → Array (Param pu)

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).params = params

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.type {pu : Purity} :

FunDecl pu → Expr

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).type = type

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.value {pu : Purity} :

FunDecl pu → Code pu

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).value = value

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.updateBinderName {pu : Purity} :

FunDecl pu → Name → FunDecl pu

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).updateBinderName x✝ = Lean.Compiler.LCNF.FunDecl.mk fvarId x✝ params type value

Instances For

@[inline]

def Lean.Compiler.LCNF.FunDecl.toParam {pu : Purity} (decl : FunDecl pu) (borrow : Bool) :

Equations

(Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value).toParam borrow = { fvarId := fvarId, binderName := binderName, type := type, borrow := borrow }

Instances For

@[inline]

def Lean.Compiler.LCNF.Cases.typeName {pu : Purity} :

Cases pu → Name

Equations

(Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts).typeName = typeName

Instances For

@[inline]

def Lean.Compiler.LCNF.Cases.resultType {pu : Purity} :

Cases pu → Expr

Equations

(Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts).resultType = resultType

Instances For

@[inline]

def Lean.Compiler.LCNF.Cases.discr {pu : Purity} :

Cases pu → FVarId

Equations

(Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts).discr = discr

Instances For

@[inline]

def Lean.Compiler.LCNF.Cases.alts {pu : Purity} :

Cases pu → Array (Alt pu)

Equations

(Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts).alts = alts

Instances For

@[inline]

def Lean.Compiler.LCNF.Cases.updateAlts {pu : Purity} :

Cases pu → Array (Alt pu) → Cases pu

Equations

(Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts).updateAlts x✝ = Lean.Compiler.LCNF.Cases.mk typeName resultType discr x✝

Instances For

def Lean.Compiler.LCNF.instInhabitedAlt.default_1 {a✝ : Purity} :

Alt a✝

Equations

Lean.Compiler.LCNF.instInhabitedAlt.default_1 = Lean.Compiler.LCNF.Alt.default default

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedAlt {a✝ : Purity} :

Inhabited (Alt a✝)

Equations

Lean.Compiler.LCNF.instInhabitedAlt = { default := Lean.Compiler.LCNF.instInhabitedAlt.default_1 }

def Lean.Compiler.LCNF.instInhabitedFunDecl.default_1 {a✝ : Purity} :

Equations

Lean.Compiler.LCNF.instInhabitedFunDecl.default_1 = Lean.Compiler.LCNF.FunDecl.mk default default default default default

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedFunDecl {a✝ : Purity} :

Inhabited (FunDecl a✝)

Equations

Lean.Compiler.LCNF.instInhabitedFunDecl = { default := Lean.Compiler.LCNF.instInhabitedFunDecl.default_1 }

def Lean.Compiler.LCNF.FunDecl.getArity {pu : Purity} (decl : FunDecl pu) :

Equations

decl.getArity = decl.params.size

Instances For

def Lean.Compiler.LCNF.Cases.getCtorNames {pu : Purity} (c : Cases pu) :

Return the constructor names that have an explicit (non-default) alternative.

Equations

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

Instances For

inductive Lean.Compiler.LCNF.CodeDecl (pu : Purity) :

let {pu : Purity} (decl : LetDecl pu) : CodeDecl pu
fun {pu : Purity} (decl : FunDecl pu) (h : pu = Purity.pure := by purity_tac) : CodeDecl pu
jp {pu : Purity} (decl : FunDecl pu) : CodeDecl pu
uset {pu : Purity} (var : FVarId) (i : Nat) (y : FVarId) (h : pu = Purity.impure := by purity_tac) : CodeDecl pu
sset {pu : Purity} (var : FVarId) (i offset : Nat) (y : FVarId) (ty : Expr) (h : pu = Purity.impure := by purity_tac) : CodeDecl pu

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedCodeDecl {a✝ : Purity} :

Inhabited (CodeDecl a✝)

Equations

Lean.Compiler.LCNF.instInhabitedCodeDecl = { default := Lean.Compiler.LCNF.instInhabitedCodeDecl.default }

def Lean.Compiler.LCNF.instInhabitedCodeDecl.default {a✝ : Purity} :

Equations

Lean.Compiler.LCNF.instInhabitedCodeDecl.default = Lean.Compiler.LCNF.CodeDecl.let default

Instances For

def Lean.Compiler.LCNF.CodeDecl.fvarId {pu : Purity} :

CodeDecl pu → FVarId

Equations

(Lean.Compiler.LCNF.CodeDecl.let decl).fvarId = decl.fvarId
(Lean.Compiler.LCNF.CodeDecl.fun decl h).fvarId = decl.fvarId
(Lean.Compiler.LCNF.CodeDecl.jp decl).fvarId = decl.fvarId
(Lean.Compiler.LCNF.CodeDecl.uset var i y h).fvarId = var
(Lean.Compiler.LCNF.CodeDecl.sset var i offset y ty h).fvarId = var

Instances For

def Lean.Compiler.LCNF.Code.toCodeDecl! {pu : Purity} :

Code pu → CodeDecl pu

Equations

(Lean.Compiler.LCNF.Code.let decl k).toCodeDecl! = Lean.Compiler.LCNF.CodeDecl.let decl
(Lean.Compiler.LCNF.Code.fun decl k h).toCodeDecl! = Lean.Compiler.LCNF.CodeDecl.fun decl h
(Lean.Compiler.LCNF.Code.jp decl k).toCodeDecl! = Lean.Compiler.LCNF.CodeDecl.jp decl
(Lean.Compiler.LCNF.Code.uset var i y k h).toCodeDecl! = Lean.Compiler.LCNF.CodeDecl.uset var i y h
(Lean.Compiler.LCNF.Code.sset var i offset ty y k h).toCodeDecl! = Lean.Compiler.LCNF.CodeDecl.sset var i offset ty y h
x✝.toCodeDecl! = panicWithPosWithDecl "Lean.Compiler.LCNF.Basic" "Lean.Compiler.LCNF.Code.toCodeDecl!" 455 7 "unreachable code has been reached"

Instances For

def Lean.Compiler.LCNF.attachCodeDecls {pu : Purity} (decls : Array (CodeDecl pu)) (code : Code pu) :

Equations

Lean.Compiler.LCNF.attachCodeDecls decls code = Lean.Compiler.LCNF.attachCodeDecls.go✝ decls decls.size code

Instances For

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqImp]

opaque Lean.Compiler.LCNF.Code.beq {pu : Purity} :

Code pu → Code pu → Bool

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqCode {pu : Purity} :

Equations

Lean.Compiler.LCNF.instBEqCode = { beq := Lean.Compiler.LCNF.Code.beq }

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.eqFunDecl]

opaque Lean.Compiler.LCNF.FunDecl.beq {pu : Purity} :

FunDecl pu → FunDecl pu → Bool

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqFunDecl {pu : Purity} :

BEq (FunDecl pu)

Equations

Lean.Compiler.LCNF.instBEqFunDecl = { beq := Lean.Compiler.LCNF.FunDecl.beq }

def Lean.Compiler.LCNF.Alt.getCode {pu : Purity} :

Alt pu → Code pu

Equations

(Lean.Compiler.LCNF.Alt.default k).getCode = k
(Lean.Compiler.LCNF.Alt.alt ctorName params k h).getCode = k
(Lean.Compiler.LCNF.Alt.ctorAlt info k h).getCode = k

Instances For

def Lean.Compiler.LCNF.Alt.getParams :

Alt Purity.pure → Array (Param Purity.pure)

Equations

(Lean.Compiler.LCNF.Alt.default code).getParams = #[]
(Lean.Compiler.LCNF.Alt.alt ctorName ps code h).getParams = ps

Instances For

def Lean.Compiler.LCNF.Alt.forCodeM {m : Type → Type u_1} {pu : Purity} [Monad m] (alt : Alt pu) (f : Code pu → m Unit) :

Equations

(Lean.Compiler.LCNF.Alt.default k).forCodeM f = f k
(Lean.Compiler.LCNF.Alt.alt ctorName params k h).forCodeM f = f k
(Lean.Compiler.LCNF.Alt.ctorAlt info k h).forCodeM f = f k

Instances For

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltCodeImp]

opaque Lean.Compiler.LCNF.Alt.updateCode {pu : Purity} (alt : Alt pu) (c : Code pu) :

Alt pu

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltImp]

opaque Lean.Compiler.LCNF.Alt.updateAlt! {pu : Purity} (alt : Alt pu) (ps' : Array (Param pu)) (k' : Code pu) :

Alt pu

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltsImp]

opaque Lean.Compiler.LCNF.Code.updateAlts! {pu : Purity} (c : Code pu) (alts : Array (Alt pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateCasesImp]

opaque Lean.Compiler.LCNF.Code.updateCases! {pu : Purity} (c : Code pu) (resultType : Expr) (discr : FVarId) (alts : Array (Alt pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetImp]

opaque Lean.Compiler.LCNF.Code.updateLet! {pu : Purity} (c : Code pu) (decl' : LetDecl pu) (k' : Code pu) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateContImp]

opaque Lean.Compiler.LCNF.Code.updateCont! {pu : Purity} (c k' : Code pu) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunImp]

opaque Lean.Compiler.LCNF.Code.updateFun! {pu : Purity} (c : Code pu) (decl' : FunDecl pu) (k' : Code pu) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateReturnImp]

opaque Lean.Compiler.LCNF.Code.updateReturn! {pu : Purity} (c : Code pu) (fvarId' : FVarId) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateJmpImp]

opaque Lean.Compiler.LCNF.Code.updateJmp! {pu : Purity} (c : Code pu) (fvarId' : FVarId) (args' : Array (Arg pu)) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUnreachImp]

opaque Lean.Compiler.LCNF.Code.updateUnreach! {pu : Purity} (c : Code pu) (type' : Expr) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateSsetImp]

opaque Lean.Compiler.LCNF.Code.updateSset! {pu : Purity} (c : Code pu) (fvarId' : FVarId) (i' offset' : Nat) (y' : FVarId) (ty' : Expr) (k' : Code pu) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateUsetImp]

opaque Lean.Compiler.LCNF.Code.updateUset! {pu : Purity} (c : Code pu) (fvarId' : FVarId) (i' : Nat) (y' : FVarId) (k' : Code pu) :

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateParamCoreImp]

opaque Lean.Compiler.LCNF.Param.updateCore {pu : Purity} (p : Param pu) (type : Expr) :

Low-level update Param function. It does not update the local context. Consider using Param.update : Param → Expr → CompilerM Param if you want the local context to be updated.

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateLetDeclCoreImp]

opaque Lean.Compiler.LCNF.LetDecl.updateCore {pu : Purity} (decl : LetDecl pu) (type : Expr) (value : LetValue pu) :

Low-level update LetDecl function. It does not update the local context. Consider using LetDecl.update : LetDecl → Expr → Expr → CompilerM LetDecl if you want the local context to be updated.

@[implemented_by _private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateFunDeclCoreImp]

opaque Lean.Compiler.LCNF.FunDecl.updateCore {pu : Purity} (decl : FunDecl pu) (type : Expr) (params : Array (Param pu)) (value : Code pu) :

Low-level update FunDecl function. It does not update the local context. Consider using FunDecl.update : LetDecl → Expr → Array Param → Code → CompilerM FunDecl if you want the local context to be updated.

def Lean.Compiler.LCNF.Cases.extractAlt! {pu : Purity} (cases : Cases pu) (ctorName : Name) :

Alt pu × Cases pu

Equations

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

Instances For

def Lean.Compiler.LCNF.Alt.mapCodeM {m : Type → Type u_1} {pu : Purity} [Monad m] (alt : Alt pu) (f : Code pu → m (Code pu)) :

m (Alt pu)

Equations

alt.mapCodeM f = do let __do_lift ← f alt.getCode pure (alt.updateCode __do_lift)

Instances For

def Lean.Compiler.LCNF.Code.isDecl {pu : Purity} :

Code pu → Bool

Equations

(Lean.Compiler.LCNF.Code.let decl k).isDecl = true
(Lean.Compiler.LCNF.Code.fun decl k h).isDecl = true
(Lean.Compiler.LCNF.Code.jp decl k).isDecl = true
x✝.isDecl = false

Instances For

def Lean.Compiler.LCNF.Code.isFun {pu : Purity} :

Code pu → Bool

Equations

(Lean.Compiler.LCNF.Code.fun decl k h).isFun = true
x✝.isFun = false

Instances For

def Lean.Compiler.LCNF.Code.isReturnOf {pu : Purity} :

Code pu → FVarId → Bool

Equations

(Lean.Compiler.LCNF.Code.return fvarId).isReturnOf x✝ = (fvarId == x✝)
x✝¹.isReturnOf x✝ = false

Instances For

def Lean.Compiler.LCNF.Code.size {pu : Purity} (c : Code pu) :

Equations

c.size = Lean.Compiler.LCNF.Code.size.go✝ c 0

Instances For

def Lean.Compiler.LCNF.Code.sizeLe {pu : Purity} (c : Code pu) (n : Nat) :

Return true iff c.size ≤ n

Equations

c.sizeLe n = match (Lean.Compiler.LCNF.Code.sizeLe.go✝ n c).run 0 with | EStateM.Result.ok a a_1 => true | EStateM.Result.error a a_1 => false

Instances For

def Lean.Compiler.LCNF.Code.forM {m : Type → Type u_1} {pu : Purity} [Monad m] (c : Code pu) (f : Code pu → m Unit) :

Equations

c.forM f = Lean.Compiler.LCNF.Code.forM.go✝ f c

Instances For

def Lean.Compiler.LCNF.Code.instantiateValueLevelParams (code : Code Purity.pure) (levelParams : List Name) (us : List Level) :

Code Purity.pure

Equations

code.instantiateValueLevelParams levelParams us = Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instCode✝ levelParams us code

Instances For

inductive Lean.Compiler.LCNF.DeclValue (pu : Purity) :

code {pu : Purity} (code : Code pu) : DeclValue pu
extern {pu : Purity} (externAttrData : ExternAttrData) : DeclValue pu

Instances For

def Lean.Compiler.LCNF.instInhabitedDeclValue.default {a✝ : Purity} :

Equations

Lean.Compiler.LCNF.instInhabitedDeclValue.default = Lean.Compiler.LCNF.DeclValue.code default

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedDeclValue {a✝ : Purity} :

Inhabited (DeclValue a✝)

Equations

Lean.Compiler.LCNF.instInhabitedDeclValue = { default := Lean.Compiler.LCNF.instInhabitedDeclValue.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqDeclValue {pu✝ : Purity} :

BEq (DeclValue pu✝)

Equations

Lean.Compiler.LCNF.instBEqDeclValue = { beq := Lean.Compiler.LCNF.instBEqDeclValue.beq }

def Lean.Compiler.LCNF.instBEqDeclValue.beq {pu✝ : Purity} :

DeclValue pu✝ → DeclValue pu✝ → Bool

Equations

Lean.Compiler.LCNF.instBEqDeclValue.beq (Lean.Compiler.LCNF.DeclValue.code a) (Lean.Compiler.LCNF.DeclValue.code b) = (a == b)
Lean.Compiler.LCNF.instBEqDeclValue.beq (Lean.Compiler.LCNF.DeclValue.extern a) (Lean.Compiler.LCNF.DeclValue.extern b) = (a == b)
Lean.Compiler.LCNF.instBEqDeclValue.beq x✝¹ x✝ = false

Instances For

def Lean.Compiler.LCNF.DeclValue.size {pu : Purity} :

DeclValue pu → Nat

Equations

(Lean.Compiler.LCNF.DeclValue.code c).size = c.size
(Lean.Compiler.LCNF.DeclValue.extern externAttrData).size = 0

Instances For

def Lean.Compiler.LCNF.DeclValue.mapCode {pu : Purity} (f : Code pu → Code pu) :

DeclValue pu → DeclValue pu

Equations

Lean.Compiler.LCNF.DeclValue.mapCode f (Lean.Compiler.LCNF.DeclValue.code c) = Lean.Compiler.LCNF.DeclValue.code (f c)
Lean.Compiler.LCNF.DeclValue.mapCode f (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = Lean.Compiler.LCNF.DeclValue.extern externAttrData

Instances For

def Lean.Compiler.LCNF.DeclValue.mapCodeM {m : Type → Type u_1} {pu : Purity} [Monad m] (f : Code pu → m (Code pu)) :

DeclValue pu → m (DeclValue pu)

Equations

Lean.Compiler.LCNF.DeclValue.mapCodeM f (Lean.Compiler.LCNF.DeclValue.code c) = do let __do_lift ← f c pure (Lean.Compiler.LCNF.DeclValue.code __do_lift)
Lean.Compiler.LCNF.DeclValue.mapCodeM f (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = pure (Lean.Compiler.LCNF.DeclValue.extern externAttrData)

Instances For

def Lean.Compiler.LCNF.DeclValue.forCodeM {m : Type → Type u_1} {pu : Purity} [Monad m] (f : Code pu → m Unit) :

DeclValue pu → m Unit

Equations

Lean.Compiler.LCNF.DeclValue.forCodeM f (Lean.Compiler.LCNF.DeclValue.code c) = f c
Lean.Compiler.LCNF.DeclValue.forCodeM f (Lean.Compiler.LCNF.DeclValue.extern externAttrData) = pure ()

Instances For

def Lean.Compiler.LCNF.DeclValue.isCodeAndM {m : Type → Type u_1} {pu : Purity} [Monad m] (v : DeclValue pu) (f : Code pu → m Bool) :

Equations

(Lean.Compiler.LCNF.DeclValue.code c).isCodeAndM f = f c
(Lean.Compiler.LCNF.DeclValue.extern externAttrData).isCodeAndM f = pure false

Instances For

structure Lean.Compiler.LCNF.Signature (pu : Purity) :

The signature of a declaration being processed by the Lean to Lean compiler passes.

name : Name
The name of the declaration from the Environment it came from
levelParams : List Name
Universe level parameter names.
type : Expr
The type of the declaration. Note that this is an erased LCNF type instead of the fully dependent one that might have been the original type of the declaration in the Environment. Furthermore, once in the impure staged of LCNF this type is only the return type.
params : Array (Param pu)
Parameters.
safe : Bool
We set this flag to false during LCNF conversion if the Lean function associated with this function was tagged as partial or unsafe. This information affects how static analyzers treat function applications of this kind. See DefinitionSafety. partial and unsafe functions may not be terminating, but Lean functions terminate, and some static analyzers exploit this fact. So, we use the following semantics. Suppose we have a (large) natural number C. We consider a nondeterministic model for computation of Lean expressions as follows: Each call to a partial/unsafe function uses up one "recursion token". Prior to consuming C recursion tokens all partial functions must be called as normal. Once the model has used up C recursion tokens, a subsequent call to a partial function has the following nondeterministic options: it can either call the function again, or return any value of the target type (even a noncomputable one). Larger values of C yield less nondeterminism in the model, but even the intersection of all choices of C yields nondeterminism where def loop : A := loop returns any value of type A. The compiler fixes a choice for C. This is a fixed constant greater than 2^2^64, which is allowed to be compiler and architecture dependent, and promises that it will produce an execution consistent with every possible nondeterministic outcome of the C-model. In the event that different nondeterministic executions disagree, the compiler is required to exhaust resources or output a looping computation.

Instances For

def Lean.Compiler.LCNF.instInhabitedSignature.default {a✝ : Purity} :

Equations

Lean.Compiler.LCNF.instInhabitedSignature.default = { name := default, levelParams := default, type := default, params := default, safe := default }

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedSignature {a✝ : Purity} :

Inhabited (Signature a✝)

Equations

Lean.Compiler.LCNF.instInhabitedSignature = { default := Lean.Compiler.LCNF.instInhabitedSignature.default }

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqSignature {pu✝ : Purity} :

BEq (Signature pu✝)

Equations

Lean.Compiler.LCNF.instBEqSignature = { beq := Lean.Compiler.LCNF.instBEqSignature.beq }

def Lean.Compiler.LCNF.instBEqSignature.beq {pu✝ : Purity} :

Signature pu✝ → Signature pu✝ → Bool

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.instBEqSignature.beq x✝¹ x✝ = false

Instances For

structure Lean.Compiler.LCNF.Decl (pu : Purity) extends Lean.Compiler.LCNF.Signature pu :

Declaration being processed by the Lean to Lean compiler passes.

name : Name
levelParams : List Name
type : Expr
params : Array (Param pu)
safe : Bool
value : DeclValue pu
The body of the declaration, usually changes as it progresses through compiler passes.
recursive : Bool
We set this flag to true during LCNF conversion. When we receive a block of functions to be compiled, we set this flag to true if there is an application to the function in the block containing it. This is an approximation, but it should be good enough because in the frontend, we invoke the compiler with blocks of strongly connected components only. We use this information to control inlining.
inlineAttr? : Option InlineAttributeKind
We store the inline attribute at LCNF declarations to make sure we can set them for auxiliary declarations created during compilation.

Instances For

def Lean.Compiler.LCNF.instInhabitedDecl.default {a✝ : Purity} :

Decl a✝

Equations

Lean.Compiler.LCNF.instInhabitedDecl.default = { toSignature := default, value := default, recursive := default, inlineAttr? := default }

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instInhabitedDecl {a✝ : Purity} :

Inhabited (Decl a✝)

Equations

Lean.Compiler.LCNF.instInhabitedDecl = { default := Lean.Compiler.LCNF.instInhabitedDecl.default }

def Lean.Compiler.LCNF.instBEqDecl.beq {pu✝ : Purity} :

Decl pu✝ → Decl pu✝ → Bool

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.instBEqDecl.beq x✝¹ x✝ = false

Instances For

@[instance_reducible]

instance Lean.Compiler.LCNF.instBEqDecl {pu✝ : Purity} :

BEq (Decl pu✝)

Equations

Lean.Compiler.LCNF.instBEqDecl = { beq := Lean.Compiler.LCNF.instBEqDecl.beq }

def Lean.Compiler.LCNF.Decl.size {pu : Purity} (decl : Decl pu) :

Equations

decl.size = decl.value.size

Instances For

def Lean.Compiler.LCNF.Decl.getArity {pu : Purity} (decl : Decl pu) :

Equations

decl.getArity = decl.params.size

Instances For

def Lean.Compiler.LCNF.Decl.inlineAttr {pu : Purity} (decl : Decl pu) :

Equations

decl.inlineAttr = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.inline => true | x => false

Instances For

def Lean.Compiler.LCNF.Decl.noinlineAttr {pu : Purity} (decl : Decl pu) :

Equations

decl.noinlineAttr = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.noinline => true | x => false

Instances For

def Lean.Compiler.LCNF.Decl.inlineIfReduceAttr {pu : Purity} (decl : Decl pu) :

Equations

decl.inlineIfReduceAttr = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.inlineIfReduce => true | x => false

Instances For

def Lean.Compiler.LCNF.Decl.alwaysInlineAttr {pu : Purity} (decl : Decl pu) :

Equations

decl.alwaysInlineAttr = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.alwaysInline => true | x => false

Instances For

def Lean.Compiler.LCNF.Decl.inlineable {pu : Purity} (decl : Decl pu) :

Return true if the given declaration has been annotated with [inline], [inline_if_reduce], [macro_inline], or [always_inline]

Equations

decl.inlineable = match decl.inlineAttr? with | some Lean.Compiler.InlineAttributeKind.noinline => false | some val => true | none => false

Instances For

def Lean.Compiler.LCNF.Decl.castPurity! {pu1 : Purity} (decl : Decl pu1) (pu2 : Purity) :

Decl pu2

Equations

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

Instances For

def Lean.Compiler.LCNF.Decl.isCasesOnParam? {pu : Purity} (decl : Decl pu) :

Return some i if decl is of the form

def f (a_0 ... a_i ...) :=
  ...
  cases a_i
  | ...
  | ...

That is, f is a sequence of declarations followed by a cases on the parameter i. We use this function to decide whether we should inline a declaration tagged with [inline_if_reduce] or not.

Equations

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

Instances For

def Lean.Compiler.LCNF.Decl.instantiateTypeLevelParams {pu : Purity} (decl : Decl pu) (us : List Level) :

Equations

decl.instantiateTypeLevelParams us = decl.type.instantiateLevelParamsNoCache decl.levelParams us

Instances For

def Lean.Compiler.LCNF.Decl.instantiateParamsLevelParams {pu : Purity} (decl : Decl pu) (us : List Level) :

Array (Param pu)

Equations

decl.instantiateParamsLevelParams us = decl.params.mapMono fun (param : Lean.Compiler.LCNF.Param pu) => param.updateCore (param.type.instantiateLevelParamsNoCache decl.levelParams us)

Instances For

def Lean.Compiler.LCNF.hasLocalInst (type : Expr) :

Return true if the arrow type contains an instance implicit argument.

Equations

One or more equations did not get rendered due to their size.
Lean.Compiler.LCNF.hasLocalInst type = pure false

Instances For

def Lean.Compiler.LCNF.Decl.isTemplateLike {pu : Purity} (decl : Decl pu) :

Return true if decl is supposed to be inlined/specialized.

Equations

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

Instances For

partial def Lean.Compiler.LCNF.FunDecl.collectUsed {pu : Purity} (decl : FunDecl pu) (s : FVarIdHashSet := ∅) :

partial def Lean.Compiler.LCNF.Code.collectUsed {pu : Purity} (code : Code pu) (s : FVarIdHashSet := ∅) :

@[inline]

def Lean.Compiler.LCNF.collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) :

Equations

Lean.Compiler.LCNF.collectUsedAtExpr s e = Lean.Compiler.LCNF.collectType✝ e s

Instances For

def Lean.Compiler.LCNF.CodeDecl.collectUsed {pu : Purity} (codeDecl : CodeDecl pu) (s : FVarIdHashSet := ∅) :

Equations

(Lean.Compiler.LCNF.CodeDecl.let decl).collectUsed s = Lean.Compiler.LCNF.collectLetValue✝ decl.value (Lean.Compiler.LCNF.collectType✝ decl.type s)
(Lean.Compiler.LCNF.CodeDecl.jp decl).collectUsed s = decl.collectUsed s
(Lean.Compiler.LCNF.CodeDecl.fun decl h).collectUsed s = decl.collectUsed s
(Lean.Compiler.LCNF.CodeDecl.sset var i offset y ty h).collectUsed s = Lean.Compiler.LCNF.collectType✝ ty ((Std.HashSet.insert s var).insert y)
(Lean.Compiler.LCNF.CodeDecl.uset var i y h).collectUsed s = (Std.HashSet.insert s var).insert y

Instances For

def Lean.Compiler.LCNF.markRecDecls {pu : Purity} (decls : Array (Decl pu)) :

Array (Decl pu)

Traverse the given block of potentially mutually recursive functions and mark a declaration f as recursive if there is an application f ... in the block. This is an overapproximation, and relies on the fact that our frontend computes strongly connected components. See comment at recursive field.

Equations

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

Instances For

def Lean.Compiler.LCNF.instantiateRangeArgs {pu : Purity} (e : Expr) (beginIdx endIdx : Nat) (args : Array (Arg pu)) :

Equations

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

Instances For

def Lean.Compiler.LCNF.instantiateRevRangeArgs {pu : Purity} (e : Expr) (beginIdx endIdx : Nat) (args : Array (Arg pu)) :

Equations

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

Instances For