Merge branch 'master' of https://git.cduce.org/cduce

tests/poly/red-black-non-constructed.cd

+
+type RBtree = Btree | Rtree
+
+(* Black rooted RB tree: *)
+type Btree = [] | <black elem='a>[ RBtree RBtree ]
+
+(* Red rooted RB tree: *)
+type Rtree = <red elem='a>[ Btree Btree ]
+
+type Wrongtree =    <red elem='a>( [ Rtree Btree ]
+                                   | [ Btree Rtree ])
+
+type Unbalanced = <black elem='a>( [ Wrongtree RBtree ]
+                                   | [ RBtree Wrongtree ])
+
+let balance ( Unbalanced -> Rtree ; 'b\Unbalanced -> 'b\Unbalanced )
+  | <black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
+  | <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
+  | <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
+  | <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ] ->
+        <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ]
+  | x -> x
+
+
+let insert (x : 'a) (t : Btree) : Btree =
+  let ins_aux ( [] -> Rtree;
+                Btree\[] -> RBtree\[];
+                Rtree -> Rtree|Wrongtree )
+    | [] -> <red elem=x>[ [] [] ]
+    | (<(color) elem=y>[ a b ]) & z ->
+           if x << y then balance <(color) elem=y>[ (ins_aux a) b ]
+	   else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ]
+	   else z
+    in match ins_aux t with
+       | <_ (y)>[ a b ] -> <black (y)>[ a b ]
+ 
\ No newline at end of file