\begin{code}
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module RepLibLite where

import GHC.Base (unsafeCoerce#)

---------------------------------------------------------------------------
-- Simple representations (Section 3)
---------------------------------------------------------------------------

data R a where
   Int    :: R Int
   Char   :: R Char 
   Arrow  :: R a -> R b -> R (a -> b)
   Data   :: DT -> [Con a] -> R a 

data Emb l a  = Emb { to     :: l -> a, 
                      from   :: a -> Maybe l }

data DT    = forall l. DT String (Rs l)
data Con a = forall l. Reps l => Con (Emb l a) 

data Nil = Nil 
data a :*: l = a :*: l
infixr 7 :*:

data Rs l where
   RNil  :: Rs Nil
   (:^:) :: Rep a => R a -> Rs l -> Rs (a :*: l)
infixr 7 :^:

class Reps l where
  reps :: Rs l
instance Reps Nil where
  reps = RNil
instance (Rep a, Reps l) => Reps (a :*: l) where
  reps = rep :^: reps

class Rep a where rep :: R a

---------------------------------------------------------------------------
-- Casting
---------------------------------------------------------------------------
compR :: R a -> R b -> Bool
compR Int           Int           = True
compR Char          Char          = True
compR (Arrow t1 t2) (Arrow s1 s2) = compR t1 s1 && compR t2 s2
compR (Data rc1 _)  (Data rc2 _)  = compDT rc1 rc2
compR  _             _            = False

compDT :: DT -> DT -> Bool
compDT (DT str1 rt1) (DT str2 rt2) =  str1 == str2 && compRs rt1 rt2

compRs :: Rs t1 -> Rs t2 -> Bool
compRs RNil         RNil         = True
compRs (r1 :^: rt1) (r2 :^: rt2) =  compR r1 r2 && compRs rt1 rt2

castR :: R a -> R b -> a -> Maybe b
castR (ra::R a) (rb::R b) = 
   if compR ra rb 
   then \(x::a) -> Just (unsafeCoerce# x::b) 
   else \x -> Nothing

cast :: (Rep a, Rep b) => a -> Maybe b
cast (x :: a) :: Maybe b = castR (rep :: R a) (rep :: R b) x

gcastR :: forall a b c. R a -> R b -> c a -> Maybe (c b)
gcastR ra rb =  if compR ra rb
                 then \(x :: c a) -> Just (unsafeCoerce# x :: c b)
                 else \x -> Nothing

gcast :: forall a b c. (Rep a, Rep b) => c a -> Maybe (c b)
gcast = gcastR (rep :: R a) (rep :: R b)      

---------------------------------------------------------------------------
-- Library operations
---------------------------------------------------------------------------

data Val a = forall l. Reps l => Val (Emb l a) l

findCon :: [Con a] -> a -> Val a
findCon (Con emb : rest) x = 
  case (from emb x) of 
    Just kids -> Val emb  kids
    Nothing -> findCon rest x

foldr_l :: (forall a. Rep a =>  a -> b -> b) -> b -> MTup R l -> l -> b
foldr_l f b MNil Nil = b
foldr_l f b (_ :+: rs) (a :*: l) = f a (foldr_l f b rs l ) 

foldl_l :: (forall a. Rep a => b -> a -> b) -> b -> MTup R l -> l -> b 
foldl_l f b MNil Nil = b
foldl_l f b (_ :+: rs) (a :*: l) = foldl_l f (f b a) rs l 

map_l :: (forall a. Rep a => a -> a) -> Rs l -> l -> l
map_l t RNil Nil = Nil
map_l t (_ :^: rs) (a :*: a1) = (t a :*: map_l t rs a1)

---------------------------------------------------------------------------
-- Simple representations of built-in types
---------------------------------------------------------------------------

instance Rep Int where rep = Int
instance Rep Char where rep = Char
instance (Rep a, Rep b) => Rep (a -> b) where rep = Arrow rep rep

-- Unit
rUnitEmb = Emb { to = \Nil -> (), 
                 from = \() -> Just Nil }

instance Rep () where 
  rep = Data (DT "()" RNil) [Con rUnitEmb]

-- Booleans
rTrueEmb = 
  Emb {  to    = \Nil -> True,
         from  = \x -> if x then Just Nil else Nothing }

rFalseEmb =  
  Emb {  to    = \Nil -> False,
         from  = \x -> if x then Nothing else Just Nil }

instance Rep Bool where
   rep = Data (DT "Bool" RNil) [Con rFalseEmb, Con rTrueEmb]
       

-- Pairs
rPairEmb :: Emb (a :*: b :*: Nil) (a,b)
rPairEmb = 
  Emb {  to    = \( t1 :*: t2 :*: Nil) -> (t1,t2),
         from  = \(a,b) -> Just (a :*: b :*: Nil) }
instance (Rep a, Rep b) => Rep (a,b) where
   rep = Data (DT "," ((rep :: R a) :^: (rep :: R b) :^: RNil)) 
           [ Con rPairEmb ]


-- Lists
rNilEmb :: Emb Nil [a]
rNilEmb = 
  Emb {   to    = \Nil -> [],
          from  = \x -> case x of 
                           (x:xs)  -> Nothing
                           []      ->  Just Nil }

rConsEmb :: Emb (a :*: [a] :*: Nil) [a]
rConsEmb = 
   Emb { to    = \(hd :*: tl :*: Nil) -> (hd : tl),
         from  = \x -> case x of 
                    (hd : tl) -> Just (hd :*: tl :*: Nil)
                    []        -> Nothing }

instance Rep a => Rep [a] where
   rep = Data (DT "[]" ((rep :: R a) :^: RNil)) [ Con rNilEmb, Con rConsEmb ]

---------------------------------------------------------------------------
-- Parameterized representations (Section 4)
---------------------------------------------------------------------------
data R1 ctx a where
    Int1    :: R1 ctx Int
    Char1   :: R1 ctx Char
    Arrow1  :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a -> b)
    Data1   :: DT -> [Con1 ctx a] -> R1 ctx a

data Con1 ctx a = 
  forall tl. Con1 (Emb tl a) (MTup ctx tl) 

data MTup ctx a where 
    MNil  :: MTup ctx Nil
    (:+:) :: (Rep a) => ctx a -> MTup ctx l -> MTup ctx (a :*: l)
infixr 7 :+:

class Sat a where
    dict :: a 

class Rep a => Rep1 ctx a where 
    rep1 :: R1 ctx a

---------------------------------------------------------------------------
-- Library operations
---------------------------------------------------------------------------

data Val1 ctx a = forall l.  Val1 (Emb l a) l (MTup (ctx) l)

findCon1 :: [Con1 ctx a] -> a -> Val1 ctx a
findCon1 (Con1 emb rec : rest) x = 
  case (from emb x) of 
     Just kids -> Val1 emb kids rec
     Nothing -> findCon1 rest x

foldr_l1 :: (forall a. Rep a => ctx a -> a -> b -> b) -> b -> (MTup (ctx) l) -> l -> b
foldr_l1 f b MNil Nil = b
foldr_l1 f b (ca :+: cl) (a :*: l) = f ca a (foldr_l1 f b cl l ) 

foldl_l1 :: (forall a. Rep a => ctx a -> b -> a -> b) -> b -> (MTup (ctx) l) ->  l -> b
foldl_l1 f b MNil Nil = b
foldl_l1 f b (ca :+: cl) (a :*: l) = foldl_l1 f (f ca b a) cl l 

map_l1 :: (forall a. Rep a => ctx a -> a -> a) -> (MTup (ctx) l) ->  l ->  l
map_l1 f MNil Nil = Nil
map_l1 f (ca :+: cl) (a :*: l) = (f ca a) :*: (map_l1 f cl l)

---------------------------------------------------------------------------
-- Parameterized representations of built-in types
---------------------------------------------------------------------------

instance Rep1 ctx Int  where rep1 = Int1
instance Rep1 ctx Char where rep1 = Char1
instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => Rep1 ctx (a -> b) where 
   rep1 = Arrow1 dict dict

-- Unit
instance Rep1 ctx ()   where 
 rep1 = Data1 (DT "()" RNil) [Con1 rUnitEmb MNil]

-- Booleans
instance Rep1 ctx Bool where 
 rep1 = Data1 (DT "Bool" RNil) [Con1 rFalseEmb MNil, Con1 rTrueEmb MNil]
  
-- Pairs
rPair1 :: forall a b ctx. (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a,b)
rPair1 ca cb = 
  case (rep :: R (a,b)) of 
     Data dt _ -> Data1 dt [Con1 rPairEmb (ca :+: cb :+: MNil)]
     
instance (Rep a, Sat (ctx a), Rep b, Sat (ctx b)) => Rep1 ctx (a,b) where
    rep1 = rPair1 dict dict

-- Lists
rList1 :: forall a ctx. Rep a => ctx a -> ctx [a] -> R1 ctx [a]
rList1 ca cl = Data1 (DT "[]" ((rep :: R a) :^: RNil)) 
     [Con1 rNilEmb MNil, Con1 rConsEmb (ca :+: cl :+: MNil) ]

instance (Rep a, Sat (ctx a), Sat (ctx [a])) => Rep1 ctx [a] where
    rep1 = rList1 dict dict
\end{code}