This module contains the basic preprocessing pipeline framework for bv_normalize.

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.withDoneResult {m : Type → Type} [Monad m] (x : m Sym.Simp.Result) : m Sym.Simp.Result

inductive Lean.Meta.Tactic.BVDecide.Normalize.Target : Type

• mvarIdTarget (mvar : MVarId) : Target
• grindTarget (goal : Grind.Goal) : Target

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedTarget : Inhabited Target

def Lean.Meta.Tactic.BVDecide.Normalize.Target.mvarId : Target → MVarId

inductive Lean.Meta.Tactic.BVDecide.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.

def Lean.Meta.Tactic.BVDecide.Normalize.MatchKind.getEnumInfo : MatchKind → InductiveVal

The enum inductive that the match discriminates on.

structure Lean.Meta.Tactic.BVDecide.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.

inductive Lean.Meta.Tactic.BVDecide.Normalize.HypSource : Type

• lctx (fvar : FVarId) : HypSource
• enumDomain (n : Name) : HypSource
• structureProjection (e : Expr) : HypSource
• andFlattened (s : HypSource) : HypSource
• grind : HypSource

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHypSource : Inhabited HypSource

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource : Hashable HypSource

def Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash : HypSource → UInt64

def Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq : HypSource → HypSource → Bool

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource : BEq HypSource

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHypSource : ToMessageData HypSource

partial def Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHypSource.go (s : HypSource) : MessageData

partial def Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHypSource.stripFlatten (s : HypSource) : HypSource

structure Lean.Meta.Tactic.BVDecide.Normalize.Hyp : Type

• name : Name
• type : Expr
• value : Expr
• source : HypSource

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHyp : Inhabited Hyp

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instBEqHyp : BEq Hyp

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instHashableHyp : Hashable Hyp

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHyp : ToMessageData Hyp

structure Lean.Meta.Tactic.BVDecide.Normalize.PreProcessContext : Type

The immutable context of the bv_normalize preprocessing pipeline.

• config : Elab.Tactic.BVDecide.BVDecideConfig

  The configuration that the tactic was called with.

• restrictedTypes : Option (Array Name)

  The types that the structure and enum analysis is restricted to, as provided by the types clause. If this is none the analysis discovers the relevant types on its own.

structure Lean.Meta.Tactic.BVDecide.Normalize.PreProcessState : Type

• rewriteSimpCache : Sym.Simp.Cache

  Cache for the Simp component of the rewriter.

• rewriteDSimpCache : Sym.DSimp.Cache

  Cache for the DSimp component of the rewriter.

• acCache : Sym.Simp.Cache

  Cache for the Simp component of the AC pass.

• typeAnalysis : TypeAnalysis

  Analysis results for the structure and enum pass if required.

• target : Target

  The target we are operating on.

• hypotheses : Array Hyp

  The set of hypotheses we are operating on. These should be interpreted from withing the lctx of the goal. But they may not necessarily be fvars registered in the goal.

• didChange : Bool

  A didChange flag for our fixpoint simplification loop.

@[reducible, inline]

abbrev Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM : Type → Type

def Lean.Meta.Tactic.BVDecide.Normalize.Hyp.applySimpResult (hyp : Hyp) (result : Sym.Simp.Result) : Sym.SymM Hyp

def Lean.Meta.Tactic.BVDecide.Normalize.Hyp.applyDSimpResult (hyp : Hyp) (result : Sym.DSimp.Result) : Sym.SymM Hyp

@[inline]

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getRestrictedTypes : PreProcessM (Option (Array Name))

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTarget : PreProcessM Target

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTargetMVarId : PreProcessM MVarId

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setTarget (target : Target) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.didChange : PreProcessM Bool

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.resetDidChange : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setDidChange : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.takeRewriteSimpCache : PreProcessM Sym.Simp.Cache

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setRewriteSimpCache (cache : Sym.Simp.Cache) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropRewriteSimpCache : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.takeRewriteDSimpCache : PreProcessM Sym.DSimp.Cache

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setRewriteDSimpCache (cache : Sym.DSimp.Cache) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropRewriteDSimpCache : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.takeACCache : PreProcessM Sym.Simp.Cache

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setACCache (cache : Sym.Simp.Cache) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropACCache : PreProcessM Unit

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropFixpointCaches : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTypeAnalysis : PreProcessM TypeAnalysis

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.markInterestingMatcher (n : Name) (k : MatchKind) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.markUninterestingConst (n : Name) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run {α : Type} (ctx : PreProcessContext) (target : Target) (x : PreProcessM α) : Grind.GrindM (α × PreProcessState)

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run' {α : Type} (ctx : PreProcessContext) (target : Target) (x : PreProcessM α) : Grind.GrindM α

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.pushHyp (hyp : Hyp) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.addHyps (hyps : Array Hyp) : PreProcessM Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getHyps : PreProcessM (Array Hyp)

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.flatMapHyps {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadRef m] [MonadLiftT PreProcessM m] (f : Hyp → m (Array Hyp)) : m Unit

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapIdxHyps {m : Type → Type} [Monad m] [MonadLiftT PreProcessM m] [MonadError m] [MonadMCtx m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [Sym.Internal.MonadShareCommon m] (f : Nat → Hyp → m Hyp) : m Bool

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapHyps {m : Type → Type} [Monad m] [MonadLiftT PreProcessM m] [MonadError m] [MonadMCtx m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [Sym.Internal.MonadShareCommon m] (f : Hyp → m Hyp) : m Bool

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.forHyps {m : Type → Type} [Monad m] [MonadLiftT PreProcessM m] [MonadError m] (f : Hyp → m Unit) : m Unit

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapSimpHyps (methods : Sym.Simp.Methods) (config : Sym.Simp.Config) : PreProcessM Bool

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapDSimpHyps (methods : Sym.DSimp.Methods) (config : Sym.DSimp.Config) : PreProcessM Bool

structure Lean.Meta.Tactic.BVDecide.Normalize.Pass : Type

A pass in the normalization pipeline. It operates on the current set of hypotheses stored in the PreProcessM monad. If it manages to find a way to close the associated goal it can indicate so by returning true. Otherwise it should always return false.

• name : Name
• run' : PreProcessM Bool

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.Pass.run (pass : Pass) : PreProcessM Bool

def Lean.Meta.Tactic.BVDecide.Normalize.Pass.fixpointPipeline (passes : List Pass) : PreProcessM Bool

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