fix oversights

This commit is contained in:
Folkert 2021-01-28 15:32:22 +01:00
parent 74e94869e3
commit 55eff1dba1
10 changed files with 87 additions and 128 deletions

View file

@ -32,10 +32,6 @@ pub fn occuring_variables(stmt: &Stmt<'_>) -> (MutSet<Symbol>, MutSet<Symbol>) {
stack.push(cont);
}
Info(_, cont) => {
stack.push(cont);
}
Invoke {
symbol,
call,
@ -712,16 +708,6 @@ impl<'a> Context<'a> {
)
}
Info(info, cont) => {
let (cont, live_vars) = self.visit_stmt(cont);
let stmt = Info(info.clone(), cont);
let stmt = self.arena.alloc(stmt);
(stmt, live_vars)
}
Invoke {
symbol,
call,
@ -928,20 +914,6 @@ pub fn collect_stmt(
collect_stmt(cont, jp_live_vars, vars)
}
Info(_, cont) => collect_stmt(cont, jp_live_vars, vars),
Jump(id, arguments) => {
vars.extend(arguments.iter().copied());
// NOTE deviation from Lean
// we fall through when no join point is available
if let Some(jvars) = jp_live_vars.get(id) {
vars.extend(jvars);
}
vars
}
Join {
id: j,
parameters,
@ -959,6 +931,18 @@ pub fn collect_stmt(
collect_stmt(b, &jp_live_vars, vars)
}
Jump(id, arguments) => {
vars.extend(arguments.iter().copied());
// NOTE deviation from Lean
// we fall through when no join point is available
if let Some(jvars) = jp_live_vars.get(id) {
vars.extend(jvars);
}
vars
}
Switch {
cond_symbol,
branches,