nordic-dev.net/rust
nordic-dev.net/rust
2
0
Fork 0
mirror of https://github.com/rust-lang/rust.git synced 2024-11-22 06:44:35 +00:00
Code Issues Packages Projects Releases Wiki Activity

Started adding support for typestate checking.

Browse Source 
I added a new field to the ast "ann" type for typestate information.
Currently, the field contains a record of a precondition bit vector and
postcondition vector, but I tried to structure things so as to make
it easy to change the representation of the typestate annotation type.
I also had to add annotations to some syntactic forms that didn't have
them before (fail, ret, be...), with all the boilerplate changes
that that would imply.

The main call to the typestate_check entry point is commented out and
the actual pre-postcondition algorithm only has a few cases
implemented, though the overall AST traversal is there. The rest of
the typestate algorithm isn't implemented yet.
This commit is contained in:
Tim Chevalier 2011-03-24 12:12:04 -07:00 committed by Graydon Hoare
parent 69a34b992b
commit 3130348ee1
13 changed files with 813 additions and 234 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/comp/driver/rustc.rs
View File

@ -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);
}

21
src/comp/front/ast.rs
View File

@ -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);
}

2
src/comp/front/lexer.rs
View File

@ -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();

36
src/comp/front/parser.rs
View File

@ -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.

98
src/comp/middle/fold.rs
View File

@ -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](_,_,_,_),

23
src/comp/middle/trans.rs
View File

@ -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;

14
src/comp/middle/ty.rs
View File

@ -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;
}

249
src/comp/middle/typeck.rs
View File

@ -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]]));
e_1 = ast.expr_ext(p, args, body, expanded, triv_ann(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; }
/* 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);

496
src/comp/middle/typestate_check.rs Normal file
View File

@ -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);
}

16
src/comp/pretty/pprust.rs
View File

@ -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);

3
src/comp/rustc.rc
View File

@ -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) {

61
src/comp/util/typestate_ann.rs Normal file
View File

@ -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);
}

23
src/lib/_vec.rs
View File

@ -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;