Merge branch 'master' of github.com:graydon/rust

11 files changed, 689 insertions, 218 deletions

diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs
index 46666a34378..d41e6d60686 100644
--- a/src/comp/front/ast.rs
+++ b/src/comp/front/ast.rs
@@ -188,7 +188,7 @@ fn binop_to_str(binop op) -> str {
 
 
 tag unop {
-    box;
+    box(mutability);
     deref;
     bitnot;
     not;
@@ -197,7 +197,10 @@ tag unop {
 
 fn unop_to_str(unop op) -> str {
     alt (op) {
-        case (box) {ret "@";}
+        case (box(?mt)) {
+            if (mt == mut) { ret "@mutable"; }
+            ret "@";
+        }
         case (deref) {ret "*";}
         case (bitnot) {ret "~";}
         case (not) {ret "!";}
@@ -255,7 +258,7 @@ tag expr_ {
     expr_tup(vec[elt], ann);
     expr_rec(vec[field], option.t[@expr], ann);
     expr_call(@expr, vec[@expr], ann);
-    expr_call_self(@expr, vec[@expr], ann);
+    expr_call_self(ident, vec[@expr], ann);
     expr_bind(@expr, vec[option.t[@expr]], ann);
     expr_spawn(spawn_dom, option.t[str], @expr, vec[@expr], ann);
     expr_binary(binop, @expr, @expr, ann);
diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs
index 4c3e6cf03be..27fdc7feb2d 100644
--- a/src/comp/front/parser.rs
+++ b/src/comp/front/parser.rs
@@ -887,17 +887,19 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr {
         }
 
         case (token.SELF) {
+            log "parsing a self-call...";
+
             p.bump();
             expect(p, token.DOT);
             // The rest is a call expression.
-            auto e = parse_bottom_expr(p);
+            auto e = parse_ident(p);
             auto pf = parse_expr;
             auto es = parse_seq[@ast.expr](token.LPAREN,
                                            token.RPAREN,
                                            some(token.COMMA),
                                            pf, p);
             hi = es.span;
-            auto ex = ast.expr_call_self(e, es.node, ast.ann_none);
+            ex = ast.expr_call_self(e, es.node, ast.ann_none);
         }
 
         case (_) {
@@ -1074,9 +1076,10 @@ impure fn parse_prefix_expr(parser p) -> @ast.expr {
 
         case (token.AT) {
             p.bump();
+            auto m = parse_mutability(p);
             auto e = parse_prefix_expr(p);
             hi = e.span;
-            ex = ast.expr_unary(ast.box, e, ast.ann_none);
+            ex = ast.expr_unary(ast.box(m), e, ast.ann_none);
         }
 
         case (_) {
diff --git a/src/comp/front/token.rs b/src/comp/front/token.rs
index 5ac9d662f1c..dcfafadf202 100644
--- a/src/comp/front/token.rs
+++ b/src/comp/front/token.rs
@@ -348,6 +348,8 @@ fn to_str(token t) -> str {
 
         /* Object type */
         case (OBJ) { ret "obj"; }
+        case (SELF) { ret "self"; }
+
 
         /* Comm and task types */
         case (CHAN) { ret "chan"; }
diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index d7a18783cbb..77c898366af 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -88,7 +88,7 @@ type ast_fold[ENV] =
          ann a) -> @expr)                         fold_expr_call,
 
      (fn(&ENV e, &span sp,
-         @expr f, vec[@expr] args,
+         ident id, vec[@expr] args,
          ann a) -> @expr)                         fold_expr_call_self,
 
      (fn(&ENV e, &span sp,
@@ -566,10 +566,9 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr {
             ret fld.fold_expr_call(env_, e.span, ff, aargs, t);
         }
 
-        case (ast.expr_call_self(?f, ?args, ?t)) {
-            auto ff = fold_expr(env_, fld, f);
+        case (ast.expr_call_self(?ident, ?args, ?t)) {
             auto aargs = fold_exprs(env_, fld, args);
-            ret fld.fold_expr_call_self(env_, e.span, ff, aargs, t);
+            ret fld.fold_expr_call_self(env_, e.span, ident, aargs, t);
         }
 
         case (ast.expr_bind(?f, ?args_opt, ?t)) {
@@ -1185,9 +1184,9 @@ fn identity_fold_expr_call[ENV](&ENV env, &span sp, @expr f,
     ret @respan(sp, ast.expr_call(f, args, a));
 }
 
-fn identity_fold_expr_call_self[ENV](&ENV env, &span sp, @expr f,
+fn identity_fold_expr_call_self[ENV](&ENV env, &span sp, ident id,
                                 vec[@expr] args, ann a) -> @expr {
-    ret @respan(sp, ast.expr_call_self(f, args, a));
+    ret @respan(sp, ast.expr_call_self(id, args, a));
 }
 
 fn identity_fold_expr_bind[ENV](&ENV env, &span sp, @expr f,
diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index c9fc39459e1..322796a4907 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -12,11 +12,14 @@ import std.option.none;
 
 import front.ast;
 import front.creader;
+import pretty.pprust;
 import driver.session;
 import middle.ty;
 import back.x86;
 import back.abi;
 
+import pretty.pprust;
+
 import middle.ty.pat_ty;
 import middle.ty.plain_ty;
 
@@ -112,12 +115,14 @@ state type crate_ctxt = rec(session.session sess,
                             vec[str] path,
                             std.sha1.sha1 sha);
 
+type self_vt = rec(ValueRef v, @ty.t t);
+
 state type fn_ctxt = rec(ValueRef llfn,
                          ValueRef lltaskptr,
                          ValueRef llenv,
                          ValueRef llretptr,
                          mutable BasicBlockRef llallocas,
-                         mutable option.t[ValueRef] llself,
+                         mutable option.t[self_vt] llself,
                          mutable option.t[ValueRef] lliterbody,
                          hashmap[ast.def_id, ValueRef] llargs,
                          hashmap[ast.def_id, ValueRef] llobjfields,
@@ -1424,7 +1429,7 @@ fn trans_malloc_boxed(@block_ctxt cx, @ty.t t) -> result {
     // Synthesize a fake box type structurally so we have something
     // to measure the size of.
     auto boxed_body = ty.plain_tup_ty(vec(plain_ty(ty.ty_int), t));
-    auto box_ptr = ty.plain_box_ty(t);
+    auto box_ptr = ty.plain_box_ty(t, ast.imm);
     auto sz = size_of(cx, boxed_body);
     auto llty = type_of(cx.fcx.ccx, box_ptr);
     ret trans_raw_malloc(sz.bcx, llty, sz.val);
@@ -2005,7 +2010,7 @@ fn iter_structural_ty_full(@block_ctxt cx,
         auto box_a_ptr = cx.build.Load(box_a_cell);
         auto box_b_ptr = cx.build.Load(box_b_cell);
         auto tnil = plain_ty(ty.ty_nil);
-        auto tbox = ty.plain_box_ty(tnil);
+        auto tbox = ty.plain_box_ty(tnil, ast.imm);
 
         auto inner_cx = new_sub_block_ctxt(cx, "iter box");
         auto next_cx = new_sub_block_ctxt(cx, "next");
@@ -2557,7 +2562,7 @@ fn trans_unary(@block_ctxt cx, ast.unop op,
                 ret res(sub.bcx, sub.bcx.build.Neg(sub.val));
             }
         }
-        case (ast.box) {
+        case (ast.box(_)) {
             auto e_ty = ty.expr_ty(e);
             auto e_val = sub.val;
             auto box_ty = node_ann_type(sub.bcx.fcx.ccx, a);
@@ -3600,20 +3605,23 @@ type generic_info = rec(@ty.t item_type,
 type lval_result = rec(result res,
                        bool is_mem,
                        option.t[generic_info] generic,
-                       option.t[ValueRef] llobj);
+                       option.t[ValueRef] llobj,
+                       option.t[@ty.t] method_ty);
 
 fn lval_mem(@block_ctxt cx, ValueRef val) -> lval_result {
     ret rec(res=res(cx, val),
             is_mem=true,
             generic=none[generic_info],
-            llobj=none[ValueRef]);
+            llobj=none[ValueRef],
+            method_ty=none[@ty.t]);
 }
 
 fn lval_val(@block_ctxt cx, ValueRef val) -> lval_result {
     ret rec(res=res(cx, val),
             is_mem=false,
             generic=none[generic_info],
-            llobj=none[ValueRef]);
+            llobj=none[ValueRef],
+            method_ty=none[@ty.t]);
 }
 
 fn trans_external_path(@block_ctxt cx, ast.def_id did,
@@ -3781,12 +3789,12 @@ fn trans_path(@block_ctxt cx, &ast.path p, &option.t[ast.def] dopt,
     fail;
 }
 
-fn trans_field(@block_ctxt cx, &ast.span sp, @ast.expr base,
+fn trans_field(@block_ctxt cx, &ast.span sp, ValueRef v, @ty.t t0,
                &ast.ident field, &ast.ann ann) -> lval_result {
-    auto r = trans_expr(cx, base);
-    auto t = ty.expr_ty(base);
-    r = autoderef(r.bcx, r.val, t);
-    t = autoderefed_ty(t);
+
+    auto r = autoderef(cx, v, t0);
+    auto t = autoderefed_ty(t0);
+
     alt (t.struct) {
         case (ty.ty_tup(_)) {
             let uint ix = ty.field_num(cx.fcx.ccx.sess, sp, field);
@@ -3808,7 +3816,10 @@ fn trans_field(@block_ctxt cx, &ast.span sp, @ast.expr base,
                                                 C_int(ix as int)));
 
             auto lvo = lval_mem(r.bcx, v);
-            ret rec(llobj = some[ValueRef](r.val) with lvo);
+            let @ty.t fn_ty = ty.method_ty_to_fn_ty(methods.(ix));
+            ret rec(llobj = some[ValueRef](r.val),
+                    method_ty = some[@ty.t](fn_ty)
+                    with lvo);
         }
         case (_) { cx.fcx.ccx.sess.unimpl("field variant in trans_field"); }
     }
@@ -3879,11 +3890,30 @@ fn trans_lval(@block_ctxt cx, @ast.expr e) -> lval_result {
             ret trans_path(cx, p, dopt, ann);
         }
         case (ast.expr_field(?base, ?ident, ?ann)) {
-            ret trans_field(cx, e.span, base, ident, ann);
+            auto r = trans_expr(cx, base);
+            auto t = ty.expr_ty(base);
+            ret trans_field(r.bcx, e.span, r.val, t, ident, ann);
         }
         case (ast.expr_index(?base, ?idx, ?ann)) {
             ret trans_index(cx, e.span, base, idx, ann);
         }
+
+        // Kind of bizarre to pass an *entire* self-call here...but let's try
+        // it
+        case (ast.expr_call_self(?ident, _, ?ann)) {
+            alt (cx.fcx.llself) {
+                case (some[self_vt](?s_vt)) {
+                    auto r =  s_vt.v;
+                    auto t =  s_vt.t;
+                    ret trans_field(cx, e.span, r, t, ident, ann);
+                }
+                case (_) {
+                    // Shouldn't happen.
+                    fail;
+                }
+
+            }
+        }
         case (_) { cx.fcx.ccx.sess.unimpl("expr variant in trans_lval"); }
     }
     fail;
@@ -3943,7 +3973,7 @@ fn trans_bind_thunk(@crate_ctxt cx,
     auto bcx = new_top_block_ctxt(fcx);
     auto lltop = bcx.llbb;
 
-    auto llclosure_ptr_ty = type_of(cx, ty.plain_box_ty(closure_ty));
+    auto llclosure_ptr_ty = type_of(cx, ty.plain_box_ty(closure_ty, ast.imm));
     auto llclosure = bcx.build.PointerCast(fcx.llenv, llclosure_ptr_ty);
 
     auto lltarget = GEP_tup_like(bcx, closure_ty, llclosure,
@@ -4380,6 +4410,9 @@ fn trans_args(@block_ctxt cx,
             }
 
             val = bcx.build.PointerCast(val, lldestty);
+        } else if (mode == ast.alias) {
+            auto lldestty = arg_tys.(i);
+            val = bcx.build.PointerCast(val, lldestty);
         }
 
         if (mode == ast.val) {
@@ -4402,6 +4435,11 @@ fn trans_call(@block_ctxt cx, @ast.expr f,
               option.t[ValueRef] lliterbody,
               vec[@ast.expr] args,
               &ast.ann ann) -> result {
+
+    // NB: 'f' isn't necessarily a function; it might be an entire self-call
+    // expression because of the hack that allows us to process self-calls
+    // with trans_call.
+
     auto f_res = trans_lval(cx, f);
     auto faddr = f_res.res.val;
     auto llenv = C_null(T_opaque_closure_ptr(cx.fcx.ccx.tn));
@@ -4425,71 +4463,21 @@ fn trans_call(@block_ctxt cx, @ast.expr f,
             llenv = bcx.build.Load(llclosure);
         }
     }
-    auto fn_ty = ty.expr_ty(f);
-    auto ret_ty = ty.ann_to_type(ann);
-    auto args_res = trans_args(f_res.res.bcx,
-                               llenv, f_res.llobj,
-                               f_res.generic,
-                               lliterbody,
-                               args, fn_ty);
-
-    auto bcx = args_res._0;
-    auto llargs = args_res._1;
-    auto llretslot = args_res._2;
-
-    /*
-    log "calling: " + val_str(cx.fcx.ccx.tn, faddr);
-
-    for (ValueRef arg in llargs) {
-        log "arg: " + val_str(cx.fcx.ccx.tn, arg);
-    }
-    */
-
-    bcx.build.FastCall(faddr, llargs);
-    auto retval = C_nil();
-
-    if (!ty.type_is_nil(ret_ty)) {
-        retval = load_scalar_or_boxed(bcx, llretslot, ret_ty);
-        // Retval doesn't correspond to anything really tangible in the frame,
-        // but it's a ref all the same, so we put a note here to drop it when
-        // we're done in this scope.
-        find_scope_cx(cx).cleanups +=
-            vec(clean(bind drop_ty(_, retval, ret_ty)));
-    }
-
-    ret res(bcx, retval);
-}
-
-fn trans_call_self(@block_ctxt cx, @ast.expr f,
-                   option.t[ValueRef] lliterbody,
-                   vec[@ast.expr] args,
-                   &ast.ann ann) -> result {
-    log "translating a self-call";
-
-    auto f_res = trans_lval(cx, f);
-    auto faddr = f_res.res.val;
-    auto llenv = C_null(T_opaque_closure_ptr(cx.fcx.ccx.tn));
 
-    alt (f_res.llobj) {
-        case (some[ValueRef](_)) {
-            // It's a vtbl entry.
-            faddr = f_res.res.bcx.build.Load(faddr);
+    let @ty.t fn_ty;
+    alt (f_res.method_ty) {
+        case (some[@ty.t](?meth)) {
+            // self-call
+            fn_ty = meth;
         }
-        case (none[ValueRef]) {
-            // It's a closure.
-            auto bcx = f_res.res.bcx;
-            auto pair = faddr;
-            faddr = bcx.build.GEP(pair, vec(C_int(0),
-                                            C_int(abi.fn_field_code)));
-            faddr = bcx.build.Load(faddr);
+        
+        case (_) {
+            fn_ty = ty.expr_ty(f);
 
-            auto llclosure = bcx.build.GEP(pair,
-                                           vec(C_int(0),
-                                               C_int(abi.fn_field_box)));
-            llenv = bcx.build.Load(llclosure);
         }
+
     }
-    auto fn_ty = ty.expr_ty(f);
+
     auto ret_ty = ty.ann_to_type(ann);
     auto args_res = trans_args(f_res.res.bcx,
                                llenv, f_res.llobj,
@@ -4760,8 +4748,9 @@ fn trans_expr(@block_ctxt cx, @ast.expr e) -> result {
             ret trans_call(cx, f, none[ValueRef], args, ann);
         }
 
-        case (ast.expr_call_self(?f, ?args, ?ann)) {
-            ret trans_call_self(cx, f, none[ValueRef], args, ann);
+        case (ast.expr_call_self(?ident, ?args, ?ann)) {
+            // A weird hack to make self-calls work.
+            ret trans_call(cx, e, none[ValueRef], args, ann);
         }
 
         case (ast.expr_cast(?e, _, ?ann)) {
@@ -4913,8 +4902,7 @@ fn trans_log(@block_ctxt cx, @ast.expr e) -> result {
 fn trans_check_expr(@block_ctxt cx, @ast.expr e) -> result {
     auto cond_res = trans_expr(cx, e);
 
-    // FIXME: need pretty-printer.
-    auto expr_str = "<expr>";
+    auto expr_str = pretty.pprust.expr_to_str(e);
     auto fail_cx = new_sub_block_ctxt(cx, "fail");
     auto fail_res = trans_fail(fail_cx, e.span, expr_str);
 
@@ -5472,7 +5460,7 @@ fn new_fn_ctxt(@crate_ctxt cx,
              llenv=llenv,
              llretptr=llretptr,
              mutable llallocas = llallocas,
-             mutable llself=none[ValueRef],
+             mutable llself=none[self_vt],
              mutable lliterbody=none[ValueRef],
              llargs=llargs,
              llobjfields=llobjfields,
@@ -5491,27 +5479,24 @@ fn new_fn_ctxt(@crate_ctxt cx,
 
 fn create_llargs_for_fn_args(&@fn_ctxt cx,
                              ast.proto proto,
-                             option.t[TypeRef] ty_self,
+                             option.t[tup(TypeRef, @ty.t)] ty_self,
                              @ty.t ret_ty,
                              &vec[ast.arg] args,
                              &vec[ast.ty_param] ty_params) {
 
-    alt (ty_self) {
-        case (some[TypeRef](_)) {
-            cx.llself = some[ValueRef](cx.llenv);
-        }
-        case (_) {
-        }
-    }
-
     auto arg_n = 3u;
 
-    if (ty_self == none[TypeRef]) {
-        for (ast.ty_param tp in ty_params) {
-            auto llarg = llvm.LLVMGetParam(cx.llfn, arg_n);
-            check (llarg as int != 0);
-            cx.lltydescs.insert(tp.id, llarg);
-            arg_n += 1u;
+    alt (ty_self) {
+        case (some[tup(TypeRef, @ty.t)](?tt)) {
+            cx.llself = some[self_vt](rec(v = cx.llenv, t = tt._1));
+        }
+        case (none[tup(TypeRef, @ty.t)]) {
+            for (ast.ty_param tp in ty_params) {
+                auto llarg = llvm.LLVMGetParam(cx.llfn, arg_n);
+                check (llarg as int != 0);
+                cx.lltydescs.insert(tp.id, llarg);
+                arg_n += 1u;
+            }
         }
     }
 
@@ -5535,17 +5520,17 @@ fn create_llargs_for_fn_args(&@fn_ctxt cx,
 // were passed and whatnot. Apparently mem2reg will mop up.
 
 fn copy_any_self_to_alloca(@fn_ctxt fcx,
-                           option.t[TypeRef] ty_self) {
+                           option.t[tup(TypeRef, @ty.t)] ty_self) {
 
     auto bcx = llallocas_block_ctxt(fcx);
 
     alt (fcx.llself) {
-        case (some[ValueRef](?self_v)) {
+        case (some[self_vt](?s_vt)) {
             alt (ty_self) {
-                case (some[TypeRef](?self_t)) {
-                    auto a = alloca(bcx, self_t);
-                    bcx.build.Store(self_v, a);
-                    fcx.llself = some[ValueRef](a);
+                case (some[tup(TypeRef, @ty.t)](?tt)) {
+                    auto a = alloca(bcx, tt._0);
+                    bcx.build.Store(s_vt.v, a);
+                    fcx.llself = some[self_vt](rec(v = a, t = s_vt.t));
                 }
             }
         }
@@ -5607,7 +5592,7 @@ fn ret_ty_of_fn(ast.ann ann) -> @ty.t {
     ret ret_ty_of_fn_ty(ty.ann_to_type(ann));
 }
 
-fn populate_fn_ctxt_from_llself(@fn_ctxt fcx, ValueRef llself) {
+fn populate_fn_ctxt_from_llself(@fn_ctxt fcx, self_vt llself) {
     auto bcx = llallocas_block_ctxt(fcx);
 
     let vec[@ty.t] field_tys = vec();
@@ -5624,7 +5609,7 @@ fn populate_fn_ctxt_from_llself(@fn_ctxt fcx, ValueRef llself) {
     let TypeRef llobj_box_ty = T_obj_ptr(bcx.fcx.ccx.tn, n_typarams);
 
     auto box_cell =
-        bcx.build.GEP(llself,
+        bcx.build.GEP(llself.v,
                       vec(C_int(0),
                           C_int(abi.obj_field_box)));
 
@@ -5677,7 +5662,7 @@ fn populate_fn_ctxt_from_llself(@fn_ctxt fcx, ValueRef llself) {
 }
 
 fn trans_fn(@crate_ctxt cx, &ast._fn f, ast.def_id fid,
-            option.t[TypeRef] ty_self,
+            option.t[tup(TypeRef, @ty.t)] ty_self,
             &vec[ast.ty_param] ty_params, &ast.ann ann) {
 
     auto llfndecl = cx.item_ids.get(fid);
@@ -5690,7 +5675,7 @@ fn trans_fn(@crate_ctxt cx, &ast._fn f, ast.def_id fid,
     copy_any_self_to_alloca(fcx, ty_self);
 
     alt (fcx.llself) {
-        case (some[ValueRef](?llself)) {
+        case (some[self_vt](?llself)) {
             populate_fn_ctxt_from_llself(fcx, llself);
         }
         case (_) {
@@ -5713,7 +5698,9 @@ fn trans_fn(@crate_ctxt cx, &ast._fn f, ast.def_id fid,
     new_builder(fcx.llallocas).Br(lltop);
 }
 
-fn trans_vtbl(@crate_ctxt cx, TypeRef self_ty,
+fn trans_vtbl(@crate_ctxt cx, 
+              TypeRef llself_ty,
+              @ty.t self_ty,
               &ast._obj ob,
               &vec[ast.ty_param] ty_params) -> ValueRef {
     let vec[ValueRef] methods = vec();
@@ -5731,7 +5718,7 @@ fn trans_vtbl(@crate_ctxt cx, TypeRef self_ty,
         alt (node_ann_type(cx, m.node.ann).struct) {
             case (ty.ty_fn(?proto, ?inputs, ?output)) {
                 llfnty = type_of_fn_full(cx, proto,
-                                         some[TypeRef](self_ty),
+                                         some[TypeRef](llself_ty),
                                          inputs, output,
                                          _vec.len[ast.ty_param](ty_params));
             }
@@ -5743,7 +5730,8 @@ fn trans_vtbl(@crate_ctxt cx, TypeRef self_ty,
         cx.item_ids.insert(m.node.id, llfn);
         cx.item_symbols.insert(m.node.id, s);
 
-        trans_fn(mcx, m.node.meth, m.node.id, some[TypeRef](self_ty),
+        trans_fn(mcx, m.node.meth, m.node.id, 
+                 some[tup(TypeRef, @ty.t)](tup(llself_ty, self_ty)),
                  ty_params, m.node.ann);
         methods += vec(llfn);
     }
@@ -5774,7 +5762,8 @@ fn trans_obj(@crate_ctxt cx, &ast._obj ob, ast.def_id oid,
 
     auto fcx = new_fn_ctxt(cx, llctor_decl);
     create_llargs_for_fn_args(fcx, ast.proto_fn,
-                              none[TypeRef], ret_ty_of_fn(ann),
+                              none[tup(TypeRef, @ty.t)], 
+                              ret_ty_of_fn(ann),
                               fn_args, ty_params);
 
     let vec[ty.arg] arg_tys = arg_tys_of_fn(ann);
@@ -5783,9 +5772,10 @@ fn trans_obj(@crate_ctxt cx, &ast._obj ob, ast.def_id oid,
     auto bcx = new_top_block_ctxt(fcx);
     auto lltop = bcx.llbb;
 
-    auto llself_ty = type_of(cx, ret_ty_of_fn(ann));
+    auto self_ty = ret_ty_of_fn(ann);
+    auto llself_ty = type_of(cx, self_ty);
     auto pair = bcx.fcx.llretptr;
-    auto vtbl = trans_vtbl(cx, llself_ty, ob, ty_params);
+    auto vtbl = trans_vtbl(cx, llself_ty, self_ty, ob, ty_params);
     auto pair_vtbl = bcx.build.GEP(pair,
                                    vec(C_int(0),
                                        C_int(abi.obj_field_vtbl)));
@@ -5819,7 +5809,7 @@ fn trans_obj(@crate_ctxt cx, &ast._obj ob, ast.def_id oid,
         let @ty.t body_ty = ty.plain_tup_ty(vec(tydesc_ty,
                                                 typarams_ty,
                                                 fields_ty));
-        let @ty.t boxed_body_ty = ty.plain_box_ty(body_ty);
+        let @ty.t boxed_body_ty = ty.plain_box_ty(body_ty, ast.imm);
 
         // Malloc a box for the body.
         auto box = trans_malloc_boxed(bcx, body_ty);
@@ -5906,7 +5896,8 @@ fn trans_tag_variant(@crate_ctxt cx, ast.def_id tag_id,
     auto fcx = new_fn_ctxt(cx, llfndecl);
 
     create_llargs_for_fn_args(fcx, ast.proto_fn,
-                              none[TypeRef], ret_ty_of_fn(variant.node.ann),
+                              none[tup(TypeRef, @ty.t)], 
+                              ret_ty_of_fn(variant.node.ann),
                               fn_args, ty_params);
 
     let vec[@ty.t] ty_param_substs = vec();
@@ -5994,7 +5985,7 @@ fn trans_item(@crate_ctxt cx, &ast.item item) {
     alt (item.node) {
         case (ast.item_fn(?name, ?f, ?tps, ?fid, ?ann)) {
             auto sub_cx = extend_path(cx, name);
-            trans_fn(sub_cx, f, fid, none[TypeRef], tps, ann);
+            trans_fn(sub_cx, f, fid, none[tup(TypeRef, @ty.t)], tps, ann);
         }
         case (ast.item_obj(?name, ?ob, ?tps, ?oid, ?ann)) {
             auto sub_cx = @rec(obj_typarams=tps,
@@ -6147,7 +6138,7 @@ fn decl_native_fn_and_pair(@crate_ctxt cx,
     auto arg_n = 3u;
     auto pass_task;
 
-    auto lltaskptr = bcx.build.PtrToInt(fcx.lltaskptr, T_int());
+    auto lltaskptr = vp2i(bcx, fcx.lltaskptr);
     alt (abi) {
         case (ast.native_abi_rust) {
             pass_task = true;
@@ -6155,7 +6146,7 @@ fn decl_native_fn_and_pair(@crate_ctxt cx,
             for each (uint i in _uint.range(0u, num_ty_param)) {
                 auto llarg = llvm.LLVMGetParam(fcx.llfn, arg_n);
                 check (llarg as int != 0);
-                call_args += vec(bcx.build.PointerCast(llarg, T_i32()));
+                call_args += vec(vp2i(bcx, llarg));
                 arg_n += 1u;
             }
         }
@@ -6168,6 +6159,26 @@ fn decl_native_fn_and_pair(@crate_ctxt cx,
         }
     }
 
+    fn push_arg(@block_ctxt cx,
+                &mutable vec[ValueRef] args,
+                ValueRef v,
+                @ty.t t) {
+        if (ty.type_is_integral(t)) {
+            auto lldsttype = T_int();
+            auto llsrctype = type_of(cx.fcx.ccx, t);
+            if (llvm.LLVMGetIntTypeWidth(lldsttype) >
+                llvm.LLVMGetIntTypeWidth(llsrctype)) {
+                args += vec(cx.build.ZExtOrBitCast(v, T_int()));
+            } else {
+                args += vec(cx.build.TruncOrBitCast(v, T_int()));
+            }
+        } else if (ty.type_is_fp(t)) {
+            args += vec(cx.build.FPToSI(v, T_int()));
+        } else {
+            args += vec(vp2i(cx, v));
+        }
+    }
+
     auto r;
     auto rptr;
     auto args = ty.ty_fn_args(fn_type);
@@ -6191,7 +6202,7 @@ fn decl_native_fn_and_pair(@crate_ctxt cx,
         for (ty.arg arg in args) {
             auto llarg = llvm.LLVMGetParam(fcx.llfn, arg_n);
             check (llarg as int != 0);
-            call_args += vec(bcx.build.PointerCast(llarg, T_i32()));
+            push_arg(bcx, call_args, llarg, arg.ty);
             arg_n += 1u;
         }
 
@@ -6782,7 +6793,7 @@ fn trans_vec_append_glue(@crate_ctxt cx) {
                     llenv=C_null(T_ptr(T_nil())),
                     llretptr=C_null(T_ptr(T_nil())),
                     mutable llallocas = llallocas,
-                    mutable llself=none[ValueRef],
+                    mutable llself=none[self_vt],
                     mutable lliterbody=none[ValueRef],
                     llargs=new_def_hash[ValueRef](),
                     llobjfields=new_def_hash[ValueRef](),
diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index d0b5fe102cc..f83bece7f20 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -26,6 +26,12 @@ type method = rec(ast.proto proto,
 
 type mt = rec(@t ty, ast.mutability mut);
 
+// Convert from method type to function type.  Pretty easy; we just drop
+// 'ident'.
+fn method_ty_to_fn_ty(method m) -> @ty.t {
+    ret plain_ty(ty_fn(m.proto, m.inputs, m.output));
+}
+
 // NB: If you change this, you'll probably want to change the corresponding
 // AST structure in front/ast.rs as well.
 type t = rec(sty struct, option.t[str] cname);
@@ -564,8 +570,8 @@ fn plain_ty(&sty st) -> @t {
     ret @rec(struct=st, cname=none[str]);
 }
 
-fn plain_box_ty(@t subty) -> @t {
-    ret plain_ty(ty_box(rec(ty=subty, mut=ast.imm)));
+fn plain_box_ty(@t subty, ast.mutability mut) -> @t {
+    ret plain_ty(ty_box(rec(ty=subty, mut=mut)));
 }
 
 fn plain_tup_ty(vec[@t] elem_tys) -> @t {
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index f726ae588c9..ab0262f1753 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -23,6 +23,7 @@ import middle.ty.ty_to_str;
 import middle.ty.type_is_integral;
 import middle.ty.type_is_scalar;
 import middle.ty.ty_params_opt_and_ty;
+import middle.ty.ty_nil;
 
 import std._str;
 import std._uint;
@@ -62,6 +63,12 @@ fn triv_ann(@ty.t t) -> ann {
     ret ast.ann_type(t, none[vec[@ty.t]], none[@ts_ann]);
 }
 
+// Used to fill in the annotation for things that have uninteresting
+// types
+fn boring_ann() -> ann {
+    ret triv_ann(plain_ty(ty_nil));
+}
+
 // Replaces parameter types inside a type with type variables.
 fn generalize_ty(@crate_ctxt cx, @ty.t t) -> @ty.t {
     state obj ty_generalizer(@crate_ctxt cx,
@@ -959,7 +966,7 @@ fn strip_boxes(@ty.t t) -> @ty.t {
 fn add_boxes(uint n, @ty.t t) -> @ty.t {
     auto t1 = t;
     while (n != 0u) {
-        t1 = ty.plain_box_ty(t1);
+        t1 = ty.plain_box_ty(t1, ast.imm);
         n -= 1u;
     }
     ret t1;
@@ -1361,7 +1368,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
                                  ann_to_type(ann), adk);
             e_1 = ast.expr_ext(p, args, body, expanded, triv_ann(t));
         }
-        /* FIXME: this should probably check the type annotations */
+        /* FIXME: should this check the type annotations? */
         case (ast.expr_fail(_))  { e_1 = e.node; } 
         case (ast.expr_log(_,_)) { e_1 = e.node; } 
         case (ast.expr_break(_)) { e_1 = e.node; }
@@ -1728,9 +1735,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
             auto oper_1 = check_expr(fcx, oper);
             auto oper_t = expr_ty(oper_1);
             alt (unop) {
-                case (ast.box) {
-                    // TODO: mutable
-                    oper_t = ty.plain_box_ty(oper_t);
+                case (ast.box(?mut)) {
+                    oper_t = ty.plain_box_ty(oper_t, mut);
                 }
                 case (ast.deref) {
                     alt (oper_t.struct) {
@@ -1772,16 +1778,19 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                                      ann));
         }
 
-        case (ast.expr_fail(_)) { // ??? ignoring ann
-            ret expr;
+        case (ast.expr_fail(_)) {
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_fail(boring_ann()));
         }
 
         case (ast.expr_break(_)) {
-            ret expr;
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_break(boring_ann()));
         }
 
         case (ast.expr_cont(_)) {
-            ret expr;
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_cont(boring_ann()));
         }
 
         case (ast.expr_ret(?expr_opt, _)) {
@@ -1793,14 +1802,16 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                          + "returning non-nil");
                     }
 
-                    ret expr;
+                    ret @fold.respan[ast.expr_]
+                        (expr.span,
+                         ast.expr_ret(none[@ast.expr], boring_ann()));
                 }
 
                 case (some[@ast.expr](?e)) {
                     auto expr_0 = check_expr(fcx, e);
                     auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0);
                     ret @fold.respan[ast.expr_]
-                        (expr.span, ast.expr_ret(some(expr_1), ann_none));
+                        (expr.span, ast.expr_ret(some(expr_1), boring_ann()));
                 }
             }
         }
@@ -1814,14 +1825,16 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                          + "putting non-nil");
                     }
 
-                    ret expr;
+                    ret @fold.respan[ast.expr_]
+                        (expr.span, ast.expr_put(none[@ast.expr],
+                                                 boring_ann()));
                 }
 
                 case (some[@ast.expr](?e)) {
                     auto expr_0 = check_expr(fcx, e);
                     auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0);
                     ret @fold.respan[ast.expr_]
-                        (expr.span, ast.expr_put(some(expr_1), ann_none));
+                        (expr.span, ast.expr_put(some(expr_1), boring_ann()));
                 }
             }
         }
@@ -1832,20 +1845,21 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
             auto expr_0 = check_expr(fcx, e);
             auto expr_1 = demand_expr(fcx, fcx.ret_ty, expr_0);
             ret @fold.respan[ast.expr_](expr.span,
-                                        ast.expr_be(expr_1, ann_none));
+                                        ast.expr_be(expr_1,
+                                                    boring_ann()));
         }
 
         case (ast.expr_log(?e,_)) {
             auto expr_t = check_expr(fcx, e);
             ret @fold.respan[ast.expr_]
-                (expr.span, ast.expr_log(expr_t, ann_none));
+                (expr.span, ast.expr_log(expr_t, boring_ann()));
         }
 
         case (ast.expr_check_expr(?e, _)) {
             auto expr_t = check_expr(fcx, e);
             demand(fcx, expr.span, plain_ty(ty.ty_bool), expr_ty(expr_t));
             ret @fold.respan[ast.expr_]
-                (expr.span, ast.expr_check_expr(expr_t, ann_none));
+                (expr.span, ast.expr_check_expr(expr_t, boring_ann()));
         }
 
         case (ast.expr_assign(?lhs, ?rhs, _)) {
@@ -2111,6 +2125,18 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
                                         ast.expr_call(f_1, args_1, ann));
         }
 
+        case (ast.expr_call_self(?ident, ?args, _)) {
+            // FIXME: What's to check here?
+
+            // FIXME: These two lines are ripped off from the expr_call case;
+            // what should they be really?
+            auto rt_1 = plain_ty(ty.ty_nil);
+            auto ann = triv_ann(rt_1);
+
+            ret @fold.respan[ast.expr_](expr.span,
+                                        ast.expr_call_self(ident, args, ann));
+        }
+
         case (ast.expr_spawn(?dom, ?name, ?f, ?args, _)) {
             auto result = check_call(fcx, f, args);
             auto f_1 = result._0;
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
index 361d70aecd1..64a17a7da0c 100644
--- a/src/comp/middle/typestate_check.rs
+++ b/src/comp/middle/typestate_check.rs
@@ -20,6 +20,8 @@ import front.ast.expr;
 import front.ast.expr_call;
 import front.ast.expr_path;
 import front.ast.expr_log;
+import front.ast.expr_block;
+import front.ast.expr_lit;
 import front.ast.path;
 import front.ast.crate_directive;
 import front.ast.fn_decl;
@@ -42,6 +44,11 @@ import front.ast.ann_none;
 import front.ast.ann_type;
 import front.ast._obj;
 import front.ast._mod;
+import front.ast.crate;
+import front.ast.mod_index_entry;
+import front.ast.mie_item;
+import front.ast.item_fn;
+import front.ast.def_local;
 
 import middle.fold;
 import middle.fold.respan;
@@ -50,6 +57,7 @@ import util.common;
 import util.common.span;
 import util.common.spanned;
 import util.common.new_str_hash;
+import util.common.new_def_hash;
 import util.typestate_ann;
 import util.typestate_ann.ts_ann;
 import util.typestate_ann.empty_pre_post;
@@ -57,9 +65,14 @@ import util.typestate_ann.true_precond;
 import util.typestate_ann.true_postcond;
 import util.typestate_ann.postcond;
 import util.typestate_ann.precond;
+import util.typestate_ann.poststate;
+import util.typestate_ann.prestate;
 import util.typestate_ann.pre_and_post;
 import util.typestate_ann.get_pre;
 import util.typestate_ann.get_post;
+import util.typestate_ann.implies;
+import util.typestate_ann.pre_and_post_state;
+import util.typestate_ann.empty_states;
 
 import middle.ty;
 import middle.ty.ann_to_type;
@@ -91,6 +104,8 @@ import std.list.cons;
 import std.list.nil;
 import std.list.foldl;
 import std.list.find;
+import std._uint;
+import std.bitv;
 
 import util.typestate_ann;
 import util.typestate_ann.difference;
@@ -98,21 +113,134 @@ import util.typestate_ann.union;
 import util.typestate_ann.pps_len;
 import util.typestate_ann.require_and_preserve;
 
-/**********************************************************************/
-/* mapping from variable name to bit number */
-type fn_info = std.map.hashmap[ident, uint];
+/**** debugging junk  ****/
+fn log_expr(@expr e) -> () {
+  let str_writer s = string_writer();
+  auto out_ = mkstate(s.get_writer(), 80u);
+  auto out = @rec(s=out_,
+                  comments=option.none[vec[front.lexer.cmnt]],
+                  mutable cur_cmnt=0u);
+
+  print_expr(out, e);
+  log(s.get_str());
+}
+
+fn log_cond(vec[uint] v) -> () {
+  auto res = "";
+  for (uint i in v) {
+    if (i == 0u) {
+      res += "0";
+    }
+    else {
+      res += "1";
+    }
+  }
+  log(res);
+}
+fn log_pp(&pre_and_post pp) -> () {
+  auto p1 = bitv.to_vec(pp.precondition);
+  auto p2 = bitv.to_vec(pp.postcondition);
+  log("pre:");
+  log_cond(p1);
+  log("post:");
+  log_cond(p2);
+}
 
-fn bit_num(ident v, fn_info m) -> uint {
+fn print_ident(&ident i) -> () {
+  log(" " + i + " ");
+}
+
+fn print_idents(vec[ident] idents) -> () {
+  if(len[ident](idents) == 0u) {
+    ret;
+  }
+  else {
+    log("an ident: " + pop[ident](idents));
+    print_idents(idents);
+  }
+}
+/**********************************************************************/
+/* mapping from variable name (def_id is assumed to be for a local
+   variable in a given function) to bit number */
+type fn_info      = std.map.hashmap[def_id, uint];
+/* mapping from function name to fn_info map */
+type _fn_info_map = std.map.hashmap[def_id, fn_info];
+ 
+fn bit_num(def_id v, fn_info m) -> uint {
+  check (m.contains_key(v));
   ret m.get(v);
 }
+
+fn var_is_local(def_id v, fn_info m) -> bool {
+  ret (m.contains_key(v));
+}
+
 fn num_locals(fn_info m) -> uint {
   ret m.size();
 }
 
+fn find_locals(_fn f) -> vec[def_id] {
+  auto res = _vec.alloc[def_id](0u);
+
+  for each (@tup(ident, block_index_entry) p
+          in f.body.node.index.items()) {
+    alt (p._1) {
+      case (ast.bie_local(?loc)) {
+        res += vec(loc.id);
+      }
+      case (_) { }
+    }
+  }
+
+  ret res;
+}
+
+fn add_var(def_id v, uint next, fn_info tbl) -> uint {
+  tbl.insert(v, next);
+  // log(v + " |-> " + _uint.to_str(next, 10u));
+  ret (next + 1u);
+}
+
+/* builds a table mapping each local var defined in f
+ to a bit number in the precondition/postcondition vectors */
 fn mk_fn_info(_fn f) -> fn_info {
-  ret new_str_hash[uint](); /* FIXME: actually implement this */
+  auto res = new_def_hash[uint]();
+  let uint next = 0u;
+  let vec[ast.arg] f_args = f.decl.inputs;
+
+  for (ast.arg v in f_args) {
+    next = add_var(v.id, next, res);
+  }
+
+  let vec[def_id] locals = find_locals(f);
+  for (def_id v in locals) {
+    next = add_var(v, next, res);
+  }
+
+  ret res;
 }
-/**********************************************************************/
+
+/* extends mk_fn_info to an item, side-effecting the map fi from 
+   function IDs to fn_info maps */
+fn mk_fn_info_item_fn(&_fn_info_map fi, &span sp, ident i, &ast._fn f,
+                 vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
+  fi.insert(id, mk_fn_info(f));
+  ret @respan(sp, item_fn(i, f, ty_params, id, a));
+}
+
+/* initializes the global fn_info_map (mapping each function ID, including
+   nested locally defined functions, onto a mapping from local variable name
+   to bit number) */
+fn mk_f_to_fn_info(@ast.crate c) -> _fn_info_map {
+  auto res = new_def_hash[fn_info]();
+
+  auto fld = fold.new_identity_fold[_fn_info_map]();
+  fld = @rec(fold_item_fn = bind mk_fn_info_item_fn(_,_,_,_,_,_,_) with *fld);
+  fold.fold_crate[_fn_info_map](res, fld, c);
+
+  ret res;
+}
+/**** Helpers ****/
 fn expr_ann(&expr e) -> ann {
   alt(e.node) {
     case (ast.expr_vec(_,_,?a)) {
@@ -214,8 +342,53 @@ fn expr_ann(&expr e) -> ann {
   }
 }
 
-fn expr_pp(&@expr e) -> pre_and_post {
-  alt (expr_ann(*e)) {
+/* returns ann_none if this is the sort
+ of statement where an ann doesn't make sense */
+fn stmt_ann(&stmt s) -> ann {
+  alt (s.node) {
+    case (stmt_decl(?d)) {
+      alt (d.node) {
+        case (decl_local(?l)) {
+          ret l.ann;
+        }
+        case (decl_item(?i)) {
+          ret ann_none; /* ????? */
+        }
+      }
+    }
+    case (stmt_expr(?e)) {
+      ret expr_ann(*e);
+    }
+    case (_) {
+      ret ann_none;
+    }
+  }
+}
+
+/* fails if e has no annotation */
+fn expr_pp(&expr e) -> pre_and_post {
+  alt (expr_ann(e)) {
+    case (ann_none) {
+      log "expr_pp: the impossible happened (no annotation)";
+      fail;
+    }
+    case (ann_type(_, _, ?maybe_pp)) {
+      alt (maybe_pp) {
+        case (none[@ts_ann]) {
+          log "expr_pp: the impossible happened (no pre/post)";
+          fail;
+        }
+        case (some[@ts_ann](?p)) {
+          ret p.conditions;
+        }
+      }
+    }
+  }
+}
+
+/* fails if e has no annotation */
+fn expr_states(&expr e) -> pre_and_post_state {
+  alt (expr_ann(e)) {
     case (ann_none) {
       log "expr_pp: the impossible happened (no annotation)";
       fail;
@@ -227,7 +400,45 @@ fn expr_pp(&@expr e) -> pre_and_post {
           fail;
         }
         case (some[@ts_ann](?p)) {
-          ret *p;
+          ret p.states;
+        }
+      }
+    }
+  }
+}
+
+/* fails if no annotation */
+fn stmt_pp(&stmt s) -> pre_and_post {
+  alt (stmt_ann(s)) {
+    case (ann_none) {
+      fail;
+    }
+    case (ann_type(_, _, ?maybe_pp)) {
+      alt (maybe_pp) {
+        case (none[@ts_ann]) {
+          fail;
+        }
+        case (some[@ts_ann](?p)) {
+          ret p.conditions;
+        }
+      }
+    }
+  }
+}
+
+/* fails if no annotation */
+fn stmt_states(&stmt s) -> pre_and_post_state {
+  alt (stmt_ann(s)) {
+    case (ann_none) {
+      fail;
+    }
+    case (ann_type(_, _, ?maybe_pp)) {
+      alt (maybe_pp) {
+        case (none[@ts_ann]) {
+          fail;
+        }
+        case (some[@ts_ann](?p)) {
+          ret p.states;
         }
       }
     }
@@ -235,21 +446,49 @@ fn expr_pp(&@expr e) -> pre_and_post {
 }
 
 fn expr_precond(&expr e) -> precond {
-  ret (expr_pp(@e)).precondition;
+  ret (expr_pp(e)).precondition;
 }
 
-fn expr_postcond(&@expr e) -> postcond {
+fn expr_postcond(&expr e) -> postcond {
   ret (expr_pp(e)).postcondition;
 }
 
-fn with_pp(ann a, @pre_and_post p) -> ann {
+fn expr_prestate(&expr e) -> prestate {
+  ret (expr_states(e)).prestate;
+}
+
+fn expr_poststate(&expr e) -> poststate {
+  ret (expr_states(e)).poststate;
+}
+
+fn stmt_precond(&stmt s) -> precond {
+  ret (stmt_pp(s)).precondition;
+}
+
+fn stmt_postcond(&stmt s) -> postcond {
+  ret (stmt_pp(s)).postcondition;
+}
+
+fn stmt_prestate(&stmt s) -> prestate {
+  ret (stmt_states(s)).prestate;
+}
+
+fn stmt_poststate(&stmt s) -> poststate {
+  ret (stmt_states(s)).poststate;
+}
+
+/* returns a new annotation where the pre_and_post is p */
+fn with_pp(ann a, pre_and_post p) -> ann {
   alt (a) {
     case (ann_none) {
       log("with_pp: the impossible happened");
       fail; /* shouldn't happen b/c code is typechecked */
     }
     case (ann_type(?t, ?ps, _)) {
-      ret (ann_type(t, ps, some[@ts_ann](p)));
+      ret (ann_type(t, ps,
+                    some[@ts_ann]
+                    (@rec(conditions=p,
+                          states=empty_states(pps_len(p))))));
     }
   }
 }
@@ -276,9 +515,14 @@ fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
 }
 
 fn union_postconds_go(postcond first, &vec[postcond] rest) -> postcond {
-  auto other = rest.(0);
-  union(first, other);
-  union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest)));
+  auto sz = _vec.len[postcond](rest);
+
+  if (sz > 0u) {
+    auto other = rest.(0);
+    union(first, other);
+    union_postconds_go(first, slice[postcond](rest, 1u, len[postcond](rest)));
+  }
+
   ret first;
 }
 
@@ -288,19 +532,7 @@ fn union_postconds(&vec[postcond] pcs) -> postcond {
   be union_postconds_go(pcs.(0), pcs);
 }
 
-fn print_ident(&ident i) -> () {
-  log(" " + i + " ");
-}
-
-fn print_idents(vec[ident] idents) -> () {
-  if(len[ident](idents) == 0u) {
-    ret;
-  }
-  else {
-    log("an ident: " + pop[ident](idents));
-    print_idents(idents);
-  }
-}
+/******* AST-traversing code ********/
 
 fn find_pre_post_mod(&_mod m) -> _mod {
   ret m; /* FIXME */
@@ -314,26 +546,29 @@ fn find_pre_post_obj(_obj o) -> _obj {
   ret o; /* FIXME */
 }
 
-impure fn find_pre_post_item(fn_info enclosing, &item i) -> item {
+fn find_pre_post_item(_fn_info_map fm, fn_info enclosing, &item i) -> item {
   alt (i.node) {
     case (ast.item_const(?id, ?t, ?e, ?di, ?a)) {
       auto e_pp = find_pre_post_expr(enclosing, *e);
+      log("1");
       ret (respan(i.span,
-                   ast.item_const(id, t, e_pp, di,
-                              with_pp(a, @expr_pp(e_pp)))));
+                  ast.item_const(id, t, e_pp, di, a)));
     }
     case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
-      auto f_pp = find_pre_post_fn(f);
+      check (fm.contains_key(di));
+      auto f_pp = find_pre_post_fn(fm, fm.get(di), f);
       ret (respan(i.span, 
                    ast.item_fn(id, f_pp, ps, di, a)));
     }
     case (ast.item_mod(?id, ?m, ?di)) {
       auto m_pp = find_pre_post_mod(m);
+      log("3");
       ret (respan(i.span,
                    ast.item_mod(id, m_pp, di)));
     }
     case (ast.item_native_mod(?id, ?nm, ?di)) {
       auto n_pp = find_pre_post_native_mod(nm);
+      log("4");
       ret (respan(i.span,
                    ast.item_native_mod(id, n_pp, di)));
     }
@@ -345,17 +580,23 @@ impure fn find_pre_post_item(fn_info enclosing, &item i) -> item {
     }
     case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
       auto o_pp = find_pre_post_obj(o);
+      log("5");
       ret (respan(i.span,
                    ast.item_obj(id, o_pp, ps, di, a)));
     }
   }
 }
 
-impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
+fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   auto num_local_vars = num_locals(enclosing);
 
   fn do_rand_(fn_info enclosing, &@expr e) -> @expr {
-    be find_pre_post_expr(enclosing, *e);
+    log("for rand " );
+    log_expr(e);
+    log("pp = ");
+    auto res = find_pre_post_expr(enclosing, *e);
+    log_pp(expr_pp(*res));
+    ret res;
   }
 
   auto do_rand = bind do_rand_(enclosing,_);
@@ -363,40 +604,78 @@ impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   alt(e.node) {
     case(expr_call(?oper, ?rands, ?a)) {
       auto pp_oper = find_pre_post_expr(enclosing, *oper);
+      log("pp_oper =");
+      log_pp(expr_pp(*pp_oper));
       
       auto f = do_rand;
       auto pp_rands = _vec.map[@expr, @expr](f, rands);
       
-      auto g = expr_pp;
-      auto pps = _vec.map[@expr, pre_and_post]      
-        (g, pp_rands);
-      _vec.push[pre_and_post](pps, expr_pp(pp_oper));
+      fn pp_one(&@expr e) -> pre_and_post {
+        be expr_pp(*e);
+      }
+      auto g = pp_one;
+      auto pps = _vec.map[@expr, pre_and_post](g, pp_rands);
+      _vec.push[pre_and_post](pps, expr_pp(*pp_oper));
       auto h = get_post;
       auto res_postconds = _vec.map[pre_and_post, postcond](h, pps);
       auto res_postcond = union_postconds(res_postconds);
-      let @pre_and_post pp =
-        @rec(precondition=seq_preconds(num_local_vars, pps),
+      let pre_and_post pp =
+        rec(precondition=seq_preconds(num_local_vars, pps),
              postcondition=res_postcond);
       let ann a_res = with_pp(a, pp);
+      log("result for call");
+      log_expr(@e);
+      log("is:");
+      log_pp(pp);
       ret (@respan(e.span,
                    expr_call(pp_oper, pp_rands, a_res)));
                         
     }
     case(expr_path(?p, ?maybe_def, ?a)) {
-      check (len[ident](p.node.idents) > 0u);
-      auto referent = p.node.idents.(0);
-      auto i = bit_num(referent, enclosing);
+      auto df;
+      alt (maybe_def) {
+        case (none[def])
+          { log("expr_path should have a def"); fail; }
+        case (some[def](?d)) { df = d; }
+      }
+
       auto res = empty_pre_post(num_local_vars);
-      require_and_preserve(i, *res);
+
+      alt (df) {
+        case (def_local(?d_id)) {
+          auto i = bit_num(d_id, enclosing);
+          require_and_preserve(i, res);
+        }
+        case (_) { /* nothing to check */ }
+      }
+
+      // Otherwise, variable is global, so it must be initialized
+      log("pre/post for:\n");
+      log_expr(@e);
+      log("is");
+      log_pp(res);
       ret (@respan
            (e.span,
             expr_path(p, maybe_def,
                       with_pp(a, res))));
     }
-    case(expr_log(?e, ?a)) {
-      auto e_pp = find_pre_post_expr(enclosing, *e);
+    case(expr_log(?arg, ?a)) {
+      log("log");
+      auto e_pp = find_pre_post_expr(enclosing, *arg);
+      log("pre/post for: ");
+      log_expr(arg);
+      log("is");
+      log_pp(expr_pp(*e_pp));
       ret (@respan(e.span,
-                   expr_log(e_pp, with_pp(a, @expr_pp(e_pp)))));
+                   expr_log(e_pp, with_pp(a, expr_pp(*e_pp)))));
+    }
+    case (expr_block(?b, ?a)) {
+      log("block!");
+      fail;
+    }
+    case (expr_lit(?l, ?a)) {
+      ret @respan(e.span,
+                  expr_lit(l, with_pp(a, empty_pre_post(num_local_vars))));
     }
     case(_) {
       log("this sort of expr isn't implemented!");
@@ -405,8 +684,8 @@ impure fn find_pre_post_expr(&fn_info enclosing, &expr e) -> @expr {
   }
 }
 
-impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
-  -> ast.stmt {
+fn find_pre_post_for_each_stmt(_fn_info_map fm, &fn_info enclosing,
+                               &ast.stmt s) -> ast.stmt {
   auto num_local_vars = num_locals(enclosing);
 
   alt(s.node) {
@@ -418,7 +697,7 @@ impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
               let @expr r = find_pre_post_expr(enclosing, *an_init.expr);
               let init_op o = an_init.op;
               let initializer a_i = rec(op=o, expr=r);
-              let ann res_ann = with_pp(alocal.ann, @expr_pp(r));
+              let ann res_ann = with_pp(alocal.ann, expr_pp(*r));
               let @local res_local =
                 @rec(ty=alocal.ty, infer=alocal.infer,
                      ident=alocal.ident, init=some[initializer](a_i),
@@ -443,24 +722,26 @@ impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
           }
         }
         case(decl_item(?anitem)) {
-          auto res_item = find_pre_post_item(enclosing, *anitem);
+          auto res_item = find_pre_post_item(fm, enclosing, *anitem);
           ret (respan(s.span, stmt_decl(@respan(adecl.span,
                                                decl_item(@res_item))))); 
         }
       }
     }
     case(stmt_expr(?e)) {
+      log_expr(e);
       let @expr e_pp = find_pre_post_expr(enclosing, *e);
       ret (respan(s.span, stmt_expr(e_pp)));
     }    
   }
 }
 
-fn find_pre_post_block(fn_info enclosing, block b) -> block {
-  fn do_one_(fn_info i, &@stmt s) -> @stmt {
-    ret (@find_pre_post_for_each_stmt(i, *s));
+fn find_pre_post_block(&_fn_info_map fm, &fn_info enclosing, block b)
+  -> block {
+  fn do_one_(_fn_info_map fm, fn_info i, &@stmt s) -> @stmt {
+    ret (@find_pre_post_for_each_stmt(fm, i, *s));
   }
-  auto do_one = bind do_one_(enclosing, _);
+  auto do_one = bind do_one_(fm, enclosing, _);
  
   auto ss = _vec.map[@stmt, @stmt](do_one, b.node.stmts);
   fn do_inner_(fn_info i, &@expr e) -> @expr {
@@ -472,24 +753,134 @@ fn find_pre_post_block(fn_info enclosing, block b) -> block {
   ret respan(b.span, b_res);
 }
 
-fn find_pre_post_fn(&_fn f) -> _fn {
-  let fn_info fi = mk_fn_info(f);
+fn find_pre_post_fn(&_fn_info_map fm, &fn_info fi, &_fn f) -> _fn {
   ret rec(decl=f.decl, proto=f.proto,
-          body=find_pre_post_block(fi, f.body));
+          body=find_pre_post_block(fm, fi, f.body));
 }
 
-fn check_item_fn(&@() ignore, &span sp, ident i, &ast._fn f,
+fn check_item_fn(&_fn_info_map fm, &span sp, ident i, &ast._fn f,
                  vec[ast.ty_param] ty_params, def_id id, ann a) -> @item {
 
-  auto res_f = find_pre_post_fn(f);  
+  check (fm.contains_key(id));
+  auto res_f = find_pre_post_fn(fm, fm.get(id), f);  
 
   ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a));
 }
 
+/* Returns a pair of a new function, with possibly a changed pre- or
+   post-state, and a boolean flag saying whether the function's pre- or 
+   poststate changed */
+fn find_pre_post_state_fn(fn_info f_info, &ast._fn f) -> tup(bool, ast._fn) {
+  log ("Implement find_pre_post_state_fn!");
+  fail;
+}
+
+fn fixed_point_states(fn_info f_info,
+                      fn (fn_info, &ast._fn) -> tup(bool, ast._fn) f,
+                      &ast._fn start) -> ast._fn {
+  auto next = f(f_info, start);
+
+  if (next._0) {
+    // something changed
+    be fixed_point_states(f_info, f, next._1);
+  }
+  else {
+    // we're done!
+    ret next._1;
+  }
+}
+
+fn check_states_expr(fn_info enclosing, &expr e) -> () {
+  let precond prec    = expr_precond(e);
+  let postcond postc  = expr_postcond(e);
+  let prestate pres   = expr_prestate(e);
+  let poststate posts = expr_poststate(e);
+
+  if (!implies(pres, prec)) {
+    log("check_states_expr: unsatisfied precondition");
+    fail;
+  }
+  if (!implies(posts, postc)) {
+    log("check_states_expr: unsatisfied postcondition");
+    fail;
+  }
+}
+
+fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
+  alt (stmt_ann(s)) {
+    case (ann_none) {
+      // Statement doesn't require an annotation -- do nothing
+      ret;
+    }
+    case (ann_type(_,_,?m_pp)) {
+      let precond prec    = stmt_precond(s);
+      let postcond postc  = stmt_postcond(s);
+      let prestate pres   = stmt_prestate(s);
+      let poststate posts = stmt_poststate(s);
+
+      if (!implies(pres, prec)) {
+        log("check_states_stmt: unsatisfied precondition");
+        fail;
+      }
+      if (!implies(posts, postc)) {
+        log("check_states_stmt: unsatisfied postcondition");
+        fail;
+      }
+    }
+  }
+}
+
+fn check_states_against_conditions(fn_info enclosing, &ast._fn f) -> () {
+  fn do_one_(fn_info i, &@stmt s) -> () {
+    check_states_stmt(i, *s);
+  }
+  auto do_one = bind do_one_(enclosing, _);
+ 
+  _vec.map[@stmt, ()](do_one, f.body.node.stmts);
+  fn do_inner_(fn_info i, &@expr e) -> () {
+    check_states_expr(i, *e);
+  }
+  auto do_inner = bind do_inner_(enclosing, _);
+  option.map[@expr, ()](do_inner, f.body.node.expr);
+  
+}
+
+fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
+                       &ast._fn f, vec[ast.ty_param] ty_params, def_id id,
+                       ann a) -> @item {
+
+  /* Look up the var-to-bit-num map for this function */
+  check(f_info_map.contains_key(id));
+  auto f_info = f_info_map.get(id);
+
+  /* Compute the pre- and post-states for this function */
+  auto g = find_pre_post_state_fn;
+  auto res_f = fixed_point_states(f_info, g, f);
+
+  /* Now compare each expr's pre-state to its precondition
+     and post-state to its postcondition */
+  check_states_against_conditions(f_info, res_f);
+
+  /* Rebuild the same function */
+  ret @respan(sp, ast.item_fn(i, res_f, ty_params, id, a));
+}
+
 fn check_crate(@ast.crate crate) -> @ast.crate {
-  auto fld = fold.new_identity_fold[@()]();
 
+  /* Build the global map from function id to var-to-bit-num-map */
+  auto fn_info_map = mk_f_to_fn_info(crate);
+
+  /* Compute the pre and postcondition for every subexpression */
+  auto fld = fold.new_identity_fold[_fn_info_map]();
   fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
+  auto with_pre_postconditions = fold.fold_crate[_fn_info_map]
+    (fn_info_map, fld, crate);
+
+  auto fld1 = fold.new_identity_fold[_fn_info_map]();
+
+  fld1 = @rec(fold_item_fn = bind check_item_fn_state(_,_,_,_,_,_,_)
+              with *fld1);
 
-  ret fold.fold_crate[@()](@(), fld, crate);
+  ret fold.fold_crate[_fn_info_map](fn_info_map, fld1,
+                                    with_pre_postconditions);
 }
diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs
index b0d6fb94187..7e0fb6cb7c9 100644
--- a/src/comp/pretty/pprust.rs
+++ b/src/comp/pretty/pprust.rs
@@ -379,6 +379,11 @@ impure fn print_literal(ps s, @ast.lit lit) {
             wrd(s.s, common.istr(val as int));
             wrd(s.s, common.ty_mach_to_str(mach));
         }
+        case (ast.lit_mach_float(?mach,?val)) {
+            // val is already a str
+            wrd(s.s, val);
+            wrd(s.s, common.ty_mach_to_str(mach));
+        }
         case (ast.lit_nil) {wrd(s.s, "()");}
         case (ast.lit_bool(?val)) {
             if (val) {wrd(s.s, "true");} else {wrd(s.s, "false");}
@@ -449,9 +454,9 @@ impure fn print_expr(ps s, &@ast.expr expr) {
             commasep_exprs(s, args);
             pclose(s);
         }
-        case (ast.expr_call_self(?func,?args,_)) {
+        case (ast.expr_call_self(?ident,?args,_)) {
             wrd(s.s, "self.");
-            print_expr(s, func);
+            print_ident(s, ident);
             popen(s);
             commasep_exprs(s, args);
             pclose(s);
@@ -718,6 +723,10 @@ impure fn print_decl(ps s, @ast.decl decl) {
     end(s.s);
 }
 
+impure fn print_ident(ps s, ast.ident ident) {
+    wrd(s.s, ident);
+}
+
 impure fn print_for_decl(ps s, @ast.decl decl) {
     alt (decl.node) {
         case (ast.decl_local(?loc)) {
diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc
index 952ea7e8c9e..47a37f3325f 100644
--- a/src/comp/rustc.rc
+++ b/src/comp/rustc.rc
@@ -62,6 +62,8 @@ auth middle.typestate_check.log_expr = impure;
 auth lib.llvm = unsafe;
 auth pretty.pprust = impure;
 auth middle.typestate_check.find_pre_post_block = impure;
+auth middle.typestate_check.find_pre_post_expr = impure;
+auth util.typestate_ann.implies = impure;
 
 mod lib {
     alt (target_os) {
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
index a4698c5d40f..071f55135f5 100644
--- a/src/comp/util/typestate_ann.rs
+++ b/src/comp/util/typestate_ann.rs
@@ -12,12 +12,21 @@ type precond  = bitv.t; /* 1 means "this variable must be initialized"
 type postcond = bitv.t; /* 1 means "this variable is initialized"
                            0 means "don't know about this variable */
 
+type prestate = bitv.t; /* 1 means "this variable is definitely initialized"
+                           0 means "don't know whether this variable is
+                           initialized" */
+type poststate = bitv.t; /* 1 means "this variable is definitely initialized"
+                            0 means "don't know whether this variable is
+                            initialized" */
+
 /* named thus so as not to confuse with prestate and poststate */
 type pre_and_post = rec(precond precondition, postcond postcondition);
 /* FIXME: once it's implemented: */
 //  : ((*.precondition).nbits == (*.postcondition).nbits);
 
-type ts_ann = pre_and_post;
+type pre_and_post_state = rec(prestate prestate, poststate poststate);
+
+type ts_ann = rec(pre_and_post conditions, pre_and_post_state states);
 
 fn true_precond(uint num_vars) -> precond {
   be bitv.create(num_vars, false);
@@ -27,11 +36,16 @@ fn true_postcond(uint num_vars) -> postcond {
   be true_precond(num_vars);
 }
 
-fn empty_pre_post(uint num_vars) -> @pre_and_post {
-  ret(@rec(precondition=true_precond(num_vars),
+fn empty_pre_post(uint num_vars) -> pre_and_post {
+  ret(rec(precondition=true_precond(num_vars),
            postcondition=true_postcond(num_vars)));
 }
 
+fn empty_states(uint num_vars) -> pre_and_post_state {
+  ret(rec(prestate=true_precond(num_vars),
+           poststate=true_postcond(num_vars)));
+}
+
 fn get_pre(&pre_and_post p) -> precond {
   ret p.precondition;
 }
@@ -57,5 +71,10 @@ fn pps_len(&pre_and_post p) -> uint {
 impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
   // sets the ith bit in p's pre and post
   bitv.set(p.precondition, i, true);
-  bitv.set(p.postcondition, i, false);
-}
\ No newline at end of file
+  bitv.set(p.postcondition, i, true);
+}
+
+fn implies(bitv.t a, bitv.t b) -> bool {
+  bitv.difference(b, a);
+  ret (bitv.equal(b, bitv.create(b.nbits, false)));
+}