integrate cap clause into type state, but not trans
This commit is contained in:
parent
b2b2a430df
commit
41ae146057
@ -3551,7 +3551,7 @@ fn trans_expr(bcx: @block_ctxt, e: @ast::expr, dest: dest) -> @block_ctxt {
|
||||
ret trans_unary(bcx, op, x, e.id, dest);
|
||||
}
|
||||
// NDM captures
|
||||
ast::expr_fn(f, cap) {
|
||||
ast::expr_fn(f, cap_clause) {
|
||||
ret trans_closure::trans_expr_fn(bcx, f, e.span, e.id, dest);
|
||||
}
|
||||
ast::expr_bind(f, args) {
|
||||
|
@ -865,7 +865,6 @@ fn copy_in_poststate_two(fcx: fn_ctxt, src_post: poststate,
|
||||
};
|
||||
}
|
||||
|
||||
|
||||
/* FIXME should refactor this better */
|
||||
fn forget_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dead_v: node_id) {
|
||||
// In the postcondition given by parent_exp, clear the bits
|
||||
@ -875,6 +874,9 @@ fn forget_in_postcond(fcx: fn_ctxt, parent_exp: node_id, dead_v: node_id) {
|
||||
some(d_id) {
|
||||
for c: norm_constraint in constraints(fcx) {
|
||||
if constraint_mentions(fcx, c, d_id) {
|
||||
log ("clearing constraint ",
|
||||
c.bit_num,
|
||||
constraint_to_str(fcx.ccx.tcx, c.c));
|
||||
clear_in_postcond(c.bit_num,
|
||||
node_id_to_ts_ann(fcx.ccx,
|
||||
parent_exp).conditions);
|
||||
|
@ -3,7 +3,7 @@ import syntax::ast;
|
||||
import ast::{_fn, stmt,
|
||||
fn_ident, node_id, crate, return_val, noreturn,
|
||||
expr};
|
||||
import syntax::visit;
|
||||
import syntax::{visit, print};
|
||||
import syntax::codemap::span;
|
||||
import middle::ty::{type_is_nil, ret_ty_of_fn};
|
||||
import tstate::ann::{
|
||||
@ -73,14 +73,12 @@ fn check_states_stmt(s: @stmt, fcx: fn_ctxt, v: visit::vt<fn_ctxt>) {
|
||||
let pres: prestate = ann_prestate(a);
|
||||
|
||||
|
||||
/*
|
||||
log_err("check_states_stmt:");
|
||||
log_stmt_err(*s);
|
||||
log_err("prec = ");
|
||||
log_tritv_err(fcx, prec);
|
||||
log_err("pres = ");
|
||||
log_tritv_err(fcx, pres);
|
||||
*/
|
||||
log("check_states_stmt:");
|
||||
log print::pprust::stmt_to_str(*s);
|
||||
log("prec = ");
|
||||
log_tritv(fcx, prec);
|
||||
log("pres = ");
|
||||
log_tritv(fcx, pres);
|
||||
|
||||
if !implies(pres, prec) {
|
||||
let ss = "";
|
||||
|
@ -339,13 +339,21 @@ fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
|
||||
find_pre_post_expr(fcx, arg);
|
||||
copy_pre_post(fcx.ccx, e.id, arg);
|
||||
}
|
||||
expr_fn(f, _) { // NDM captures
|
||||
expr_fn(f, cap_clause) {
|
||||
let rslt = expr_pp(fcx.ccx, e);
|
||||
clear_pp(rslt);
|
||||
for @{def, span} in *freevars::get_freevars(fcx.ccx.tcx, e.id) {
|
||||
for def in *freevars::get_freevars(fcx.ccx.tcx, e.id) {
|
||||
log ("handle_var_def: def=", def);
|
||||
handle_var_def(fcx, rslt, def, "upvar");
|
||||
handle_var_def(fcx, rslt, def.def, "upvar");
|
||||
}
|
||||
|
||||
vec::iter(cap_clause.moves) { |cap_item|
|
||||
log ("forget_in_postcond: ", cap_item);
|
||||
forget_in_postcond(fcx, e.id, cap_item.id);
|
||||
}
|
||||
|
||||
let ann = node_id_to_ts_ann(fcx.ccx, e.id);
|
||||
log_cond(tritv::to_vec(ann.conditions.postcondition));
|
||||
}
|
||||
expr_block(b) {
|
||||
find_pre_post_block(fcx, b);
|
||||
|
@ -320,6 +320,19 @@ fn join_then_else(fcx: fn_ctxt, antec: @expr, conseq: blk,
|
||||
ret changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_cap_clause(fcx: fn_ctxt, e_id: node_id,
|
||||
pres: prestate, cap_clause: capture_clause)
|
||||
-> bool
|
||||
{
|
||||
let ccx = fcx.ccx;
|
||||
let pres_changed = set_prestate_ann(ccx, e_id, pres);
|
||||
let post = tritv_clone(pres);
|
||||
vec::iter(cap_clause.moves) { |cap_item|
|
||||
forget_in_poststate(fcx, post, cap_item.id);
|
||||
}
|
||||
ret set_poststate_ann(ccx, e_id, post) || pres_changed;
|
||||
}
|
||||
|
||||
fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
|
||||
let num_constrs = num_constraints(fcx.enclosing);
|
||||
|
||||
@ -358,7 +371,9 @@ fn find_pre_post_state_expr(fcx: fn_ctxt, pres: prestate, e: @expr) -> bool {
|
||||
}
|
||||
expr_mac(_) { fcx.ccx.tcx.sess.bug("unexpanded macro"); }
|
||||
expr_lit(l) { ret pure_exp(fcx.ccx, e.id, pres); }
|
||||
expr_fn(f, _) { ret pure_exp(fcx.ccx, e.id, pres); } // NDM Captures
|
||||
expr_fn(_, cap_clause) {
|
||||
ret find_pre_post_state_cap_clause(fcx, e.id, pres, *cap_clause);
|
||||
}
|
||||
expr_block(b) {
|
||||
ret find_pre_post_state_block(fcx, pres, b) |
|
||||
set_prestate_ann(fcx.ccx, e.id, pres) |
|
||||
|
Loading…
Reference in New Issue
Block a user