rustc: Flatten annotations
This commit is contained in:
parent
a90df393f9
commit
5047ab0b0c
11 changed files with 307 additions and 589 deletions
|
|
@ -21,20 +21,10 @@ type def_id = tup(crate_num, def_num);
|
|||
type ty_param = ident;
|
||||
|
||||
// Annotations added during successive passes.
|
||||
tag ann {
|
||||
ann_none(uint);
|
||||
ann_type(uint,
|
||||
middle::ty::t,
|
||||
option::t[vec[middle::ty::t]], /* ty param substs */
|
||||
option::t[@ts_ann]); /* pre- and postcondition for typestate */
|
||||
}
|
||||
|
||||
fn ann_tag(&ann a) -> uint {
|
||||
ret alt (a) {
|
||||
case (ann_none(?t)) { t }
|
||||
case (ann_type(?t, _, _, _)) { t }
|
||||
};
|
||||
}
|
||||
type ann = rec(uint id,
|
||||
middle::ty::t ty,
|
||||
option::t[vec[middle::ty::t]] tps,
|
||||
option::t[@ts_ann] ts);
|
||||
|
||||
tag def {
|
||||
def_fn(def_id);
|
||||
|
|
|
|||
|
|
@ -147,7 +147,11 @@ fn new_parser(session::session sess,
|
|||
fn get_chpos() -> uint {ret rdr.get_chpos();}
|
||||
|
||||
fn get_ann() -> ast::ann {
|
||||
auto rv = ast::ann_none(next_ann_var);
|
||||
// TODO: Remove ty, tps, and ts. ty and tps should be unused
|
||||
// by now.
|
||||
auto rv = rec(id=next_ann_var, ty=0u,
|
||||
tps=none[vec[middle::ty::t]],
|
||||
ts=none[@middle::tstate::ann::ts_ann]);
|
||||
next_ann_var += 1u;
|
||||
ret rv;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -193,7 +193,7 @@ fn resolve_names(&@env e, &ast::crate c) {
|
|||
case (ast::expr_path(?p, ?a)) {
|
||||
auto df = lookup_path_strict(*e, *sc, exp.span, p.node.idents,
|
||||
ns_value);
|
||||
e.def_map.insert(ast::ann_tag(a), df);
|
||||
e.def_map.insert(a.id, df);
|
||||
}
|
||||
case (_) {}
|
||||
}
|
||||
|
|
@ -203,7 +203,7 @@ fn resolve_names(&@env e, &ast::crate c) {
|
|||
case (ast::ty_path(?p, ?a)) {
|
||||
auto new_def = lookup_path_strict(*e, *sc, t.span,
|
||||
p.node.idents, ns_type);
|
||||
e.def_map.insert(ast::ann_tag(a), new_def);
|
||||
e.def_map.insert(a.id, new_def);
|
||||
}
|
||||
case (_) {}
|
||||
}
|
||||
|
|
@ -219,7 +219,7 @@ fn resolve_names(&@env e, &ast::crate c) {
|
|||
ns_value);
|
||||
alt (fnd) {
|
||||
case (ast::def_variant(?did, ?vid)) {
|
||||
e.def_map.insert(ast::ann_tag(a), fnd);
|
||||
e.def_map.insert(a.id, fnd);
|
||||
}
|
||||
case (_) {
|
||||
e.sess.span_err(p.span, "not a tag variant: " +
|
||||
|
|
|
|||
|
|
@ -3804,7 +3804,7 @@ fn collect_upvars(&@block_ctxt cx, &ast::block bloc,
|
|||
fn walk_expr(env e, &@ast::expr expr) {
|
||||
alt (expr.node) {
|
||||
case (ast::expr_path(?path, ?ann)) {
|
||||
alt (e.def_map.get(ast::ann_tag(ann))) {
|
||||
alt (e.def_map.get(ann.id)) {
|
||||
case (ast::def_arg(?did)) {
|
||||
vec::push[ast::def_id](e.refs, did);
|
||||
}
|
||||
|
|
@ -4126,7 +4126,7 @@ fn trans_pat_match(&@block_ctxt cx, &@ast::pat pat, ValueRef llval,
|
|||
auto lldiscrim = cx.build.Load(lldiscrimptr);
|
||||
|
||||
auto vdef = ast::variant_def_ids
|
||||
(cx.fcx.lcx.ccx.tcx.def_map.get(ast::ann_tag(ann)));
|
||||
(cx.fcx.lcx.ccx.tcx.def_map.get(ann.id));
|
||||
auto variant_tag = 0;
|
||||
|
||||
auto variants = tag_variants(cx.fcx.lcx.ccx, vdef._0);
|
||||
|
|
@ -4205,7 +4205,7 @@ fn trans_pat_binding(&@block_ctxt cx, &@ast::pat pat,
|
|||
|
||||
// Get the appropriate variant for this tag.
|
||||
auto vdef = ast::variant_def_ids
|
||||
(cx.fcx.lcx.ccx.tcx.def_map.get(ast::ann_tag(ann)));
|
||||
(cx.fcx.lcx.ccx.tcx.def_map.get(ann.id));
|
||||
|
||||
auto lltagptr = cx.build.PointerCast(llval,
|
||||
T_opaque_tag_ptr(cx.fcx.lcx.ccx.tn));
|
||||
|
|
@ -4368,7 +4368,7 @@ fn lookup_discriminant(&@local_ctxt lcx, &ast::def_id tid, &ast::def_id vid)
|
|||
}
|
||||
|
||||
fn trans_path(&@block_ctxt cx, &ast::path p, &ast::ann ann) -> lval_result {
|
||||
alt (cx.fcx.lcx.ccx.tcx.def_map.get(ast::ann_tag(ann))) {
|
||||
alt (cx.fcx.lcx.ccx.tcx.def_map.get(ann.id)) {
|
||||
case (ast::def_arg(?did)) {
|
||||
alt (cx.fcx.llargs.find(did)) {
|
||||
case (none[ValueRef]) {
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ import std::option::some;
|
|||
import std::option::maybe;
|
||||
|
||||
import front::ast;
|
||||
import front::ast::ann_tag;
|
||||
import front::ast::def;
|
||||
import front::ast::def_fn;
|
||||
import front::ast::_fn;
|
||||
|
|
@ -17,8 +16,6 @@ import front::ast::expr_path;
|
|||
import front::ast::ident;
|
||||
import front::ast::controlflow;
|
||||
import front::ast::ann;
|
||||
import front::ast::ann_none;
|
||||
import front::ast::ann_type;
|
||||
import front::ast::ts_ann;
|
||||
import front::ast::stmt;
|
||||
import front::ast::expr;
|
||||
|
|
@ -188,27 +185,15 @@ fn ann_to_ts_ann(ann a, uint nv) -> @ts_ann {
|
|||
}
|
||||
|
||||
|
||||
fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
log("ann_to_ts_ann_fail: didn't expect ann_none here");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_,_,_,?ty)) {
|
||||
ret ty;
|
||||
}
|
||||
}
|
||||
}
|
||||
fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] { ret a.ts; }
|
||||
|
||||
fn ann_to_ts_ann_strict(ann a) -> @ts_ann {
|
||||
alt (ann_to_ts_ann_fail(a)) {
|
||||
case (none[@ts_ann]) {
|
||||
log("ann_to_ts_ann_fail: didn't expect ann_none here");
|
||||
case (none[@ts_ann]) {
|
||||
log("ann_to_ts_ann_strict: didn't expect none here");
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?t)) {
|
||||
ret t;
|
||||
}
|
||||
case (some[@ts_ann](?t)) { ret t; }
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -320,18 +305,9 @@ fn block_poststate(&block b) -> poststate {
|
|||
|
||||
/* returns a new annotation where the pre_and_post is p */
|
||||
fn with_pp(ann a, pre_and_post p) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
log("with_pp: the impossible happened");
|
||||
fail; /* shouldn't happen b/c code is typechecked */
|
||||
}
|
||||
case (ann_type(?i, ?t, ?ps, _)) {
|
||||
ret (ann_type(i, t, ps,
|
||||
some[@ts_ann]
|
||||
(@rec(conditions=p,
|
||||
states=empty_states(pps_len(p))))));
|
||||
}
|
||||
}
|
||||
ret rec(id=a.id, ty=a.ty, tps=a.tps,
|
||||
ts=some[@ts_ann](@rec(conditions=p,
|
||||
states=empty_states(pps_len(p)))));
|
||||
}
|
||||
|
||||
fn set_prestate_ann(&ann a, &prestate pre) -> bool {
|
||||
|
|
@ -379,50 +355,22 @@ fn fixed_point_states(&fn_ctxt fcx,
|
|||
}
|
||||
|
||||
fn init_ann(&fn_info fi, &ann a) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
// log("init_ann: shouldn't see ann_none");
|
||||
// fail;
|
||||
log("warning: init_ann: saw ann_none");
|
||||
ret a; // Would be better to fail so we can catch bugs that
|
||||
// result in an uninitialized ann -- but don't want to have to
|
||||
// write code to handle native_mods properly
|
||||
}
|
||||
case (ann_type(?i, ?t, ?ps, _)) {
|
||||
ret ann_type(i, t, ps, some[@ts_ann](@empty_ann(num_locals(fi))));
|
||||
}
|
||||
}
|
||||
ret rec(id=a.id, ty=a.ty, tps=a.tps,
|
||||
ts=some[@ts_ann](@empty_ann(num_locals(fi))));
|
||||
}
|
||||
|
||||
fn init_blank_ann(&() ignore, &ann a) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
// log("init_blank_ann: shouldn't see ann_none");
|
||||
//fail;
|
||||
log("warning: init_blank_ann: saw ann_none");
|
||||
ret a;
|
||||
}
|
||||
case (ann_type(?i, ?t, ?ps,_)) {
|
||||
ret ann_type(i, t, ps, some[@ts_ann](@empty_ann(0u)));
|
||||
}
|
||||
}
|
||||
ret rec(id=a.id, ty=a.ty, tps=a.tps, ts=some[@ts_ann](@empty_ann(0u)));
|
||||
}
|
||||
|
||||
fn init_block(&fn_info fi, &span sp, &block_ b) -> block {
|
||||
log("init_block:");
|
||||
log_block(respan(sp, b));
|
||||
alt(b.a) {
|
||||
case (ann_none(_)) {
|
||||
log("init_block: shouldn't see ann_none");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _, _, _)) {
|
||||
auto fld0 = new_identity_fold[fn_info]();
|
||||
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
|
||||
ret fold_block[fn_info](fi, fld0, respan(sp, b));
|
||||
}
|
||||
}
|
||||
auto fld0 = new_identity_fold[fn_info]();
|
||||
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
|
||||
ret fold_block[fn_info](fi, fld0, respan(sp, b));
|
||||
}
|
||||
|
||||
fn num_locals(fn_info m) -> uint {
|
||||
|
|
@ -445,7 +393,7 @@ fn controlflow_def_id(&crate_ctxt ccx, &def_id d) -> controlflow {
|
|||
There's no case for fail b/c we assume e is the callee and it
|
||||
seems unlikely that one would apply "fail" to arguments. */
|
||||
fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
|
||||
auto f = ann_tag(expr_ann(e));
|
||||
auto f = expr_ann(e).id;
|
||||
alt (ccx.tcx.def_map.find(f)) {
|
||||
case (some[def](def_fn(?d))) { ret controlflow_def_id(ccx, d); }
|
||||
case (some[def](def_obj_field(?d))) { ret controlflow_def_id(ccx, d); }
|
||||
|
|
@ -454,11 +402,9 @@ fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
|
|||
}
|
||||
|
||||
fn ann_to_def_strict(&crate_ctxt ccx, &ann a) -> def {
|
||||
alt (ccx.tcx.def_map.find(ann_tag(a))) {
|
||||
alt (ccx.tcx.def_map.find(a.id)) {
|
||||
case (none[def]) {
|
||||
log_err("ann_to_def: node_id " +
|
||||
uistr(ann_tag(a)) +
|
||||
" has no def");
|
||||
log_err("ann_to_def: node_id " + uistr(a.id) + " has no def");
|
||||
fail;
|
||||
}
|
||||
case (some[def](?d)) { ret d; }
|
||||
|
|
@ -466,7 +412,7 @@ fn ann_to_def_strict(&crate_ctxt ccx, &ann a) -> def {
|
|||
}
|
||||
|
||||
fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] {
|
||||
ret ccx.tcx.def_map.find(ann_tag(a));
|
||||
ret ccx.tcx.def_map.find(a.id);
|
||||
}
|
||||
|
||||
//
|
||||
|
|
|
|||
|
|
@ -80,8 +80,6 @@ import front::ast::controlflow;
|
|||
import front::ast::return;
|
||||
import front::ast::noreturn;
|
||||
import front::ast::_fn;
|
||||
import front::ast::ann_none;
|
||||
import front::ast::ann_type;
|
||||
import front::ast::_obj;
|
||||
import front::ast::_mod;
|
||||
import front::ast::crate;
|
||||
|
|
|
|||
|
|
@ -92,8 +92,6 @@ import front::ast::init_op;
|
|||
import front::ast::controlflow;
|
||||
import front::ast::return;
|
||||
import front::ast::noreturn;
|
||||
import front::ast::ann_none;
|
||||
import front::ast::ann_type;
|
||||
import front::ast::_obj;
|
||||
import front::ast::_mod;
|
||||
import front::ast::crate;
|
||||
|
|
@ -243,7 +241,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
|
|||
/*
|
||||
log_err("states:");
|
||||
log_expr_err(*e);
|
||||
log_err(ast.ann_tag(middle.ty.expr_ann(e)));
|
||||
log_err(middle::ty::expr_ann(e).id);
|
||||
*/
|
||||
|
||||
/* FIXME could get rid of some of the copy/paste */
|
||||
|
|
|
|||
|
|
@ -1452,7 +1452,7 @@ fn eq_ty(&t a, &t b) -> bool { ret a == b; }
|
|||
|
||||
fn ann_to_ty_param_substs_opt_and_ty(&node_type_table ntt, &ast::ann ann)
|
||||
-> ty_param_substs_opt_and_ty {
|
||||
alt (ntt.(ast::ann_tag(ann))) {
|
||||
alt (ntt.(ann.id)) {
|
||||
case (none[ty::ty_param_substs_opt_and_ty]) {
|
||||
log_err "ann_to_ty_param_substs_opt_and_ty() called on an " +
|
||||
"untyped node";
|
||||
|
|
@ -1495,19 +1495,25 @@ fn ann_to_monotype(ctxt cx, &node_type_table ntt, ast::ann a) -> t {
|
|||
}
|
||||
|
||||
|
||||
// Turns a type into an ann_type, using defaults for other fields.
|
||||
// Turns a type and optional type parameters into an annotation, using
|
||||
// defaults for other fields.
|
||||
fn mk_ann_type(uint node_id, t typ, option::t[vec[t]] tps) -> ast::ann {
|
||||
ret rec(id=node_id, ty=typ, tps=tps, ts=none[@ts_ann]);
|
||||
}
|
||||
|
||||
// Turns a type into an annotation, using defaults for other fields.
|
||||
fn triv_ann(uint node_id, t typ) -> ast::ann {
|
||||
ret ast::ann_type(node_id, typ, none[vec[t]], none[@ts_ann]);
|
||||
ret mk_ann_type(node_id, typ, none[vec[t]]);
|
||||
}
|
||||
|
||||
// Creates a nil type annotation.
|
||||
fn plain_ann(uint node_id, ctxt tcx) -> ast::ann {
|
||||
ret ast::ann_type(node_id, mk_nil(tcx), none[vec[t]], none[@ts_ann]);
|
||||
ret triv_ann(node_id, mk_nil(tcx));
|
||||
}
|
||||
|
||||
// Creates a _|_ type annotation.
|
||||
fn bot_ann(uint node_id, ctxt tcx) -> ast::ann {
|
||||
ret ast::ann_type(node_id, mk_bot(tcx), none[vec[t]], none[@ts_ann]);
|
||||
ret triv_ann(node_id, mk_bot(tcx));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -77,8 +77,6 @@ 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 front::ast::crate;
|
||||
|
|
@ -389,42 +387,19 @@ fn mk_f_to_fn_info(@ast::crate c) -> fn_info_map {
|
|||
}
|
||||
/**** Helpers ****/
|
||||
fn ann_to_ts_ann(ann a, uint nv) -> ts_ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) { ret empty_ann(nv); }
|
||||
case (ann_type(_,_,_,?t)) {
|
||||
alt (t) {
|
||||
alt (a.ts) {
|
||||
/* Kind of inconsistent. empty_ann()s everywhere
|
||||
or an option of a ts_ann? */
|
||||
or an option of a ts_ann? */
|
||||
case (none[@ts_ann]) { ret empty_ann(nv); }
|
||||
case (some[@ts_ann](?t)) { ret *t; }
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
log("ann_to_ts_ann_fail: didn't expect ann_none here");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_,_,_,?t)) {
|
||||
ret t;
|
||||
}
|
||||
}
|
||||
}
|
||||
fn ann_to_ts_ann_fail(ann a) -> option::t[@ts_ann] { ret a.ts; }
|
||||
|
||||
fn ann_to_ts_ann_fail_more(ann a) -> @ts_ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
log("ann_to_ts_ann_fail: didn't expect ann_none here");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_,_,_,?t)) {
|
||||
assert (! is_none[@ts_ann](t));
|
||||
ret get[@ts_ann](t);
|
||||
}
|
||||
}
|
||||
assert (! is_none[@ts_ann](a.ts));
|
||||
ret get[@ts_ann](a.ts);
|
||||
}
|
||||
|
||||
fn ann_to_poststate(ann a) -> poststate {
|
||||
|
|
@ -447,44 +422,24 @@ fn stmt_to_ann(&stmt s) -> option::t[@ts_ann] {
|
|||
|
||||
/* fails if e has no annotation */
|
||||
fn expr_states(@expr e) -> pre_and_post_state {
|
||||
alt (expr_ann(e)) {
|
||||
case (ann_none(_)) {
|
||||
log_err "expr_pp: the impossible happened (no annotation)";
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _, _, ?maybe_pp)) {
|
||||
alt (maybe_pp) {
|
||||
alt (a.ts) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err "expr_pp: the impossible happened (no pre/post)";
|
||||
fail;
|
||||
log_err "expr_pp: the impossible happened (no pre/post)";
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?p)) {
|
||||
ret p.states;
|
||||
}
|
||||
}
|
||||
case (some[@ts_ann](?p)) { ret p.states; }
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* fails if e has no annotation */
|
||||
fn expr_pp(@expr e) -> pre_and_post {
|
||||
alt (expr_ann(e)) {
|
||||
case (ann_none(_)) {
|
||||
log_err "expr_pp: the impossible happened (no annotation)";
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _, _, ?maybe_pp)) {
|
||||
alt (maybe_pp) {
|
||||
alt (expr_ann(e).ts) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err "expr_pp: the impossible happened (no pre/post)";
|
||||
fail;
|
||||
log_err "expr_pp: the impossible happened (no pre/post)";
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?p)) {
|
||||
ret p.conditions;
|
||||
}
|
||||
}
|
||||
case (some[@ts_ann](?p)) { ret p.conditions; }
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn stmt_pp(&stmt s) -> pre_and_post {
|
||||
|
|
@ -502,42 +457,22 @@ fn stmt_pp(&stmt s) -> pre_and_post {
|
|||
/* fails if b has no annotation */
|
||||
/* FIXME: factor out code in the following two functions (block_ts_ann) */
|
||||
fn block_pp(&block b) -> pre_and_post {
|
||||
alt (b.node.a) {
|
||||
case (ann_none(_)) {
|
||||
log_err "block_pp: the impossible happened (no ann)";
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _,_,?t)) {
|
||||
alt (t) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err "block_pp: the impossible happened (no ty)";
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?ts)) {
|
||||
ret ts.conditions;
|
||||
}
|
||||
}
|
||||
}
|
||||
alt (b.node.a.ts) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err "block_pp: the impossible happened (no ty)";
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?ts)) { ret ts.conditions; }
|
||||
}
|
||||
}
|
||||
|
||||
fn block_states(&block b) -> pre_and_post_state {
|
||||
alt (b.node.a) {
|
||||
case (ann_none(_)) {
|
||||
log_err "block_pp: the impossible happened (no ann)";
|
||||
alt (b.node.a.ts) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err "block_states: the impossible happened (no ty)";
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _,_,?t)) {
|
||||
alt (t) {
|
||||
case (none[@ts_ann]) {
|
||||
log_err "block_states: the impossible happened (no ty)";
|
||||
fail;
|
||||
}
|
||||
case (some[@ts_ann](?ts)) {
|
||||
ret ts.states;
|
||||
}
|
||||
}
|
||||
}
|
||||
case (some[@ts_ann](?ts)) { ret ts.states; }
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -602,18 +537,9 @@ fn block_poststate(&block b) -> poststate {
|
|||
|
||||
/* returns a new annotation where the pre_and_post is p */
|
||||
fn with_pp(ann a, pre_and_post p) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
log("with_pp: the impossible happened");
|
||||
fail; /* shouldn't happen b/c code is typechecked */
|
||||
}
|
||||
case (ann_type(?tg, ?t, ?ps, _)) {
|
||||
ret (ann_type(tg, t, ps,
|
||||
some[@ts_ann]
|
||||
(@rec(conditions=p,
|
||||
states=empty_states(pps_len(p))))));
|
||||
}
|
||||
}
|
||||
ret rec(id=ann.id, ty=ann.ty, tps=ann.tps,
|
||||
ts=some[@ts_ann](@rec(conditions=p,
|
||||
states=empty_states(pps_len(p)))));
|
||||
}
|
||||
|
||||
// Given a list of pres and posts for exprs e0 ... en,
|
||||
|
|
@ -834,7 +760,7 @@ fn find_pre_post_expr(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
|||
case (expr_path(?p, ?a)) {
|
||||
auto res = empty_pre_post(num_local_vars);
|
||||
|
||||
alt (dm.get(ast::ann_tag(a))) {
|
||||
alt (dm.get(a.id)) {
|
||||
case (def_local(?d_id)) {
|
||||
auto i = bit_num(d_id, enclosing);
|
||||
require_and_preserve(i, res);
|
||||
|
|
@ -881,7 +807,7 @@ fn find_pre_post_expr(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
|||
case (expr_assign(?lhs, ?rhs, ?a)) {
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
alt (dm.get(ast::ann_tag(a_lhs))) {
|
||||
alt (dm.get(a_lhs.id))) {
|
||||
case (def_local(?d_id)) {
|
||||
find_pre_post_expr(dm, fm, enclosing, rhs);
|
||||
set_pre_and_post(a, expr_pp(rhs));
|
||||
|
|
@ -902,7 +828,7 @@ fn find_pre_post_expr(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
|||
case (expr_recv(?lhs, ?rhs, ?a)) {
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
alt (dm.get(ast::ann_tag(a_lhs))) {
|
||||
alt (dm.get(a_lhs.id)) {
|
||||
case (def_local(?d_id)) {
|
||||
find_pre_post_expr(dm, fm, enclosing, rhs);
|
||||
set_pre_and_post(a, expr_pp(rhs));
|
||||
|
|
@ -1291,76 +1217,36 @@ fn find_pre_post_state_item(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
|||
}
|
||||
|
||||
fn set_prestate_ann(@ann a, prestate pre) -> bool {
|
||||
alt (*a) {
|
||||
case (ann_type(_, _,_,?ts_a)) {
|
||||
assert (! is_none[@ts_ann](ts_a));
|
||||
ret set_prestate(get[@ts_ann](ts_a), pre);
|
||||
}
|
||||
case (ann_none(_)) {
|
||||
log("set_prestate_ann: expected an ann_type here");
|
||||
fail;
|
||||
}
|
||||
}
|
||||
assert (! is_none[@ts_ann](a.ts));
|
||||
ret set_prestate(get[@ts_ann](a.ts), pre);
|
||||
}
|
||||
|
||||
|
||||
fn extend_prestate_ann(ann a, prestate pre) -> bool {
|
||||
alt (a) {
|
||||
case (ann_type(_,_,_,?ts_a)) {
|
||||
assert (! is_none[@ts_ann](ts_a));
|
||||
ret extend_prestate((get[@ts_ann](ts_a)).states.prestate, pre);
|
||||
}
|
||||
case (ann_none(_)) {
|
||||
log("set_prestate_ann: expected an ann_type here");
|
||||
fail;
|
||||
}
|
||||
}
|
||||
assert (! is_none[@ts_ann](a.ts));
|
||||
ret extend_prestate((get[@ts_ann](a.ts)).states.prestate, pre);
|
||||
}
|
||||
|
||||
fn set_poststate_ann(ann a, poststate post) -> bool {
|
||||
alt (a) {
|
||||
case (ann_type(_, _,_,?ts_a)) {
|
||||
assert (! is_none[@ts_ann](ts_a));
|
||||
ret set_poststate(get[@ts_ann](ts_a), post);
|
||||
}
|
||||
case (ann_none(_)) {
|
||||
log("set_poststate_ann: expected an ann_type here");
|
||||
fail;
|
||||
}
|
||||
}
|
||||
assert (! is_none[@ts_ann](a.ts));
|
||||
ret set_poststate(get[@ts_ann](a.ts), post);
|
||||
}
|
||||
|
||||
fn extend_poststate_ann(ann a, poststate post) -> bool {
|
||||
alt (a) {
|
||||
case (ann_type(_, _,_,?ts_a)) {
|
||||
assert (! is_none[@ts_ann](ts_a));
|
||||
ret extend_poststate((*get[@ts_ann](ts_a)).states.poststate, post);
|
||||
}
|
||||
case (ann_none(_)) {
|
||||
log("set_poststate_ann: expected an ann_type here");
|
||||
fail;
|
||||
}
|
||||
}
|
||||
assert (! is_none[@ts_ann](a.ts));
|
||||
ret extend_poststate((*get[@ts_ann](a.ts)).states.poststate, post);
|
||||
}
|
||||
|
||||
fn set_pre_and_post(&ann a, pre_and_post pp) -> () {
|
||||
alt (a) {
|
||||
case (ann_type(_, _,_,?ts_a)) {
|
||||
assert (! is_none[@ts_ann](ts_a));
|
||||
auto t = *get[@ts_ann](ts_a);
|
||||
/* log("set_pre_and_post, old =");
|
||||
log_pp(t.conditions);
|
||||
log("new =");
|
||||
log_pp(pp);
|
||||
*/
|
||||
set_precondition(t, pp.precondition);
|
||||
set_postcondition(t, pp.postcondition);
|
||||
}
|
||||
case (ann_none(_)) {
|
||||
log_err("set_pre_and_post: expected an ann_type here");
|
||||
fail;
|
||||
}
|
||||
}
|
||||
assert (! is_none[@ts_ann](a.ts));
|
||||
auto t = *get[@ts_ann](a.ts);
|
||||
/* log("set_pre_and_post, old =");
|
||||
log_pp(t.conditions);
|
||||
log("new =");
|
||||
log_pp(pp);
|
||||
*/
|
||||
set_precondition(t, pp.precondition);
|
||||
set_postcondition(t, pp.postcondition);
|
||||
}
|
||||
|
||||
fn seq_states(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
||||
|
|
@ -1518,7 +1404,7 @@ fn find_pre_post_state_expr(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
|||
|
||||
alt (lhs.node) {
|
||||
case (expr_path(_, ?a_lhs)) {
|
||||
alt (dm.get(ast::ann_tag(a_lhs))) {
|
||||
alt (dm.get(a_lhs.id)) {
|
||||
case (def_local(?d_id)) {
|
||||
// assignment to local var
|
||||
changed = pure_exp(a_lhs, pres) || changed;
|
||||
|
|
@ -1546,7 +1432,7 @@ fn find_pre_post_state_expr(&def_map dm, &fn_info_map fm, &fn_info enclosing,
|
|||
|
||||
alt (lhs.node) {
|
||||
case (expr_path(?p, ?a_lhs)) {
|
||||
alt (dm.get(ast::ann_tag(a_lhs))) {
|
||||
alt (dm.get(a_lhs.id)) {
|
||||
case (def_local(?d_id)) {
|
||||
// receive to local var
|
||||
changed = pure_exp(a_lhs, pres) || changed;
|
||||
|
|
@ -2040,52 +1926,22 @@ fn check_obj_state(def_map dm, &fn_info_map f_info_map,
|
|||
}
|
||||
|
||||
fn init_ann(&fn_info fi, &ann a) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
// log("init_ann: shouldn't see ann_none");
|
||||
// fail;
|
||||
log("warning: init_ann: saw ann_none");
|
||||
ret a; // Would be better to fail so we can catch bugs that
|
||||
// result in an uninitialized ann -- but don't want to have to
|
||||
// write code to handle native_mods properly
|
||||
}
|
||||
case (ann_type(?tg, ?t,?ps,_)) {
|
||||
ret ann_type(tg, t, ps,
|
||||
some[@ts_ann](@empty_ann(num_locals(fi))));
|
||||
}
|
||||
}
|
||||
ret rec(id=a.id, ty=a.ty, tps=a.tps,
|
||||
ts=some[@ts_ann](@empty_ann(num_locals(fi))));
|
||||
}
|
||||
|
||||
fn init_blank_ann(&() ignore, &ann a) -> ann {
|
||||
alt (a) {
|
||||
case (ann_none(_)) {
|
||||
// log("init_blank_ann: shouldn't see ann_none");
|
||||
//fail;
|
||||
log("warning: init_blank_ann: saw ann_none");
|
||||
ret a;
|
||||
}
|
||||
case (ann_type(?tg, ?t,?ps,_)) {
|
||||
ret ann_type(tg, t, ps, some[@ts_ann](@empty_ann(0u)));
|
||||
}
|
||||
}
|
||||
ret rec(id=a.id, ty=a.ty, tps=a.tps, ts=some[@ts_ann](@empty_ann(0u)));
|
||||
}
|
||||
|
||||
fn init_block(&fn_info fi, &span sp, &block_ b) -> block {
|
||||
log("init_block:");
|
||||
log_block(respan(sp, b));
|
||||
alt(b.a) {
|
||||
case (ann_none(_)) {
|
||||
log("init_block: shouldn't see ann_none");
|
||||
fail;
|
||||
}
|
||||
case (ann_type(_, _, ?ps, _)) {
|
||||
auto fld0 = fold::new_identity_fold[fn_info]();
|
||||
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
|
||||
ret fold::fold_block[fn_info](fi, fld0, respan(sp, b));
|
||||
}
|
||||
}
|
||||
|
||||
auto fld0 = fold::new_identity_fold[fn_info]();
|
||||
|
||||
fld0 = @rec(fold_ann = bind init_ann(_,_) with *fld0);
|
||||
ret fold::fold_block[fn_info](fi, fld0, respan(sp, b));
|
||||
}
|
||||
|
||||
fn item_fn_anns(&fn_info_map fm, &span sp, ident i, &ast::_fn f,
|
||||
|
|
|
|||
|
|
@ -175,17 +175,6 @@ fn log_block_err(&ast::block b) -> () {
|
|||
log_err(block_to_str(b));
|
||||
}
|
||||
|
||||
fn log_ann(&ast::ann a) -> () {
|
||||
alt (a) {
|
||||
case (ast::ann_none(_)) {
|
||||
log("ann_none");
|
||||
}
|
||||
case (ast::ann_type(_,_,_,_)) {
|
||||
log("ann_type");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn fun_to_str(&ast::_fn f, str name, vec[ast::ty_param] params) -> str {
|
||||
let str_writer s = string_writer();
|
||||
auto out_ = mkstate(s.get_writer(), 80u);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue