max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/compiler/ir): we don't need collector

Browse source
This commit is contained in:
Leonardo de Moura 2018-04-23 08:56:22 -07:00
parent 055518bacf
commit c0d782ce3c
1 changed files with 0 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
library/init/compiler/ir.lean
View file

@ -232,62 +232,6 @@ def valid_ssa (d : decl) : bool :=
let (e, _) := d.valid_ssa.run.run (mk_var2blockid, mk_var_set)
in e.to_bool
/- Collect used variables -/
@[reducible] def collector : Type :=
state var_set unit
def var.collect (x : var) : collector :=
do s ← get, put (s.insert x)
def instr.collect_vars : instr → collector
| (instr.lit x _ _) := x.collect
| (instr.cast x _ y) := x.collect >> y.collect
| (instr.unop x _ _ y) := x.collect >> y.collect
| (instr.binop x _ _ y z) := x.collect >> y.collect >> z.collect
| (instr.call xs _ ys) := xs.mmap' var.collect >> ys.mmap' var.collect
| (instr.cnstr o _ _ _) := o.collect
| (instr.set o _ x) := o.collect >> x.collect
| (instr.get x y _) := x.collect >> y.collect
| (instr.sets o _ x) := o.collect >> x.collect
| (instr.gets x _ y _) := x.collect >> y.collect
| (instr.closure x _ ys) := x.collect >> ys.mmap' var.collect
| (instr.apply x ys) := x.collect >> ys.mmap' var.collect
| (instr.array a sz c) := a.collect >> sz.collect >> c.collect
| (instr.write a i v) := a.collect >> i.collect >> v.collect
| (instr.read x a i) := x.collect >> a.collect >> i.collect
| (instr.sarray x _ sz c) := x.collect >> sz.collect >> c.collect
| (instr.swrite a i v) := a.collect >> i.collect >> v.collect
| (instr.sread x _ a i) := x.collect >> a.collect >> i.collect
| (instr.inc x) := x.collect
| (instr.decs x) := x.collect
| (instr.dealloc x) := x.collect
| (instr.dec x) := x.collect
def phi.collect_vars : phi → collector
| {x := x, ys := ys, ..} := x.collect >> ys.mmap' var.collect
def terminator.collect_vars : terminator → collector
| (terminator.ret ys) := ys.mmap' var.collect
| (terminator.case x _) := x.collect
| (terminator.jmp _) := return ()
def block.collect_vars : block → collector
| {phis := ps, instrs := is, term := r, ..} :=
ps.mmap' phi.collect_vars >>
is.mmap' instr.collect_vars >>
r.collect_vars
def arg.collect : arg → collector
| {n := x, ..} := x.collect
def decl.collect_vars : decl → collector
| {as := as, bs := bs, ..} :=
as.mmap' arg.collect >> bs.mmap' block.collect_vars
def collect_vars (d : decl) : var_set :=
let (_, r) := d.collect_vars.run mk_var_set
in r
/- Check blockids -/
@[reducible] def blockid_check : Type :=
except_t string (state blockid_set) unit