This module contains the basic preprocessing pipeline framework for bv_normalize.

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

Contains the result of the type analysis to be used in the structures and enums pass.

• interestingStructures : Std.HashSet Name

  Structures that are interesting for the structures pass.

• interestingEnums : Std.HashSet Name

  Inductives enums that are interesting for the enums pass.

• uninteresting : Std.HashSet Name

  Other types that we've seen that are not interesting, currently only used as a cache.

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.

• typeAnalysis : TypeAnalysis

  Analysis results for the structure and enum pass if required.

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

@[inline]

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.

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.getTypeAnalysis : PreProcessM TypeAnalysis

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.getTypeAnalysis = do let __do_lift ← get pure __do_lift.typeAnalysis

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.lookupInterestingStructure (n : Name) : PreProcessM (Option Bool)

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.modifyTypeAnalysis (f : TypeAnalysis → TypeAnalysis) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.markInterestingStructure (n : Name) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.markInterestingEnum (n : Name) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.markUninterestingType (n : Name) : PreProcessM Unit

Equations

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

@[inline]

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)

@[inline]

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.