{-# LANGUAGE GADTs, EmptyDataDecls, RankNTypes #-}
module Example where

data Tree = Bin Tree Tree | Leaf Int deriving Show

type T_Tree = T_Tree_s1

data T_Tree_s1  where  C_Tree_s1  ::  { inv_Tree_s1  :: forall t . K_Tree_s1  t ->  t }  ->  T_Tree_s1
data T_Tree_s2  where  C_Tree_s2  ::  { inv_Tree_s2  :: forall t . K_Tree_s2  t ->  t }  ->  T_Tree_s2
data T_Tree_s3  where  C_Tree_s3  ::  { inv_Tree_s3  :: forall t . K_Tree_s3  t ->  t }  ->  T_Tree_s3

data K_Tree_s1 t where
  K_Tree_v1 :: K_Tree_s1 T_Tree_v1
  K_Tree_v3 :: K_Tree_s1 T_Tree_v3

data K_Tree_s2 t where
  K_Tree_v2 :: K_Tree_s2 T_Tree_v2

data K_Tree_s3 t where  -- empty data declaration

type T_Tree_v1  =         IO (Int,         T_Tree_s2)
type T_Tree_v2  = Int ->  IO (Tree,        T_Tree_s3)
type T_Tree_v3  = Int ->  IO (Int,  Tree,  T_Tree_s3)


tree = sem_Bin (sem_Leaf 5) (sem_Bin (sem_Leaf 2) (sem_Leaf 3))
tst1 = do (_, repl, _) <- inv_Tree_s1 tree K_Tree_v3 2
          putStrLn (show repl)


sem_Leaf :: Int -> T_Tree
sem_Leaf field_x = st1 where
  st1        =  let     k1 :: K_Tree_s1 t -> t
                        k1 K_Tree_v1  = v1
                        k1 K_Tree_v3  = v3
--                        k1 _          = error "unreachable"

                        v1            = do  loc_x <- return f1
                                            lhs_gath  <- return . id $ id loc_x
                                            return (lhs_gath, st2)

                        v3 lhs_mini   = do  loc_x <- return f1
                                            lhs_gath  <- return . id $ id loc_x
                                            lhs_repl  <- return . id $ f2 lhs_mini
                                            return (lhs_gath, lhs_repl, st3)
                in      C_Tree_s1 k1

  st2        =  let     k2 :: K_Tree_s2 t -> t
                        k2 K_Tree_v2  = v2
--                        k2 _          = error "unreachable"

                        v2 lhs_mini   =  do lhs_repl  <- return . id $ f2 lhs_mini
                                            return (lhs_repl, st3)
                in      C_Tree_s2 k2
  st3        =  let     k3 :: K_Tree_s3 t -> t
                        k3 _          = error "unreachable"
                in      C_Tree_s3 k3

  f1   = field_x
  f2   = Leaf


sem_Bin :: T_Tree -> T_Tree -> T_Tree
sem_Bin field_l field_r = st1 where
  st1        =  let     k1 :: K_Tree_s1 t -> t
                        k1 K_Tree_v1  = v1
                        k1 K_Tree_v3  = v3
--                        k1 _          = error "unreachable"

                        v1 :: T_Tree_v1
                        v1            = do  l1 <- return f1
                                            r1 <- return f2
                                            (l_gath, l2)  <- inv_Tree_s1 l1 K_Tree_v1
                                            (r_gath, r2)  <- inv_Tree_s1 r1 K_Tree_v1
                                            lhs_gath      <- return . id $ f3 l_gath r_gath
                                            return (lhs_gath, st2 l2 r2 l_gath r_gath)

                        v3 :: T_Tree_v3
                        v3 lhs_mini   = do  l1             <- return f1
                                            r1             <- return f2
                                            (l_gath, l2)   <- inv_Tree_s1 l1 K_Tree_v1
                                            (r_gath, r2)   <- inv_Tree_s1 r1 K_Tree_v1
                                            lhs_gath       <- return . id $ f3 l_gath r_gath
                                            l_mini         <- return . id $ id r_gath
                                            r_mini         <- return . id $ id l_gath
                                            (l_repl, l3)   <- inv_Tree_s2 l2 K_Tree_v2 l_mini
                                            (r_repl, r3)   <- inv_Tree_s2 r2 K_Tree_v2 r_mini
                                            lhs_repl       <- return . id $ f4 l_repl r_repl
                                            return (lhs_gath, lhs_repl, st3)
                in      C_Tree_s1 k1

  st2 l2 r2 l_gath r_gath
             =  let     k2 :: K_Tree_s2 t -> t
                        k2 K_Tree_v2  = v2
--                        k2 _          = error "unreachable"

                        v2 :: T_Tree_v2
                        v2 lhs_mini   =  do  l_mini         <- return . id $ id r_gath
                                             r_mini         <- return . id $ id l_gath
                                             (l_repl, l3)   <- inv_Tree_s2 l2 K_Tree_v2 l_mini
                                             (r_repl, r3)   <- inv_Tree_s2 r2 K_Tree_v2 r_mini
                                             lhs_repl       <- return . id $ f4 l_repl r_repl
                                             return (lhs_repl, st3)
                in      C_Tree_s2 k2

  st3        =  let     k3 :: K_Tree_s3 t -> t
                        k3 _          = error "unreachable"
                in      C_Tree_s3 k3

  f1  = field_l
  f2  = field_r
  f3  = min
  f4  = Bin