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

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.