about summary refs log tree commit diff
path: root/src/comp
diff options
context:
space:
mode:
authorTim Chevalier <chevalier@alum.wellesley.edu>2011-05-18 16:59:34 -0700
committerGraydon Hoare <graydon@mozilla.com>2011-05-19 11:40:16 -0700
commitc0f728712ba018ae0a3993232bf5b259e0c312ad (patch)
tree6c223ab27d6b5703d4188e31b4a7faa41c7b0924 /src/comp
parent2cd769e35898df0a84c797c610748a59034a9b93 (diff)
downloadrust-c0f728712ba018ae0a3993232bf5b259e0c312ad.tar.gz
rust-c0f728712ba018ae0a3993232bf5b259e0c312ad.zip
Rewrite pre_postconditions to use walk instead of fold
Diffstat (limited to 'src/comp')
-rw-r--r--src/comp/middle/tstate/ck.rs13
-rw-r--r--src/comp/middle/tstate/pre_post_conditions.rs9
2 files changed, 7 insertions, 15 deletions
diff --git a/src/comp/middle/tstate/ck.rs b/src/comp/middle/tstate/ck.rs
index 5de793d64b0..9adbd55f474 100644
--- a/src/comp/middle/tstate/ck.rs
+++ b/src/comp/middle/tstate/ck.rs
@@ -62,7 +62,7 @@ import bitvectors::promises;
 
 import annotate::annotate_crate;
 import collect_locals::mk_f_to_fn_info;
-import pre_post_conditions::check_item_fn;
+import pre_post_conditions::fn_pre_post;
 import states::find_pre_post_state_fn;
 
 fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
@@ -199,11 +199,10 @@ fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
     annotate_crate(ccx, *crate);
 
     /* Compute the pre and postcondition for every subexpression */
-    
-    auto fld = new_identity_fold[crate_ctxt]();
-    fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
-    auto with_pre_postconditions =
-           fold_crate[crate_ctxt](ccx, fld, crate);
+    auto do_pre_post = walk::default_visitor();
+    do_pre_post = rec(visit_fn_pre = bind fn_pre_post(ccx, _, _, _)
+                      with do_pre_post);
+    walk::walk_crate(do_pre_post, *crate);
     
     auto fld1 = new_identity_fold[crate_ctxt]();
 
@@ -211,7 +210,7 @@ fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
                 fold_obj     = bind check_obj_state(_,_,_,_)
                 with *fld1);
     
-    ret fold_crate[crate_ctxt](ccx, fld1, with_pre_postconditions);
+    ret fold_crate[crate_ctxt](ccx, fld1, crate);
 }
 
 //
diff --git a/src/comp/middle/tstate/pre_post_conditions.rs b/src/comp/middle/tstate/pre_post_conditions.rs
index 30437a4eeb5..ed52142f1ad 100644
--- a/src/comp/middle/tstate/pre_post_conditions.rs
+++ b/src/comp/middle/tstate/pre_post_conditions.rs
@@ -679,18 +679,11 @@ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
     find_pre_post_block(fcx, f.body);
 }
 
-fn check_item_fn(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
-                 &vec[ty_param] ty_params,
-                 &def_id id, &ann a) -> @item {
-    log("check_item_fn:");
-    log_fn(f, i, ty_params);
-
+fn fn_pre_post(crate_ctxt ccx, &_fn f, &ident i, &def_id id) -> () {
     assert (ccx.fm.contains_key(id));
     auto fcx = rec(enclosing=ccx.fm.get(id),
                    id=id, name=i, ccx=ccx);
     find_pre_post_fn(fcx, f);  
-
-    ret @respan(sp, item_fn(i, f, ty_params, id, a));
 }
 
 //