implementation module typeproperties

import StdEnv

import general, StdCompare

::	TypeClassification = 
	{	tc_signs	:: TypeSignTree
	,	tc_props	:: TypePropTree
	}

::	SignClassification	=
	{	sc_pos_vect	:: !BITVECT
	,	sc_neg_vect	:: !BITVECT
	}
/*
IsPositive sign_class index :== sign_class.sc_pos_vect bitand (1 << index) <> 0
IsNegative sign_class index :== sign_class.sc_neg_vect bitand (1 << index) <> 0
*/
::	PropClassification	:== BITVECT

TopSignClass	:== { sc_pos_vect = bitnot 0, sc_neg_vect = bitnot 0 }
ArrowSignClass	:== { sc_pos_vect = 2, sc_neg_vect = 1 }
PosSignClass	:== { sc_pos_vect = bitnot 0, sc_neg_vect = 0 }

:: Sign =
	{	pos_sign :: !Bool
	,	neg_sign :: !Bool
	}


TopSign			:== { pos_sign = True,	neg_sign = True }
BottomSign		:== { pos_sign = False,	neg_sign = False }
PositiveSign	:== { pos_sign = True,	neg_sign = False }
NegativeSign	:== { pos_sign = False,	neg_sign = True }

::	TypeSign key =
	{	ts_cons_var_signs	:: !key
	,	ts_type_sign		:: !SignClassification
	}

::	TypeProp key =
	{	ts_cons_var_props	:: !key
	,	ts_type_prop		:: !PropClassification
	}

::	VarBind a key =
	{	vb_number			:: !key
	,	vb_value			:: !a
	}

::	TypeSignTree 	:== BinTree (TypeSign [SignClassification])
::	TypePropTree 	:== BinTree (TypeProp [PropClassification])
::	EnvTree	a 		:== BinTree (VarBind a Int)

::	BinTree a = BT_Node !a !(BinTree a) !(BinTree a) | BT_Empty

class key m :: (m a) -> a

instance key TypeSign
where
	key {ts_cons_var_signs} = ts_cons_var_signs

instance key TypeProp
where
	key {ts_cons_var_props} = ts_cons_var_props

instance key (VarBind a)
where
	key {vb_number} = vb_number

EmptyTypeClassification :: TypeClassification
EmptyTypeClassification = { tc_signs = BT_Empty, tc_props = BT_Empty }

treeInsert :: !k !(m k) !(BinTree (m k)) -> BinTree (m k) | =< k & key m
treeInsert new_key el BT_Empty
	= BT_Node el BT_Empty BT_Empty
treeInsert new_key new_el tree=:(BT_Node el left right)
	# cmp = new_key =< key el
	| cmp == Smaller
		= BT_Node el (treeInsert new_key new_el left) right
		= BT_Node el left (treeInsert new_key new_el right)
	
treeRetrieve :: !k !(BinTree (m k)) -> !Optional (m k) | =< k & key m
treeRetrieve search_key BT_Empty
	= No
treeRetrieve search_key tree=:(BT_Node el left right)
	# cmp = search_key =< key el
	| cmp == Equal
		= Yes el
	| cmp == Smaller
		= treeRetrieve search_key left
		= treeRetrieve search_key right

signClassToSign :: !SignClassification !Int -> Sign
signClassToSign {sc_pos_vect,sc_neg_vect} index
	= { pos_sign = sc_pos_vect bitand (1 << index) <> 0, neg_sign = sc_neg_vect bitand (1 << index) <> 0}

instance <<< Sign
where
	(<<<) file {pos_sign,neg_sign}
		| pos_sign
			| neg_sign
				= file <<< "T"
				= file <<< "+"
		| neg_sign
			= file <<< "-"
			= file <<< "L"
		
instance =< SignClassification
where
	=< sc1 sc2
		| sc1.sc_pos_vect == sc2.sc_pos_vect
			| sc1.sc_neg_vect == sc2.sc_neg_vect
				= Equal
			| sc1.sc_neg_vect < sc2.sc_neg_vect
				= Smaller
				= Greater
		| sc1.sc_pos_vect < sc2.sc_pos_vect
			= Smaller
			= Greater

retrieveSignClassification :: ![SignClassification] !TypeClassification -> Optional (TypeSign [SignClassification])
retrieveSignClassification cons_classes {tc_signs}
	= treeRetrieve cons_classes tc_signs

addSignClassification :: ![SignClassification] !SignClassification !TypeClassification -> !TypeClassification
addSignClassification hio_signs sign_class tc=:{tc_signs}
	= { tc & tc_signs = treeInsert hio_signs { ts_cons_var_signs = hio_signs, ts_type_sign = sign_class } tc_signs }

retrievePropClassification :: ![PropClassification] !TypeClassification -> Optional (TypeProp [PropClassification])
retrievePropClassification cons_classes {tc_props}
	= treeRetrieve cons_classes tc_props

addPropClassification :: ![PropClassification] !PropClassification !TypeClassification -> !TypeClassification
addPropClassification hio_props prop_class tc=:{tc_props}
	= { tc & tc_props = treeInsert hio_props { ts_cons_var_props = hio_props, ts_type_prop = prop_class } tc_props }

instance * Sign
where
	(*) sign1 sign2
		| sign1.pos_sign
			| sign1.neg_sign
				= sign1
				= sign2
		| sign1.neg_sign
			= { pos_sign = sign2.neg_sign, neg_sign = sign2.pos_sign }
			= sign1

/*			
		= {	pos_sign = sign1.pos_sign * sign2.pos_sign || sign1.neg_sign * sign2.neg_sign,
			neg_sign = sign1.pos_sign * sign2.neg_sign || sign1.neg_sign * sign2.pos_sign }
		
instance * Bool
where
	(*) b1 b2 = b1 && b2 || not b1 && not b2

*/