Lean.Util.FoldConsts

source

@[inline]

abbrev Lean.Expr.FoldConstsImpl.cacheSize :

USize

Equations

Lean.Expr.FoldConstsImpl.cacheSize = 8192

source

structure Lean.Expr.FoldConstsImpl.State :

Type

visitedTerms : Array Lean.Expr
visitedConsts : Lean.NameHashSet

source

@[inline]

abbrev Lean.Expr.FoldConstsImpl.FoldM (α : Type) :

Type

Equations

Lean.Expr.FoldConstsImpl.FoldM = StateM Lean.Expr.FoldConstsImpl.State

source

unsafe def Lean.Expr.FoldConstsImpl.visited (e : Lean.Expr) (size : USize) :

Lean.Expr.FoldConstsImpl.FoldM Bool

Equations

Lean.Expr.FoldConstsImpl.visited e size = do let s ← get let h : USize := ptrAddrUnsafe e let i : USize := h % size let k : Lean.Expr := Array.uget s.visitedTerms i (_ : USize.toNat (ptrAddrUnsafe e % size) < Array.size s.visitedTerms) if (ptrAddrUnsafe k == h) = true then pure true else do modify fun s => { visitedTerms := Array.uset s.visitedTerms i e (_ : USize.toNat (ptrAddrUnsafe e % size) < Array.size s.visitedTerms), visitedConsts := s.visitedConsts } pure false

source

unsafe def Lean.Expr.FoldConstsImpl.fold {α : Type} (f : Lean.Name → α → α) (size : USize) (e : Lean.Expr) (acc : α) :

Lean.Expr.FoldConstsImpl.FoldM α

Equations

Lean.Expr.FoldConstsImpl.fold f size e acc = (fun visit => visit e acc) (Lean.Expr.FoldConstsImpl.fold.visit f size)

source

unsafe def Lean.Expr.FoldConstsImpl.fold.visit {α : Type} (f : Lean.Name → α → α) (size : USize) (e : Lean.Expr) (acc : α) :

Lean.Expr.FoldConstsImpl.FoldM α

Equations

Lean.Expr.FoldConstsImpl.fold.visit f size e acc = do let a ← Lean.Expr.FoldConstsImpl.visited e size if a = true then pure acc else match e with | Lean.Expr.forallE x d b x_1 => do let a ← Lean.Expr.FoldConstsImpl.fold.visit f size d acc Lean.Expr.FoldConstsImpl.fold.visit f size b a | Lean.Expr.lam x d b x_1 => do let a ← Lean.Expr.FoldConstsImpl.fold.visit f size d acc Lean.Expr.FoldConstsImpl.fold.visit f size b a | Lean.Expr.mdata x b x_1 => Lean.Expr.FoldConstsImpl.fold.visit f size b acc | Lean.Expr.letE x t v b x_1 => do let a ← Lean.Expr.FoldConstsImpl.fold.visit f size t acc let a ← Lean.Expr.FoldConstsImpl.fold.visit f size v a Lean.Expr.FoldConstsImpl.fold.visit f size b a | Lean.Expr.app f a x => do let a_1 ← Lean.Expr.FoldConstsImpl.fold.visit f size f acc Lean.Expr.FoldConstsImpl.fold.visit f size a a_1 | Lean.Expr.proj x x_1 b x_2 => Lean.Expr.FoldConstsImpl.fold.visit f size b acc | Lean.Expr.const c x x_1 => do let s ← get if Lean.NameHashSet.contains s.visitedConsts c = true then pure acc else do modify fun s => { visitedTerms := s.visitedTerms, visitedConsts := Lean.NameHashSet.insert s.visitedConsts c } pure (f c acc) | x => pure acc

source

unsafe def Lean.Expr.FoldConstsImpl.initCache :

Lean.Expr.FoldConstsImpl.State

Equations

Lean.Expr.FoldConstsImpl.initCache = { visitedTerms := mkArray (USize.toNat Lean.Expr.FoldConstsImpl.cacheSize) (cast Lean.Expr.FoldConstsImpl.initCache.proof_1 ()), visitedConsts := ∅ }

source

@[inline]

unsafe def Lean.Expr.FoldConstsImpl.foldUnsafe {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Name → α → α) :

α

Equations

Lean.Expr.FoldConstsImpl.foldUnsafe e init f = StateT.run' (Lean.Expr.FoldConstsImpl.fold f Lean.Expr.FoldConstsImpl.cacheSize e init) Lean.Expr.FoldConstsImpl.initCache

source

@[implementedBy Lean.Expr.FoldConstsImpl.foldUnsafe]

constant Lean.Expr.foldConsts {α : Type} (e : Lean.Expr) (init : α) (f : Lean.Name → α → α) :

α

source

def Lean.Expr.getUsedConstants (e : Lean.Expr) :

Array Lean.Name

Equations

Lean.Expr.getUsedConstants e = Lean.Expr.foldConsts e #[] fun c cs => Array.push cs c

source

def Lean.getMaxHeight (env : Lean.Environment) (e : Lean.Expr) :

UInt32

Equations

Lean.getMaxHeight env e = Lean.Expr.foldConsts e 0 fun constName max => match Lean.Environment.find? env constName with | some (Lean.ConstantInfo.defnInfo val) => match val.hints with | Lean.ReducibilityHints.regular h => if h > max then h else max | x => max | x => max