module Generics.MultiRec.LR where
import Generics.MultiRec
class LRBase a where
leftb :: a
rightb :: a
instance LRBase Int where
leftb = 0
rightb = 1
instance LRBase Integer where
leftb = 0
rightb = 1
instance LRBase Char where
leftb = 'L'
rightb = 'R'
instance LRBase Bool where
leftb = True
rightb = False
instance LRBase a => LRBase [a] where
leftb = []
rightb = [rightb]
class LR phi (f :: (* -> *) -> * -> *) where
leftf :: phi ix -> (forall ix'. El phi ix' => phi ix' -> r ix') -> [f r ix]
rightf :: phi ix -> (forall ix'. El phi ix' => phi ix' -> r ix') -> [f r ix]
instance El phi xi => LR phi (I xi) where
leftf _ f = [I (f proof)]
rightf _ f = [I (f proof)]
instance LRBase a => LR phi (K a) where
leftf _ _ = [K leftb]
rightf _ _ = [K rightb]
instance LR phi U where
leftf _ _ = [U]
rightf _ _ = [U]
instance (LR phi f, LR phi g) => LR phi (f :+: g) where
leftf p f = map L (leftf p f) ++ map R (leftf p f)
rightf p f = map R (rightf p f) ++ map L (rightf p f)
instance (LR phi f, LR phi g) => LR phi (f :*: g) where
leftf p f = zipWith (:*:) (leftf p f) (leftf p f)
rightf p f = zipWith (:*:) (rightf p f) (rightf p f)
instance LR phi f => LR phi (C c f) where
leftf p f = map C (leftf p f)
rightf p f = map C (rightf p f)
instance (El phi ix, LR phi f, EqS phi) => LR phi (f :>: ix) where
leftf p f = case eqS (proof :: phi ix) p of
Just Refl -> map Tag (leftf p f)
Nothing -> []
rightf p f = case eqS (proof :: phi ix) p of
Just Refl -> map Tag (rightf p f)
Nothing -> []
instance LR phi f => LR phi ([] :.: f) where
leftf p f = [D []]
rightf p f = map (\v -> D [v]) $ rightf p f
left :: (Fam phi, LR phi (PF phi)) => phi ix -> ix
left p = to p $ safeHead $ leftf p (I0 . left)
right :: (Fam phi, LR phi (PF phi)) => phi ix -> ix
right p = to p $ safeHead $ rightf p (I0 . right)
safeHead [] = error "Internal error, left or right returned []"
safeHead (x:xs) = x