Add a precondition on vec::zip
vec::zip now has the precondition that the two argument vectors are the same length. Changed uses of it to reflect that. Also added a few vector-enumerating utilities to vec.rs, which necessitated in making some functions in u8 declared-pure.
This commit is contained in:
parent
d37e8cfc67
commit
268533a920
5 changed files with 54 additions and 14 deletions
|
@ -1,26 +1,26 @@
|
|||
|
||||
|
||||
fn add(x: u8, y: u8) -> u8 { ret x + y; }
|
||||
pure fn add(x: u8, y: u8) -> u8 { ret x + y; }
|
||||
|
||||
fn sub(x: u8, y: u8) -> u8 { ret x - y; }
|
||||
pure fn sub(x: u8, y: u8) -> u8 { ret x - y; }
|
||||
|
||||
fn mul(x: u8, y: u8) -> u8 { ret x * y; }
|
||||
pure fn mul(x: u8, y: u8) -> u8 { ret x * y; }
|
||||
|
||||
fn div(x: u8, y: u8) -> u8 { ret x / y; }
|
||||
pure fn div(x: u8, y: u8) -> u8 { ret x / y; }
|
||||
|
||||
fn rem(x: u8, y: u8) -> u8 { ret x % y; }
|
||||
pure fn rem(x: u8, y: u8) -> u8 { ret x % y; }
|
||||
|
||||
fn lt(x: u8, y: u8) -> bool { ret x < y; }
|
||||
pure fn lt(x: u8, y: u8) -> bool { ret x < y; }
|
||||
|
||||
fn le(x: u8, y: u8) -> bool { ret x <= y; }
|
||||
pure fn le(x: u8, y: u8) -> bool { ret x <= y; }
|
||||
|
||||
fn eq(x: u8, y: u8) -> bool { ret x == y; }
|
||||
pure fn eq(x: u8, y: u8) -> bool { ret x == y; }
|
||||
|
||||
fn ne(x: u8, y: u8) -> bool { ret x != y; }
|
||||
pure fn ne(x: u8, y: u8) -> bool { ret x != y; }
|
||||
|
||||
fn ge(x: u8, y: u8) -> bool { ret x >= y; }
|
||||
pure fn ge(x: u8, y: u8) -> bool { ret x >= y; }
|
||||
|
||||
fn gt(x: u8, y: u8) -> bool { ret x > y; }
|
||||
pure fn gt(x: u8, y: u8) -> bool { ret x > y; }
|
||||
|
||||
iter range(lo: u8, hi: u8) -> u8 { while lo < hi { put lo; lo += 1u8; } }
|
||||
// Local Variables:
|
||||
|
|
|
@ -57,12 +57,15 @@ fn init_elt_mut<@T>(t: &T, n_elts: uint) -> [mutable T] {
|
|||
ret v;
|
||||
}
|
||||
|
||||
// FIXME: Possible typestate postcondition:
|
||||
// len(result) == len(v) (needs issue #586)
|
||||
fn to_mut<@T>(v: &[T]) -> [mutable T] {
|
||||
let vres = [mutable];
|
||||
for t: T in v { vres += [mutable t]; }
|
||||
ret vres;
|
||||
}
|
||||
|
||||
// Same comment as from_mut
|
||||
fn from_mut<@T>(v: &[mutable T]) -> [T] {
|
||||
let vres = [];
|
||||
for t: T in v { vres += [t]; }
|
||||
|
@ -253,14 +256,23 @@ fn position_pred<T>(f: fn(&T) -> bool, v: &[T]) -> option::t<uint> {
|
|||
ret none;
|
||||
}
|
||||
|
||||
pure fn same_length<T, U>(xs: &[T], ys: &[U]) -> bool {
|
||||
let xlen = unchecked { vec::len(xs) };
|
||||
let ylen = unchecked { vec::len(ys) };
|
||||
xlen == ylen
|
||||
}
|
||||
|
||||
// FIXME: if issue #586 gets implemented, could have a postcondition
|
||||
// saying the two result lists have the same length -- or, could
|
||||
// return a nominal record with a constraint saying that, instead of
|
||||
// returning a tuple (contingent on issue #869)
|
||||
fn unzip<@T, @U>(v: &[(T, U)]) -> ([T], [U]) {
|
||||
let as = [], bs = [];
|
||||
for (a, b) in v { as += [a]; bs += [b]; }
|
||||
ret (as, bs);
|
||||
}
|
||||
|
||||
// FIXME make the lengths being equal a constraint
|
||||
fn zip<@T, @U>(v: &[T], u: &[U]) -> [(T, U)] {
|
||||
fn zip<@T, @U>(v: &[T], u: &[U]) : same_length(v, u) -> [(T, U)] {
|
||||
let zipped = [];
|
||||
let sz = len(v), i = 0u;
|
||||
assert (sz == len(u));
|
||||
|
@ -293,6 +305,27 @@ fn reversed<@T>(v: &[T]) -> [T] {
|
|||
ret rs;
|
||||
}
|
||||
|
||||
// Generating vecs.
|
||||
fn enum_chars(start:u8, end:u8) : u8::le(start, end) -> [char] {
|
||||
let i = start;
|
||||
let r = [];
|
||||
while (i <= end) {
|
||||
r += [i as char];
|
||||
i += (1u as u8);
|
||||
}
|
||||
ret r;
|
||||
}
|
||||
|
||||
fn enum_uints(start:uint, end:uint) : uint::le(start, end) -> [uint] {
|
||||
let i = start;
|
||||
let r = [];
|
||||
while (i <= end) {
|
||||
r += [i];
|
||||
i += 1u;
|
||||
}
|
||||
ret r;
|
||||
}
|
||||
|
||||
// Iterate over a list with with the indexes
|
||||
iter iter2<@T>(v: &[T]) -> (uint, T) {
|
||||
let i = 0u;
|
||||
|
|
|
@ -49,7 +49,11 @@ fn test_simple() {
|
|||
fn lteq(a: &int, b: &int) -> bool { int::le(a, b) }
|
||||
sort::quick_sort(lteq, names);
|
||||
|
||||
let pairs = vec::zip(expected, vec::from_mut(names));
|
||||
let immut_names = vec::from_mut(names);
|
||||
|
||||
// Silly, but what else can we do?
|
||||
check vec::same_length(expected, immut_names);
|
||||
let pairs = vec::zip(expected, immut_names);
|
||||
for (a, b) in pairs { log #fmt["%d %d", a, b]; assert (a == b); }
|
||||
}
|
||||
|
||||
|
|
|
@ -86,6 +86,7 @@ fn sort_tests() {
|
|||
"test::ignored_tests_result_in_ignored", "test::parse_ignored_flag",
|
||||
"test::sort_tests"];
|
||||
|
||||
check vec::same_length(expected, filtered);
|
||||
let pairs = vec::zip(expected, filtered);
|
||||
|
||||
|
||||
|
|
|
@ -302,6 +302,8 @@ fn test_any_and_all() {
|
|||
fn test_zip_unzip() {
|
||||
let v1 = [1, 2, 3];
|
||||
let v2 = [4, 5, 6];
|
||||
|
||||
check same_length(v1, v2); // Silly, but what else can we do?
|
||||
let z1 = vec::zip(v1, v2);
|
||||
|
||||
assert ((1, 4) == z1[0]);
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue