definition module BitSet;

import StdEnv;

BITS_IN_WORD	:== 32;
DIV_WSIZE x		:== x >> 5;
MOD_WSIZE x		:== x bitand (dec BITS_IN_WORD);

// FINITE SET REPRESENTATION
:: BitSet
	= {
		n_elements	:: !Int
	,	map			:: !.{#Int}
	};

EmptyBitSet :: !.BitSet;

// optimalizeren niet direct de gehele bitset aanmaken.
NewBitSet :: !Int -> .BitSet;
ClearBitSet :: !.BitSet -> !.BitSet;


EqualBitSet :: !*BitSet !*BitSet -> (!Bool,!*BitSet,!*BitSet);
DelBitSet :: !*BitSet !a -> !*BitSet | fromInt, toInt a;
AddBitSet :: !*BitSet !a -> !*BitSet | toInt a;
//isBitSetMember :: !.BitSet !a -> !(!Bool,!.BitSet) | toInt a;
ComplementBitSet :: !*BitSet -> !*BitSet;
//enum_setSt :: (Int -> .(.a -> .a)) !*BitSet .a -> *(*BitSet,.a);
//enum_setSt :: (Int -> .(.a -> .a)) !.BitSet .a -> (.BitSet,.a);
enum_setSt :: (Int -> .(.a -> .a)) !u:BitSet .a -> (v:BitSet,.a), [u <= v];

isBitSetMember :: !u:BitSet !Int -> (Bool,v:BitSet), [u <= v];

// 
isBitSetMemberE	select_func s elem :== isBitSetMemberE2 select_func s elem;
where {
//	isBitSetMemberE2 :: (!Int !.a -> (!Int,!.a)) !.a !Int -> (!Bool,!.a);
	isBitSetMemberE2 select_func s elem
		#! div_wsize
			= DIV_WSIZE elem;
		#! (map_elem,s)
			= select_func div_wsize s;
		#! map_elem
			= map_elem bitand (1 << (MOD_WSIZE elem));
		= (map_elem <> 0,s);
};

AddBitSetE select_func update_func s elem :== AddBitSetE select_func update_func s elem;
where {
	AddBitSetE select_func update_func s elem
		#! div_wsize
			= DIV_WSIZE elem;
		#! (map_elem,s)
			= select_func div_wsize s;
		#! map_elem
			= map_elem bitor (1 << (MOD_WSIZE elem));
		#! s
			= update_func map_elem div_wsize s;
		= s;
};

DelBitSetE select_func update_func s elem :== DelBitSetE select_func update_func s elem;
where {
	DelBitSetE select_func update_func s elem
		#! div_wsize
			= DIV_WSIZE elem;
		#! (map_elem,s)
			= select_func div_wsize s;
		#! map_elem
			= map_elem bitand (bitnot (1 << (MOD_WSIZE elem)));
		#! s
			= update_func map_elem div_wsize s;
		= s;		
};