Working code ... still need to type it.

tests/poly/red-black.cd

@@ -120,10 +120,9 @@ let cardinal ( RBtree('a) -> Int )   (* better type: [] -> 0, Any\[] -> [1--*] *
 (* The though case: deletion *)
 
 
-
    (* remove the rightmost leave of the tree and return a flag to state
-      whether the resulting tree decreased the the depth of black nodes 
-   
+      whether the resulting tree decreased the the depth of black nodes *)
+      
    let remove_min (RBtree('a)\[] -> [RBtree('a) Bool 'a])
        (* black leaf: remove it and flag the depth decrease *)
      | <black elem=x>[ [] [] ] ->                 
@@ -133,37 +132,78 @@ let cardinal ( RBtree('a) -> Int )   (* better type: [] -> 0, Any\[] -> [1--*] *
                      | (<red elem=y>[ l r ] [] )] ->
           [ <black elem=y>[ l r ] `false x ]
        (* you cannot have a red node with one empty sibling *)  
-     | <black elem=x>[ ([] <red ..>Any)
+     | <black elem=Any>[ ([] <red ..>Any)
                      | (<red ..>Any []) ] ->
-          raise "false"
+          raise "impossible"
        (* red node with at least on empty child : remove it without any flag *)
      | <red elem=x>[ ([] n) | (n []) ] ->
           [ n `false x ]
        (* general case of a node with two non empty childs *)
-     | <(c) elem=x>[ l r ] ->
+     | <(c) elem=x>[ l\[] r\[] ] ->
          let [ ll d e ] = remove_min l in
-	 let tree = <(c) elem=x>[ ll r] in
+	 let tree = <(c) elem=x>[ ll r ] in
 	 if d then
             (bubble_left tree)@[e]
 	 else
 	    [ tree `false e ]
-*)	    
-
-
-(* BUG TYPE ERROR *)
-
-let blackify( (<_ ('a)>'b)  -> <black ('a)>'b )
-  | <_ x>y -> <black x>y
-  | _ -> raise "false"
-    
-
-let redify( (<_ ('a)>'b)  -> <black ('a)>'b )
-  | <_ x>y -> <red x>y
-
-(*
-let bubble_left
-  | <(c) elem=e>[ l r] ->
-       (<black elem=e>[ (blackify l) (balance(redify r)) ], c=`black]
-
-*)
-
+     | _ -> raise "impossible"
+
+   let blackify( (<_ ('a)>'b)  -> <black ('a)>'b )
+     | <_ (x)>y -> <black (x)>y
+
+   let redify( (<_ ('a)>'b)  -> <red ('a)>'b )
+     | <_ (x)>y -> <red (x)>y
+
+
+
+  (* increase the black depth of the right child of the argument and
+     flag whether the black depth of the tree is still to be incremented  *)
+
+   let bubble_right ( RBtree('a)\[] -> (Btree('a) , Bool) )
+     | <black elem=y>[<red elem=x>[ ll\[] <black elem=re>[c d]] (e&<black ..>_) ] ->
+         ( <black elem=re>[ <black elem=x>[(balance (redify ll)) c]
+                            <black elem=y>[d e]
+                	  ] , `true)
+     | <_ ..>[ [] _ ] ->
+          raise "impossible"
+     | <(c) elem=e>[ l r ] ->
+          (<black elem=e>[ (balance(redify l)) r ] , (c = `black))
+
+
+  (* increase the right depth of the right child of the argument and
+     flag whether the black depth of the tree is still to be incremented  *)  
+
+    let bubble_left ( RBtree('a)\[] -> (Btree('a) , Bool) )
+      | <black elem=z>[ (e&<black ..>_) <red elem=x>[ <black elem=w>[a b] ll\[] ] ] ->
+         ( <black elem=w>[ <black elem=z>[ e a ]
+                           <black elem=x>[ b (balance (redify ll)) ]
+                	 ] , `true )
+      | <_ ..>[ _ [] ] -> 
+          raise "impossible"
+      | <(c) elem=e>[ l r ] ->
+          (<black elem=e>[ l (balance (redify r)) ], (c = `black))
+  
+
+let remove(x : 'a)(t : RBtree('a) ) : RBtree('a) =
+  let remove_aux(RBtree('a) -> (RBtree('a),Bool) )
+    | [] ->
+         ([],`false)
+    | <(c) elem=y>[ l r ] & tree ->
+        if (x << y ) then
+	  let (ll,d) = remove_aux l in
+	  let tree = <(c) elem=y>[ ll r ] in   (* we must prove that tree is well-formed *)
+	  if d then bubble_left tree else (tree,`false)
+	else if (x >> y) then
+	  let (rr,d) = remove_aux r in
+	  let tree = <(c) elem=y>[ l rr ] in
+	  if d then bubble_right tree else (tree,`false)
+	else (* x = y *)
+	   match tree with
+	     | <(c) ..>[ [] [] ] -> ([], (c = `black))
+	     | <black ..>[ ([] y) | (y []) ] -> (blackify y,`false)
+	     | <(c) ..>[ l r ] ->
+	          let [ ll d z ] = remove_min l in
+		  let tree = <(c) elem=z>[ ll r] in
+		  if d then bubble_left tree else (tree, `false)
+   in
+   let (sol,_) = remove_aux t in sol
\ No newline at end of file