This module contains the basic preprocessing pipeline framework for bv_normalize.

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessState : Type

• rewriteCache : Std.HashSet FVarId

  Contains FVarId that we already know are in bv_normalize simp normal form and thus don't need to be processed again when we visit the next time.

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM : Type → Type

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.getConfig : PreProcessM BVDecideConfig

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.getConfig = read

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.checkRewritten (fvar : FVarId) : PreProcessM Bool

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.checkRewritten fvar = do let __do_lift ← get pure (__do_lift.rewriteCache.contains fvar)

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.rewriteFinished (fvar : FVarId) : PreProcessM Unit

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.run {α : Type} (cfg : BVDecideConfig) (goal : MVarId) (x : PreProcessM α) : MetaM α

Equations

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

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass : Type

A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes the goal fully, indicated by returning none.

• name : Name
• run' : MVarId → PreProcessM (Option MVarId)

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.run (pass : Pass) (goal : MVarId) : PreProcessM (Option MVarId)

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.fixpointPipeline (passes : List Pass) (goal : MVarId) : PreProcessM (Option MVarId)

Repeatedly run a list of Pass until they either close the goal or an iteration doesn't change the goal anymore.