type element = int;;

type color = Red | Black;;

type bicolor_tree = Empty |
							Cons of (color * element * bicolor_tree * bicolor_tree)
;;

let tree_empty = Empty;;

let tree1 =
	Cons (Black, 15,
		Cons (Black, 10,
			Empty,
			Empty
		),
		Cons (Red, 22,
			Cons (Black, 17,
				Empty,
				Empty
			),
			Cons (Black, 253,
				Empty,
				Cons (Red, 254,
					Empty,
					Empty
				)
			)
		)
	)
;;

let tree2 =
	Cons (Black, 17,
		Cons (Black, 15,
			Cons(Black, 10,
				Empty,
				Empty
			),
			Cons(Black, 16,
				Empty,
				Empty
			)
		),
		Cons (Black, 253,
			Cons (Black, 22,
				Empty,
				Empty
			),
			Cons (Black, 254,
				Empty,
				Empty
			)
		)
	)
;;

(* Ex 1 *)



(* Exercice précédent *)

(*Preuve : Fonction prenant un arbre en paramètre et transforme sa racine en noir s'il n'est pas vide.*)
(* Pour un arbre (Red, e, ag, ad) :*)
(* 	on renvoie un arbre (Black, e, ag, ad)*)
(* Sinon on renvoie l'arbre non modifié.*)
let black_root = function tree ->
	match tree with
	| Cons (Red, e, ag, ad) -> Cons (Black, e, ag, ad)
	| _ -> tree
;;

(*Preuve : Fonction de test pour savoir si la racine de l'arbre est rouge.*)
(* Pour un arbre (Red, e, ag, ad) :*)
(* 	on renvoie vrai*)
(* Sinon on renvoie faux.*)
let root_is_red = function tree ->
	match tree with
	| Cons (Red, _, _, _) -> true
	| _ -> false
;;

(*Preuve : Fonction de test pour savoir si la racine du fils gauche d'un arbre est rouge.*)
(* Pour un arbre (_, e, ag, ad) avec la racine de ag rouge.*)
(* 	on renvoie vrai*)
(* Sinon on renvoie faux.*)
let son_left_is_red = function tree ->
	match tree with
	| Cons (_, _, ag, _) when (root_is_red ag) -> true
	| _ -> false
;;

(*Preuve : Fonction de test pour savoir si la racine du fils droit d'un arbre est rouge.*)
(* Pour un arbre (_, e, ag, ad) avec la racine de ad rouge.*)
(* 	on renvoie vrai*)
(* Sinon on renvoie faux.*)
let son_right_is_red = function tree ->
	match tree with
	| Cons (_, _, _, ad) when (root_is_red ad) -> true
	| _ -> false
;;

(*Preuve : Fonction de test pour savoir si la racine d'un arbre et un de ses fils sont rouges.*)
(* Pour un arbre (Red, e, ag, ad) avec au moins une racine de ag ou ad rouge.*)
(* 	on renvoie vrai*)
(* Sinon on renvoie faux.*)
let double_red_son = function tree ->
	((root_is_red tree) && ((son_left_is_red tree) || (son_right_is_red tree)))
;;

(*Preuve : Fonction de recoloration d'un arbre.*)
(* Pour un arbre non vide avec des fils non vides :*)
(* 	on renvoie la racine rouge, et les deux racines des fils noirs.*)
(* Sinon on renvoie l'arbre non modifié.*)
let recoloring_abin = function tree ->
	match tree with
	| Cons (_, g, Cons (_, p, pl, pr), Cons (_, f, fl, fr))	->
			Cons (Red, g, Cons (Black, p, pl, pr),	Cons (Black, f, fl, fr))
	| _ -> tree
;;

(*Preuve : Fonction de rotation droite de la racine et de son fils gauche.*)
(* Pour un arbre non vide avec son fils gauche non vide :*)
(* 	on renvoie la rotation droite.*)
(* Sinon on renvoie l'arbre non modifié.*)
let rotate_right = function tree ->
	match tree with
	| Cons (cn, n, Cons (cm, m, a1, a2), a3) ->	Cons (cm, m, a1, Cons (cn, n, a2, a3))
	| _ -> tree
;;

(*Preuve : Fonction de rotation gauche de la racine et de son fils droit.*)
(* Pour un arbre non vide avec son fils droit non vide :*)
(* 	on renvoie la rotation gauche.*)
(* Sinon on renvoie l'arbre non modifié.*)
let rotate_left = function tree ->
	match tree with
	| Cons (cm, m, a1, Cons (cn, n, a2, a3)) ->	Cons (cn, n, Cons (cm, m, a1, a2), a3)
	| _ -> tree
;;

(*Preuve : Fonction de recoloration d'un arbre qui va effectuer une rotation.*)
(* Pour un arbre non vide de racine noire et un fils gauche non vide de racine rouge :*)
(* 	on renvoie la racine rouge, et la racine du fils gauche noire.*)
(* Pour un arbre non vide de racine noire et un fils droit non vide de racine rouge :*)
(* 	on renvoie la racine rouge, et la racine du fils droit noire.*)
(* Sinon on renvoie l'arbre non modifié.*)
let recolor_in_rotation = function tree ->
	match tree with
	| Cons (Black, g, Cons (Red, p, a1, a2), ad) ->	Cons (Red, g, Cons (Black, p, a1, a2), ad)
	| Cons (Black, g, ag, Cons (Red, p, a1, a2)) ->	Cons (Red, g, ag, Cons (Black, p, a1, a2))
	| _ -> tree
;;

(*Preuve : Fonction d'équilibre d'un arbre bicolor.*)
(* Pour un arbre non vide de racine noire dont le fils gauche de racine rouge et le fils droit de racine rouge*)
(* 	ont au moins une fois deux noeuds rouges d'affilé :*)
(* 		on renvoie l'arbre recoloré avec la racine rouge, et les deux racines des fils noirs.*)
(* *)
(* Pour un arbre non vide de racine noire dont le fils gauche a deux noeuds rouges d'affilé*)
(* 	et dont la racine du fils gauche du fils gauche est rouge :*)
(* 		on renvoie la rotation droite de l'arbre de racine rouge, et la racine du fils gauche noire.*)
(* *)
(* Pour un arbre non vide de racine noire dont le fils gauche a deux noeuds rouges d'affilé*)
(* 	et dont la racine du fils gauche du fils droit est rouge :*)
(* 		on renvoie l'arbre équilibré de l'arbre de racine noire dont le fils gauche a subi une rotation gauche.*)
(* *)
(* Pour un arbre non vide de racine noire dont le fils droit a deux noeuds rouges d'affilé*)
(* 	et dont la racine du fils droit du fils gauche est rouge :*)
(* 		on renvoie l'arbre équilibré de l'arbre de racine noire dont le fils droit a subi une rotation droite.*)
(* *)
(* Pour un arbre non vide de racine noire dont le fils droit a deux noeuds rouges d'affilé*)
(* 	et dont la racine du fils droit du fils droit est rouge :*)
(* 		on renvoie la rotation gauche de l'arbre de racine rouge, et la racine du fils droit noire.*)
(* *)
(* Sinon on renvoie l'arbre non modifié.*)
let rec balancing = function tree->
		match tree with
		| Cons (Black, g, ag, ad)	when (((double_red_son ad) || (double_red_son ag))
																&& (root_is_red ag) && (root_is_red ad))
			-> (recoloring_abin tree)
		| Cons (Black, g, ag, ad) when ((double_red_son ag) && (son_left_is_red ag))
			-> rotate_right (recolor_in_rotation tree)
		| Cons (Black, g, ag, ad)	when ((double_red_son ag) && (son_right_is_red ag))
			-> balancing (Cons (Black, g, (rotate_left ag), ad))
		| Cons (Black, g, ag, ad)	when ((double_red_son ad) && (son_left_is_red ad))
			-> balancing (Cons (Black, g, ag, (rotate_right ad)))
		| Cons (Black, g, ag, ad)	when ((double_red_son ad) && (son_right_is_red ad))
			-> rotate_left (recolor_in_rotation tree)
		| _ -> tree
;;

(*Preuve : Fonction d'ajout d'un élèment dans un arbre bicolor.*)
(* Pour un arbre vide :*)
(* 	on renvoie la racine noire avec l'élèment.*)
(* *)
(* Pour un arbre non vide dont l'élèment est plus petit que l'élèment que l'on souhaite ajouter :*)
(* 	on renvoie l'arbre équilibré ou l'on a ajouté l'élèment dans le sous-arbre droit.*)
(* *)
(* Pour un arbre non vide dont l'élèment est plus grand que l'élèment que l'on souhaite ajouter :*)
(* 	on renvoie l'arbre équilibré ou l'on a ajouté l'élèment dans le sous-arbre gauche.*)
(* *)
(* Sinon on renvoie l'arbre non modifié.*)
let ajout_abic = fun abic element ->
	let rec aux = fun abic element ->
		match abic with
  	| Empty -> Cons (Red, element, Empty, Empty)
  	| Cons (c, e, a1, a2) when e < element ->	(balancing (Cons (c, e, a1, (aux a2 element))))
  	| Cons (c, e, a1, a2) when e > element ->	(balancing (Cons (c, e, (aux a1 element), a2)))
  	| _ -> abic
	in (black_root (aux abic element))
;;

(**
	*	Permet de savoir si un élement donné est dans un arbre bicolor donné.
	* .@param : element + bicolor_tree
	* .@return : bool
	*)
let rec bicolor_tree_is_in = fun tree element ->
	match tree with
	| Empty -> false
	| Cons (_, e, tl, _) when e > element -> (bicolor_tree_is_in tl element)
	| Cons (_, e, _, tr) when e < element -> (bicolor_tree_is_in tr element)
	| _ -> true
;;

(**
	*	Permet de savoir si un arbre bicolor donné est vide.
	* .@param : bicolor_tree
	* .@return : bool
	*)
let bicolor_tree_is_empty = function tree ->
	(tree = Empty)
;;

(**
	*	Permet de savoir si un arbre est bien un arbre binaire de recherche.
	* .@param : bicolor_tree
	* .@return : bool
	*)
let bicolor_tree_is_binary_search_tree = function tree ->
	if (bicolor_tree_is_empty tree) then
		true
	else
		(* Preuve :*)
		(* - Pour un arbre (_, e, empty, empty) :*)
		(*		La valeur booléenne est vraie puisqu'un arbre à un noeud est un arbre binaire de recherche*)
		(* 		Le minumum et le maximum de l'arbre est l'élèment e*)
		(* - Pour un arbre (_, e, empty, tr) *)
		(*		La valeur booléenne correspond à :*)
		(* 			vrai, si la valeur minimale du sous-arbre droit est plus grande que l'élèment e et *)
		(* 			si le sous-arbre droit est un arbre binaire de recherche par induction.*)
		(* 		Le minimum correspond à l'élèment e car tous les elèments du sous-arbre droit*)
		(* 			sont plus grands que l'élèment e par définition d'un arbre binaire de recherche.*)
		(* 		Le maximum correpond à la valeur maximale du sous arbre droit par induction.*)
		(* Pour un arbre (_, e, tl, empty) : on peut appliquer la symétrie avec le cas précédent*)
		(* Pour un arbre (_, e, tl, tr) : on applique avec les deux cas précédents*)
		let rec aux = function
			| Cons(_, e, Empty, Empty) ->
					(true, e, e)
			| Cons(_, e, Empty, tr) ->
  				let (b, min, max) = (aux tr)
  				in ((b && (min > e)), e, max)
			| Cons(_, e, tl, Empty) ->
  				let (b, min, max) = (aux tl)
  				in ((b && (max < e)), min, e)
			| Cons(_, e, tl, tr) ->
  				let (tr, minr, maxr) = (aux tr)
  				and (tl, minl, maxl) = (aux tl)
  				in ((tr && tl && (minr > e) && (maxl < e)), minl, maxr)
			| Empty -> failwith ""
		in
			let (b,_,_) = (aux tree)
			in b
;;

(**
	*	Permet de connaître la couleur de la radine d'un arbre coloré donné.
	* .@param : bicolor_tree
	* .@return : color
	*)
let bicolor_tree_color_root = function tree ->
	match tree with
	| Empty -> failwith "bicolor_tree_color_root: The tree is empty"
	| Cons (color, _, _, _) -> color
;;

(**
	*	Permet de savoir si un arbre est bien un arbre bicolor.
	* .@param : bicolor_tree
	* .@return : bool
	*)
let tree_is_bicolor_tree = function tree ->
	if (bicolor_tree_is_empty tree)
		then true
	else
		if (((bicolor_tree_is_binary_search_tree tree) = false)
    			|| ((bicolor_tree_color_root tree) != Black))
			then false
		else
  		(* Preuve :*)
  		(* - Pour un arbre (color, _, empty, empty) :*)
  		(*		La valeur booléenne est vraie puisqu'un arbre à un noeud est un arbre coloré*)
  		(* 		Le nombre de noeud correspond à si la couleur de la racine est noire.*)
			(* 		La coleur correspond à la couleur de la racine*)
  		(* - Pour un arbre (color, _, empty, tr) *)
  		(*		La valeur booléenne correspond à :*)
  		(* 			vrai, si la couleur de la racine du sous-arbre gauche est noire*)
			(* 				ou que la couleur de la racine est noire et *)
			(*			si le nombre de noeuds noirs du sous arbre gauche est égale au nombre*)
			(* 				de noeuds noirs : 0 puisque le sous arbre droit est vide.*)
			(* 			si le sous-arbre gauche est un arbre coloré par induction.*)
  		(* 		Le nombre de noeuds noirs correspond au nombre de noeuds noirs du sous arbre gauche*)
			(* 			obtenu par induction + le noeud de la racine de l'arbre s'il est noir.*)
  		(* Pour un arbre (color, _, tl, empty) : on peut appliquer la symétrie avec le cas précédent*)
  		(* Pour un arbre (color, _, tl, tr) : on applique avec les deux cas précédents*)
			let rec aux = function
				| Cons(color, _, Empty, Empty) ->
					let nb_node_black =
						if (color = Black)
							then 1
						else 0
					in (nb_node_black, true, color)
  			| Cons(color, _, tl, Empty) ->
					let (nb_node_black_tl, bool_tl, color_tl) = (aux tl)
					in
						let nb_node_black =
							if (color = Black) then nb_node_black_tl + 1
							else nb_node_black_tl
						and	b = (bool_tl
										&& ((color_tl = Black) || (color = Black))
										&& (nb_node_black_tl = 0))
						in (nb_node_black, b, color)
  			| Cons(color, _, Empty, tr) ->
					let (nb_node_black_tr, bool_tr, color_tr) = (aux tr)
					in
						let nb_node_black =
							if (color = Black)
								then nb_node_black_tr + 1
							else nb_node_black_tr
						and	b = (bool_tr
										&& ((color_tr = Black) || (color = Black))
										&& (nb_node_black_tr = 0))
						in (nb_node_black, b, color)
				| Cons (color, _, tl, tr) ->
					let (nb_node_black_tl, bool_tl, color_tl) = (aux tl)
					and (nb_node_black_tr, bool_tr, color_tr) = (aux tr)
					in
						let b = (bool_tl && bool_tr
							&& (nb_node_black_tl = nb_node_black_tr))
						and nb_node_black =
							if (color = Black)
								then nb_node_black_tl + 1
							else nb_node_black_tl
						in (nb_node_black, b, color)
				| Empty -> failwith "bicolor_tree_color_root: Error"
			in
				let (_, b, _) = (aux tree)
				in b
;;

(* Test *)

let rec ajout_n_random_element_in_abic = fun abic n ->
	if (n <= 0) then abic
	else (ajout_n_random_element_in_abic
      		(ajout_abic abic (Random.int 100))
      		(n - 1))
;;

let test = fun n ->
    	let a = (ajout_n_random_element_in_abic Empty n)
    	in (tree_is_bicolor_tree a)
;;