{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-missing-export-lists #-}
{-# OPTIONS_GHC -Wno-missing-exported-signatures #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.Tree.AVL.FullExtern.Examples where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.FullExtern
  ( AVL (AVL),
    ITree (EmptyITree),
    delete,
    insert,
    lookup,
    mkAVL,
  )
import Data.Tree.ITree (ITree (EmptyITree, ForkITree))
import Data.Tree.Node (mkNode)
import Prelude (Bool (False, True), Float, Int, ($))

-- | Proxies for the node keys
p0 :: Proxy 0
p0 = Proxy 0
forall {k} (t :: k). Proxy t
Proxy :: Proxy 0

p1 :: Proxy 1
p1 = Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1

p2 :: Proxy 2
p2 = Proxy 2
forall {k} (t :: k). Proxy t
Proxy :: Proxy 2

p3 :: Proxy 3
p3 = Proxy 3
forall {k} (t :: k). Proxy t
Proxy :: Proxy 3

p4 :: Proxy 4
p4 = Proxy 4
forall {k} (t :: k). Proxy t
Proxy :: Proxy 4

p5 :: Proxy 5
p5 = Proxy 5
forall {k} (t :: k). Proxy t
Proxy :: Proxy 5

p6 :: Proxy 6
p6 = Proxy 6
forall {k} (t :: k). Proxy t
Proxy :: Proxy 6

p7 :: Proxy 7
p7 = Proxy 7
forall {k} (t :: k). Proxy t
Proxy :: Proxy 7

emptyTree :: ITree 'EmptyTree
emptyTree = ITree 'EmptyTree
EmptyITree

-- | Insert several values in a row and check the BST and AVL invariants at the end
avl :: AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
avl = ITree
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree
              'EmptyTree
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
forall (t :: Tree). (IsBSTC t, IsBalancedC t) => ITree t -> AVL t
mkAVL ITree
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
t
  where
    t :: ITree
  (Insert
     4
     Char
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree)))
t =
      Node 4 Char
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Insert
        4
        Char
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 4 -> Char -> Node 4 Char
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 4
p4 Char
'f') (ITree
   ('ForkTree
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
         (Node 2 Int)
         ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
      (Node 5 [Int])
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
         (Node 7 [Bool])
         'EmptyTree))
 -> ITree
      (Insert
         4
         Char
         ('ForkTree
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
               (Node 2 Int)
               ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
            (Node 5 [Int])
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
               (Node 7 [Bool])
               'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Insert
        4
        Char
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
        Node 2 Int
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Insert
        2
        Int
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 2 -> Int -> Node 2 Int
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 2
p2 (Int
4 :: Int)) (ITree
   ('ForkTree
      ('ForkTree
         'EmptyTree
         (Node 0 Float)
         ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
      (Node 5 [Int])
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
         (Node 7 [Bool])
         'EmptyTree))
 -> ITree
      (Insert
         2
         Int
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
            (Node 5 [Int])
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
               (Node 7 [Bool])
               'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Insert
        2
        Int
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
          Node 6 [Char]
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Insert
        6
        [Char]
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 6 -> [Char] -> Node 6 [Char]
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 6
p6 [Char]
"lala") (ITree
   ('ForkTree
      ('ForkTree
         'EmptyTree
         (Node 0 Float)
         ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
      (Node 5 [Int])
      ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
 -> ITree
      (Insert
         6
         [Char]
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
            (Node 5 [Int])
            ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Insert
        6
        [Char]
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
            Node 3 Bool
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 5 [Int])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Insert
        3
        Bool
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 3 -> Bool -> Node 3 Bool
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 3
p3 Bool
True) (ITree
   ('ForkTree
      ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
      (Node 5 [Int])
      ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
 -> ITree
      (Insert
         3
         Bool
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
            (Node 5 [Int])
            ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 5 [Int])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Insert
        3
        Bool
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
              Node 5 [Int]
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        5
        [Int]
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 5 -> [Int] -> Node 5 [Int]
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 5
p5 ([Int
1, Int
2, Int
3] :: [Int])) (ITree
   ('ForkTree
      ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Insert
         5
         [Int]
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        5
        [Int]
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$
                Node 0 Float
-> ITree ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)
-> ITree
     (Insert 0 Float ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 0 -> Float -> Node 0 Float
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 0
p0 (Float
1.8 :: Float)) (ITree ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)
 -> ITree
      (Insert 0 Float ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> ITree ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)
-> ITree
     (Insert 0 Float ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
forall a b. (a -> b) -> a -> b
$
                  Node 7 [Bool]
-> ITree 'EmptyTree -> ITree (Insert 7 [Bool] 'EmptyTree)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert (Proxy 7 -> [Bool] -> Node 7 [Bool]
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy 7
p7 [Bool
False]) ITree 'EmptyTree
emptyTree

-- | For performing a lookup, it's necessary to take the ITree @t@ out of the AVL constructor
l1' :: [Char]
l1' = case AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
avl of
  AVL ITree
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
t IsBSTT
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
_ IsBalancedT
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
_ -> Proxy 6
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree
              'EmptyTree
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> [Char]
forall (x :: Nat) a (t :: Tree) (l :: Tree) (n :: Nat) a1
       (r :: Tree).
(Lookupable x a t, t ~ 'ForkTree l (Node n a1) r,
 Member x t t ~ 'True) =>
Proxy x -> ITree t -> a
lookup Proxy 6
p6 ITree
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
t

-- | Compile time error: key 1 is not in the tree avl and left subtree at node with key 4 has height +2 greater than the right subtree
-- avlError = mkAVL $
--   ForkITree (ForkITree
--             (ForkITree
--               EmptyITree (mkNode p0 'a') EmptyITree)
--               (mkNode p7 4)
--               EmptyITree)
--             (mkNode p4 'f')
--             EmptyITree

-- | Delete several values in a row and check the BST and AVL invariants at the end
avlt2 :: AVL 'EmptyTree
avlt2 = case AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
avl of
  AVL ITree
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
t IsBSTT
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
_ IsBalancedT
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
_ -> ITree 'EmptyTree -> AVL 'EmptyTree
forall (t :: Tree). (IsBSTC t, IsBalancedC t) => ITree t -> AVL t
mkAVL ITree 'EmptyTree
ITree (Delete 7 ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
t'
    where
      t' :: ITree (Delete 7 ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
t' =
        Proxy 7
-> ITree ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)
-> ITree
     (Delete 7 ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 7
p7 (ITree ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)
 -> ITree
      (Delete 7 ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> ITree ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)
-> ITree
     (Delete 7 ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
forall a b. (a -> b) -> a -> b
$
          Proxy 4
-> ITree
     ('ForkTree
        'EmptyTree
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        4
        ('ForkTree
           'EmptyTree
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 4
p4 (ITree
   ('ForkTree
      'EmptyTree
      (Node 4 Char)
      ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
 -> ITree
      (Delete
         4
         ('ForkTree
            'EmptyTree
            (Node 4 Char)
            ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
-> ITree
     ('ForkTree
        'EmptyTree
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        4
        ('ForkTree
           'EmptyTree
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
            Proxy 1
-> ITree
     ('ForkTree
        'EmptyTree
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        1
        ('ForkTree
           'EmptyTree
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 1
p1 (ITree
   ('ForkTree
      'EmptyTree
      (Node 4 Char)
      ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
 -> ITree
      (Delete
         1
         ('ForkTree
            'EmptyTree
            (Node 4 Char)
            ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
-> ITree
     ('ForkTree
        'EmptyTree
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        1
        ('ForkTree
           'EmptyTree
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
              Proxy 0
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        0
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 0
p0 (ITree
   ('ForkTree
      ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
      (Node 4 Char)
      ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
 -> ITree
      (Delete
         0
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
            (Node 4 Char)
            ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        0
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$
                Proxy 2
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           'EmptyTree)
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        2
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              'EmptyTree)
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 2
p2 (ITree
   ('ForkTree
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
         (Node 2 Int)
         'EmptyTree)
      (Node 4 Char)
      ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
 -> ITree
      (Delete
         2
         ('ForkTree
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
               (Node 2 Int)
               'EmptyTree)
            (Node 4 Char)
            ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           'EmptyTree)
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))
-> ITree
     (Delete
        2
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              'EmptyTree)
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$ Proxy 6
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           'EmptyTree)
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Delete
        6
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              'EmptyTree)
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 6
p6 (ITree
   ('ForkTree
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
         (Node 2 Int)
         'EmptyTree)
      (Node 4 Char)
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
         (Node 7 [Bool])
         'EmptyTree))
 -> ITree
      (Delete
         6
         ('ForkTree
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
               (Node 2 Int)
               'EmptyTree)
            (Node 4 Char)
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
               (Node 7 [Bool])
               'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           'EmptyTree)
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Delete
        6
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              'EmptyTree)
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall a b. (a -> b) -> a -> b
$ Proxy 5
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Delete
        5
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 5
p5 (ITree
   ('ForkTree
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
         (Node 2 Int)
         ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
      (Node 5 [Int])
      ('ForkTree
         ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
         (Node 7 [Bool])
         'EmptyTree))
 -> ITree
      (Delete
         5
         ('ForkTree
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
               (Node 2 Int)
               ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
            (Node 5 [Int])
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
               (Node 7 [Bool])
               'EmptyTree))))
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Delete
        5
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall a b. (a -> b) -> a -> b
$ Proxy 3
-> ITree
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree
              'EmptyTree
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
        (Node 5 [Int])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
-> ITree
     (Delete
        3
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 3 Bool)
                 ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
           (Node 5 [Int])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
              (Node 7 [Bool])
              'EmptyTree)))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy 3
p3 ITree
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree
           'EmptyTree
           (Node 3 Bool)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)))
     (Node 5 [Int])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree))
t