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)
Instances For
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)
Instances For
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)