#lang ivy1.6

include collections

module set(index,elem) = {

    instance arr:array(index.t,elem)

    alias t = arr.t

    function contains(X:t,y:elem) = exists Z. 0 <= Z & Z < arr.end(X) & arr.value(X,Z) = y

    action emptyset returns(s:t)
    action add(s:t,e:elem) returns (s:t)
    action remove(s:t,e:elem) returns (res:t)
    
    object spec = {
	after emptyset {
	    assert ~contains(s,X)
	}
	after add {
	    assert contains(s,X) <-> (contains(old s,X) | X = e)
	}
	after remove {
	    assert contains(res,X) <-> (contains(s,X) & X ~= e)
	}
    }

    object impl = {
	implement emptyset {
	    s := arr.create(0,0)
	}
	
	implement add {
	    if ~contains(s,e) {
                s := arr.resize(s,index.next(arr.end(s)),e)
	    }
        }

	function remove_step (s:t,e:elem,i:index.t,y:elem)
	    = (exists Z. 0 <= Z & Z < i & arr.value(s,Z) = y) & y ~= e

	property I >= 0 & index.succ(I,J) ->
	    (remove_step(X,E,J,Y) <-> (remove_step(X,E,I,Y) | arr.value(X,I) = Y & Y ~= E))

	property I = arr.end(X) ->
	    (remove_step(X,E,I,Y) <-> (contains(X,Y) & Y~=E))

	implement remove {
	    local i:index.t, end:index.t {
		i := 0;
		res := arr.create(0,0);
		end := arr.end(s);
		while i < end
		    invariant 0 <= i & i <= end
		    invariant contains(res,Y) = remove_step(s,e,i,Y)
		{
		    local f:elem {
			f := arr.get(s,i);
			if  f ~= e {
			    res := add(res,f)
			}
		    };
		    i := index.next(i)
		}
	    }
	}
    }
}

include order

instance index : unbounded_sequence
type elem

instance s : set(index,elem)

export s.emptyset
export s.add
export s.remove

isolate iso_s = s with index
extract iso_impl = s,index