{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Safe #-}
{-# 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.BST.FullExtern.Examples where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.FullExtern
  ( BST (BST),
    ITree (EmptyITree),
    delete,
    insert,
    lookup,
    mkBST,
  )
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 invariants at the end
bst :: BST
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
bst = ITree
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
-> BST
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 3 Bool)
                 ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
forall (t :: Tree). IsBSTC t => ITree t -> BST t
mkBST ITree
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
t
  where
    t :: ITree
  (Insert
     4
     Char
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 3 Bool)
                 'EmptyTree)
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree))
t =
      Node 4 Char
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 3 Bool)
                 'EmptyTree)
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        4
        Char
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree
                    ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                    (Node 3 Bool)
                    'EmptyTree)
                 (Node 5 [Int])
                 ('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
         'EmptyTree
         (Node 0 Float)
         ('ForkTree
            ('ForkTree
               ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
               (Node 3 Bool)
               'EmptyTree)
            (Node 5 [Int])
            ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Insert
         4
         Char
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree
                  ('ForkTree
                     ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                     (Node 3 Bool)
                     'EmptyTree)
                  (Node 5 [Int])
                  ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 3 Bool)
                 'EmptyTree)
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        4
        Char
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree
                    ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                    (Node 3 Bool)
                    'EmptyTree)
                 (Node 5 [Int])
                 ('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
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        2
        Int
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
                 (Node 5 [Int])
                 ('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
            ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
            (Node 5 [Int])
            ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Insert
         2
         Int
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree
                  ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
                  (Node 5 [Int])
                  ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        2
        Int
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
                 (Node 5 [Int])
                 ('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
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
              (Node 5 [Int])
              'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        6
        [Char]
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
                 (Node 5 [Int])
                 '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
            ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
            (Node 5 [Int])
            'EmptyTree))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Insert
         6
         [Char]
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree
                  ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
                  (Node 5 [Int])
                  'EmptyTree))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
              (Node 5 [Int])
              'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        6
        [Char]
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree)
                 (Node 5 [Int])
                 'EmptyTree))
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$
            Node 3 Bool
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        3
        Bool
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 5 [Int]) '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)
         ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Insert
         3
         Bool
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Insert
        3
        Bool
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 5 [Int]) '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

-- bstError = mkBST $
--   ForkITree (ForkITree EmptyITree (mkNode p7 4) EmptyITree)
--             (mkNode p4 'f')
--             EmptyITree

-- | For performing a lookup, it's necessary to take the ITree @t@ out of the BST constructor
l1 :: [Char]
l1 = case BST
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
bst of
  BST ITree
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
t IsBSTT
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
_ -> Proxy 6
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 3 Bool)
                 ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
              (Node 5 [Int])
              ('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
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
t

-- -- | Error: key 1 is not in the tree bst
-- err = case bst of
--     BST t _ -> lookup p1 t

-- | Delete several values in a row and check the BST invariants at the end
bst2 :: BST 'EmptyTree
bst2 = case BST
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
bst of
  BST ITree
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
t IsBSTT
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
_ -> ITree 'EmptyTree -> BST 'EmptyTree
forall (t :: Tree). IsBSTC t => ITree t -> BST t
mkBST ITree '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
        ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        4
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 4 Char) '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
      ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Delete
         4
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        4
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$
            Proxy 1
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        1
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 4 Char) '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
      ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Delete
         1
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        1
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$
              Proxy 0
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        0
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 4 Char) '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)
         ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Delete
         0
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        0
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$
                Proxy 2
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 4 Char)
              'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        2
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 4 Char)
                 '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
         'EmptyTree
         (Node 0 Float)
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
            (Node 4 Char)
            'EmptyTree))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Delete
         2
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree
                  ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                  (Node 4 Char)
                  'EmptyTree))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 4 Char)
              'EmptyTree))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        2
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 4 Char)
                 'EmptyTree))
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$ Proxy 6
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 4 Char)
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        6
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 4 Char)
                 ('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
         'EmptyTree
         (Node 0 Float)
         ('ForkTree
            ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
            (Node 4 Char)
            ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Delete
         6
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree
                  ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                  (Node 4 Char)
                  ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 4 Char)
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        6
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 4 Char)
                 ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$ Proxy 5
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 'EmptyTree
                 (Node 2 Int)
                 ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        5
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree
                    'EmptyTree
                    (Node 2 Int)
                    ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
                 (Node 5 [Int])
                 ('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
         'EmptyTree
         (Node 0 Float)
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 2 Int)
               ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
            (Node 5 [Int])
            ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
      (Node 7 [Bool])
      'EmptyTree)
 -> ITree
      (Delete
         5
         ('ForkTree
            ('ForkTree
               'EmptyTree
               (Node 0 Float)
               ('ForkTree
                  ('ForkTree
                     'EmptyTree
                     (Node 2 Int)
                     ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
                  (Node 5 [Int])
                  ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
            (Node 7 [Bool])
            'EmptyTree)))
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 'EmptyTree
                 (Node 2 Int)
                 ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        5
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree
                    'EmptyTree
                    (Node 2 Int)
                    ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
                 (Node 5 [Int])
                 ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
           (Node 7 [Bool])
           'EmptyTree))
forall a b. (a -> b) -> a -> b
$ Proxy 3
-> ITree
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 0 Float)
           ('ForkTree
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                 (Node 3 Bool)
                 ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
              (Node 5 [Int])
              ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
        (Node 7 [Bool])
        'EmptyTree)
-> ITree
     (Delete
        3
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 0 Float)
              ('ForkTree
                 ('ForkTree
                    ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
                    (Node 3 Bool)
                    ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
                 (Node 5 [Int])
                 ('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
        'EmptyTree
        (Node 0 Float)
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
              (Node 3 Bool)
              ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
           (Node 5 [Int])
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
     (Node 7 [Bool])
     'EmptyTree)
t