source
structure Lean.Compiler.LCNF.ToMonoM.State :
Type

- typeParams : FVarIdHashSet
- noncomputableVars : Std.HashMap FVarId Name

Instances For

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ToMonoM (α : Type) :
Type
Equations

- Lean.Compiler.LCNF.ToMonoM = StateRefT' IO.RealWorld Lean.Compiler.LCNF.ToMonoM.State Lean.Compiler.LCNF.CompilerM

Instances For

source
def Lean.Compiler.LCNF.Param.toMono (param : Param) :
ToMonoM Param
Equations

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

Instances For

source
def Lean.Compiler.LCNF.throwNoncomputableError {α : Type} (declName : Name) :
ToMonoM α
Equations

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

Instances For

source
def Lean.Compiler.LCNF.checkFVarUse (fvarId : FVarId) :
ToMonoM Unit
Equations

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

Instances For

source
def Lean.Compiler.LCNF.checkFVarUseDeferred (resultFVar fvarId : FVarId) :
ToMonoM Unit
Equations

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

Instances For

source
@[inline]
def Lean.Compiler.LCNF.argToMonoBase (check : FVarId → ToMonoM Unit) (arg : Arg) :
ToMonoM Arg
Equations

- One or more equations did not get rendered due to their size.
- Lean.Compiler.LCNF.argToMonoBase check Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.Arg.erased
- Lean.Compiler.LCNF.argToMonoBase check (Lean.Compiler.LCNF.Arg.type expr) = pure Lean.Compiler.LCNF.Arg.erased

Instances For

source
def Lean.Compiler.LCNF.argToMono (arg : Arg) :
ToMonoM Arg
Equations

- Lean.Compiler.LCNF.argToMono arg = Lean.Compiler.LCNF.argToMonoBase Lean.Compiler.LCNF.checkFVarUse arg

Instances For

source
def Lean.Compiler.LCNF.argToMonoDeferredCheck (resultFVar : FVarId) (arg : Arg) :
ToMonoM Arg
Equations

- Lean.Compiler.LCNF.argToMonoDeferredCheck resultFVar arg = Lean.Compiler.LCNF.argToMonoBase (Lean.Compiler.LCNF.checkFVarUseDeferred resultFVar) arg

Instances For

source
def Lean.Compiler.LCNF.argsToMonoWithFnType (resultFVar : FVarId) (args : Array Arg) (type : Expr) :
ToMonoM (Array Arg)
Equations

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

Instances For

source
def Lean.Compiler.LCNF.argsToMonoRedArg (resultFVar : FVarId) (args : Array Arg) (params : Array Param) (redArgs : Array Arg) :
ToMonoM (Array Arg)
Equations

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

Instances For

source
def Lean.Compiler.LCNF.ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array Arg) :
ToMonoM LetValue
Equations

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

Instances For

source
partial def Lean.Compiler.LCNF.LetValue.toMono (e : LetValue) (resultFVar : FVarId) :
ToMonoM LetValue
source
def Lean.Compiler.LCNF.LetDecl.toMono (decl : LetDecl) :
ToMonoM LetDecl
Equations

- decl.toMono = do let type ← liftM (Lean.Compiler.LCNF.toMonoType decl.type) let value ← decl.value.toMono decl.fvarId liftM (decl.update type value)

Instances For

source
def Lean.Compiler.LCNF.mkFieldParamsForComputedFields (ctorType : Expr) (numParams numNewFields : Nat) (oldFields : Array Param) :
ToMonoM (Array Param)
Equations

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

Instances For

source
partial def Lean.Compiler.LCNF.FunDecl.toMono (decl : FunDecl) :
ToMonoM FunDecl
source
partial def Lean.Compiler.LCNF.decToMono (c : Cases) :
(c.typeName == `Decidable) = true → ToMonoM Code

Convert `cases` `Decidable` => `Bool`

source
partial def Lean.Compiler.LCNF.casesNatToMono (c : Cases) :
(c.typeName == `Nat) = true → ToMonoM Code

Eliminate `cases` for `Nat`.

source
partial def Lean.Compiler.LCNF.casesIntToMono (c : Cases) :
(c.typeName == `Int) = true → ToMonoM Code

Eliminate `cases` for `Int`.

source
partial def Lean.Compiler.LCNF.casesUIntToMono (c : Cases) (uintName : Name) :
(c.typeName == uintName) = true → ToMonoM Code

Eliminate `cases` for `UInt` types.

source
partial def Lean.Compiler.LCNF.casesArrayToMono (c : Cases) :
(c.typeName == `Array) = true → ToMonoM Code

Eliminate `cases` for `Array.

source
partial def Lean.Compiler.LCNF.casesByteArrayToMono (c : Cases) :
(c.typeName == `ByteArray) = true → ToMonoM Code

Eliminate `cases` for `ByteArray.

source
partial def Lean.Compiler.LCNF.casesFloatArrayToMono (c : Cases) :
(c.typeName == `FloatArray) = true → ToMonoM Code

Eliminate `cases` for `FloatArray.

source
partial def Lean.Compiler.LCNF.casesStringToMono (c : Cases) :
(c.typeName == `String) = true → ToMonoM Code

Eliminate `cases` for `String.

source
partial def Lean.Compiler.LCNF.casesThunkToMono (c : Cases) :
(c.typeName == `Thunk) = true → ToMonoM Code

Eliminate `cases` for `Thunk.

source
partial def Lean.Compiler.LCNF.casesTaskToMono (c : Cases) :
(c.typeName == `Task) = true → ToMonoM Code

Eliminate `cases` for `Task.

source
partial def Lean.Compiler.LCNF.trivialStructToMono (info : TrivialStructureInfo) (c : Cases) :
ToMonoM Code

Eliminate `cases` for trivial structure. See `hasTrivialStructure?`

source
partial def Lean.Compiler.LCNF.Code.toMono (code : Code) :
ToMonoM Code
source
def Lean.Compiler.LCNF.Decl.toMono (decl : Decl) :
CompilerM Decl
Equations

- decl.toMono = StateRefT'.run' (Lean.Compiler.LCNF.Decl.toMono.go✝ decl) { }

Instances For

source
def Lean.Compiler.LCNF.toMono :
Pass
Equations

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

Instances For