rustc: Use fewer boxes in typestate
This commit is contained in:
parent
57f399bd63
commit
89aa28289b
@ -31,7 +31,7 @@ type poststate = t;
|
||||
*/
|
||||
|
||||
/* named thus so as not to confuse with prestate and poststate */
|
||||
type pre_and_post = @{precondition: precond, postcondition: postcond};
|
||||
type pre_and_post = {precondition: precond, postcondition: postcond};
|
||||
|
||||
|
||||
/* FIXME: once it's implemented: */
|
||||
@ -39,7 +39,7 @@ type pre_and_post = @{precondition: precond, postcondition: postcond};
|
||||
// : ((*.precondition).nbits == (*.postcondition).nbits);
|
||||
type pre_and_post_state = {prestate: prestate, poststate: poststate};
|
||||
|
||||
type ts_ann = @{conditions: pre_and_post, states: pre_and_post_state};
|
||||
type ts_ann = {conditions: pre_and_post, states: pre_and_post_state};
|
||||
|
||||
fn true_precond(num_vars: uint) -> precond { ret create_tritv(num_vars); }
|
||||
|
||||
@ -58,8 +58,8 @@ fn false_postcond(num_vars: uint) -> postcond {
|
||||
}
|
||||
|
||||
fn empty_pre_post(num_vars: uint) -> pre_and_post {
|
||||
ret @{precondition: empty_prestate(num_vars),
|
||||
postcondition: empty_poststate(num_vars)};
|
||||
ret {precondition: empty_prestate(num_vars),
|
||||
postcondition: empty_poststate(num_vars)};
|
||||
}
|
||||
|
||||
fn empty_states(num_vars: uint) -> pre_and_post_state {
|
||||
@ -68,8 +68,8 @@ fn empty_states(num_vars: uint) -> pre_and_post_state {
|
||||
}
|
||||
|
||||
fn empty_ann(num_vars: uint) -> ts_ann {
|
||||
ret @{conditions: empty_pre_post(num_vars),
|
||||
states: empty_states(num_vars)};
|
||||
ret {conditions: empty_pre_post(num_vars),
|
||||
states: empty_states(num_vars)};
|
||||
}
|
||||
|
||||
fn get_pre(&&p: pre_and_post) -> precond { ret p.precondition; }
|
||||
@ -224,8 +224,8 @@ fn ann_prestate(a: ts_ann) -> prestate { ret a.states.prestate; }
|
||||
fn ann_poststate(a: ts_ann) -> poststate { ret a.states.poststate; }
|
||||
|
||||
fn pp_clone(p: pre_and_post) -> pre_and_post {
|
||||
ret @{precondition: clone(p.precondition),
|
||||
postcondition: clone(p.postcondition)};
|
||||
ret {precondition: clone(p.precondition),
|
||||
postcondition: clone(p.postcondition)};
|
||||
}
|
||||
|
||||
fn clone(p: prestate) -> prestate { ret tritv_clone(p); }
|
||||
|
@ -80,8 +80,8 @@ fn seq_preconds(fcx: fn_ctxt, pps: [pre_and_post]) -> precond {
|
||||
let next_first_post = clone(first.postcondition);
|
||||
seq_tritv(next_first_post, second.postcondition);
|
||||
idx += 1u;
|
||||
first = @{precondition: next_first,
|
||||
postcondition: next_first_post};
|
||||
first = {precondition: next_first,
|
||||
postcondition: next_first_post};
|
||||
} else { ret first.precondition; }
|
||||
}
|
||||
}
|
||||
|
@ -413,8 +413,8 @@ fn find_pre_post_expr(fcx: fn_ctxt, e: @expr) {
|
||||
}
|
||||
let antec_pp = pp_clone(expr_pp(fcx.ccx, ex));
|
||||
let e_pp =
|
||||
@{precondition: empty_prestate(num_local_vars),
|
||||
postcondition: false_postcond(num_local_vars)};
|
||||
{precondition: empty_prestate(num_local_vars),
|
||||
postcondition: false_postcond(num_local_vars)};
|
||||
let g = bind combine_pp(antec_pp, fcx, _, _);
|
||||
let alts_overall_pp =
|
||||
vec::foldl(e_pp, alt_pps, g);
|
||||
|
Loading…
x
Reference in New Issue
Block a user