{-# OPTIONS_GHC -fglasgow-exts #-}
{-# LANGUAGE TemplateHaskell #-}

-- Regular library and Logic datatype and representation

module Regular where

data K a r       = K { unK :: a }
data I r         = I { unI :: r }
data U r         = U
data (f :+: g) r = L (f r) | R (g r)
data (f :*: g) r = f r :*: g r
data C c f r =  C { unC :: f r }

infixr 6 :+:
infixr 7 :*:

class Constructor c where
  conName   :: t c (f :: * -> *) r -> String
  conFixity :: t c (f :: * -> *) r -> Fixity
  conFixity = const Prefix

data Fixity = Prefix | Infix Associativity Int
  deriving (Eq, Show, Ord, Read)

data Associativity = LeftAssociative | RightAssociative | NotAssociative
  deriving (Eq, Show, Ord, Read)

class Regular a where
  type PF a :: * -> *
  from      :: a -> PF a a
  to        :: PF a a -> a

instance Functor I where
  fmap f (I r) = I (f r)
instance Functor (K a) where
  fmap _ (K a) = K a
instance Functor U where
  fmap _ U = U
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap f (L x) = L (fmap f x)
  fmap f (R y) = R (fmap f y)
instance (Functor f, Functor g) => Functor (f :*: g) where
  fmap f (x :*: y) = fmap f x :*: fmap f y
instance Functor f => Functor (C c f) where
  fmap f (C r) = C (fmap f r)

class GMap f where
  gmap :: (a -> b) -> f a -> f b
instance GMap I where
  gmap f (I r) = I (f r)
instance GMap (K a) where
  gmap _ (K x)  = K x
instance GMap U where
  gmap _ U = U
instance (GMap f, GMap g) => GMap (f :+: g) where
  gmap f (L x) = L (gmap f x)
  gmap f (R x) = R (gmap f x)
instance (GMap f, GMap g) => GMap (f :*: g) where
  gmap f (x :*: y) = (:*:) (gmap f x) (gmap f y)
instance GMap f => GMap (C c f) where
  gmap f (C x) = C (gmap f x)