This module contains the implementation of the reflection monad, used by all other components of this directory.

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVBinOp : Lean.ToExpr Std.Tactic.BVDecide.BVBinOp

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVUnOp : Lean.ToExpr Std.Tactic.BVDecide.BVUnOp

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr {w : Nat} : Lean.ToExpr (Std.Tactic.BVDecide.BVExpr w)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go {w : Nat} : Std.Tactic.BVDecide.BVExpr w → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go (Std.Tactic.BVDecide.BVExpr.var idx) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BVExpr.var) (Lean.toExpr w) (Lean.toExpr idx)
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVExpr.go (Std.Tactic.BVDecide.BVExpr.const val) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BVExpr.const) (Lean.toExpr w) (Lean.toExpr val)

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVBinPred : Lean.ToExpr Std.Tactic.BVDecide.BVBinPred

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprGate : Lean.ToExpr Std.Tactic.BVDecide.Gate

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVPred : Lean.ToExpr Std.Tactic.BVDecide.BVPred

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBVPred.go : Std.Tactic.BVDecide.BVPred → Lean.Expr

Equations

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

instance Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr {α : Type} [Lean.ToExpr α] : Lean.ToExpr (Std.Tactic.BVDecide.BoolExpr α)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr.go {α : Type} [Lean.ToExpr α] : Std.Tactic.BVDecide.BoolExpr α → Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.instToExprBoolExpr.go (Std.Tactic.BVDecide.BoolExpr.const b) = Lean.mkApp2 (Lean.mkConst `Std.Tactic.BVDecide.BoolExpr.const) (Lean.toTypeExpr α) (Lean.toExpr b)

structure Lean.Elab.Tactic.BVDecide.Frontend.State : Type

The state of the reflection monad

• atoms : Std.HashMap Lean.Expr (Nat × Nat)

  The atoms encountered so far. Saved as a map from BitVec expressions to a (width, atomNumber) pair.

• atomsAssignmentCache : Lean.Expr

  A cache for atomsAssignment.

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.M (α : Type) : Type

The reflection monad, used to track BitVec variables that we see as we traverse the context.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.M = StateRefT' IO.RealWorld Lean.Elab.Tactic.BVDecide.Frontend.State Lean.MetaM

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVExpr : Type

A reified version of an Expr representing a BVExpr.

• width : Nat
• bvExpr : Std.Tactic.BVDecide.BVExpr self.width

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = originalBVExpr.

• expr : Lean.Expr

  A cache for toExpr bvExpr.

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVPred : Type

A reified version of an Expr representing a BVPred.

• bvPred : Std.Tactic.BVDecide.BVPred

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvPred.eval atomsAssignment = originalBVPredExpr.

• expr : Lean.Expr

  A cache for toExpr bvPred

structure Lean.Elab.Tactic.BVDecide.Frontend.ReifiedBVLogical : Type

A reified version of an Expr representing a BVLogicalExpr.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• evalsAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = originalBVLogicalExpr.

• expr : Lean.Expr

  A cache for toExpr bvExpr

structure Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical : Type

A reified version of an Expr representing a BVLogicalExpr that we know to be true.

• bvExpr : Std.Tactic.BVDecide.BVLogicalExpr

  The reified expression.

• satAtAtoms : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

  A proof that bvExpr.eval atomsAssignment = true.

• expr : Lean.Expr

  A cache for toExpr bvExpr

def Lean.Elab.Tactic.BVDecide.Frontend.M.run {α : Type} (m : Lean.Elab.Tactic.BVDecide.Frontend.M α) : Lean.MetaM α

Run a reflection computation as a MetaM one.

Equations

• m.run = StateRefT'.run' m { atoms := ∅, atomsAssignmentCache := Lean.mkConst `List.nil [Lean.Level.zero] }

def Lean.Elab.Tactic.BVDecide.Frontend.M.atoms : Lean.Elab.Tactic.BVDecide.Frontend.M (List (Nat × Lean.Expr))

Retrieve the atoms as pairs of their width and expression.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.M.atomsAssignment : Lean.Elab.Tactic.BVDecide.Frontend.M Lean.Expr

Retrieve a BitVec.Assignment representing the atoms we found so far.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.M.atomsAssignment = do let __do_lift ← getThe Lean.Elab.Tactic.BVDecide.Frontend.State pure __do_lift.atomsAssignmentCache

def Lean.Elab.Tactic.BVDecide.Frontend.M.lookup (e : Lean.Expr) (width : Nat) : Lean.Elab.Tactic.BVDecide.Frontend.M Nat

Look up an expression in the atoms, recording it if it has not previously appeared.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.M.lookup.updateAtomsAssignment : Lean.Elab.Tactic.BVDecide.Frontend.M Unit

Equations

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

structure Lean.Elab.Tactic.BVDecide.Frontend.LemmaState : Type

The state of the lemma reflection monad.

• lemmas : Array Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical

  The list of top level lemmas that got created on the fly during reflection.

@[reducible, inline]

abbrev Lean.Elab.Tactic.BVDecide.Frontend.LemmaM (α : Type) : Type

The lemma reflection monad. It extends the usual reflection monad M by adding the ability to add additional top level lemmas on the fly.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.LemmaM = StateRefT' IO.RealWorld Lean.Elab.Tactic.BVDecide.Frontend.LemmaState Lean.Elab.Tactic.BVDecide.Frontend.M

def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.run {α : Type} (m : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM α) (state : Lean.Elab.Tactic.BVDecide.Frontend.LemmaState := { lemmas := #[] }) : Lean.Elab.Tactic.BVDecide.Frontend.M (α × Array Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical)

Equations

• m.run state = do let __discr ← StateRefT'.run m state match __discr with | (res, state) => pure (res, state.lemmas)

def Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.addLemma (lemma : Lean.Elab.Tactic.BVDecide.Frontend.SatAtBVLogical) : Lean.Elab.Tactic.BVDecide.Frontend.LemmaM Unit

Add another top level lemma.

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.LemmaM.addLemma lemma = modify fun (s : Lean.Elab.Tactic.BVDecide.Frontend.LemmaState) => { lemmas := s.lemmas.push lemma }