Documentation

Lean.Compiler.LCNF.Probing

@[reducible, inline]

abbrev Lean.Compiler.LCNF.Probe (α : Type u_1) (β : Type) :

Type u_1

Equations

Lean.Compiler.LCNF.Probe α β = (Array α → Lean.Compiler.LCNF.CompilerM (Array β))

@[inline]

def Lean.Compiler.LCNF.Probe.map {α : Type u_1} {β : Type} (f : α → CompilerM β) :

Probe α β

Equations

Lean.Compiler.LCNF.Probe.map f data = Array.mapM f data

@[inline]

def Lean.Compiler.LCNF.Probe.filter {α : Type} (f : α → CompilerM Bool) :

Probe α α

Equations

Lean.Compiler.LCNF.Probe.filter f data = Array.filterM f data

@[inline]

def Lean.Compiler.LCNF.Probe.sorted {α : Type} [Inhabited α] [LT α] [DecidableLT α] :

Probe α α

Equations

Lean.Compiler.LCNF.Probe.sorted data = pure (data.qsort fun (x1 x2 : α) => decide (x1 < x2))

@[inline]

def Lean.Compiler.LCNF.Probe.sortedBySize :

Probe Decl (Nat × Decl)

Equations

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

def Lean.Compiler.LCNF.Probe.countUnique {α : Type} [ToString α] [BEq α] [Hashable α] :

Probe α (α × Nat)

Equations

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

@[inline]

def Lean.Compiler.LCNF.Probe.countUniqueSorted {α : Type} [ToString α] [BEq α] [Hashable α] [Inhabited α] :

Probe α (α × Nat)

Equations

Lean.Compiler.LCNF.Probe.countUniqueSorted = Lean.Compiler.LCNF.Probe.countUnique >=> fun (data : Array (α × Nat)) => pure (data.qsort fun (l r : α × Nat) => decide (l.snd < r.snd))

def Lean.Compiler.LCNF.Probe.getLetValues :

Probe Decl LetValue

Equations

Lean.Compiler.LCNF.Probe.getLetValues decls = do let __discr ← (Lean.Compiler.LCNF.Probe.getLetValues.start decls).run #[] match __discr with | (fst, res) => pure res

partial def Lean.Compiler.LCNF.Probe.getLetValues.go (c : Code) :

StateRefT' IO.RealWorld (Array LetValue) CompilerM Unit

def Lean.Compiler.LCNF.Probe.getLetValues.start (decls : Array Decl) :

StateRefT' IO.RealWorld (Array LetValue) CompilerM Unit

Equations

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

def Lean.Compiler.LCNF.Probe.getJps :

Probe Decl FunDecl

Equations

Lean.Compiler.LCNF.Probe.getJps decls = do let __discr ← (Lean.Compiler.LCNF.Probe.getJps.start decls).run #[] match __discr with | (fst, res) => pure res

partial def Lean.Compiler.LCNF.Probe.getJps.go (code : Code) :

StateRefT' IO.RealWorld (Array FunDecl) CompilerM Unit

def Lean.Compiler.LCNF.Probe.getJps.start (decls : Array Decl) :

StateRefT' IO.RealWorld (Array FunDecl) CompilerM Unit

Equations

Lean.Compiler.LCNF.Probe.getJps.start decls = Array.forM (fun (x : Lean.Compiler.LCNF.Decl) => Lean.Compiler.LCNF.DeclValue.forCodeM Lean.Compiler.LCNF.Probe.getJps.go x.value) decls

def Lean.Compiler.LCNF.Probe.filterByLet (f : LetDecl → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByLet f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByLet.go f)

partial def Lean.Compiler.LCNF.Probe.filterByLet.go (f : LetDecl → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByFun (f : FunDecl → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByFun f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByFun.go f)

partial def Lean.Compiler.LCNF.Probe.filterByFun.go (f : FunDecl → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByJp (f : FunDecl → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByJp f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByJp.go f)

partial def Lean.Compiler.LCNF.Probe.filterByJp.go (f : FunDecl → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByFunDecl (f : FunDecl → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByFunDecl f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByFunDecl.go f)

partial def Lean.Compiler.LCNF.Probe.filterByFunDecl.go (f : FunDecl → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByCases (f : Cases → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByCases f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByCases.go f)

partial def Lean.Compiler.LCNF.Probe.filterByCases.go (f : Cases → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByJmp (f : FVarId → Array Arg → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByJmp f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByJmp.go f)

partial def Lean.Compiler.LCNF.Probe.filterByJmp.go (f : FVarId → Array Arg → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByReturn (f : FVarId → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByReturn f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByReturn.go f)

partial def Lean.Compiler.LCNF.Probe.filterByReturn.go (f : FVarId → CompilerM Bool) :

Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByUnreach (f : Expr → CompilerM Bool) :

Probe Decl Decl

Equations

Lean.Compiler.LCNF.Probe.filterByUnreach f = Lean.Compiler.LCNF.Probe.filter fun (x : Lean.Compiler.LCNF.Decl) => x.value.isCodeAndM (Lean.Compiler.LCNF.Probe.filterByUnreach.go f)

partial def Lean.Compiler.LCNF.Probe.filterByUnreach.go (f : Expr → CompilerM Bool) :

Code → CompilerM Bool

@[inline]

def Lean.Compiler.LCNF.Probe.declNames :

Probe Decl Name

Equations

Lean.Compiler.LCNF.Probe.declNames = Lean.Compiler.LCNF.Probe.map fun (decl : Lean.Compiler.LCNF.Decl) => pure decl.name

@[inline]

def Lean.Compiler.LCNF.Probe.toString {α : Type u_1} [ToString α] :

Probe α String

Equations

Lean.Compiler.LCNF.Probe.toString = Lean.Compiler.LCNF.Probe.map fun (x : α) => pure (toString x)

@[inline]

def Lean.Compiler.LCNF.Probe.count {α : Type u_1} :

Equations

Lean.Compiler.LCNF.Probe.count data = pure #[data.size]

@[inline]

def Lean.Compiler.LCNF.Probe.sum :

Equations

Lean.Compiler.LCNF.Probe.sum data = pure #[Array.foldl (fun (x1 x2 : Nat) => x1 + x2) 0 data]

@[inline]

def Lean.Compiler.LCNF.Probe.tail {α : Type} (n : Nat) :

Probe α α

Equations

Lean.Compiler.LCNF.Probe.tail n data = pure (let a := data; ↑(a.toSubarray (data.size - n)))

@[inline]

def Lean.Compiler.LCNF.Probe.head {α : Type} (n : Nat) :

Probe α α

Equations

Lean.Compiler.LCNF.Probe.head n data = pure ↑(data.toSubarray 0 n)

def Lean.Compiler.LCNF.Probe.runOnDeclsNamed {β : Type} (declNames : Array Name) (probe : Probe Decl β) (phase : Phase := Phase.base) :

CoreM (Array β)

Equations

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

def Lean.Compiler.LCNF.Probe.runOnModule {β : Type} (moduleName : Name) (probe : Probe Decl β) (phase : Phase := Phase.base) :

CoreM (Array β)

Equations

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

def Lean.Compiler.LCNF.Probe.runGlobally {β : Type} (probe : Probe Decl β) (phase : Phase := Phase.base) :

CoreM (Array β)

Equations

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

def Lean.Compiler.LCNF.Probe.toPass {β : Type} [ToString β] (probe : Probe Decl β) (phase : Phase) :

Equations

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