module Generics.LIGD.Base where
data Unit = Unit deriving Show
data a :+: b = L a | R b deriving Show
data a :*: b = a :*: b deriving Show
infixr 5 :+:
infixr 6 :*:
data EP a b = EP { from :: (a -> b), to :: (b -> a) }
data Rep :: * -> * where
RChar :: Rep Char
RInt :: Rep Int
RString :: Rep String
RUnit :: Rep Unit
RSum :: Rep a -> Rep b -> Rep (a :+: b)
RProd :: Rep a -> Rep b -> Rep (a :*: b)
RCon :: String -> Rep a -> Rep a
RType :: EP b a -> Rep a -> Rep b
data Rep1 :: (* -> *) -> * -> * where
RChar1 :: Rep1 g Char
RInt1 :: Rep1 g Int
RUnit1 :: Rep1 g Unit
RSum1 :: Rep1 g a -> Rep1 g b -> Rep1 g (a :+: b)
RProd1 :: Rep1 g a -> Rep1 g b -> Rep1 g (a :*: b)
RCon1 :: String -> Rep1 g a -> Rep1 g a
RType1 :: EP b a -> Rep1 g a -> Rep1 g b
RVar1 :: g a -> Rep1 g a
data Rep2 :: (* -> * -> *) -> * -> * -> * where
RChar2 :: Rep2 g Char Char
RInt2 :: Rep2 g Int Int
RUnit2 :: Rep2 g Unit Unit
RSum2 :: Rep2 g a b -> Rep2 g c d -> Rep2 g (a :+: c) (b :+: d)
RProd2 :: Rep2 g a b -> Rep2 g c d -> Rep2 g (a :*: c) (b :*: d)
RCon2 :: String -> Rep2 g a b -> Rep2 g a b
RType2 :: EP a c -> EP b d -> Rep2 g c d -> Rep2 g a b
RVar2 :: g a b -> Rep2 g a b