# TODO: transition specifications
array = pyimport "Array"

.Array!: ClassType
.Array! <: array.Array
.Array!.
    '''
    Append object to the end of the list.
    '''
    '''erg
    arr = ![1, 2]
    arr.push! 3
    assert arr == [1, 2, 3]
    '''
    push!: |T, N: Nat|(self: Array!(T, N), elem: T) => NoneType
    '''
    Extend the list by appending all the items from `iterable`.
    '''
    '''erg
    arr = ![1, 2]
    arr.extend! [3, 4]
    assert arr == [1, 2, 3, 4]
    '''
    extend!: |T, N: Nat|(self: Array!(T, N), iterable: Iterable(T)) => NoneType
    '''
    Insert `elem` before `index`.
    '''
    '''erg
    arr = ![1, 2]
    arr.insert! 0, 3
    assert arr == [3, 1, 2]
    '''
    insert!: |T, N: Nat|(self: Array!(T, N), index: Nat, elem: T) => NoneType
    '''
    Remove the first item from the list whose value is `value`.
    '''
    '''erg
    arr = ![1, 2]
    arr.remove! 1
    assert arr == [2]
    '''
    remove!: |T, N: Nat|(self: Array!(T, N), value: T) => NoneType
    '''
    Remove the item at the given position in the list, and return it.
    '''
    '''erg
    arr = ![1, 2]
    i = arr.pop!()
    assert arr == [1]
    assert i == 2
    '''
    pop!: |T, N: Nat|(self: Array!(T, N), index := Nat or {-1}) => T
    '''
    Remove all items from the list.
    '''
    '''erg
    arr = ![1, 2]
    arr.clear!()
    assert arr == []
    '''
    clear!: |T, N: Nat|(self: Array!(T, N)) => NoneType
    '''
    Sort the list in ascending order and return `None`.

    The sort is in-place (i.e. the list itself is modified) and stable (i.e. the
    order of two equal elements is maintained).

    If a `key` function is given, apply it once to each list item and sort them,
    ascending or descending, according to their function values.

    The `reverse` flag can be set to sort in descending order.
    '''
    '''erg
    arr = ![3, 1, 2]
    arr.sort!()
    assert arr == [1, 2, 3]
    '''
    sort!: |T, N: Nat|(self: Array!(T, N)) => NoneType
    '''
    Reverse the elements of the list in-place and return `None`.
    '''
    '''erg
    arr = ![3, 1, 2]
    arr.reverse!()
    assert arr == [2, 1, 3]
    '''
    reverse!: |T, N: Nat|(self: Array!(T, N)) => NoneType
    '''
    Update each element of the array according to the passed function `f`.
    '''
    '''erg
    arr = ![1, 2]
    arr.strict_map! x -> x + 1
    assert arr == [3, 4]
    '''
    strict_map!: |T, N: Nat|(self: Array!(T, N), f: T -> T) => NoneType
    '''
    Update `index`-th element of the array according to the passed function `f`.
    '''
    '''erg
    arr = ![1, 2]
    arr.udpate_nth! 0, x -> x + 1
    assert arr == [2, 2]
    '''
    update_nth!: |T, N: Nat|(self: Array!(T, N), index: Nat, f: T -> T) => NoneType
    '''
    Return a (deep) copy of the array.
    '''
    '''erg
    arr = ![1, 2]
    arr_copy = arr.copy()
    arr_copy.push! 3
    assert arr_copy == [1, 2, 3]
    assert arr == [1, 2]
    '''
    copy: |T, N: Nat|(self: Ref(Array!(T, N))) => Array!(T, N)