This module contains the implementation of the pre processing pass for handling enum inductive types.

The implementation:

1. generates mappings from enum inductives occurring in the goal to sufficiently large BitVec and replaces equality on the enum inductives with equality on these mapping functions.
2. Constant folds these mappings if appropriate.
3. Adds bounds on the values returned by the mappings if the size of the enum inductive does not fit into a power of two.
4. Handles applications of these mappings to ite, cond and basic match statements.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecSuffix : String

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.eqIffEnumToBitVecEqSuffix : String

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecLeSuffix : String

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.matchEqCondSuffix : String

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEnumToBitVecFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive construct a function of type declName → BitVec w that maps declName constructors to their numeric indices as BitVec.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEqIffEnumToBitVecEqFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive, construct a proof of ∀ (x y : declName) : x = y ↔ x.enumToBitVec = y.enumToBitVec.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEnumToBitVecLeFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive, construct a proof of ∀ (x : declName) : x.enumToBitVec ≤ domainSize - 1 where domainSize is the amount of constructors of declName.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getMatchEqCondFor (declName : Name) : MetaM Name

Obtain a theorem that translates .match_x applications on enum inductives to chains of cond applications. If the specific .match_x that this is being called on is unsupported throw an error.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecCtor : Meta.Simp.Simproc

This simproc should be set up to trigger on expressions of the form EnumInductive.enumToBitVec x. It will check if x is a constructor and if that is the case constant fold it to the corresponding BitVec value.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumsPass : Pass

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumsPass.postprocess (goal : MVarId) : StateRefT' IO.RealWorld Lean.Elab.Tactic.BVDecide.Frontend.Normalize.PostProcessState✝ MetaM MVarId