Remove effect system from src.

This commit is contained in:
Graydon Hoare 2011-04-19 13:35:49 -07:00
parent d9d5eb82a7
commit d2bd07dcb0
83 changed files with 507 additions and 1037 deletions

View file

@ -85,20 +85,20 @@ fn pps_len(&pre_and_post p) -> uint {
ret p.precondition.nbits;
}
impure fn require_and_preserve(uint i, &pre_and_post p) -> () {
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, true);
}
impure fn set_in_postcond(uint i, &pre_and_post p) -> bool {
fn set_in_postcond(uint i, &pre_and_post p) -> bool {
// sets the ith bit in p's post
auto was_set = bitv.get(p.postcondition, i);
bitv.set(p.postcondition, i, true);
ret !was_set;
}
impure fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
// sets the ith bit in p's post
auto was_set = bitv.get(s.poststate, i);
bitv.set(s.poststate, i, true);
@ -107,35 +107,35 @@ impure fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
// Sets all the bits in a's precondition to equal the
// corresponding bit in p's precondition.
impure fn set_precondition(&ts_ann a, &precond p) -> () {
fn set_precondition(&ts_ann a, &precond p) -> () {
bitv.copy(a.conditions.precondition, p);
}
// Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition.
impure fn set_postcondition(&ts_ann a, &postcond p) -> () {
fn set_postcondition(&ts_ann a, &postcond p) -> () {
bitv.copy(a.conditions.postcondition, p);
}
// Sets all the bits in a's prestate to equal the
// corresponding bit in p's prestate.
impure fn set_prestate(&ts_ann a, &prestate p) -> bool {
fn set_prestate(&ts_ann a, &prestate p) -> bool {
ret bitv.copy(a.states.prestate, p);
}
// Sets all the bits in a's postcondition to equal the
// corresponding bit in p's postcondition.
impure fn set_poststate(&ts_ann a, &poststate p) -> bool {
fn set_poststate(&ts_ann a, &poststate p) -> bool {
ret bitv.copy(a.states.poststate, p);
}
// Set all the bits in p that are set in new
impure fn extend_prestate(&prestate p, &poststate new) -> bool {
fn extend_prestate(&prestate p, &poststate new) -> bool {
ret bitv.union(p, new);
}
// Set all the bits in p that are set in new
impure fn extend_poststate(&poststate p, &poststate new) -> bool {
fn extend_poststate(&poststate p, &poststate new) -> bool {
ret bitv.union(p, new);
}
@ -150,7 +150,7 @@ fn ann_prestate(&ts_ann a) -> prestate {
// returns true if a implies b
// that is, returns true except if for some bits c and d,
// c = 1 and d = 0
impure fn implies(bitv.t a, bitv.t b) -> bool {
fn implies(bitv.t a, bitv.t b) -> bool {
auto tmp = bitv.clone(b);
bitv.difference(tmp, a);
ret bitv.is_false(tmp);