{-# LANGUAGE EmptyDataDecls, TypeFamilies, TemplateHaskell, FlexibleInstances, TypeOperators, MultiParamTypeClasses, GADTs, UndecidableInstances #-}

{-# OPTIONS_GHC -fcontext-stack=50 #-}

module Examples.ExG where

import qualified Examples.Ex as Ex
import Examples.ReflectAux



data Leaf a; data Branch a

data Zero a; data Even a; data Odd a

concat `fmap` mapM derive
  [''Ex.Tree1, ''Leaf, ''Branch,
   ''Ex.Even, ''Zero, ''Even,
   ''Ex.Odd, ''Odd]

type instance Tag (Leaf a) = $(return $ encode "Leaf")
newtype instance RM m (N (Leaf a)) = Leaf a
instance (True ~ IsEQ (Compare a a)) => DC (Leaf a) where
  occName _ = "Leaf"
  type Range (Leaf a) = Ex.Tree1 a
  fr ~(Leaf a) = Ex.Leaf a
type instance Rep (Leaf a) = D a
instance Generic (Leaf a) where
  rep ~(Leaf a) = D a
  obj ~(D a) = Leaf a

type instance Tag (Branch a) = $(return $ encode "Branch")
data instance RM m (N (Branch a)) =
  Branch (Med m (Ex.Tree1 a)) (Med m (Ex.Tree1 a))
instance (True ~ IsEQ (Compare a a)) => DC (Branch a) where
  occName _ = "Branch"
  type Range (Branch a) = Ex.Tree1 a
  fr ~(Branch a b) = Ex.Branch a b
type instance Rep (Branch a) = R (Ex.Tree1 a) :* R (Ex.Tree1 a)
instance Generic (Branch a) where
  rep ~(Branch a b) = FF (R a, R b)
  obj ~(FF (R a, R b)) = Branch a b

type instance Inhabitants (DCU (Ex.Tree1 a)) = N (Leaf a) :+ N (Branch a)
instance (True ~ IsEQ (Compare a a)) => DT (Ex.Tree1 a) where
  packageName _ = "yoko-0.1"
  moduleName _ = "Examples.ExG"
  type Siblings (Ex.Tree1 a) = N (Ex.Tree1 a)
  data DCU (Ex.Tree1 a) dc where
    Leaf_ :: DCU (Ex.Tree1 a) (Leaf a)
    Branch_ :: DCU (Ex.Tree1 a) (Branch a)
  disband (Ex.Leaf a) = disbanded $ Leaf a
  disband (Ex.Branch a b) = disbanded $ Branch a b
instance Finite (DCU (Ex.Tree1 a)) where
  toUni x = Uni $ case x of
    Leaf_ -> OnLeft $ Here Refl
    Branch_ -> OnRight $ Here Refl
instance (a ~ b) => (Leaf b) ::: DCU (Ex.Tree1 a) where inhabits = Leaf_
instance (a ~ b) => (Branch b) ::: DCU (Ex.Tree1 a) where inhabits = Branch_
instance EqT (DCU (Ex.Tree1 a)) where eqT = eqTFin