aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/comp/driver/rustc.rs5
-rw-r--r--src/comp/front/ast.rs21
-rw-r--r--src/comp/front/lexer.rs2
-rw-r--r--src/comp/front/parser.rs36
-rw-r--r--src/comp/middle/fold.rs98
-rw-r--r--src/comp/middle/trans.rs23
-rw-r--r--src/comp/middle/ty.rs14
-rw-r--r--src/comp/middle/typeck.rs251
-rw-r--r--src/comp/middle/typestate_check.rs496
-rw-r--r--src/comp/pretty/pprust.rs16
-rw-r--r--src/comp/rustc.rc3
-rw-r--r--src/comp/util/typestate_ann.rs61
-rw-r--r--src/lib/_vec.rs23
13 files changed, 814 insertions, 235 deletions
diff --git a/src/comp/driver/rustc.rs b/src/comp/driver/rustc.rs
index 9ab21622..a1fdb387 100644
--- a/src/comp/driver/rustc.rs
+++ b/src/comp/driver/rustc.rs
@@ -8,6 +8,7 @@ import middle.trans;
import middle.resolve;
import middle.ty;
import middle.typeck;
+import middle.typestate_check;
import util.common;
import std.map.mk_hashmap;
@@ -63,11 +64,11 @@ impure fn compile_input(session.session sess,
auto crate = parse_input(sess, p, input);
crate = creader.read_crates(sess, crate, library_search_paths);
crate = resolve.resolve_crate(sess, crate);
-
auto typeck_result = typeck.check_crate(sess, crate);
crate = typeck_result._0;
auto type_cache = typeck_result._1;
-
+ // FIXME: uncomment once typestate_check works
+ // crate = typestate_check.check_crate(crate);
trans.trans_crate(sess, crate, type_cache, output, shared);
}
diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs
index 0bd18382..46666a34 100644
--- a/src/comp/front/ast.rs
+++ b/src/comp/front/ast.rs
@@ -6,6 +6,7 @@ import util.common.span;
import util.common.spanned;
import util.common.ty_mach;
import util.common.filename;
+import util.typestate_ann.ts_ann;
type ident = str;
@@ -21,7 +22,9 @@ type ty_param = rec(ident ident, def_id id);
// Annotations added during successive passes.
tag ann {
ann_none;
- ann_type(@middle.ty.t, option.t[vec[@middle.ty.t]] /* ty param substs */);
+ ann_type(@middle.ty.t,
+ option.t[vec[@middle.ty.t]], /* ty param substs */
+ option.t[@ts_ann]); /* pre- and postcondition for typestate */
}
tag def {
@@ -274,14 +277,14 @@ tag expr_ {
expr_index(@expr, @expr, ann);
expr_path(path, option.t[def], ann);
expr_ext(path, vec[@expr], option.t[@expr], @expr, ann);
- expr_fail;
- expr_break;
- expr_cont;
- expr_ret(option.t[@expr]);
- expr_put(option.t[@expr]);
- expr_be(@expr);
- expr_log(@expr);
- expr_check_expr(@expr);
+ expr_fail(ann);
+ expr_break(ann);
+ expr_cont(ann);
+ expr_ret(option.t[@expr], ann);
+ expr_put(option.t[@expr], ann);
+ expr_be(@expr, ann);
+ expr_log(@expr, ann);
+ expr_check_expr(@expr, ann);
expr_port(ann);
expr_chan(@expr, ann);
}
diff --git a/src/comp/front/lexer.rs b/src/comp/front/lexer.rs
index 6cead0bc..5a9c2b11 100644
--- a/src/comp/front/lexer.rs
+++ b/src/comp/front/lexer.rs
@@ -419,7 +419,7 @@ impure fn scan_number(mutable char c, reader rdr) -> token.token {
if (is_dec_integer) {
accum_int = digits_to_string(dec_str);
}
-
+
c = rdr.curr();
n = rdr.next();
diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs
index f7d355a4..4c3e6cf0 100644
--- a/src/comp/front/parser.rs
+++ b/src/comp/front/parser.rs
@@ -794,14 +794,14 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr {
case (token.FAIL) {
p.bump();
- ex = ast.expr_fail;
+ ex = ast.expr_fail(ast.ann_none);
}
case (token.LOG) {
p.bump();
auto e = parse_expr(p);
auto hi = e.span;
- ex = ast.expr_log(e);
+ ex = ast.expr_log(e, ast.ann_none);
}
case (token.CHECK) {
@@ -810,7 +810,7 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr {
case (token.LPAREN) {
auto e = parse_expr(p);
auto hi = e.span;
- ex = ast.expr_check_expr(e);
+ ex = ast.expr_check_expr(e, ast.ann_none);
}
case (_) {
p.get_session().unimpl("constraint-check stmt");
@@ -822,36 +822,36 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr {
p.bump();
alt (p.peek()) {
case (token.SEMI) {
- ex = ast.expr_ret(none[@ast.expr]);
+ ex = ast.expr_ret(none[@ast.expr], ast.ann_none);
}
case (_) {
auto e = parse_expr(p);
hi = e.span;
- ex = ast.expr_ret(some[@ast.expr](e));
+ ex = ast.expr_ret(some[@ast.expr](e), ast.ann_none);
}
}
}
case (token.BREAK) {
p.bump();
- ex = ast.expr_break;
+ ex = ast.expr_break(ast.ann_none);
}
case (token.CONT) {
p.bump();
- ex = ast.expr_cont;
+ ex = ast.expr_cont(ast.ann_none);
}
case (token.PUT) {
p.bump();
alt (p.peek()) {
case (token.SEMI) {
- ex = ast.expr_put(none[@ast.expr]);
+ ex = ast.expr_put(none[@ast.expr], ast.ann_none);
}
case (_) {
auto e = parse_expr(p);
hi = e.span;
- ex = ast.expr_put(some[@ast.expr](e));
+ ex = ast.expr_put(some[@ast.expr](e), ast.ann_none);
}
}
}
@@ -862,7 +862,7 @@ impure fn parse_bottom_expr(parser p) -> @ast.expr {
// FIXME: Is this the right place for this check?
if /*check*/ (ast.is_call_expr(e)) {
hi = e.span;
- ex = ast.expr_be(e);
+ ex = ast.expr_be(e, ast.ann_none);
}
else {
p.err("Non-call expression in tail call");
@@ -1651,14 +1651,14 @@ fn stmt_ends_with_semi(@ast.stmt stmt) -> bool {
case (ast.expr_field(_,_,_)) { ret true; }
case (ast.expr_index(_,_,_)) { ret true; }
case (ast.expr_path(_,_,_)) { ret true; }
- case (ast.expr_fail) { ret true; }
- case (ast.expr_break) { ret true; }
- case (ast.expr_cont) { ret true; }
- case (ast.expr_ret(_)) { ret true; }
- case (ast.expr_put(_)) { ret true; }
- case (ast.expr_be(_)) { ret true; }
- case (ast.expr_log(_)) { ret true; }
- case (ast.expr_check_expr(_)) { ret true; }
+ case (ast.expr_fail(_)) { ret true; }
+ case (ast.expr_break(_)) { ret true; }
+ case (ast.expr_cont(_)) { ret true; }
+ case (ast.expr_ret(_,_)) { ret true; }
+ case (ast.expr_put(_,_)) { ret true; }
+ case (ast.expr_be(_,_)) { ret true; }
+ case (ast.expr_log(_,_)) { ret true; }
+ case (ast.expr_check_expr(_,_)) { ret true; }
}
}
// We should not be calling this on a cdir.
diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs
index 8138d1a3..d7a18783 100644
--- a/src/comp/middle/fold.rs
+++ b/src/comp/middle/fold.rs
@@ -178,26 +178,26 @@ type ast_fold[ENV] =
@expr expanded,
ann a) -> @expr) fold_expr_ext,
- (fn(&ENV e, &span sp) -> @expr) fold_expr_fail,
+ (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_fail,
- (fn(&ENV e, &span sp) -> @expr) fold_expr_break,
+ (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_break,
- (fn(&ENV e, &span sp) -> @expr) fold_expr_cont,
+ (fn(&ENV e, &span sp, ann a) -> @expr) fold_expr_cont,
(fn(&ENV e, &span sp,
- &option.t[@expr] rv) -> @expr) fold_expr_ret,
+ &option.t[@expr] rv, ann a) -> @expr) fold_expr_ret,
(fn(&ENV e, &span sp,
- &option.t[@expr] rv) -> @expr) fold_expr_put,
+ &option.t[@expr] rv, ann a) -> @expr) fold_expr_put,
(fn(&ENV e, &span sp,
- @expr e) -> @expr) fold_expr_be,
+ @expr e, ann a) -> @expr) fold_expr_be,
(fn(&ENV e, &span sp,
- @expr e) -> @expr) fold_expr_log,
+ @expr e, ann a) -> @expr) fold_expr_log,
(fn(&ENV e, &span sp,
- @expr e) -> @expr) fold_expr_check_expr,
+ @expr e, ann a) -> @expr) fold_expr_check_expr,
(fn(&ENV e, &span sp,
ann a) -> @expr) fold_expr_port,
@@ -717,19 +717,19 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr {
exp, t);
}
- case (ast.expr_fail) {
- ret fld.fold_expr_fail(env_, e.span);
+ case (ast.expr_fail(?t)) {
+ ret fld.fold_expr_fail(env_, e.span, t);
}
- case (ast.expr_break) {
- ret fld.fold_expr_break(env_, e.span);
+ case (ast.expr_break(?t)) {
+ ret fld.fold_expr_break(env_, e.span, t);
}
- case (ast.expr_cont) {
- ret fld.fold_expr_cont(env_, e.span);
+ case (ast.expr_cont(?t)) {
+ ret fld.fold_expr_cont(env_, e.span, t);
}
- case (ast.expr_ret(?oe)) {
+ case (ast.expr_ret(?oe, ?t)) {
auto oee = none[@expr];
alt (oe) {
case (some[@expr](?x)) {
@@ -737,10 +737,10 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr {
}
case (_) { /* fall through */ }
}
- ret fld.fold_expr_ret(env_, e.span, oee);
+ ret fld.fold_expr_ret(env_, e.span, oee, t);
}
- case (ast.expr_put(?oe)) {
+ case (ast.expr_put(?oe, ?t)) {
auto oee = none[@expr];
alt (oe) {
case (some[@expr](?x)) {
@@ -748,22 +748,22 @@ fn fold_expr[ENV](&ENV env, ast_fold[ENV] fld, &@expr e) -> @expr {
}
case (_) { /* fall through */ }
}
- ret fld.fold_expr_put(env_, e.span, oee);
+ ret fld.fold_expr_put(env_, e.span, oee, t);
}
- case (ast.expr_be(?x)) {
+ case (ast.expr_be(?x, ?t)) {
auto ee = fold_expr(env_, fld, x);
- ret fld.fold_expr_be(env_, e.span, ee);
+ ret fld.fold_expr_be(env_, e.span, ee, t);
}
- case (ast.expr_log(?x)) {
+ case (ast.expr_log(?x, ?t)) {
auto ee = fold_expr(env_, fld, x);
- ret fld.fold_expr_log(env_, e.span, ee);
+ ret fld.fold_expr_log(env_, e.span, ee, t);
}
- case (ast.expr_check_expr(?x)) {
+ case (ast.expr_check_expr(?x, ?t)) {
auto ee = fold_expr(env_, fld, x);
- ret fld.fold_expr_check_expr(env_, e.span, ee);
+ ret fld.fold_expr_check_expr(env_, e.span, ee, t);
}
case (ast.expr_port(?t)) {
@@ -1308,38 +1308,40 @@ fn identity_fold_expr_ext[ENV](&ENV env, &span sp,
ret @respan(sp, ast.expr_ext(p, args, body, expanded, a));
}
-fn identity_fold_expr_fail[ENV](&ENV env, &span sp) -> @expr {
- ret @respan(sp, ast.expr_fail);
+fn identity_fold_expr_fail[ENV](&ENV env, &span sp, ann a) -> @expr {
+ ret @respan(sp, ast.expr_fail(a));
}
-fn identity_fold_expr_break[ENV](&ENV env, &span sp) -> @expr {
- ret @respan(sp, ast.expr_break);
+fn identity_fold_expr_break[ENV](&ENV env, &span sp, ann a) -> @expr {
+ ret @respan(sp, ast.expr_break(a));
}
-fn identity_fold_expr_cont[ENV](&ENV env, &span sp) -> @expr {
- ret @respan(sp, ast.expr_cont);
+fn identity_fold_expr_cont[ENV](&ENV env, &span sp, ann a) -> @expr {
+ ret @respan(sp, ast.expr_cont(a));
}
fn identity_fold_expr_ret[ENV](&ENV env, &span sp,
- &option.t[@expr] rv) -> @expr {
- ret @respan(sp, ast.expr_ret(rv));
+ &option.t[@expr] rv, ann a) -> @expr {
+ ret @respan(sp, ast.expr_ret(rv, a));
}
fn identity_fold_expr_put[ENV](&ENV env, &span sp,
- &option.t[@expr] rv) -> @expr {
- ret @respan(sp, ast.expr_put(rv));
+ &option.t[@expr] rv, ann a) -> @expr {
+ ret @respan(sp, ast.expr_put(rv, a));
}
-fn identity_fold_expr_be[ENV](&ENV env, &span sp, @expr x) -> @expr {
- ret @respan(sp, ast.expr_be(x));
+fn identity_fold_expr_be[ENV](&ENV env, &span sp, @expr x, ann a) -> @expr {
+ ret @respan(sp, ast.expr_be(x, a));
}
-fn identity_fold_expr_log[ENV](&ENV e, &span sp, @expr x) -> @expr {
- ret @respan(sp, ast.expr_log(x));
+fn identity_fold_expr_log[ENV](&ENV e, &span sp, @expr x,
+ ann a) -> @expr {
+ ret @respan(sp, ast.expr_log(x, a));
}
-fn identity_fold_expr_check_expr[ENV](&ENV e, &span sp, @expr x) -> @expr {
- ret @respan(sp, ast.expr_check_expr(x));
+fn identity_fold_expr_check_expr[ENV](&ENV e, &span sp, @expr x, ann a)
+ -> @expr {
+ ret @respan(sp, ast.expr_check_expr(x, a));
}
fn identity_fold_expr_port[ENV](&ENV e, &span sp, ann a) -> @expr {
@@ -1621,15 +1623,15 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] {
fold_expr_index = bind identity_fold_expr_index[ENV](_,_,_,_,_),
fold_expr_path = bind identity_fold_expr_path[ENV](_,_,_,_,_),
fold_expr_ext = bind identity_fold_expr_ext[ENV](_,_,_,_,_,_,_),
- fold_expr_fail = bind identity_fold_expr_fail[ENV](_,_),
- fold_expr_break = bind identity_fold_expr_break[ENV](_,_),
- fold_expr_cont = bind identity_fold_expr_cont[ENV](_,_),
- fold_expr_ret = bind identity_fold_expr_ret[ENV](_,_,_),
- fold_expr_put = bind identity_fold_expr_put[ENV](_,_,_),
- fold_expr_be = bind identity_fold_expr_be[ENV](_,_,_),
- fold_expr_log = bind identity_fold_expr_log[ENV](_,_,_),
+ fold_expr_fail = bind identity_fold_expr_fail[ENV](_,_,_),
+ fold_expr_break = bind identity_fold_expr_break[ENV](_,_,_),
+ fold_expr_cont = bind identity_fold_expr_cont[ENV](_,_,_),
+ fold_expr_ret = bind identity_fold_expr_ret[ENV](_,_,_,_),
+ fold_expr_put = bind identity_fold_expr_put[ENV](_,_,_,_),
+ fold_expr_be = bind identity_fold_expr_be[ENV](_,_,_,_),
+ fold_expr_log = bind identity_fold_expr_log[ENV](_,_,_,_),
fold_expr_check_expr
- = bind identity_fold_expr_check_expr[ENV](_,_,_),
+ = bind identity_fold_expr_check_expr[ENV](_,_,_,_),
fold_expr_port = bind identity_fold_expr_port[ENV](_,_,_),
fold_expr_chan = bind identity_fold_expr_chan[ENV](_,_,_,_),
diff --git a/src/comp/middle/trans.rs b/src/comp/middle/trans.rs
index c018ad57..eb848f76 100644
--- a/src/comp/middle/trans.rs
+++ b/src/comp/middle/trans.rs
@@ -2497,7 +2497,7 @@ fn node_ann_type(@crate_ctxt cx, &ast.ann a) -> @ty.t {
case (ast.ann_none) {
cx.sess.bug("missing type annotation");
}
- case (ast.ann_type(?t, _)) {
+ case (ast.ann_type(?t, _, _)) {
ret target_type(cx, t);
}
}
@@ -2509,7 +2509,7 @@ fn node_ann_ty_params(&ast.ann a) -> vec[@ty.t] {
log "missing type annotation";
fail;
}
- case (ast.ann_type(_, ?tps_opt)) {
+ case (ast.ann_type(_, ?tps_opt, _)) {
alt (tps_opt) {
case (none[vec[@ty.t]]) {
log "type annotation has no ty params";
@@ -3638,7 +3638,7 @@ fn lval_generic_fn(@block_ctxt cx,
cx.fcx.ccx.sess.bug("no type annotation for path!");
fail;
}
- case (ast.ann_type(?monoty_, ?tps)) {
+ case (ast.ann_type(?monoty_, ?tps, _)) {
monoty = monoty_;
tys = option.get[vec[@ty.t]](tps);
}
@@ -4775,35 +4775,35 @@ fn trans_expr(@block_ctxt cx, @ast.expr e) -> result {
ret trans_expr(cx, expanded);
}
- case (ast.expr_fail) {
+ case (ast.expr_fail(_)) {
ret trans_fail(cx, e.span, "explicit failure");
}
- case (ast.expr_log(?a)) {
+ case (ast.expr_log(?a, _)) {
ret trans_log(cx, a);
}
- case (ast.expr_check_expr(?a)) {
+ case (ast.expr_check_expr(?a, _)) {
ret trans_check_expr(cx, a);
}
- case (ast.expr_break) {
+ case (ast.expr_break(?a)) {
ret trans_break(cx);
}
- case (ast.expr_cont) {
+ case (ast.expr_cont(?a)) {
ret trans_cont(cx);
}
- case (ast.expr_ret(?e)) {
+ case (ast.expr_ret(?e, _)) {
ret trans_ret(cx, e);
}
- case (ast.expr_put(?e)) {
+ case (ast.expr_put(?e, _)) {
ret trans_put(cx, e);
}
- case (ast.expr_be(?e)) {
+ case (ast.expr_be(?e, _)) {
ret trans_be(cx, e);
}
@@ -4855,6 +4855,7 @@ fn trans_log(@block_ctxt cx, @ast.expr e) -> result {
auto sub = trans_expr(cx, e);
auto e_ty = ty.expr_ty(e);
+
if (ty.type_is_fp(e_ty)) {
let TypeRef tr;
let bool is32bit = false;
diff --git a/src/comp/middle/ty.rs b/src/comp/middle/ty.rs
index 829a5e5f..d0b5fe10 100644
--- a/src/comp/middle/ty.rs
+++ b/src/comp/middle/ty.rs
@@ -593,7 +593,7 @@ fn ann_to_type(&ast.ann ann) -> @t {
log "ann_to_type() called on node with no type";
fail;
}
- case (ast.ann_type(?ty, _)) {
+ case (ast.ann_type(?ty, _, _)) {
ret ty;
}
}
@@ -785,12 +785,12 @@ fn expr_ty(@ast.expr expr) -> @t {
case (ast.expr_send(_, _, ?ann)) { ret ann_to_type(ann); }
case (ast.expr_recv(_, _, ?ann)) { ret ann_to_type(ann); }
- case (ast.expr_fail) { ret plain_ty(ty_nil); }
- case (ast.expr_log(_)) { ret plain_ty(ty_nil); }
- case (ast.expr_check_expr(_)) { ret plain_ty(ty_nil); }
- case (ast.expr_ret(_)) { ret plain_ty(ty_nil); }
- case (ast.expr_put(_)) { ret plain_ty(ty_nil); }
- case (ast.expr_be(_)) { ret plain_ty(ty_nil); }
+ case (ast.expr_fail(_)) { ret plain_ty(ty_nil); }
+ case (ast.expr_log(_,_)) { ret plain_ty(ty_nil); }
+ case (ast.expr_check_expr(_,_)) { ret plain_ty(ty_nil); }
+ case (ast.expr_ret(_,_)) { ret plain_ty(ty_nil); }
+ case (ast.expr_put(_,_)) { ret plain_ty(ty_nil); }
+ case (ast.expr_be(_,_)) { ret plain_ty(ty_nil); }
}
fail;
}
diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs
index d0481b6a..f726ae58 100644
--- a/src/comp/middle/typeck.rs
+++ b/src/comp/middle/typeck.rs
@@ -1,5 +1,6 @@
import front.ast;
import front.ast.ann;
+import front.ast.ann_none;
import front.ast.mutability;
import front.creader;
import middle.fold;
@@ -32,6 +33,8 @@ import std.option;
import std.option.none;
import std.option.some;
+import util.typestate_ann.ts_ann;
+
type ty_table = hashmap[ast.def_id, @ty.t];
tag any_item {
@@ -54,6 +57,11 @@ type fn_ctxt = rec(@ty.t ret_ty,
// Used for ast_ty_to_ty() below.
type ty_getter = fn(ast.def_id) -> ty.ty_params_opt_and_ty;
+// Turns a type into an ann_type, using defaults for other fields.
+fn triv_ann(@ty.t t) -> ann {
+ ret ast.ann_type(t, none[vec[@ty.t]], none[@ts_ann]);
+}
+
// 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,
@@ -227,7 +235,7 @@ fn instantiate_path(@fn_ctxt fcx, &ast.path pth, &ty_params_opt_and_ty tpt,
}
}
- ret ast.ann_type(t, ty_substs_opt);
+ ret ast.ann_type(t, ty_substs_opt, none[@ts_ann]);
}
// Returns the type parameters and polytype of an item, if it's an item that
@@ -674,9 +682,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
auto tpt = tup(params_opt, result_ty);
type_cache.insert(variant.node.id, tpt);
-
- auto variant_t = rec(
- ann=ast.ann_type(result_ty, none[vec[@ty.t]])
+ auto variant_t = rec(ann=triv_ann(result_ty)
with variant.node
);
result += vec(fold.respan[ast.variant_](variant.span, variant_t));
@@ -767,8 +773,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
ast.def_id id, ast.ann a) -> @ast.item {
check (e.type_cache.contains_key(id));
auto typ = e.type_cache.get(id)._1;
- auto item = ast.item_const(i, t, ex, id,
- ast.ann_type(typ, none[vec[@ty.t]]));
+ auto item = ast.item_const(i, t, ex, id, triv_ann(typ));
ret @fold.respan[ast.item_](sp, item);
}
@@ -777,8 +782,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
ast.def_id id, ast.ann a) -> @ast.item {
check (e.type_cache.contains_key(id));
auto typ = e.type_cache.get(id)._1;
- auto item = ast.item_fn(i, f, ty_params, id,
- ast.ann_type(typ, none[vec[@ty.t]]));
+ auto item = ast.item_fn(i, f, ty_params, id, triv_ann(typ));
ret @fold.respan[ast.item_](sp, item);
}
@@ -788,7 +792,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
check (e.type_cache.contains_key(id));
auto typ = e.type_cache.get(id)._1;
auto item = ast.native_item_fn(i, ln, d, ty_params, id,
- ast.ann_type(typ, none[vec[@ty.t]]));
+ triv_ann(typ));
ret @fold.respan[ast.native_item_](sp, item);
}
@@ -832,8 +836,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
auto meth_tfn = plain_ty(ty.ty_fn(meth_ty.proto,
meth_ty.inputs,
meth_ty.output));
- m_ = rec(
- ann=ast.ann_type(meth_tfn, none[vec[@ty.t]])
+ m_ = rec(ann=triv_ann(meth_tfn)
with meth.node
);
m = @rec(node=m_ with *meth);
@@ -842,8 +845,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
auto g = bind getter(e.sess, e.id_to_ty_item, e.type_cache, _);
for (ast.obj_field fld in ob.fields) {
let @ty.t fty = ast_ty_to_ty(g, fld.ty);
- let ast.obj_field f = rec(
- ann=ast.ann_type(fty, none[vec[@ty.t]])
+ let ast.obj_field f = rec(ann=triv_ann(fty)
with fld
);
_vec.push[ast.obj_field](fields, f);
@@ -852,8 +854,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
auto ob_ = rec(methods = methods,
fields = fields
with ob);
- auto item = ast.item_obj(i, ob_, ty_params, odid,
- ast.ann_type(t, none[vec[@ty.t]]));
+ auto item = ast.item_obj(i, ob_, ty_params, odid, triv_ann(t));
ret @fold.respan[ast.item_](sp, item);
}
@@ -862,8 +863,7 @@ fn collect_item_types(session.session sess, @ast.crate crate)
ast.def_id id, ast.ann a) -> @ast.item {
check (e.type_cache.contains_key(id));
auto typ = e.type_cache.get(id)._1;
- auto item = ast.item_ty(i, t, ty_params, id,
- ast.ann_type(typ, none[vec[@ty.t]]));
+ auto item = ast.item_ty(i, t, ty_params, id, triv_ann(typ));
ret @fold.respan[ast.item_](sp, item);
}
@@ -879,7 +879,8 @@ fn collect_item_types(session.session sess, @ast.crate crate)
ty_params);
auto typ = e.type_cache.get(id)._1;
auto item = ast.item_tag(i, variants_t, ty_params, id,
- ast.ann_type(typ, none[vec[@ty.t]]));
+ ast.ann_type(typ, none[vec[@ty.t]],
+ none[@ts_ann]));
ret @fold.respan[ast.item_](sp, item);
}
@@ -1034,16 +1035,20 @@ fn demand_pat(&@fn_ctxt fcx, @ty.t expected, @ast.pat pat) -> @ast.pat {
alt (pat.node) {
case (ast.pat_wild(?ann)) {
auto t = demand(fcx, pat.span, expected, ann_to_type(ann));
- p_1 = ast.pat_wild(ast.ann_type(t, none[vec[@ty.t]]));
+ p_1 = ast.pat_wild(ast.ann_type(t, none[vec[@ty.t]],
+ none[@ts_ann]));
}
case (ast.pat_lit(?lit, ?ann)) {
auto t = demand(fcx, pat.span, expected, ann_to_type(ann));
- p_1 = ast.pat_lit(lit, ast.ann_type(t, none[vec[@ty.t]]));
+ p_1 = ast.pat_lit(lit, ast.ann_type(t, none[vec[@ty.t]],
+ none[@ts_ann]));
}
case (ast.pat_bind(?id, ?did, ?ann)) {
auto t = demand(fcx, pat.span, expected, ann_to_type(ann));
fcx.locals.insert(did, t);
- p_1 = ast.pat_bind(id, did, ast.ann_type(t, none[vec[@ty.t]]));
+ p_1 = ast.pat_bind(id, did, ast.ann_type(t,
+ none[vec[@ty.t]],
+ none[@ts_ann]));
}
case (ast.pat_tag(?id, ?subpats, ?vdef_opt, ?ann)) {
auto t = demand(fcx, pat.span, expected, ann_to_type(ann));
@@ -1086,7 +1091,8 @@ fn demand_pat(&@fn_ctxt fcx, @ty.t expected, @ast.pat pat) -> @ast.pat {
// Nullary tag variant.
check (subpats_len == 0u);
p_1 = ast.pat_tag(id, subpats, vdef_opt,
- ast.ann_type(t, tps_opt));
+ ast.ann_type(t, tps_opt,
+ none[@ts_ann]));
}
case (ty.ty_fn(_, ?args, ?tag_ty)) {
// N-ary tag variant.
@@ -1101,7 +1107,8 @@ fn demand_pat(&@fn_ctxt fcx, @ty.t expected, @ast.pat pat) -> @ast.pat {
i += 1u;
}
p_1 = ast.pat_tag(id, new_subpats, vdef_opt,
- ast.ann_type(tag_ty, tps_opt));
+ ast.ann_type(tag_ty, tps_opt,
+ none[@ts_ann]));
}
}
}
@@ -1142,7 +1149,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
fail;
}
}
- e_1 = ast.expr_vec(es_1, mut, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_vec(es_1, mut, triv_ann(t));
}
case (ast.expr_tup(?es_0, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
@@ -1161,7 +1168,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
fail;
}
}
- e_1 = ast.expr_tup(elts_1, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_tup(elts_1, triv_ann(t));
}
case (ast.expr_rec(?fields_0, ?base_0, ?ann)) {
@@ -1214,12 +1221,11 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
fail;
}
}
- e_1 = ast.expr_rec(fields_1, base_1,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_rec(fields_1, base_1, triv_ann(t));
}
case (ast.expr_bind(?sube, ?es, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_bind(sube, es, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_bind(sube, es, triv_ann(t));
}
case (ast.expr_call(?sube, ?es, ?ann)) {
// NB: we call 'demand_full' and pass in adk only in cases where
@@ -1227,35 +1233,30 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
// like expr_binary or expr_bind can't, so there's no need.
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_call(sube, es, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_call(sube, es, triv_ann(t));
}
case (ast.expr_call_self(?sube, ?es, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_call_self(sube,
- es,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_call_self(sube, es, triv_ann(t));
}
case (ast.expr_binary(?bop, ?lhs, ?rhs, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_binary(bop, lhs, rhs,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_binary(bop, lhs, rhs, triv_ann(t));
}
case (ast.expr_unary(?uop, ?sube, ?ann)) {
// See note in expr_unary for why we're calling demand_full.
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_unary(uop, sube,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_unary(uop, sube, triv_ann(t));
}
case (ast.expr_lit(?lit, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_lit(lit, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_lit(lit, triv_ann(t));
}
case (ast.expr_cast(?sube, ?ast_ty, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_cast(sube, ast_ty,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_cast(sube, ast_ty, triv_ann(t));
}
case (ast.expr_if(?cond, ?then_0, ?else_0, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
@@ -1270,60 +1271,52 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
else_1 = some[@ast.expr](e_1);
}
}
- e_1 = ast.expr_if(cond, then_1, else_1,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_if(cond, then_1, else_1, triv_ann(t));
}
case (ast.expr_for(?decl, ?seq, ?bloc, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_for(decl, seq, bloc,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_for(decl, seq, bloc, triv_ann(t));
}
case (ast.expr_for_each(?decl, ?seq, ?bloc, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_for_each(decl, seq, bloc,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_for_each(decl, seq, bloc, triv_ann(t));
}
case (ast.expr_while(?cond, ?bloc, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_while(cond, bloc,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_while(cond, bloc, triv_ann(t));
}
case (ast.expr_do_while(?bloc, ?cond, ?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_do_while(bloc, cond,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_do_while(bloc, cond, triv_ann(t));
}
case (ast.expr_block(?bloc, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_block(bloc, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_block(bloc, triv_ann(t));
}
case (ast.expr_assign(?lhs_0, ?rhs_0, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
auto lhs_1 = demand_expr(fcx, expected, lhs_0);
auto rhs_1 = demand_expr(fcx, expected, rhs_0);
- e_1 = ast.expr_assign(lhs_1, rhs_1,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_assign(lhs_1, rhs_1, triv_ann(t));
}
case (ast.expr_assign_op(?op, ?lhs_0, ?rhs_0, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
auto lhs_1 = demand_expr(fcx, expected, lhs_0);
auto rhs_1 = demand_expr(fcx, expected, rhs_0);
- e_1 = ast.expr_assign_op(op, lhs_1, rhs_1,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_assign_op(op, lhs_1, rhs_1, triv_ann(t));
}
case (ast.expr_field(?lhs, ?rhs, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_field(lhs, rhs, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_field(lhs, rhs, triv_ann(t));
}
case (ast.expr_index(?base, ?index, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_index(base, index,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_index(base, index, triv_ann(t));
}
case (ast.expr_path(?pth, ?d, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
@@ -1338,7 +1331,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
"did you pass it to check_expr() first?";
fail;
}
- case (ast.ann_type(_, ?tps_opt)) {
+ case (ast.ann_type(_, ?tps_opt, _)) {
alt (tps_opt) {
case (none[vec[@ty.t]]) {
auto defn = option.get[ast.def](d);
@@ -1359,26 +1352,28 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
}
}
- e_1 = ast.expr_path(pth, d, ast.ann_type(t, ty_params_opt));
+ e_1 = ast.expr_path(pth, d,
+ ast.ann_type(t, ty_params_opt,
+ none[@ts_ann]));
}
case (ast.expr_ext(?p, ?args, ?body, ?expanded, ?ann)) {
auto t = demand_full(fcx, e.span, expected,
ann_to_type(ann), adk);
- e_1 = ast.expr_ext(p, args, body, expanded,
- ast.ann_type(t, none[vec[@ty.t]]));
- }
- case (ast.expr_fail) { e_1 = e.node; }
- case (ast.expr_log(_)) { e_1 = e.node; }
- case (ast.expr_break) { e_1 = e.node; }
- case (ast.expr_cont) { e_1 = e.node; }
- case (ast.expr_ret(_)) { e_1 = e.node; }
- case (ast.expr_put(_)) { e_1 = e.node; }
- case (ast.expr_be(_)) { e_1 = e.node; }
- case (ast.expr_check_expr(_)) { e_1 = e.node; }
+ e_1 = ast.expr_ext(p, args, body, expanded, triv_ann(t));
+ }
+ /* FIXME: this should probably 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; }
+ case (ast.expr_cont(_)) { e_1 = e.node; }
+ case (ast.expr_ret(_,_)) { e_1 = e.node; }
+ case (ast.expr_put(_,_)) { e_1 = e.node; }
+ case (ast.expr_be(_,_)) { e_1 = e.node; }
+ case (ast.expr_check_expr(_,_)) { e_1 = e.node; }
case (ast.expr_port(?ann)) {
auto t = demand(fcx, e.span, expected, ann_to_type(ann));
- e_1 = ast.expr_port(ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_port(triv_ann(t));
}
case (ast.expr_chan(?es, ?ann)) {
@@ -1394,7 +1389,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
fail;
}
}
- e_1 = ast.expr_chan(es_1, ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_chan(es_1, triv_ann(t));
}
case (ast.expr_alt(?discrim, ?arms_0, ?ann)) {
@@ -1407,8 +1402,7 @@ fn demand_expr_full(&@fn_ctxt fcx, @ty.t expected, @ast.expr e,
index=arm_0.index);
arms_1 += vec(arm_1);
}
- e_1 = ast.expr_alt(discrim, arms_1,
- ast.ann_type(t, none[vec[@ty.t]]));
+ e_1 = ast.expr_alt(discrim, arms_1, triv_ann(t));
}
case (_) {
@@ -1449,8 +1443,7 @@ fn writeback_local(&option.t[@fn_ctxt] env, &span sp, @ast.local local)
+ local.ident);
}
auto local_ty = fcx.locals.get(local.id);
- auto local_wb = @rec(
- ann=ast.ann_type(local_ty, none[vec[@ty.t]])
+ auto local_wb = @rec(ann=triv_ann(local_ty)
with *local
);
ret @fold.respan[ast.decl_](sp, ast.decl_local(local_wb));
@@ -1502,15 +1495,13 @@ fn check_pat(&@fn_ctxt fcx, @ast.pat pat) -> @ast.pat {
auto new_pat;
alt (pat.node) {
case (ast.pat_wild(_)) {
- new_pat = ast.pat_wild(ast.ann_type(next_ty_var(fcx.ccx),
- none[vec[@ty.t]]));
+ new_pat = ast.pat_wild(triv_ann(next_ty_var(fcx.ccx)));
}
case (ast.pat_lit(?lt, _)) {
- new_pat = ast.pat_lit(lt, ast.ann_type(check_lit(lt),
- none[vec[@ty.t]]));
+ new_pat = ast.pat_lit(lt, triv_ann(check_lit(lt)));
}
case (ast.pat_bind(?id, ?def_id, _)) {
- auto ann = ast.ann_type(next_ty_var(fcx.ccx), none[vec[@ty.t]]);
+ auto ann = triv_ann(next_ty_var(fcx.ccx));
new_pat = ast.pat_bind(id, def_id, ann);
}
case (ast.pat_tag(?p, ?subpats, ?vdef_opt, _)) {
@@ -1670,7 +1661,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto lhs_1 = demand_expr(fcx, rhs_t0, lhs_0);
auto rhs_1 = demand_expr(fcx, expr_ty(lhs_1), rhs_0);
- auto ann = ast.ann_type(rhs_t0, none[vec[@ty.t]]);
+ auto ann = triv_ann(rhs_t0);
ret tup(lhs_1, rhs_1, ann);
}
@@ -1698,7 +1689,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
alt (expr.node) {
case (ast.expr_lit(?lit, _)) {
auto typ = check_lit(lit);
- auto ann = ast.ann_type(typ, none[vec[@ty.t]]);
+ auto ann = triv_ann(typ);
ret @fold.respan[ast.expr_](expr.span, ast.expr_lit(lit, ann));
}
@@ -1726,7 +1717,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
case (_) { /* fall through */ }
}
- auto ann = ast.ann_type(t, none[vec[@ty.t]]);
+ auto ann = triv_ann(t);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_binary(binop, lhs_1, rhs_1,
ann));
@@ -1757,7 +1748,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
case (_) { oper_t = strip_boxes(oper_t); }
}
- auto ann = ast.ann_type(oper_t, none[vec[@ty.t]]);
+ auto ann = triv_ann(oper_t);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_unary(unop, oper_1, ann));
}
@@ -1775,25 +1766,25 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
case (ast.expr_ext(?p, ?args, ?body, ?expanded, _)) {
auto exp_ = check_expr(fcx, expanded);
auto t = expr_ty(exp_);
- auto ann = ast.ann_type(t, none[vec[@ty.t]]);
+ auto ann = triv_ann(t);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_ext(p, args, body, exp_,
ann));
}
- case (ast.expr_fail) {
+ case (ast.expr_fail(_)) { // ??? ignoring ann
ret expr;
}
- case (ast.expr_break) {
+ case (ast.expr_break(_)) {
ret expr;
}
- case (ast.expr_cont) {
+ case (ast.expr_cont(_)) {
ret expr;
}
- case (ast.expr_ret(?expr_opt)) {
+ case (ast.expr_ret(?expr_opt, _)) {
alt (expr_opt) {
case (none[@ast.expr]) {
auto nil = plain_ty(ty.ty_nil);
@@ -1808,13 +1799,13 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
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)));
+ ret @fold.respan[ast.expr_]
+ (expr.span, ast.expr_ret(some(expr_1), ann_none));
}
}
}
- case (ast.expr_put(?expr_opt)) {
+ case (ast.expr_put(?expr_opt, _)) {
alt (expr_opt) {
case (none[@ast.expr]) {
auto nil = plain_ty(ty.ty_nil);
@@ -1829,31 +1820,32 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
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)));
+ ret @fold.respan[ast.expr_]
+ (expr.span, ast.expr_put(some(expr_1), ann_none));
}
}
}
- case (ast.expr_be(?e)) {
+ case (ast.expr_be(?e, _)) {
/* FIXME: prove instead of check */
check (ast.is_call_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_be(expr_1));
+ ast.expr_be(expr_1, ann_none));
}
- case (ast.expr_log(?e)) {
+ case (ast.expr_log(?e,_)) {
auto expr_t = check_expr(fcx, e);
- ret @fold.respan[ast.expr_](expr.span, ast.expr_log(expr_t));
+ ret @fold.respan[ast.expr_]
+ (expr.span, ast.expr_log(expr_t, ann_none));
}
- case (ast.expr_check_expr(?e)) {
+ 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));
+ ret @fold.respan[ast.expr_]
+ (expr.span, ast.expr_check_expr(expr_t, ann_none));
}
case (ast.expr_assign(?lhs, ?rhs, _)) {
@@ -1891,7 +1883,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
}
auto rhs_1 = demand_expr(fcx, item_t, rhs_0);
- auto ann = ast.ann_type(chan_t, none[vec[@ty.t]]);
+ auto ann = triv_ann(chan_t);
auto newexpr = ast.expr_send(lhs_1, rhs_1, ann);
ret @fold.respan[ast.expr_](expr.span, newexpr);
}
@@ -1914,7 +1906,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
}
auto lhs_1 = demand_expr(fcx, item_t, lhs_0);
- auto ann = ast.ann_type(item_t, none[vec[@ty.t]]);
+ auto ann = triv_ann(item_t);
auto newexpr = ast.expr_recv(lhs_1, rhs_1, ann);
ret @fold.respan[ast.expr_](expr.span, newexpr);
}
@@ -1943,7 +1935,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto thn_1 = demand_block(fcx, elsopt_t, thn_0);
- auto ann = ast.ann_type(elsopt_t, none[vec[@ty.t]]);
+ auto ann = triv_ann(elsopt_t);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_if(cond_1, thn_1,
elsopt_1, ann));
@@ -1957,7 +1949,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
// FIXME: enforce that the type of the decl is the element type
// of the seq.
- auto ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(ty.ty_nil));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_for(decl_1, seq_1,
body_1, ann));
@@ -1968,7 +1960,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto seq_1 = check_expr(fcx, seq);
auto body_1 = check_block(fcx, body);
- auto ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(ty.ty_nil));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_for_each(decl_1, seq_1,
body_1, ann));
@@ -1979,7 +1971,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto cond_1 = demand_expr(fcx, plain_ty(ty.ty_bool), cond_0);
auto body_1 = check_block(fcx, body);
- auto ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(ty.ty_nil));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_while(cond_1, body_1, ann));
}
@@ -1989,7 +1981,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto cond_1 = demand_expr(fcx, plain_ty(ty.ty_bool), cond_0);
auto body_1 = check_block(fcx, body);
- auto ann = ast.ann_type(block_ty(body_1), none[vec[@ty.t]]);
+ auto ann = triv_ann(block_ty(body_1));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_do_while(body_1, cond_1,
ann));
@@ -2039,7 +2031,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto expr_1 = demand_expr(fcx, pattern_ty, expr_0);
- auto ann = ast.ann_type(result_ty, none[vec[@ty.t]]);
+ auto ann = triv_ann(result_ty);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_alt(expr_1, arms_1, ann));
}
@@ -2049,10 +2041,10 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto ann;
alt (b_0.node.expr) {
case (some[@ast.expr](?expr)) {
- ann = ast.ann_type(expr_ty(expr), none[vec[@ty.t]]);
+ ann = triv_ann(expr_ty(expr));
}
case (none[@ast.expr]) {
- ann = ast.ann_type(plain_ty(ty.ty_nil), none[vec[@ty.t]]);
+ ann = triv_ann(plain_ty(ty.ty_nil));
}
}
ret @fold.respan[ast.expr_](expr.span,
@@ -2092,7 +2084,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
}
auto t_1 = plain_ty(ty.ty_fn(proto_1, arg_tys_1, rt_1));
- auto ann = ast.ann_type(t_1, none[vec[@ty.t]]);
+ auto ann = triv_ann(t_1);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_bind(result._0, result._1,
ann));
@@ -2114,7 +2106,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
}
}
- auto ann = ast.ann_type(rt_1, none[vec[@ty.t]]);
+ auto ann = triv_ann(rt_1);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_call(f_1, args_1, ann));
}
@@ -2143,7 +2135,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
// FIXME: Other typechecks needed
- auto ann = ast.ann_type(plain_ty(ty.ty_task), none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(ty.ty_task));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_spawn(dom, name,
f_1, args_1, ann));
@@ -2162,7 +2154,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
+ ty_to_str(t_1));
}
- auto ann = ast.ann_type(t_1, none[vec[@ty.t]]);
+ auto ann = triv_ann(t_1);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_cast(e_1, t, ann));
}
@@ -2186,7 +2178,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
}
auto vec_sty = ty.ty_vec(rec(ty=t, mut=mut));
- auto ann = ast.ann_type(plain_ty(vec_sty), none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(vec_sty));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_vec(args_1, mut, ann));
}
@@ -2202,8 +2194,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
elts_mt += vec(rec(ty=expr_t, mut=e.mut));
}
- auto ann = ast.ann_type(plain_ty(ty.ty_tup(elts_mt)),
- none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(ty.ty_tup(elts_mt)));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_tup(elts_1, ann));
}
@@ -2234,8 +2225,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
alt (base) {
case (none[@ast.expr]) {
- ann = ast.ann_type(plain_ty(ty.ty_rec(fields_t)),
- none[vec[@ty.t]]);
+ ann = triv_ann(plain_ty(ty.ty_rec(fields_t)));
}
case (some[@ast.expr](?bexpr)) {
@@ -2255,7 +2245,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
}
}
- ann = ast.ann_type(bexpr_t, none[vec[@ty.t]]);
+ ann = triv_ann(bexpr_t);
for (ty.field f in fields_t) {
auto found = false;
@@ -2290,7 +2280,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
fcx.ccx.sess.span_err(expr.span,
"bad index on tuple");
}
- auto ann = ast.ann_type(args.(ix).ty, none[vec[@ty.t]]);
+ auto ann = triv_ann(args.(ix).ty);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_field(base_1,
field,
@@ -2304,8 +2294,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
fcx.ccx.sess.span_err(expr.span,
"bad index on record");
}
- auto ann = ast.ann_type(fields.(ix).mt.ty,
- none[vec[@ty.t]]);
+ auto ann = triv_ann(fields.(ix).mt.ty);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_field(base_1,
field,
@@ -2322,7 +2311,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
auto meth = methods.(ix);
auto t = plain_ty(ty.ty_fn(meth.proto,
meth.inputs, meth.output));
- auto ann = ast.ann_type(t, none[vec[@ty.t]]);
+ auto ann = triv_ann(t);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_field(base_1,
field,
@@ -2352,7 +2341,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
"non-integral type of vec index: "
+ ty_to_str(idx_t));
}
- auto ann = ast.ann_type(mt.ty, none[vec[@ty.t]]);
+ auto ann = triv_ann(mt.ty);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_index(base_1,
idx_1,
@@ -2366,7 +2355,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
+ ty_to_str(idx_t));
}
auto t = ty.ty_machine(common.ty_u8);
- auto ann = ast.ann_type(plain_ty(t), none[vec[@ty.t]]);
+ auto ann = triv_ann(plain_ty(t));
ret @fold.respan[ast.expr_](expr.span,
ast.expr_index(base_1,
idx_1,
@@ -2384,7 +2373,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
case (ast.expr_port(_)) {
auto t = next_ty_var(fcx.ccx);
auto pt = plain_ty(ty.ty_port(t));
- auto ann = ast.ann_type(pt, none[vec[@ty.t]]);
+ auto ann = triv_ann(pt);
ret @fold.respan[ast.expr_](expr.span, ast.expr_port(ann));
}
@@ -2394,7 +2383,7 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr {
alt (port_t.struct) {
case (ty.ty_port(?subtype)) {
auto ct = plain_ty(ty.ty_chan(subtype));
- auto ann = ast.ann_type(ct, none[vec[@ty.t]]);
+ auto ann = triv_ann(ct);
ret @fold.respan[ast.expr_](expr.span,
ast.expr_chan(expr_1, ann));
}
@@ -2573,7 +2562,7 @@ fn check_item_fn(&@crate_ctxt ccx, &span sp, ast.ident ident, &ast._fn f,
auto output_ty = ast_ty_to_ty_crate(ccx, f.decl.output);
auto fn_sty = ty.ty_fn(f.proto, inputs, output_ty);
- auto fn_ann = ast.ann_type(plain_ty(fn_sty), none[vec[@ty.t]]);
+ auto fn_ann = triv_ann(plain_ty(fn_sty));
auto item = ast.item_fn(ident, f, ty_params, id, fn_ann);
ret @fold.respan[ast.item_](sp, item);
diff --git a/src/comp/middle/typestate_check.rs b/src/comp/middle/typestate_check.rs
new file mode 100644
index 00000000..9b670fc1
--- /dev/null
+++ b/src/comp/middle/typestate_check.rs
@@ -0,0 +1,496 @@
+import front.ast;
+import front.ast.ann;
+import front.ast.ty;
+import front.ast.mutability;
+import front.ast.item;
+import front.ast.block;
+import front.ast.block_;
+import front.ast.block_index_entry;
+import front.ast.decl;
+import front.ast.stmt;
+import front.ast.stmt_;
+import front.ast.stmt_decl;
+import front.ast.stmt_expr;
+import front.ast.decl_local;
+import front.ast.decl_item;
+import front.ast.ident;
+import front.ast.def_id;
+import front.ast.ann;
+import front.ast.init;
+import front.ast.expr;
+import front.ast.expr_call;
+import front.ast.expr_path;
+import front.ast.expr_log;
+import front.ast.path;
+import front.ast.crate_directive;
+import front.ast.fn_decl;
+import front.ast._obj;
+import front.ast.native_mod;
+import front.ast.variant;
+import front.ast.ty_param;
+import front.ast.ty;
+import front.ast.proto;
+import front.ast.pat;
+import front.ast.binop;
+import front.ast.unop;
+import front.ast.def;
+import front.ast.lit;
+import front.ast.init_op;
+import front.ast.initializer;
+import front.ast.local;
+import front.ast._fn;
+import front.ast.ann_none;
+import front.ast.ann_type;
+import front.ast._obj;
+import front.ast._mod;
+
+import middle.fold;
+import middle.fold.respan;
+import driver.session;
+import util.common;
+import util.common.span;
+import util.common.spanned;
+import util.common.new_str_hash;
+import util.typestate_ann;
+import util.typestate_ann.ts_ann;
+import util.typestate_ann.empty_pre_post;
+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.pre_and_post;
+import util.typestate_ann.get_pre;
+import util.typestate_ann.get_post;
+
+import middle.ty;
+import middle.ty.ann_to_type;
+import middle.ty.arg;
+import middle.ty.block_ty;
+import middle.ty.expr_ty;
+import middle.ty.ty_to_str;
+
+import pretty.pprust.print_block;
+import pretty.pprust.print_expr;
+import pretty.pp.mkstate;
+import std.io.stdout;
+import std.io.str_writer;
+import std.io.string_writer;
+import std._vec.map;
+import std._vec;
+import std._vec.len;
+import std._vec.pop;
+import std._vec.push;
+import std._vec.slice;
+import std.option;
+import std.option.t;
+import std.option.some;
+import std.option.none;
+import std.map.hashmap;
+import std.list;
+import std.list.list;
+import std.list.cons;
+import std.list.nil;
+import std.list.foldl;
+import std.list.find;
+
+import util.typestate_ann;
+import util.typestate_ann.difference;
+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];
+
+fn bit_num(ident v, fn_info m) -> uint {
+ ret m.get(v);
+}
+fn num_locals(fn_info m) -> uint {
+ ret m.size();
+}
+
+fn mk_fn_info(_fn f) -> fn_info {
+ ret new_str_hash[uint](); /* FIXME: actually implement this */
+}
+/**********************************************************************/
+fn expr_ann(&expr e) -> ann {
+ alt(e.node) {
+ case (ast.expr_vec(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_tup(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_rec(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_call(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_bind(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_binary(_,_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_unary(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_lit(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_cast(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_if(_,_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_while(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_for(_,_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_for_each(_,_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_do_while(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_alt(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_block(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_assign(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_assign_op(_,_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_send(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_recv(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_field(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_index(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_path(_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_ext(_,_,_,_,?a)) {
+ ret a;
+ }
+ case (ast.expr_fail(?a)) {
+ ret a;
+ }
+ case (ast.expr_ret(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_put(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_be(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_log(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_check_expr(_,?a)) {
+ ret a;
+ }
+ case (ast.expr_port(?a)) {
+ ret a;
+ }
+ case (ast.expr_chan(_,?a)) {
+ ret a;
+ }
+ }
+}
+
+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;
+ }
+ }
+ }
+ }
+}
+
+fn expr_precond(&expr e) -> precond {
+ ret (expr_pp(@e)).precondition;
+}
+
+fn expr_postcond(&@expr e) -> postcond {
+ ret (expr_pp(e)).postcondition;
+}
+
+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)));
+ }
+ }
+}
+
+// Given a list of pres and posts for exprs e0 ... en,
+// return the precondition for evaluating each expr in order.
+// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
+// precondition shouldn't include x.
+fn seq_preconds(uint num_vars, vec[pre_and_post] pps) -> precond {
+ let uint sz = len[pre_and_post](pps);
+
+ if (sz == 0u) {
+ ret true_precond(num_vars);
+ }
+ else {
+ auto first = pps.(0);
+ check (pps_len(first) == num_vars);
+ let precond rest = seq_preconds(num_vars,
+ slice[pre_and_post](pps, 1u, sz));
+ difference(rest, first.postcondition);
+ union(first.precondition, rest);
+ ret (first.precondition);
+ }
+}
+
+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)));
+ ret first;
+}
+
+fn union_postconds(&vec[postcond] pcs) -> postcond {
+ check (len[postcond](pcs) > 0u);
+
+ 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);
+ }
+}
+
+fn find_pre_post_mod(&_mod m) -> _mod {
+ ret m; /* FIXME */
+}
+
+fn find_pre_post_native_mod(&native_mod m) -> native_mod {
+ ret m; /* FIXME */
+}
+
+fn find_pre_post_obj(_obj o) -> _obj {
+ ret o; /* FIXME */
+}
+
+impure fn find_pre_post_item(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);
+ ret (respan(i.span,
+ ast.item_const(id, t, e_pp, di,
+ with_pp(a, @expr_pp(e_pp)))));
+ }
+ case (ast.item_fn(?id, ?f, ?ps, ?di, ?a)) {
+ auto f_pp = find_pre_post_fn(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);
+ 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);
+ ret (respan(i.span,
+ ast.item_native_mod(id, n_pp, di)));
+ }
+ case (ast.item_ty(_,_,_,_,_)) {
+ ret i;
+ }
+ case (ast.item_tag(_,_,_,_)) {
+ ret i;
+ }
+ case (ast.item_obj(?id, ?o, ?ps, ?di, ?a)) {
+ auto o_pp = find_pre_post_obj(o);
+ 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 {
+ auto num_local_vars = num_locals(enclosing);
+
+ fn do_rand_(fn_info enclosing, &@expr e) -> @expr {
+ be find_pre_post_expr(enclosing, *e);
+ }
+
+ auto do_rand = bind do_rand_(enclosing,_);
+
+ alt(e.node) {
+ case(expr_call(?oper, ?rands, ?a)) {
+ auto pp_oper = find_pre_post_expr(enclosing, *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));
+ 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),
+ postcondition=res_postcond);
+ let ann a_res = with_pp(a, 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 res = empty_pre_post(num_local_vars);
+ require_and_preserve(i, *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);
+ ret (@respan(e.span,
+ expr_log(e_pp, with_pp(a, @expr_pp(e_pp)))));
+ }
+ case(_) {
+ log("this sort of expr isn't implemented!");
+ fail;
+ }
+ }
+}
+
+impure fn find_pre_post_for_each_stmt(&fn_info enclosing, &ast.stmt s)
+ -> ast.stmt {
+ auto num_local_vars = num_locals(enclosing);
+
+ alt(s.node) {
+ case(ast.stmt_decl(?adecl)) {
+ alt(adecl.node) {
+ case(ast.decl_local(?alocal)) {
+ alt(alocal.init) {
+ case(some[ast.initializer](?an_init)) {
+ 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 @local res_local =
+ @rec(ty=alocal.ty, infer=alocal.infer,
+ ident=alocal.ident, init=some[initializer](a_i),
+ id=alocal.id, ann=res_ann);
+ let stmt_ res = stmt_decl(@respan(adecl.span,
+ decl_local(res_local)));
+ ret (respan(s.span, res));
+ }
+ case(none[ast.initializer]) {
+ // log("pre/post for init of " + alocal.ident + ": none");
+ let ann res_ann = with_pp(alocal.ann,
+ empty_pre_post(num_local_vars));
+ let @local res_local =
+ @rec(ty=alocal.ty, infer=alocal.infer,
+ ident=alocal.ident, init=none[initializer],
+ id=alocal.id, ann=res_ann);
+ let stmt_ res =
+ stmt_decl
+ (@respan(adecl.span, decl_local(res_local)));
+ ret (respan (s.span, res));
+ }
+ }
+ }
+ case(decl_item(?anitem)) {
+ auto res_item = find_pre_post_item(enclosing, *anitem);
+ ret (respan(s.span, stmt_decl(@respan(adecl.span,
+ decl_item(@res_item)))));
+ }
+ }
+ }
+ case(stmt_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));
+ }
+ auto do_one = bind do_one_(enclosing, _);
+
+ auto ss = _vec.map[@stmt, @stmt](do_one, b.node.stmts);
+ fn do_inner_(fn_info i, &@expr e) -> @expr {
+ ret find_pre_post_expr(i, *e);
+ }
+ auto do_inner = bind do_inner_(enclosing, _);
+ let option.t[@expr] e_ = option.map[@expr, @expr](do_inner, b.node.expr);
+ let block_ b_res = rec(stmts=ss, expr=e_, index=b.node.index);
+ ret respan(b.span, b_res);
+}
+
+fn find_pre_post_fn(&_fn f) -> _fn {
+ let fn_info fi = mk_fn_info(f);
+ ret rec(decl=f.decl, proto=f.proto,
+ body=find_pre_post_block(fi, f.body));
+}
+
+fn check_item_fn(&@() ignore, &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);
+
+ 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[@()]();
+
+ fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
+
+ ret fold.fold_crate[@()](@(), fld, crate);
+}
diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs
index f3b0f3fe..b0d6fb94 100644
--- a/src/comp/pretty/pprust.rs
+++ b/src/comp/pretty/pprust.rs
@@ -611,16 +611,16 @@ impure fn print_expr(ps s, &@ast.expr expr) {
case (ast.expr_path(?path,_,_)) {
print_path(s, path);
}
- case (ast.expr_fail) {
+ case (ast.expr_fail(_)) {
wrd(s.s, "fail");
}
- case (ast.expr_break) {
+ case (ast.expr_break(_)) {
wrd(s.s, "break");
}
- case (ast.expr_cont) {
+ case (ast.expr_cont(_)) {
wrd(s.s, "cont");
}
- case (ast.expr_ret(?result)) {
+ case (ast.expr_ret(?result,_)) {
wrd(s.s, "ret");
alt (result) {
case (option.some[@ast.expr](?expr)) {
@@ -630,7 +630,7 @@ impure fn print_expr(ps s, &@ast.expr expr) {
case (_) {}
}
}
- case (ast.expr_put(?result)) {
+ case (ast.expr_put(?result,_)) {
wrd(s.s, "put");
alt (result) {
case (option.some[@ast.expr](?expr)) {
@@ -640,15 +640,15 @@ impure fn print_expr(ps s, &@ast.expr expr) {
case (_) {}
}
}
- case (ast.expr_be(?result)) {
+ case (ast.expr_be(?result,_)) {
wrd1(s, "be");
print_expr(s, result);
}
- case (ast.expr_log(?expr)) {
+ case (ast.expr_log(?expr,_)) {
wrd1(s, "log");
print_expr(s, expr);
}
- case (ast.expr_check_expr(?expr)) {
+ case (ast.expr_check_expr(?expr,_)) {
wrd1(s, "check");
popen_h(s);
print_expr(s, expr);
diff --git a/src/comp/rustc.rc b/src/comp/rustc.rc
index e15d1842..afa84711 100644
--- a/src/comp/rustc.rc
+++ b/src/comp/rustc.rc
@@ -39,6 +39,7 @@ mod pretty {
mod util {
mod common;
+ mod typestate_ann;
}
auth driver.rustc.main = impure;
@@ -55,8 +56,10 @@ auth middle.trans.copy_any_self_to_alloca = impure;
auth middle.trans.copy_args_to_allocas = impure;
auth middle.trans.trans_block = impure;
auth middle.trans.alloc_ty = impure;
+auth middle.typestate_check.log_expr = impure;
auth lib.llvm = unsafe;
auth pretty.pprust = impure;
+auth middle.typestate_check.find_pre_post_block = impure;
mod lib {
alt (target_os) {
diff --git a/src/comp/util/typestate_ann.rs b/src/comp/util/typestate_ann.rs
new file mode 100644
index 00000000..a4698c5d
--- /dev/null
+++ b/src/comp/util/typestate_ann.rs
@@ -0,0 +1,61 @@
+import front.ast.ident;
+import std._vec;
+import std.bitv;
+
+/*
+ This says: this expression requires the idents in <pre> to be initialized,
+ and given the precondition, it guarantees that the idents in <post> are
+ initialized.
+ */
+type precond = bitv.t; /* 1 means "this variable must be initialized"
+ 0 means "don't care about this variable" */
+type postcond = bitv.t; /* 1 means "this variable is initialized"
+ 0 means "don't know about this variable */
+
+/* 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;
+
+fn true_precond(uint num_vars) -> precond {
+ be bitv.create(num_vars, false);
+}
+
+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),
+ postcondition=true_postcond(num_vars)));
+}
+
+fn get_pre(&pre_and_post p) -> precond {
+ ret p.precondition;
+}
+
+fn get_post(&pre_and_post p) -> postcond {
+ ret p.postcondition;
+}
+
+fn difference(&precond p1, &precond p2) -> bool {
+ be bitv.difference(p1, p2);
+}
+
+fn union(&precond p1, &precond p2) -> bool {
+ be bitv.difference(p1, p2);
+}
+
+fn pps_len(&pre_and_post p) -> uint {
+ // gratuitous check
+ check (p.precondition.nbits == p.postcondition.nbits);
+ ret p.precondition.nbits;
+}
+
+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
diff --git a/src/lib/_vec.rs b/src/lib/_vec.rs
index c3fc7035..f2b169ef 100644
--- a/src/lib/_vec.rs
+++ b/src/lib/_vec.rs
@@ -207,6 +207,29 @@ fn map2[T,U,V](&operator2[T,U,V] f, &vec[mutable? T] v0, &vec[mutable? U] v1)
ret u;
}
+fn find[T](fn (&T) -> bool f, &vec[mutable? T] v) -> option.t[T] {
+ for (T elt in v) {
+ if (f(elt)) {
+ ret some[T](elt);
+ }
+ }
+
+ ret none[T];
+}
+
+fn foldl[T, U](fn (&U, &T) -> U p, &U z, &vec[T] v) -> U {
+ auto sz = len[T](v);
+
+ if (sz == 0u) {
+ ret z;
+ }
+ else {
+ auto rest = slice[T](v, 1u, sz);
+
+ ret (p(foldl[T,U](p, z, rest), v.(0)));
+ }
+}
+
// Local Variables:
// mode: rust;
// fill-column: 78;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 09:16:31 +0000