original.name="Template_Valid_29"
======
>>> main.whiley
// test case from std::collection
public type uint is (int i) where i >= 0

property equals<T>(T[] lhs, T[] rhs, uint n) -> (bool r):
    return n <= |lhs| && n <= |rhs| &&
           all { k in 0..n | lhs[k] == rhs[k] }

public type Vector<T> is {
    T[] items,
    uint length
} where length <= |items|

function add<T>(Vector<T> vec, T item) -> (Vector<T> nvec)
// Length increases by exactly one
ensures nvec.length == (vec.length+1)
// All existing items unchanged
ensures equals(vec.items,nvec.items,vec.length)
// Item was added
ensures nvec.items[vec.length] == item:
    //
    if vec.length == |vec.items|:
        // vec is full so must resize
        uint nlen = (vec.length*2)+1
        // double size of internal array
        T[] nitems = [item; nlen]
        uint i = 0
        // copy items
        while i < vec.length && nlen > |vec.items|
        where |nitems| == nlen
        where equals(vec.items,nitems,i)
        where nitems[vec.length] == item:
           nitems[i] = vec.items[i]
           i = i + 1
        //
        vec.items = nitems
    else:
        vec.items[vec.length] = item
    //
    vec.length = vec.length + 1        
    //
    return vec

public export method test():
    // integers first
    Vector<int> vi_1 = { items: [1,2,3], length: 2 }    
    Vector<int> vi_2 = add(vi_1,0)
    Vector<int> vi_3 = add(vi_2,4)    
    assert vi_2.length == 3 && equals(vi_2.items,[1,2,0],3)
    assert vi_3.length == 4 && equals(vi_3.items,[1,2,0,4],4)
    // booleans second
    Vector<bool> vb_1 = { items: [true,false,true,false], length: 3 }
    Vector<bool> vb_2 = add(vb_1,true)
    Vector<bool> vb_3 = add(vb_2,false)
    assert vb_2.length == 4 && equals(vb_2.items, [true,false,true,true], 4)
    assert vb_3.length == 5 && equals(vb_3.items, [true,false,true,true,false], 5)

---