module Data.Tree.AVL.Set
(
genUnion,genUnionMaybe,genUnions,
genDifference,genDifferenceMaybe,genSymDifference,
genIntersection,genIntersectionMaybe,
genIntersectionToListL,genIntersectionAsListL,
genIntersectionMaybeToListL,genIntersectionMaybeAsListL,
genIsSubsetOf,genIsSubsetOfBy
) where
import Prelude
import Data.Tree.AVL.Types(AVL(..))
import Data.Tree.AVL.Height(addHeight)
import Data.Tree.AVL.Internals.HJoin(spliceH)
import Data.Tree.AVL.Internals.HSet(unionH,unionMaybeH,
intersectionH,intersectionMaybeH,
differenceH,differenceMaybeH,symDifferenceH)
import Data.COrdering
#ifdef __GLASGOW_HASKELL__
import GHC.Base
#include "ghcdefs.h"
#else
#include "h98defs.h"
#endif
genUnion :: (e -> e -> COrdering e) -> AVL e -> AVL e -> AVL e
genUnion c = gu where
gu E t1 = t1
gu t0 E = t0
gu t0@(N l0 _ _ ) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(2) l1)
gu t0@(N l0 _ _ ) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(1) l1)
gu t0@(N l0 _ _ ) t1@(P _ _ r1) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(2) r1)
gu t0@(Z l0 _ _ ) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(2) l1)
gu t0@(Z l0 _ _ ) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(1) l1)
gu t0@(Z l0 _ _ ) t1@(P _ _ r1) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(2) r1)
gu t0@(P _ _ r0) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(2) l1)
gu t0@(P _ _ r0) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(1) l1)
gu t0@(P _ _ r0) t1@(P _ _ r1) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(2) r1)
gu_ t0 h0 t1 h1 = case unionH c t0 h0 t1 h1 of UBT2(t,_) -> t
genUnionMaybe :: (e -> e -> COrdering (Maybe e)) -> AVL e -> AVL e -> AVL e
genUnionMaybe c = gu where
gu E t1 = t1
gu t0 E = t0
gu t0@(N l0 _ _ ) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(2) l1)
gu t0@(N l0 _ _ ) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(1) l1)
gu t0@(N l0 _ _ ) t1@(P _ _ r1) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(2) r1)
gu t0@(Z l0 _ _ ) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(2) l1)
gu t0@(Z l0 _ _ ) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(1) l1)
gu t0@(Z l0 _ _ ) t1@(P _ _ r1) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(2) r1)
gu t0@(P _ _ r0) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(2) l1)
gu t0@(P _ _ r0) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(1) l1)
gu t0@(P _ _ r0) t1@(P _ _ r1) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(2) r1)
gu_ t0 h0 t1 h1 = case unionMaybeH c t0 h0 t1 h1 of UBT2(t,_) -> t
genUnions :: (e -> e -> COrdering e) -> [AVL e] -> AVL e
genUnions c = gus E L(0) where
gus a _ [] = a
gus a ha ( E :avls) = gus a ha avls
gus a ha (t@(N l _ _):avls) = case unionH c a ha t (addHeight L(2) l) of UBT2(a_,ha_) -> gus a_ ha_ avls
gus a ha (t@(Z l _ _):avls) = case unionH c a ha t (addHeight L(1) l) of UBT2(a_,ha_) -> gus a_ ha_ avls
gus a ha (t@(P _ _ r):avls) = case unionH c a ha t (addHeight L(2) r) of UBT2(a_,ha_) -> gus a_ ha_ avls
genIntersection :: (a -> b -> COrdering c) -> AVL a -> AVL b -> AVL c
genIntersection c t0 t1 = case intersectionH c t0 t1 of UBT2(t,_) -> t
genIntersectionMaybe :: (a -> b -> COrdering (Maybe c)) -> AVL a -> AVL b -> AVL c
genIntersectionMaybe c t0 t1 = case intersectionMaybeH c t0 t1 of UBT2(t,_) -> t
genIntersectionToListL :: (a -> b -> COrdering c) -> AVL a -> AVL b -> [c] -> [c]
genIntersectionToListL comp = i where
i E _ cs = cs
i _ E cs = cs
i (N l0 e0 r0) (N l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (N l0 e0 r0) (Z l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (N l0 e0 r0) (P l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (Z l0 e0 r0) (N l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (Z l0 e0 r0) (Z l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (Z l0 e0 r0) (P l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (P l0 e0 r0) (N l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (P l0 e0 r0) (Z l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (P l0 e0 r0) (P l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i' l0 e0 r0 l1 e1 r1 cs =
case comp e0 e1 of
Lt -> case forkR r0 e1 of
UBT5(rl0,_,mbc1,rr0,_) -> case forkL e0 l1 of
UBT5(ll1,_,mbc0,lr1,_) ->
let cs' = i rr0 r1 cs
cs'' = cs' `seq` case mbc1 of
Nothing -> i rl0 lr1 cs'
Just c1 -> i rl0 lr1 (c1:cs')
in cs'' `seq` case mbc0 of
Nothing -> i l0 ll1 cs''
Just c0 -> i l0 ll1 (c0:cs'')
Eq c -> let cs' = i r0 r1 cs in cs' `seq` i l0 l1 (c:cs')
Gt -> case forkL e0 r1 of
UBT5(rl1,_,mbc0,rr1,_) -> case forkR l0 e1 of
UBT5(ll0,_,mbc1,lr0,_) ->
let cs' = i r0 rr1 cs
cs'' = cs' `seq` case mbc0 of
Nothing -> i lr0 rl1 cs'
Just c0 -> i lr0 rl1 (c0:cs')
in cs'' `seq` case mbc1 of
Nothing -> i ll0 l1 cs''
Just c1 -> i ll0 l1 (c1:cs'')
forkL e0 t1 = forkL_ t1 L(0) where
forkL_ E h = UBT5(E,h,Nothing,E,h)
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 t0 e1 = forkR_ t0 L(0) where
forkR_ E h = UBT5(E,h,Nothing,E,h)
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_)
genIntersectionAsListL :: (a -> b -> COrdering c) -> AVL a -> AVL b -> [c]
genIntersectionAsListL c setA setB = genIntersectionToListL c setA setB []
genIntersectionMaybeToListL :: (a -> b -> COrdering (Maybe c)) -> AVL a -> AVL b -> [c] -> [c]
genIntersectionMaybeToListL comp = i where
i E _ cs = cs
i _ E cs = cs
i (N l0 e0 r0) (N l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (N l0 e0 r0) (Z l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (N l0 e0 r0) (P l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (Z l0 e0 r0) (N l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (Z l0 e0 r0) (Z l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (Z l0 e0 r0) (P l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (P l0 e0 r0) (N l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (P l0 e0 r0) (Z l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i (P l0 e0 r0) (P l1 e1 r1) cs = i' l0 e0 r0 l1 e1 r1 cs
i' l0 e0 r0 l1 e1 r1 cs =
case comp e0 e1 of
Lt -> case forkR r0 e1 of
UBT5(rl0,_,mbc1,rr0,_) -> case forkL e0 l1 of
UBT5(ll1,_,mbc0,lr1,_) ->
let cs' = i rr0 r1 cs
cs'' = cs' `seq` case mbc1 of
Nothing -> i rl0 lr1 cs'
Just c1 -> i rl0 lr1 (c1:cs')
in cs'' `seq` case mbc0 of
Nothing -> i l0 ll1 cs''
Just c0 -> i l0 ll1 (c0:cs'')
Eq mbc -> let cs' = i r0 r1 cs in cs' `seq` case mbc of
Nothing -> i l0 l1 cs'
Just c -> i l0 l1 (c:cs')
Gt -> case forkL e0 r1 of
UBT5(rl1,_,mbc0,rr1,_) -> case forkR l0 e1 of
UBT5(ll0,_,mbc1,lr0,_) ->
let cs' = i r0 rr1 cs
cs'' = cs' `seq` case mbc0 of
Nothing -> i lr0 rl1 cs'
Just c0 -> i lr0 rl1 (c0:cs')
in cs'' `seq` case mbc1 of
Nothing -> i ll0 l1 cs''
Just c1 -> i ll0 l1 (c1:cs'')
forkL e0 t1 = forkL_ t1 L(0) where
forkL_ E h = UBT5(E,h,Nothing,E,h)
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 t0 e1 = forkR_ t0 L(0) where
forkR_ E h = UBT5(E,h,Nothing,E,h)
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_)
genIntersectionMaybeAsListL :: (a -> b -> COrdering (Maybe c)) -> AVL a -> AVL b -> [c]
genIntersectionMaybeAsListL c setA setB = genIntersectionMaybeToListL c setA setB []
genDifference :: (a -> b -> Ordering) -> AVL a -> AVL b -> AVL a
genDifference c t0 t1 = case differenceH c t0 L(0) t1 of UBT2(t,_) -> t
genDifferenceMaybe :: (a -> b -> COrdering (Maybe a)) -> AVL a -> AVL b -> AVL a
genDifferenceMaybe c t0 t1 = case differenceMaybeH c t0 L(0) t1 of UBT2(t,_) -> t
genIsSubsetOf :: (a -> b -> Ordering) -> AVL a -> AVL b -> Bool
genIsSubsetOf comp = s where
s E _ = True
s _ E = False
s (N l0 e0 r0) (N l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (N l0 e0 r0) (Z l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (N l0 e0 r0) (P l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (Z l0 e0 r0) (N l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (Z l0 e0 r0) (Z l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (Z l0 e0 r0) (P l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (P l0 e0 r0) (N l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (P l0 e0 r0) (Z l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (P l0 e0 r0) (P l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s' l0 e0 r0 l1 e1 r1 =
case comp e0 e1 of
LT -> case forkL e0 l1 of
UBT5(False,_ ,_,_ ,_) -> False
UBT5(True ,ll1,_,lr1,_) -> (s l0 ll1) && case forkR r0 e1 of
UBT4(rl0,_,rr0,_) -> (s rl0 lr1) && (s rr0 r1)
EQ -> (s l0 l1) && (s r0 r1)
GT -> case forkL e0 r1 of
UBT5(False,_ ,_,_ ,_) -> False
UBT5(True ,rl1,_,rr1,_) -> (s r0 rr1) && case forkR l0 e1 of
UBT4(ll0,_,lr0,_) -> (s lr0 rl1) && (s ll0 l1)
forkL e0 t = forkL_ t L(0) where
forkL_ E h = UBT5(False,E,h,E,h)
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(False,t0,ht0,t1,ht1) -> UBT5(False,t0,ht0,t1,ht1)
UBT5(True ,t0,ht0,t1,ht1) -> case spliceH t1 ht1 e r hr of
UBT2(t1_,ht1_) -> UBT5(True,t0,ht0,t1_,ht1_)
EQ -> UBT5(True,l,hl,r,hr)
GT -> case forkL_ r hr of
UBT5(False,t0,ht0,t1,ht1) -> UBT5(False,t0,ht0,t1,ht1)
UBT5(True ,t0,ht0,t1,ht1) -> case spliceH l hl e t0 ht0 of
UBT2(t0_,ht0_) -> UBT5(True,t0_,ht0_,t1,ht1)
forkR t e1 = forkR_ t L(0) where
forkR_ E h = UBT4(E,h,E,h)
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(t0,ht0,t1,ht1) -> case spliceH l hl e t0 ht0 of
UBT2(t0_,ht0_) -> UBT4(t0_,ht0_,t1,ht1)
EQ -> UBT4(l,hl,r,hr)
GT -> case forkR_ l hl of
UBT4(t0,ht0,t1,ht1) -> case spliceH t1 ht1 e r hr of
UBT2(t1_,ht1_) -> UBT4(t0,ht0,t1_,ht1_)
genIsSubsetOfBy :: (a -> b -> COrdering Bool) -> AVL a -> AVL b -> Bool
genIsSubsetOfBy comp = s where
s E _ = True
s _ E = False
s (N l0 e0 r0) (N l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (N l0 e0 r0) (Z l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (N l0 e0 r0) (P l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (Z l0 e0 r0) (N l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (Z l0 e0 r0) (Z l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (Z l0 e0 r0) (P l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (P l0 e0 r0) (N l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (P l0 e0 r0) (Z l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s (P l0 e0 r0) (P l1 e1 r1) = s' l0 e0 r0 l1 e1 r1
s' l0 e0 r0 l1 e1 r1 =
case comp e0 e1 of
Lt -> case forkL e0 l1 of
UBT5(False,_ ,_,_ ,_) -> False
UBT5(True ,ll1,_,lr1,_) -> (s l0 ll1) && case forkR r0 e1 of
UBT5(False,_ ,_,_ ,_) -> False
UBT5(True ,rl0,_,rr0,_) -> (s rl0 lr1) && (s rr0 r1)
Eq True -> (s l0 l1) && (s r0 r1)
Eq False -> False
Gt -> case forkL e0 r1 of
UBT5(False,_ ,_,_ ,_) -> False
UBT5(True ,rl1,_,rr1,_) -> (s r0 rr1) && case forkR l0 e1 of
UBT5(False,_ ,_,_ ,_) -> False
UBT5(True ,ll0,_,lr0,_) -> (s lr0 rl1) && (s ll0 l1)
forkL e0 t = forkL_ t L(0) where
forkL_ E h = UBT5(False,E,h,E,h)
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(False,t0,ht0,t1,ht1) -> UBT5(False,t0,ht0,t1,ht1)
UBT5(True ,t0,ht0,t1,ht1) -> case spliceH t1 ht1 e r hr of
UBT2(t1_,ht1_) -> UBT5(True,t0,ht0,t1_,ht1_)
Eq b -> UBT5(b,l,hl,r,hr)
Gt -> case forkL_ r hr of
UBT5(False,t0,ht0,t1,ht1) -> UBT5(False,t0,ht0,t1,ht1)
UBT5(True ,t0,ht0,t1,ht1) -> case spliceH l hl e t0 ht0 of
UBT2(t0_,ht0_) -> UBT5(True,t0_,ht0_,t1,ht1)
forkR t e1 = forkR_ t L(0) where
forkR_ E h = UBT5(True,E,h,E,h)
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(False,t0,ht0,t1,ht1) -> UBT5(False,t0,ht0,t1,ht1)
UBT5(True ,t0,ht0,t1,ht1) -> case spliceH l hl e t0 ht0 of
UBT2(t0_,ht0_) -> UBT5(True,t0_,ht0_,t1,ht1)
Eq b -> UBT5(b,l,hl,r,hr)
Gt -> case forkR_ l hl of
UBT5(False,t0,ht0,t1,ht1) -> UBT5(False,t0,ht0,t1,ht1)
UBT5(True ,t0,ht0,t1,ht1) -> case spliceH t1 ht1 e r hr of
UBT2(t1_,ht1_) -> UBT5(True,t0,ht0,t1_,ht1_)
genSymDifference :: (e -> e -> Ordering) -> AVL e -> AVL e -> AVL e
genSymDifference c = gu where
gu E t1 = t1
gu t0 E = t0
gu t0@(N l0 _ _ ) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(2) l1)
gu t0@(N l0 _ _ ) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(1) l1)
gu t0@(N l0 _ _ ) t1@(P _ _ r1) = gu_ t0 (addHeight L(2) l0) t1 (addHeight L(2) r1)
gu t0@(Z l0 _ _ ) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(2) l1)
gu t0@(Z l0 _ _ ) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(1) l1)
gu t0@(Z l0 _ _ ) t1@(P _ _ r1) = gu_ t0 (addHeight L(1) l0) t1 (addHeight L(2) r1)
gu t0@(P _ _ r0) t1@(N l1 _ _ ) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(2) l1)
gu t0@(P _ _ r0) t1@(Z l1 _ _ ) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(1) l1)
gu t0@(P _ _ r0) t1@(P _ _ r1) = gu_ t0 (addHeight L(2) r0) t1 (addHeight L(2) r1)
gu_ t0 h0 t1 h1 = case symDifferenceH c t0 h0 t1 h1 of UBT2(t,_) -> t