def tacticSimp_alive_meta : Lean.ParserDescr

We eliminate our alive framework's metavarible machinery. At the end of this pass, all InstcombineTransformDialect.instantiate* must be eliminated, and all Width.mvar should be resolved into Width.concrete.

Equations

• tacticSimp_alive_meta = Lean.ParserDescr.node `tacticSimp_alive_meta 1024 (Lean.ParserDescr.nonReservedSymbol "simp_alive_meta" false)

def tacticSimp_alive_ssa : Lean.ParserDescr

Eliminate the SSA structure of the program

• We first simplify Com.refinement to see the context Γv.
• We simp_peephole Γv to simplify context accesses by variables.
• We simplify the translation overhead.

Equations

• tacticSimp_alive_ssa = Lean.ParserDescr.node `tacticSimp_alive_ssa 1024 (Lean.ParserDescr.nonReservedSymbol "simp_alive_ssa" false)

def tacticSimp_alive_peephole : Lean.ParserDescr

simp_alive_peephole extends simp_peephole to simplify goals about refinement of LLVM programs into statements about just bitvectors.

That is, the tactic expects a goal of the form: Com.Refinement com₁ com₂ That is, goals of the form Com.refine, com₁.denote Γv ⊑ com₂.denote Γv , where com₁ and com₂ are programs in the LLVM dialect.

Equations

• tacticSimp_alive_peephole = Lean.ParserDescr.node `tacticSimp_alive_peephole 1024 (Lean.ParserDescr.nonReservedSymbol "simp_alive_peephole" false)