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

Equations

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

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedTarget = { default := Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedTarget.default }

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

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.Target.mvarIdTarget mvar).mvarId = mvar
• (Lean.Meta.Tactic.BVDecide.Normalize.Target.grindTarget goal).mvarId = goal.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.

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.MatchKind.simpleEnum info ctors).getEnumInfo = info
• (Lean.Meta.Tactic.BVDecide.Normalize.MatchKind.enumWithDefault info ctors).getEnumInfo = info

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHypSource = { default := Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHypSource.default }

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource = { hash := Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash }

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.lctx a) = mixHash 0 (hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.enumDomain a) = mixHash 1 (hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.structureProjection a) = mixHash 2 (hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash a.andFlattened = mixHash 3 (Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash Lean.Meta.Tactic.BVDecide.Normalize.HypSource.grind = 4

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.lctx a) (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.lctx b) = (a == b)
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.enumDomain a) (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.enumDomain b) = (a == b)
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq a.andFlattened b.andFlattened = Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq a b
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq Lean.Meta.Tactic.BVDecide.Normalize.HypSource.grind Lean.Meta.Tactic.BVDecide.Normalize.HypSource.grind = true
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq x✝¹ x✝ = false

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource = { beq := Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq }

@[instance_reducible]

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

Equations

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

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHyp = { default := Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHyp.default }

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHyp = { beq := fun (lhs rhs : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => lhs.type == rhs.type }

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHyp = { hash := fun (hyp : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => hash hyp.type }

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHyp = { toMessageData := fun (hyp : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => Lean.toMessageData hyp.type }

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• hyp.applySimpResult (Lean.Meta.Sym.Simp.Result.rfl done dep) = pure hyp

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

Equations

• hyp.applyDSimpResult result = pure { name := hyp.name, type := Lean.Meta.Sym.DSimp.Result.getResultExpr hyp.type result, value := hyp.value, source := hyp.source }

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getConfig = do let __do_lift ← read pure __do_lift.config

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getRestrictedTypes = do let __do_lift ← read pure __do_lift.restrictedTypes

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTarget = do let __do_lift ← get pure __do_lift.target

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTargetMVarId = do let __do_lift ← get pure __do_lift.target.mvarId

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.didChange = do let __do_lift ← get pure __do_lift.didChange

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropRewriteSimpCache = discard Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.takeRewriteSimpCache

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropRewriteDSimpCache = discard Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.takeRewriteDSimpCache

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropACCache = discard Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.takeACCache

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.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.Meta.Tactic.BVDecide.Normalize.PreProcessM.markUninterestingConst (n : Name) : PreProcessM Unit

Equations

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

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run ctx target x = (ReaderT.run x ctx).run { target := target }

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run' ctx target x = (ReaderT.run x ctx).run' { target := target }

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getHyps = do let __do_lift ← get pure __do_lift.hypotheses

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapHyps f = Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapIdxHyps fun (x : Nat) (hyp : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => f hyp

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.forHyps f = do let hyps ← liftM Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getHyps Array.forM f hyps

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapSimpHyps methods config = (Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapSimpHyps.go✝ methods config).run' { }

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

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapDSimpHyps methods config = (Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapDSimpHyps.go✝ methods config).run' { }

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

Equations

• pass.run = Lean.withTraceNode `Meta.Tactic.bv (fun (x : Except Lean.Exception Bool) => pure (Lean.toMessageData "Running pass: " ++ Lean.toMessageData pass.name)) pass.run'

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.

Equations

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