Mapping from variable to projections
Instances For
Instances For
Instances For
Create a mapping from variables to projections. This function assumes variable ids have been normalized
Instances For
- projMap : Lean.IR.ExpandResetReuse.ProjMap
Instances For
Return true iff x
is consumed in all branches of the current block.
Here consumption means the block contains a dec x
or reuse x ...
.
Auxiliary function for eraseProjIncFor
Try to erase inc
instructions on projections of y
occurring in the tail of bs
.
Return the updated bs
and a bit mask specifying which inc
s have been removed.
Instances For
Replace reuse x ctor ...
with ctor ...
, and remoce dec x
replace
x := reset y; b
with
inc z_1; ...; inc z_i; dec y; b'
where z_i
's are the variables in mask
,
and b'
is b
where we removed dec x
and replaced reuse x ctor_i ...
with ctor_i ...
.
Instances For
Instances For
Instances For
Given set x[i] := y
, return true iff y := proj[i] x
Instances For
Given uset x[i] := y
, return true iff y := uproj[i] x
Instances For
Given sset x[n, i] := y
, return true iff y := sproj[n, i] x
Instances For
Remove unnecessary set/uset/sset
operations
replace
x := reset y; b
with
let f_i_1 := proj[i_1] y;
...
let f_i_k := proj[i_k] y;
b'
where i_j
s are the field indexes
that the code did not touch immediately before the reset.
That is mask[j] == none
.
b'
is b
where y
dec x
is replaced with del y
,
and z := reuse x ctor_i ws; F
is replaced with
set x i ws[i]
operations, and we replace z
with x
in F
Instances For
Instances For
(Try to) expand reset
and reuse
instructions.