AvlTree-2.4: Data/Tree/AVL/Internals/HSet.hs
{-# OPTIONS_GHC -fglasgow-exts #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Tree.AVL.Internals.HSet
-- Copyright : (c) Adrian Hey 2004,2005
-- License : BSD3
--
-- Maintainer : http://homepages.nildram.co.uk/~ahey/em.png
-- Stability : stable
-- Portability : portable
--
-- Set primitives on AVL trees with (height information supplied where needed).
-- All the functions in this module use essentially the same symetric \"Divide and Conquer\" algorithm.
-----------------------------------------------------------------------------
module Data.Tree.AVL.Internals.HSet
(-- * Union primitives.
unionH,unionMaybeH,
-- * Intersection primitives.
intersectionH,intersectionMaybeH,
-- * Difference primitives.
differenceH,differenceMaybeH,symDifferenceH,
) where
import Data.Tree.AVL.Types(AVL(..))
import Data.Tree.AVL.Internals.HJoin(spliceH,joinH)
import Data.COrdering
#ifdef __GLASGOW_HASKELL__
import GHC.Base
#include "ghcdefs.h"
#else
#include "h98defs.h"
#endif
-- | Uses the supplied combining comparison to evaluate the union of two sets represented as
-- sorted AVL trees of known height. Whenever the combining comparison is applied, the first
-- comparison argument is an element of the first tree and the second comparison argument is
-- an element of the second tree.
--
-- Complexity: Not sure, but I'd appreciate it if someone could figure it out.
-- (Faster than Hedge union from Data.Set at any rate).
unionH :: (e -> e -> COrdering e) -> AVL e -> UINT -> AVL e -> UINT -> UBT2(AVL e,UINT)
unionH c = u where
-- u :: AVL e -> UINT -> AVL e -> UINT -> UBT2(AVL e,UINT)
u E _ t1 h1 = UBT2(t1,h1)
u t0 h0 E _ = UBT2(t0,h0)
u (N l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (N l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (N l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u (Z l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (Z l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (Z l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u (P l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (P l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (P l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u_ l0 hl0 e0 r0 hr0 l1 hl1 e1 r1 hr1 =
case c e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
Lt -> case forkR r0 hr0 e1 of
UBT5(rl0,hrl0,e1_,rr0,hrr0) -> case forkL e0 l1 hl1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,hll1,e0_,lr1,hlr1) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case u l0 hl0 ll1 hll1 of
UBT2(l,hl) -> case u rl0 hrl0 lr1 hlr1 of
UBT2(m,hm) -> case u rr0 hrr0 r1 hr1 of
UBT2(r,hr) -> case spliceH m hm e1_ r hr of
UBT2(t,ht) -> spliceH l hl e0_ t ht
-- e0 = e1
Eq e -> case u l0 hl0 l1 hl1 of
UBT2(l,hl) -> case u r0 hr0 r1 hr1 of
UBT2(r,hr) -> spliceH l hl e r hr
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
Gt -> case forkL e0 r1 hr1 of
UBT5(rl1,hrl1,e0_,rr1,hrr1) -> case forkR l0 hl0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT5(ll0,hll0,e1_,lr0,hlr0) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case u ll0 hll0 l1 hl1 of
UBT2(l,hl) -> case u lr0 hlr0 rl1 hrl1 of
UBT2(m,hm) -> case u r0 hr0 rr1 hrr1 of
UBT2(r,hr) -> case spliceH l hl e1_ m hm of
UBT2(t,ht) -> spliceH t ht e0_ r hr
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1)
-- forkL :: e -> AVL e -> UINT -> UBT5(AVL e,UINT,e,AVL e,UINT)
forkL e0 t1 ht1 = forkL_ t1 ht1 where
forkL_ E _ = UBT5(E, L(0), e0, E, L(0))
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case c e0 e of
Lt -> case forkL_ l hl of
UBT5(l0,hl0,e0_,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,e0_,l1_,hl1_)
Eq e0_ -> UBT5(l,hl,e0_,r,hr)
Gt -> case forkL_ r hr of
UBT5(l0,hl0,e0_,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,e0_,l1,hl1)
-- forkR :: AVL e -> UINT -> e -> UBT5(AVL e,UINT,e,AVL e,UINT)
forkR t0 ht0 e1 = forkR_ t0 ht0 where
forkR_ E _ = UBT5(E, L(0), e1, E, L(0))
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case c e e1 of
Lt -> case forkR_ r hr of
UBT5(l0,hl0,e1_,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,e1_,l1,hl1)
Eq e1_ -> UBT5(l,hl,e1_,r,hr)
Gt -> case forkR_ l hl of
UBT5(l0,hl0,e1_,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,e1_,l1_,hl1_)
-----------------------------------------------------------------------
-------------------------- unionH Ends Here ---------------------------
-----------------------------------------------------------------------
-- | Similar to _unionH_, but the resulting tree does not include elements in cases where
-- the supplied combining comparison returns @(Eq Nothing)@.
--
-- Complexity: Not sure, but I_d appreciate it if someone could figure it out.
unionMaybeH :: (e -> e -> COrdering (Maybe e)) -> AVL e -> UINT -> AVL e -> UINT -> UBT2(AVL e,UINT)
unionMaybeH c = u where
-- u :: AVL e -> UINT -> AVL e -> UINT -> UBT2(AVL e,UINT)
u E _ t1 h1 = UBT2(t1,h1)
u t0 h0 E _ = UBT2(t0,h0)
u (N l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (N l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (N l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u (Z l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (Z l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (Z l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u (P l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (P l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (P l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u_ l0 hl0 e0 r0 hr0 l1 hl1 e1 r1 hr1 =
case c e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
Lt -> case forkR r0 hr0 e1 of
UBT5(rl0,hrl0,mbe1_,rr0,hrr0) -> case forkL e0 l1 hl1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,hll1,mbe0_,lr1,hlr1) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case u l0 hl0 ll1 hll1 of
UBT2(l,hl) -> case u rl0 hrl0 lr1 hlr1 of
UBT2(m,hm) -> case u rr0 hrr0 r1 hr1 of
UBT2(r,hr) -> case (case mbe1_ of
Just e1_ -> spliceH m hm e1_ r hr
Nothing -> joinH m hm r hr
) of
UBT2(t,ht) -> case mbe0_ of
Just e0_ -> spliceH l hl e0_ t ht
Nothing -> joinH l hl t ht
-- e0 = e1
Eq mbe -> case u l0 hl0 l1 hl1 of
UBT2(l,hl) -> case u r0 hr0 r1 hr1 of
UBT2(r,hr) -> case mbe of
Just e -> spliceH l hl e r hr
Nothing -> joinH l hl r hr
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
Gt -> case forkL e0 r1 hr1 of
UBT5(rl1,hrl1,mbe0_,rr1,hrr1) -> case forkR l0 hl0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT5(ll0,hll0,mbe1_,lr0,hlr0) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case u ll0 hll0 l1 hl1 of
UBT2(l,hl) -> case u lr0 hlr0 rl1 hrl1 of
UBT2(m,hm) -> case u r0 hr0 rr1 hrr1 of
UBT2(r,hr) -> case (case mbe1_ of
Just e1_ -> spliceH l hl e1_ m hm
Nothing -> joinH l hl m hm
) of
UBT2(t,ht) -> case mbe0_ of
Just e0_ -> spliceH t ht e0_ r hr
Nothing -> joinH t ht r hr
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1)
-- forkL :: e -> AVL e -> UINT -> UBT5(AVL e,UINT,Maybe e,AVL e,UINT)
forkL e0 t1 ht1 = forkL_ t1 ht1 where
forkL_ E _ = UBT5(E, L(0), Just e0, E, L(0))
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case c e0 e of
Lt -> case forkL_ l hl of
UBT5(l0,hl0,mbe0_,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,mbe0_,l1_,hl1_)
Eq mbe0_ -> UBT5(l,hl,mbe0_,r,hr)
Gt -> case forkL_ r hr of
UBT5(l0,hl0,mbe0_,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,mbe0_,l1,hl1)
-- forkR :: AVL e -> UINT -> e -> UBT5(AVL e,UINT,Maybe e,AVL e,UINT)
forkR t0 ht0 e1 = forkR_ t0 ht0 where
forkR_ E _ = UBT5(E, L(0), Just e1, E, L(0))
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case c e e1 of
Lt -> case forkR_ r hr of
UBT5(l0,hl0,mbe1_,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,mbe1_,l1,hl1)
Eq mbe1_ -> UBT5(l,hl,mbe1_,r,hr)
Gt -> case forkR_ l hl of
UBT5(l0,hl0,mbe1_,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,mbe1_,l1_,hl1_)
-----------------------------------------------------------------------
----------------------- unionMaybeH Ends Here -------------------------
-----------------------------------------------------------------------
-- | Uses the supplied combining comparison to evaluate the intersection of two sets represented as
-- sorted AVL trees. This function requires no height information at all for
-- the two tree inputs. The absolute height of the resulting tree is returned also.
--
-- Complexity: Not sure, but I_d appreciate it if someone could figure it out.
intersectionH :: (a -> b -> COrdering c) -> AVL a -> AVL b -> UBT2(AVL c,UINT)
intersectionH comp = i where
-- i :: AVL a -> AVL b -> UBT2(AVL c,UINT)
i E _ = UBT2(E,L(0))
i _ E = UBT2(E,L(0))
i (N l0 e0 r0) (N l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (N l0 e0 r0) (Z l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (N l0 e0 r0) (P l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (Z l0 e0 r0) (N l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (Z l0 e0 r0) (Z l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (Z l0 e0 r0) (P l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (P l0 e0 r0) (N l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (P l0 e0 r0) (Z l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (P l0 e0 r0) (P l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i_ l0 e0 r0 l1 e1 r1 =
case comp e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
Lt -> case forkR r0 e1 of
UBT5(rl0,_,mbc1,rr0,_) -> case forkL e0 l1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,_,mbc0,lr1,_) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case i rr0 r1 of
UBT2(r,hr) -> case i rl0 lr1 of
UBT2(m,hm) -> case i l0 ll1 of
UBT2(l,hl) -> case (case mbc1 of
Just c1 -> spliceH m hm c1 r hr
Nothing -> joinH m hm r hr
) of
UBT2(t,ht) -> case mbc0 of
Just c0 -> spliceH l hl c0 t ht
Nothing -> joinH l hl t ht
-- e0 = e1
Eq c -> case i l0 l1 of
UBT2(l,hl) -> case i r0 r1 of
UBT2(r,hr) -> spliceH l hl c r hr
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
Gt -> case forkL e0 r1 of
UBT5(rl1,_,mbc0,rr1,_) -> case forkR l0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT5(ll0,_,mbc1,lr0,_) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case i r0 rr1 of
UBT2(r,hr) -> case i lr0 rl1 of
UBT2(m,hm) -> case i ll0 l1 of
UBT2(l,hl) -> case (case mbc0 of
Just c0 -> spliceH m hm c0 r hr
Nothing -> joinH m hm r hr
) of
UBT2(t,ht) -> case mbc1 of
Just c1 -> spliceH l hl c1 t ht
Nothing -> joinH l hl t ht
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1)
-- forkL :: a -> AVL b -> UBT5(AVL b,UINT,Maybe c,AVL b,UINT)
forkL e0 t1 = forkL_ t1 L(0) where
forkL_ E h = UBT5(E,h,Nothing,E,h) -- Relative heights!!
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case comp e0 e of
Lt -> case forkL_ l hl of
UBT5(l0,hl0,mbc0,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,mbc0,l1_,hl1_)
Eq c0 -> UBT5(l,hl,Just c0,r,hr)
Gt -> case forkL_ r hr of
UBT5(l0,hl0,mbc0,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,mbc0,l1,hl1)
-- forkR :: AVL a -> b -> UBT5(AVL a,UINT,Maybe c,AVL a,UINT)
forkR t0 e1 = forkR_ t0 L(0) where
forkR_ E h = UBT5(E,h,Nothing,E,h) -- Relative heights!!
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case comp e e1 of
Lt -> case forkR_ r hr of
UBT5(l0,hl0,mbc1,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,mbc1,l1,hl1)
Eq c1 -> UBT5(l,hl,Just c1,r,hr)
Gt -> case forkR_ l hl of
UBT5(l0,hl0,mbc1,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,mbc1,l1_,hl1_)
-----------------------------------------------------------------------
---------------------- intersectionH Ends Here ------------------------
-----------------------------------------------------------------------
-- | Similar to _intersectionH_, but the resulting tree does not include elements in cases where
-- the supplied combining comparison returns @(Eq Nothing)@.
--
-- Complexity: Not sure, but I_d appreciate it if someone could figure it out.
intersectionMaybeH :: (a -> b -> COrdering (Maybe c)) -> AVL a -> AVL b -> UBT2(AVL c,UINT)
intersectionMaybeH comp = i where
-- i :: AVL a -> AVL b -> UBT2(AVL c,UINT)
i E _ = UBT2(E,L(0))
i _ E = UBT2(E,L(0))
i (N l0 e0 r0) (N l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (N l0 e0 r0) (Z l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (N l0 e0 r0) (P l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (Z l0 e0 r0) (N l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (Z l0 e0 r0) (Z l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (Z l0 e0 r0) (P l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (P l0 e0 r0) (N l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (P l0 e0 r0) (Z l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i (P l0 e0 r0) (P l1 e1 r1) = i_ l0 e0 r0 l1 e1 r1
i_ l0 e0 r0 l1 e1 r1 =
case comp e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
Lt -> case forkR r0 e1 of
UBT5(rl0,_,mbc1,rr0,_) -> case forkL e0 l1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,_,mbc0,lr1,_) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case i rr0 r1 of
UBT2(r,hr) -> case i rl0 lr1 of
UBT2(m,hm) -> case i l0 ll1 of
UBT2(l,hl) -> case (case mbc1 of
Just c1 -> spliceH m hm c1 r hr
Nothing -> joinH m hm r hr
) of
UBT2(t,ht) -> case mbc0 of
Just c0 -> spliceH l hl c0 t ht
Nothing -> joinH l hl t ht
-- e0 = e1
Eq mbc -> case i l0 l1 of
UBT2(l,hl) -> case i r0 r1 of
UBT2(r,hr) -> case mbc of
Just c -> spliceH l hl c r hr
Nothing -> joinH l hl r hr
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
Gt -> case forkL e0 r1 of
UBT5(rl1,_,mbc0,rr1,_) -> case forkR l0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT5(ll0,_,mbc1,lr0,_) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case i r0 rr1 of
UBT2(r,hr) -> case i lr0 rl1 of
UBT2(m,hm) -> case i ll0 l1 of
UBT2(l,hl) -> case (case mbc0 of
Just c0 -> spliceH m hm c0 r hr
Nothing -> joinH m hm r hr
) of
UBT2(t,ht) -> case mbc1 of
Just c1 -> spliceH l hl c1 t ht
Nothing -> joinH l hl t ht
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1)
-- forkL :: a -> AVL b -> UBT5(AVL b,UINT,Maybe c,AVL b,UINT)
forkL e0 t1 = forkL_ t1 L(0) where
forkL_ E h = UBT5(E,h,Nothing,E,h) -- Relative heights!!
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case comp e0 e of
Lt -> case forkL_ l hl of
UBT5(l0,hl0,mbc0,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,mbc0,l1_,hl1_)
Eq mbc0_ -> UBT5(l,hl,mbc0_,r,hr)
Gt -> case forkL_ r hr of
UBT5(l0,hl0,mbc0,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,mbc0,l1,hl1)
-- forkR :: AVL a -> b -> UBT5(AVL a,UINT,Maybe c,AVL a,UINT)
forkR t0 e1 = forkR_ t0 L(0) where
forkR_ E h = UBT5(E,h,Nothing,E,h) -- Relative heights!!
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case comp e e1 of
Lt -> case forkR_ r hr of
UBT5(l0,hl0,mbc1,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,mbc1,l1,hl1)
Eq mbc1_ -> UBT5(l,hl,mbc1_,r,hr)
Gt -> case forkR_ l hl of
UBT5(l0,hl0,mbc1,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,mbc1,l1_,hl1_)
-----------------------------------------------------------------------
-------------------- intersectionMaybeH Ends Here ---------------------
-----------------------------------------------------------------------
-- | Uses the supplied comparison to evaluate the difference between two sets represented as
-- sorted AVL trees.
--
-- N.B. This function works with relative heights for the first tree and needs no height
-- information for the second tree, so it_s OK to initialise the height of the first to zero,
-- rather than calculating the absolute height. However, if you do this the height of the resulting
-- tree will be incorrect also (it will have the same fixed offset as the first tree).
--
-- Complexity: Not sure, but I_d appreciate it if someone could figure it out.
differenceH :: (a -> b -> Ordering) -> AVL a -> UINT -> AVL b -> UBT2(AVL a,UINT)
differenceH comp = d where
-- d :: AVL a -> UINT -> AVL b -> UBT2(AVL a,UINT)
d E h0 _ = UBT2(E ,h0) -- Relative heights!!
d t0 h0 E = UBT2(t0,h0)
d (N l0 e0 r0) h0 (N l1 e1 r1) = d_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (N l0 e0 r0) h0 (Z l1 e1 r1) = d_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (N l0 e0 r0) h0 (P l1 e1 r1) = d_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (Z l0 e0 r0) h0 (N l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (Z l0 e0 r0) h0 (Z l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (Z l0 e0 r0) h0 (P l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (P l0 e0 r0) h0 (N l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 e1 r1
d (P l0 e0 r0) h0 (Z l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 e1 r1
d (P l0 e0 r0) h0 (P l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 e1 r1
d_ l0 hl0 e0 r0 hr0 l1 e1 r1 =
case comp e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
LT -> case forkR r0 hr0 e1 of
UBT4(rl0,hrl0, rr0,hrr0) -> case forkL e0 l1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,_ ,be0,lr1,_ ) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case d rr0 hrr0 r1 of -- right
UBT2(r,hr) -> case d rl0 hrl0 lr1 of -- middle
UBT2(m,hm) -> case d l0 hl0 ll1 of -- left
UBT2(l,hl) -> case joinH m hm r hr of -- join middle right
UBT2(y,hy) -> if be0
then spliceH l hl e0 y hy
else joinH l hl y hy
-- e0 = e1
EQ -> case d r0 hr0 r1 of -- right
UBT2(r,hr) -> case d l0 hl0 l1 of -- left
UBT2(l,hl) -> joinH l hl r hr
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
GT -> case forkL e0 r1 of
UBT5(rl1,_ ,be0,rr1,_ ) -> case forkR l0 hl0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT4(ll0,hll0, lr0,hlr0) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case d r0 hr0 rr1 of -- right
UBT2(r,hr) -> case d lr0 hlr0 rl1 of -- middle
UBT2(m,hm) -> case d ll0 hll0 l1 of -- left
UBT2(l,hl) -> case joinH l hl m hm of -- join left middle
UBT2(x,hx) -> if be0
then spliceH x hx e0 r hr
else joinH x hx r hr
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1), and for other algorithmic reasons in this case.
-- N.B. forkL returns True if t1 does not contain e0 (I.E. If e0 is an element of the result).
-- forkL :: a -> AVL b -> UBT5(AVL b, UINT, Bool, AVL b, UINT)
forkL e0 t1 = forkL_ t1 L(0) where
forkL_ E h = UBT5(E,h,True,E,h) -- Relative heights!!
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case comp e0 e of
LT -> case forkL_ l hl of
UBT5(x0,hx0,be0,x1,hx1) -> case spliceH x1 hx1 e r hr of
UBT2(x1_,hx1_) -> UBT5(x0,hx0,be0,x1_,hx1_)
EQ -> UBT5(l,hl,False,r,hr)
GT -> case forkL_ r hr of
UBT5(x0,hx0,be0,x1,hx1) -> case spliceH l hl e x0 hx0 of
UBT2(x0_,hx0_) -> UBT5(x0_,hx0_,be0,x1,hx1)
-- N.B. forkR t0, according to e1. Neither of the resulting forks will contain an element
-- which is "equal" to e1.
-- forkR :: AVL a -> UINT -> b -> UBT4(AVL a, UINT, AVL a, UINT)
forkR t0 ht0 e1 = forkR_ t0 ht0 where
forkR_ E h = UBT4(E,h,E,h) -- Relative heights!!
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case comp e e1 of
LT -> case forkR_ r hr of
UBT4(x0,hx0,x1,hx1) -> case spliceH l hl e x0 hx0 of
UBT2(x0_,hx0_) -> UBT4(x0_,hx0_,x1,hx1)
EQ -> UBT4(l,hl,r,hr) -- e1 is dropped.
GT -> case forkR_ l hl of
UBT4(x0,hx0,x1,hx1) -> case spliceH x1 hx1 e r hr of
UBT2(x1_,hx1_) -> UBT4(x0,hx0,x1_,hx1_)
-----------------------------------------------------------------------
----------------------- differenceH Ends Here -------------------------
-----------------------------------------------------------------------
-- | Similar to _differenceH_, but the resulting tree also includes those elements a\_ for which the
-- combining comparison returns @Eq (Just a\_)@.
--
-- N.B. This function works with relative heights for the first tree and needs no height
-- information for the second tree, so it_s OK to initialise the height of the first to zero,
-- rather than calculating the absolute height. However, if you do this the height of the resulting
-- tree will be incorrect also (it will have the same fixed offset as the first tree).
--
-- Complexity: Not sure, but I_d appreciate it if someone could figure it out.
differenceMaybeH :: (a -> b -> COrdering (Maybe a)) -> AVL a -> UINT -> AVL b -> UBT2(AVL a,UINT)
differenceMaybeH comp = d where
-- d :: AVL a -> UINT -> AVL b -> UBT2(AVL a,UINT)
d E h0 _ = UBT2(E ,h0) -- Relative heights!!
d t0 h0 E = UBT2(t0,h0)
d (N l0 e0 r0) h0 (N l1 e1 r1) = d_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (N l0 e0 r0) h0 (Z l1 e1 r1) = d_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (N l0 e0 r0) h0 (P l1 e1 r1) = d_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (Z l0 e0 r0) h0 (N l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (Z l0 e0 r0) h0 (Z l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (Z l0 e0 r0) h0 (P l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 e1 r1
d (P l0 e0 r0) h0 (N l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 e1 r1
d (P l0 e0 r0) h0 (Z l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 e1 r1
d (P l0 e0 r0) h0 (P l1 e1 r1) = d_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 e1 r1
d_ l0 hl0 e0 r0 hr0 l1 e1 r1 =
case comp e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
Lt -> case forkR r0 hr0 e1 of
UBT5( rl0,hrl0,mbe1,rr0,hrr0) -> case forkL e0 l1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,_ ,mbe0,lr1,_ ) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case d rr0 hrr0 r1 of -- right
UBT2(r,hr) -> case d rl0 hrl0 lr1 of -- middle
UBT2(m,hm) -> case d l0 hl0 ll1 of -- left
UBT2(l,hl) -> case (case mbe1 of
Just e1_ -> spliceH m hm e1_ r hr -- splice middle right with e1_
Nothing -> joinH m hm r hr) of -- join middle right
UBT2(y,hy) -> case mbe0 of
Just e0_ -> spliceH l hl e0_ y hy
Nothing -> joinH l hl y hy
-- e0 = e1
Eq mbe0 -> case d r0 hr0 r1 of -- right
UBT2(r,hr) -> case d l0 hl0 l1 of -- left
UBT2(l,hl) -> case mbe0 of
Just e0_ -> spliceH l hl e0_ r hr -- retain updated e0
Nothing -> joinH l hl r hr -- discard original e0
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
Gt -> case forkL e0 r1 of
UBT5( rl1,_ ,mbe0,rr1,_ ) -> case forkR l0 hl0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT5(ll0,hll0,mbe1,lr0,hlr0) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case d r0 hr0 rr1 of -- right
UBT2(r,hr) -> case d lr0 hlr0 rl1 of -- middle
UBT2(m,hm) -> case d ll0 hll0 l1 of -- left
UBT2(l,hl) -> case (case mbe1 of
Just e1_ -> spliceH l hl e1_ m hm -- splice left middle with e1_
Nothing -> joinH l hl m hm) of -- join left middle
UBT2(x,hx) -> case mbe0 of
Just e0_ -> spliceH x hx e0_ r hr
Nothing -> joinH x hx r hr
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1), and for other algorithmic reasons in this case.
-- N.B. forkL returns (Just e0) if t1 does not contain e0 (I.E. If original e0 is an element of the result).
-- forkL :: a -> AVL b -> UBT5(AVL b, UINT, Maybe a, AVL b, UINT)
forkL e0 t1 = forkL_ t1 L(0) where
forkL_ E h = UBT5(E,h,Just e0,E,h) -- Relative heights!!
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case comp e0 e of
Lt -> case forkL_ l hl of
UBT5(x0,hx0,mbe0,x1,hx1) -> case spliceH x1 hx1 e r hr of
UBT2(x1_,hx1_) -> UBT5(x0,hx0,mbe0,x1_,hx1_)
Eq mbe0 -> UBT5(l,hl,mbe0,r,hr)
Gt -> case forkL_ r hr of
UBT5(x0,hx0,mbe0,x1,hx1) -> case spliceH l hl e x0 hx0 of
UBT2(x0_,hx0_) -> UBT5(x0_,hx0_,mbe0,x1,hx1)
-- N.B. forkR t0, according to e1. Returns Nothing if t0 does not contain e1.
-- forkR :: AVL a -> UINT -> b -> UBT5(AVL a, UINT, Maybe a, AVL a, UINT)
forkR t0 ht0 e1 = forkR_ t0 ht0 where
forkR_ E h = UBT5(E,h,Nothing,E,h) -- Relative heights!!
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case comp e e1 of
Lt -> case forkR_ r hr of
UBT5(x0,hx0,mbe1,x1,hx1) -> case spliceH l hl e x0 hx0 of
UBT2(x0_,hx0_) -> UBT5(x0_,hx0_,mbe1,x1,hx1)
Eq mbe1 -> UBT5(l,hl,mbe1,r,hr)
Gt -> case forkR_ l hl of
UBT5(x0,hx0,mbe1,x1,hx1) -> case spliceH x1 hx1 e r hr of
UBT2(x1_,hx1_) -> UBT5(x0,hx0,mbe1,x1_,hx1_)
-----------------------------------------------------------------------
--------------------- differenceMaybeH Ends Here ----------------------
-----------------------------------------------------------------------
-- | The symmetric difference is the set of elements which occur in one set or the other but /not both/.
--
-- Complexity: Not sure, but I_d appreciate it if someone could figure it out.
symDifferenceH :: (e -> e -> Ordering) -> AVL e -> UINT -> AVL e -> UINT -> UBT2(AVL e,UINT)
symDifferenceH c = u where
-- u :: AVL e -> UINT -> AVL e -> UINT -> UBT2(AVL e,UINT)
u E _ t1 h1 = UBT2(t1,h1)
u t0 h0 E _ = UBT2(t0,h0)
u (N l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (N l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (N l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT2(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u (Z l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (Z l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (Z l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT1(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u (P l0 e0 r0) h0 (N l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT2(h1) e1 r1 DECINT1(h1)
u (P l0 e0 r0) h0 (Z l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT1(h1) e1 r1 DECINT1(h1)
u (P l0 e0 r0) h0 (P l1 e1 r1) h1 = u_ l0 DECINT1(h0) e0 r0 DECINT2(h0) l1 DECINT1(h1) e1 r1 DECINT2(h1)
u_ l0 hl0 e0 r0 hr0 l1 hl1 e1 r1 hr1 =
case c e0 e1 of
-- e0 < e1, so (l0 < e0 < e1) & (e0 < e1 < r1)
LT -> case forkR r0 hr0 e1 of
UBT5(rl0,hrl0,be1,rr0,hrr0) -> case forkL e0 l1 hl1 of -- (e0 < rl0 < e1) & (e0 < e1 < rr0)
UBT5(ll1,hll1,be0,lr1,hlr1) -> -- (ll1 < e0 < e1) & (e0 < lr1 < e1)
-- (l0 + ll1) < e0 < (rl0 + lr1) < e1 < (rr0 + r1)
case u l0 hl0 ll1 hll1 of
UBT2(l,hl) -> case u rl0 hrl0 lr1 hlr1 of
UBT2(m,hm) -> case u rr0 hrr0 r1 hr1 of
UBT2(r,hr) -> case (if be1 then spliceH m hm e1 r hr
else joinH m hm r hr
) of
UBT2(t,ht) -> if be0 then spliceH l hl e0 t ht
else joinH l hl t ht
-- e0 = e1
EQ -> case u l0 hl0 l1 hl1 of
UBT2(l,hl) -> case u r0 hr0 r1 hr1 of
UBT2(r,hr) -> joinH l hl r hr
-- e1 < e0, so (l1 < e1 < e0) & (e1 < e0 < r0)
GT -> case forkL e0 r1 hr1 of
UBT5(rl1,hrl1,be0,rr1,hrr1) -> case forkR l0 hl0 e1 of -- (e1 < rl1 < e0) & (e1 < e0 < rr1)
UBT5(ll0,hll0,be1,lr0,hlr0) -> -- (ll0 < e1 < e0) & (e1 < lr0 < e0)
-- (ll0 + l1) < e1 < (lr0 + rl1) < e0 < (r0 + rr1)
case u ll0 hll0 l1 hl1 of
UBT2(l,hl) -> case u lr0 hlr0 rl1 hrl1 of
UBT2(m,hm) -> case u r0 hr0 rr1 hrr1 of
UBT2(r,hr) -> case (if be1 then spliceH l hl e1 m hm
else joinH l hl m hm
) of
UBT2(t,ht) -> if be0 then spliceH t ht e0 r hr
else joinH t ht r hr
-- We need 2 different versions of fork (L & R) to ensure that comparison arguments are used in
-- the right order (c e0 e1)
-- forkL :: e -> AVL e -> UINT -> UBT5(AVL e,UINT,Bool,AVL e,UINT)
forkL e0 t1 ht1 = forkL_ t1 ht1 where
forkL_ E _ = UBT5(E, L(0), True, E, L(0))
forkL_ (N l e r) h = forkL__ l DECINT2(h) e r DECINT1(h)
forkL_ (Z l e r) h = forkL__ l DECINT1(h) e r DECINT1(h)
forkL_ (P l e r) h = forkL__ l DECINT1(h) e r DECINT2(h)
forkL__ l hl e r hr = case c e0 e of
LT -> case forkL_ l hl of
UBT5(l0,hl0,be0,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,be0,l1_,hl1_)
EQ -> UBT5(l,hl,False,r,hr)
GT -> case forkL_ r hr of
UBT5(l0,hl0,be0,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,be0,l1,hl1)
-- forkR :: AVL e -> UINT -> e -> UBT5(AVL e,UINT,Bool,AVL e,UINT)
forkR t0 ht0 e1 = forkR_ t0 ht0 where
forkR_ E _ = UBT5(E, L(0), True, E, L(0))
forkR_ (N l e r) h = forkR__ l DECINT2(h) e r DECINT1(h)
forkR_ (Z l e r) h = forkR__ l DECINT1(h) e r DECINT1(h)
forkR_ (P l e r) h = forkR__ l DECINT1(h) e r DECINT2(h)
forkR__ l hl e r hr = case c e e1 of
LT -> case forkR_ r hr of
UBT5(l0,hl0,be1,l1,hl1) -> case spliceH l hl e l0 hl0 of
UBT2(l0_,hl0_) -> UBT5(l0_,hl0_,be1,l1,hl1)
EQ -> UBT5(l,hl,False,r,hr)
GT -> case forkR_ l hl of
UBT5(l0,hl0,be1,l1,hl1) -> case spliceH l1 hl1 e r hr of
UBT2(l1_,hl1_) -> UBT5(l0,hl0,be1,l1_,hl1_)
-----------------------------------------------------------------------
----------------------- symDifferenceH Ends Here ----------------------
-----------------------------------------------------------------------