avl_ext.hs

{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module Avl_ext where

import qualified Prelude

#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#if __GLASGOW_HASKELL__ >= 900
import qualified GHC.Exts
#endif
#else
-- HUGS
import qualified IOExts
#endif

#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
#if __GLASGOW_HASKELL__ >= 900
unsafeCoerce = GHC.Exts.unsafeCoerce#
#else
unsafeCoerce = GHC.Base.unsafeCoerce#
#endif
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif

type Pred t = t -> Prelude.Bool

type Rel t = t -> Pred t

type Axiom t = t -> t -> Prelude.Bool

data Mixin_of t =
   Mixin (Rel t) (Axiom t)

op :: (Mixin_of a1) -> Rel a1
op m =
  case m of {
   Mixin op0 _ -> op0}

type Type = Mixin_of Any
  -- singleton inductive, whose constructor was Pack
  
type Sort = Any

class0 :: Type -> Mixin_of Sort
class0 cT =
  cT

eq_op :: Type -> Rel Sort
eq_op t =
  op (class0 t)

type Mixin_of0 t =
  (Pred t) -> Prelude.Integer -> Prelude.Maybe t
  -- singleton inductive, whose constructor was Mixin
  
data Class_of t =
   Class (Mixin_of t) (Mixin_of0 t)

base :: (Class_of a1) -> Mixin_of a1
base c =
  case c of {
   Class base4 _ -> base4}

data Mixin_of1 t0 =
   Mixin0 (Rel Sort) (Rel Sort)

lt :: (Mixin_of a1) -> (Mixin_of1 a1) -> Rel Sort
lt _ m =
  case m of {
   Mixin0 _ lt1 -> lt1}

data Class_of0 t =
   Class0 (Class_of t) (Mixin_of1 t)

base0 :: (Class_of0 a1) -> Class_of a1
base0 c =
  case c of {
   Class0 base4 _ -> base4}

mixin :: (Class_of0 a1) -> Mixin_of1 a1
mixin c =
  case c of {
   Class0 _ mixin0 -> mixin0}

type Type0 = Class_of0 Any
  -- singleton inductive, whose constructor was Pack
  
type Sort0 = Any

class1 :: () -> Type0 -> Class_of0 Sort0
class1 _ cT =
  cT

lt0 :: () -> Type0 -> Rel Sort0
lt0 disp t =
  lt (base (base0 (class1 disp t))) (mixin (class1 disp t))

data Mixin_of2 t0 =
   Mixin1 (Sort0 -> Sort0 -> Sort0) (Sort0 -> Sort0 -> Sort0)

data Class_of1 t =
   Class1 (Class_of0 t) (Mixin_of2 t)

base1 :: (Class_of1 a1) -> Class_of0 a1
base1 c =
  case c of {
   Class1 base4 _ -> base4}

type Class_of2 t = Class_of1 t
  -- singleton inductive, whose constructor was Class
  
base2 :: (Class_of2 a1) -> Class_of1 a1
base2 c =
  c

type Class_of3 t = Class_of2 t
  -- singleton inductive, whose constructor was Class
  
base3 :: (Class_of3 a1) -> Class_of2 a1
base3 c =
  c

type Type1 = Class_of3 Any
  -- singleton inductive, whose constructor was Pack
  
type Sort1 = Any

class2 :: () -> Type1 -> Class_of3 Sort1
class2 _ cT =
  cT

eqType :: () -> Type1 -> Type
eqType disp cT =
  base (base0 (base1 (base2 (base3 (class2 disp cT)))))

porderType :: () -> Type1 -> Type0
porderType disp cT =
  base1 (base2 (base3 (class2 disp cT)))

data Tree a =
   Leaf
 | Node (Tree a) a (Tree a)

leaf :: Tree a1
leaf =
  Leaf

is_node :: (Tree a1) -> Prelude.Bool
is_node t =
  case t of {
   Leaf -> Prelude.False;
   Node _ _ _ -> Prelude.True}

cmp :: () -> Type1 -> Sort1 -> Sort1 -> Base.Ordering
cmp disp t x y =
  case lt0 disp (porderType disp t) x y of {
   Prelude.True -> Base.LT;
   Prelude.False -> case eq_op (eqType disp t) x y of {
                     Prelude.True -> Base.EQ;
                     Prelude.False -> Base.GT}}

isin_a :: () -> Type1 -> (Tree ((,) Sort1 a1)) -> Sort1 -> Prelude.Bool
isin_a disp t t0 x =
  case t0 of {
   Leaf -> Prelude.False;
   Node l p r ->
    case p of {
     (,) a _ ->
      case cmp disp t x a of {
       Base.LT -> isin_a disp t l x;
       Base.EQ -> Prelude.True;
       Base.GT -> isin_a disp t r x}}}

data Bal0 =
   Lh
 | Bal
 | Rh

eqbal :: Bal0 -> Bal0 -> Prelude.Bool
eqbal b1 b2 =
  case b1 of {
   Lh -> case b2 of {
          Lh -> Prelude.True;
          _ -> Prelude.False};
   Bal -> case b2 of {
           Bal -> Prelude.True;
           _ -> Prelude.False};
   Rh -> case b2 of {
          Rh -> Prelude.True;
          _ -> Prelude.False}}

eqbalP :: Axiom Bal0
eqbalP __top_assumption_ =
  let {
   _evar_0_ = \__top_assumption_0 ->
    let {_evar_0_ = Prelude.True} in
    let {_evar_0_0 = Prelude.False} in
    let {_evar_0_1 = Prelude.False} in
    case __top_assumption_0 of {
     Lh -> _evar_0_;
     Bal -> _evar_0_0;
     Rh -> _evar_0_1}}
  in
  let {
   _evar_0_0 = \__top_assumption_0 ->
    let {_evar_0_0 = Prelude.False} in
    let {_evar_0_1 = Prelude.True} in
    let {_evar_0_2 = Prelude.False} in
    case __top_assumption_0 of {
     Lh -> _evar_0_0;
     Bal -> _evar_0_1;
     Rh -> _evar_0_2}}
  in
  let {
   _evar_0_1 = \__top_assumption_0 ->
    let {_evar_0_1 = Prelude.False} in
    let {_evar_0_2 = Prelude.False} in
    let {_evar_0_3 = Prelude.True} in
    case __top_assumption_0 of {
     Lh -> _evar_0_1;
     Bal -> _evar_0_2;
     Rh -> _evar_0_3}}
  in
  case __top_assumption_ of {
   Lh -> _evar_0_;
   Bal -> _evar_0_0;
   Rh -> _evar_0_1}

bal_eqMixin :: Mixin_of Bal0
bal_eqMixin =
  Mixin eqbal eqbalP

bal_eqType :: Type
bal_eqType =
  unsafeCoerce bal_eqMixin

type Tree_bal a = Tree ((,) a Bal0)

is_bal :: (Tree_bal a1) -> Prelude.Bool
is_bal t =
  case t of {
   Leaf -> Prelude.False;
   Node _ p _ -> case p of {
                  (,) _ b -> eq_op bal_eqType (unsafeCoerce b) (unsafeCoerce Bal)}}

incr :: (Tree_bal a1) -> (Tree_bal a1) -> Prelude.Bool
incr t t' =
  (Prelude.||) (Prelude.not (is_node t)) ((Prelude.&&) (is_bal t) (Prelude.not (is_bal t')))

rot2 :: (Tree_bal a1) -> a1 -> (Tree_bal a1) -> a1 -> (Tree_bal a1) -> Tree_bal a1
rot2 a x b z c =
  case b of {
   Leaf -> leaf;
   Node b1 p b2 ->
    case p of {
     (,) y bb ->
      let {
       bb1 = case eq_op bal_eqType (unsafeCoerce bb) (unsafeCoerce Rh) of {
              Prelude.True -> Lh;
              Prelude.False -> Bal}}
      in
      let {
       bb2 = case eq_op bal_eqType (unsafeCoerce bb) (unsafeCoerce Lh) of {
              Prelude.True -> Rh;
              Prelude.False -> Bal}}
      in
      Node (Node a ((,) x bb1) b1) ((,) y Bal) (Node b2 ((,) z bb2) c)}}

balL_b :: (Tree_bal a1) -> a1 -> Bal0 -> (Tree_bal a1) -> Tree_bal a1
balL_b ab z bb c =
  case bb of {
   Lh ->
    case ab of {
     Leaf -> leaf;
     Node a p b ->
      case p of {
       (,) x b0 ->
        case b0 of {
         Lh -> Node a ((,) x Bal) (Node b ((,) z Bal) c);
         Bal -> Node a ((,) x Rh) (Node b ((,) z Lh) c);
         Rh -> rot2 a x b z c}}};
   Bal -> Node ab ((,) z Lh) c;
   Rh -> Node ab ((,) z Bal) c}

balR_b :: (Tree_bal a1) -> a1 -> Bal0 -> (Tree_bal a1) -> Tree_bal a1
balR_b a x bb bc =
  case bb of {
   Lh -> Node a ((,) x Bal) bc;
   Bal -> Node a ((,) x Rh) bc;
   Rh ->
    case bc of {
     Leaf -> leaf;
     Node b p c ->
      case p of {
       (,) z b0 ->
        case b0 of {
         Lh -> rot2 a x b z c;
         Bal -> Node (Node a ((,) x Rh) b) ((,) z Lh) c;
         Rh -> Node (Node a ((,) x Bal) b) ((,) z Bal) c}}}}

insert_b :: () -> Type1 -> Sort1 -> (Tree_bal Sort1) -> Tree_bal Sort1
insert_b disp t x t0 =
  case t0 of {
   Leaf -> Node leaf ((,) x Bal) leaf;
   Node l p r ->
    case p of {
     (,) a b ->
      case cmp disp t x a of {
       Base.LT ->
        let {l' = insert_b disp t x l} in
        case incr l l' of {
         Prelude.True -> balL_b l' a b r;
         Prelude.False -> Node l' ((,) a b) r};
       Base.EQ -> Node l ((,) a b) r;
       Base.GT ->
        let {r' = insert_b disp t x r} in
        case incr r r' of {
         Prelude.True -> balR_b l a b r';
         Prelude.False -> Node l ((,) a b) r'}}}}

decr :: (Tree_bal a1) -> (Tree_bal a1) -> Prelude.Bool
decr t t' =
  (Prelude.&&) (is_node t)
    ((Prelude.||) (Prelude.not (is_node t')) ((Prelude.&&) (Prelude.not (is_bal t)) (is_bal t')))

split_max_b :: (Tree_bal a1) -> a1 -> Bal0 -> (Tree_bal a1) -> (,) (Tree_bal a1) a1
split_max_b l a ba r =
  case r of {
   Leaf -> (,) l a;
   Node lr p rr ->
    case p of {
     (,) ar br ->
      case split_max_b lr ar br rr of {
       (,) r' a' ->
        let {
         t' = case decr r r' of {
               Prelude.True -> balL_b l a ba r';
               Prelude.False -> Node l ((,) a ba) r'}}
        in
        (,) t' a'}}}

delete_b :: () -> Type1 -> Sort1 -> (Tree_bal Sort1) -> Tree_bal Sort1
delete_b disp t x t0 =
  case t0 of {
   Leaf -> leaf;
   Node l p r ->
    case p of {
     (,) a ba ->
      case cmp disp t x a of {
       Base.LT ->
        let {l' = delete_b disp t x l} in
        case decr l l' of {
         Prelude.True -> balR_b l' a ba r;
         Prelude.False -> Node l' ((,) a ba) r};
       Base.EQ ->
        case l of {
         Leaf -> r;
         Node ll p0 rl ->
          case p0 of {
           (,) al bl ->
            case split_max_b ll al bl rl of {
             (,) l' a' ->
              case decr l l' of {
               Prelude.True -> balR_b l' a' ba r;
               Prelude.False -> Node l' ((,) a' ba) r}}}};
       Base.GT ->
        let {r' = delete_b disp t x r} in
        case decr r r' of {
         Prelude.True -> balL_b l a ba r';
         Prelude.False -> Node l ((,) a ba) r'}}}}