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 β))

Instances For

@[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

Instances For

@[inline]

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

Probe α α

Equations

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

Instances For

@[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))

Instances For

@[inline]

def Lean.Compiler.LCNF.Probe.sortedBySize (pu : Purity) :

Probe (Decl pu) (Nat × Decl pu)

Equations

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

Instances For

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.

Instances For

@[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))

Instances For

def Lean.Compiler.LCNF.Probe.getLetValues (pu : Purity) :

Probe (Decl pu) (LetValue pu)

Equations

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

Instances For

def Lean.Compiler.LCNF.Probe.getJps (pu : Purity) :

Probe (Decl pu) (FunDecl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

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

Probe (Decl pu) (Decl pu)

Equations

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

Instances For

@[inline]

def Lean.Compiler.LCNF.Probe.declNames (pu : Purity) :

Probe (Decl pu) Name

Equations

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

Instances For

@[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)

Instances For

@[inline]

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

Equations

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

Instances For

@[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]

Instances For

@[inline]

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

Probe α α

Equations

Lean.Compiler.LCNF.Probe.tail n data = pure ↑(Std.Rci.Sliceable.mkSlice data (data.size - n)...*)

Instances For

@[inline]

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

Probe α α

Equations

Lean.Compiler.LCNF.Probe.head n data = pure ↑(Std.Rio.Sliceable.mkSlice data *...n)

Instances For

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

Equations

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

Instances For