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.

2 files changed, 46 insertions, 13 deletions

diff --git a/src/lib/u8.rs b/src/lib/u8.rs
index 8a0430884d1..5dea03b0bdd 100644
--- a/src/lib/u8.rs
+++ b/src/lib/u8.rs
@@ -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:
diff --git a/src/lib/vec.rs b/src/lib/vec.rs
index 28c347cd2c8..daa1d499d58 100644
--- a/src/lib/vec.rs
+++ b/src/lib/vec.rs
@@ -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;