integrate cap clause into type state, but not trans

5 files changed, 38 insertions, 15 deletions

diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index b355c99a8bc..bb68175987e 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -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) {
diff --git a/src/comp/middle/tstate/auxiliary.rs b/src/comp/middle/tstate/auxiliary.rs
index 579d4bdd813..d105a7dd579 100644
--- a/src/comp/middle/tstate/auxiliary.rs
+++ b/src/comp/middle/tstate/auxiliary.rs
@@ -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);
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 3fd1721c8f0..e8a1d2e938e 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -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 = "";
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 3ff12bcafc9..5cfdd0301a6 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -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);
diff --git a/src/comp/middle/tstate/states.rs b/src/comp/middle/tstate/states.rs
index 701ac5e04b0..209899c26b1 100644
--- a/src/comp/middle/tstate/states.rs
+++ b/src/comp/middle/tstate/states.rs
@@ -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) |