Documentation

Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Basic

This module contains the basic preprocessing pipeline framework for bv_normalize.

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

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

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

source
@[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.
source
@[inline]
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.getConfig :
PreProcessM BVDecideConfig
Equations
source
@[inline]
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.checkRewritten (fvar : FVarId) :
PreProcessM Bool
Equations
source
@[inline]
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.checkAcNf (fvar : FVarId) :
PreProcessM Bool
Equations
source
@[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.
source
@[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.
source
@[inline]
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PreProcessM.getTypeAnalysis :
PreProcessM TypeAnalysis
Equations
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
@[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.
source
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.

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