This module contains the basic preprocessing pipeline framework for bv_normalize.

inductive Lean.Elab.Tactic.BVDecide.Frontend.Normalize.MatchKind : Type

The various kinds of matches supported by the match to cond infrastructure.

• simpleEnum (info : InductiveVal) (ctors : Array ConstructorVal) : MatchKind

  It is a full match statement on an enum inductive with one constructor handled per arm. The ctors are listed in the order they occur in the match statement in ctors.

• enumWithDefault (info : InductiveVal) (ctors : Array ConstructorVal) : MatchKind

  It is a match statement on an enum inductive with a default arm, all explicitly handled ctors are listed in ctors in the order they occur in the match statement.

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.

• interestingMatchers : Std.HashMap Name MatchKind

  func.match_x auxiliary declarations that we consider interesting.

• 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.

• acNfCache : Std.HashSet FVarId

  Contains FVarId that we already know have been run through the AC normal form and thus don't 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.checkAcNf (fvar : FVarId) : PreProcessM Bool

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.checkAcNf fvar = do let __do_lift ← get pure (__do_lift.acNfCache.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.acNfFinished (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.markInterestingMatcher (n : Name) (k : MatchKind) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.markUninterestingConst (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.