{-# OPTIONS -fglasgow-exts #-}


data DCI a b = DCI { text  :: String, 
                      to    :: (b -> a),
                      from  :: (a -> Maybe b) }

data Ex a = forall b. Ex (Rep b, a b)

data R c a where
    Runit  :: R c ()
    Rint   :: R c Int
    Rbool  :: R c Bool
    Rtimes :: R c a -> R c b -> R c (a,b)
    Rname  :: String -> [DC c b] -> R c b
    Rex    :: (forall b. R c b -> R c (a b)) -> R c (Ex a)
    Run    :: c a -> R c a         

data DC c a = forall b. DC (R c b) (DCI a b) 


data R2 c a1 a2 where
    Runit2  :: R2 c () ()
    Rint2   :: R2 c Int Int 
    Rbool2  :: R2 c Bool Bool
    Rtimes2 :: R2 c a1 a2 -> R2 c b1 b2 -> R2 c (a1,b1) (a2,b2)
    Rname2  :: String -> [DC2 c b1 b2] -> R2 c b1 b2 
    Rex2    :: (forall b1 b2. R2 c b1 b2 -> R2 c (a1 b1) (a2 b2)) -> R2 c (Ex a1) (Ex a2)
    Run2    :: c a1 a2 -> R2 c a1 a2         

data DC2 c a1 a2  = forall b1 b2. DC2 (R2 c b1 b2) 
	                                   (DCI a1 b1)
                                      (DCI a2 b2)

data Rep b = Rep (forall c1. R c1 b) (forall c2. R2 c2 b b)


{-----------------------------------------------------------------------}

-- Representations of some datatypes.

data Fruit = Apple Int | Orange
rfruit = Rname "Fruit" [rapple, rorange]
rapple :: DC c Fruit
rapple = DC Rint
			   (DCI { text = "Apple",
                   to   = Apple,
                   from = unApple })
    where unApple (Apple y) = Just y
          unApple _         = Nothing
rorange :: DC c Fruit
rorange = DC Runit
			    (DCI { text = "Orange",
                    to   = const Orange, 
                    from = unOrange })
    where unOrange Orange = Just ()
          unOrange _      = Nothing

--
-- Lists

rlist :: R c a -> R c [a]
rlist ra = Rname "List" [rnil, rcons ra]

rnil :: DC c [a] 
rnil = DC Runit
          (DCI { text = "[]",
                 to   = const [],
                 from = unNil }) 
       where unNil [] = Just ()
             unNil _  = Nothing
rcons :: R c a -> DC c [a]
rcons ra = DC (Rtimes ra (rlist ra))
              (DCI { text = ":",
                     to   = \(t1,t2) -> (t1 : t2),
                     from = unCons })
        where unCons (t1:t2) = Just (t1,t2)
              unCons _       = Nothing


rlist2 :: R2 c a b -> R2 c [a] [b]
rlist2 ra = Rname2 "List" [rnil2, rcons2 ra]

rnil2 :: DC2 c [a] [b] 
rnil2 = DC2 Runit2 dci dci
       where unNil [] = Just ()
             unNil _  = Nothing
             dci = (DCI { text = "[]",
                          to   = const [],
                          from = unNil }) 

rcons2 :: R2 c a b -> DC2 c [a] [b]
rcons2 ra = DC2 (Rtimes2 ra (rlist2 ra)) dci dci
        where unCons (t1:t2) = Just (t1,t2)
              unCons _       = Nothing
              dci = (DCI { text = ":",
                           to   = \(t1,t2) -> (t1 : t2),
                           from = unCons })


--
-- Trees

data Tree a = Leaf a | Node (Tree a) (Tree a)
rtree :: R c a -> R c (Tree a)
rtree ra = Rname "Tree" [rleaf ra, rnode ra]

rleaf :: R c a -> DC c (Tree a)
rleaf ra = DC ra
              (DCI { text = "Leaf",
                     to   = Leaf,
                     from = unLeaf }) 
    where unLeaf (Leaf x) = Just x
          unLeaf _  = Nothing
rnode :: R c a -> DC c (Tree a)
rnode ra = DC (Rtimes (rtree ra) (rtree ra))
              (DCI { text = "Node",
                     to   = \(t1,t2) -> (Node t1 t2),
                     from = unNode })
        where unNode (Node t1 t2) = Just (t1,t2)
              unNode _            = Nothing


{-----------------------------------------------------------------------}

--
-- Functions

newtype Size a = S (a -> Int)
unS (S a) = a

size' :: R Size a -> Size a 
size' Runit = S $ \x -> 0
size' Rint = S $ \x -> 0
size' Rbool = S $ \x -> 0
size' (Rtimes ra rb) = S $ \(v1,v2) -> size ra v1 + size rb v2
size' (Rname str cons) = S $ \v -> 
              let loop (DC rb dci : rest) = 
                     case (from dci) v of 
                        Just y -> size rb y
                        Nothing -> loop rest
                  loop [] = error "impossible"
              in loop cons
size' (Rex xa) = S $ \(Ex w) ->
					  let (rep,z) = w in 
				     size (xa (Run (S $ \x -> 0))) z
size' (Run p) = p

size :: R Size a -> a -> Int
size = unS . size'  

length :: [a] -> Int
length = size (rlist (Run (S $ \x -> 1)))

-- Show
--

newtype RepShow a = RS (a -> String)
unRS (RS a) = a
rshow :: R RepShow a -> a -> String
rshow = unRS . show'
show' :: R RepShow a -> RepShow a
show' Rint = RS show
show' Runit  = RS (const "()")
show' (Rtimes xa xb) = RS $ \v -> 
           "(" ++ rshow xa (fst v) ++ "," 
               ++ rshow xb (snd v) ++ ")"
show' (Rname string cons) =  RS $ \v -> 
             let loop (DC rep dci : rest) = 
                   case (from dci v) of  
                     Just s  -> 
                       let s' = rshow rep s in
                       if s' == "()" then  (text dci)
                       else text dci ++ " " ++ s'
                     Nothing -> loop rest
                 loop [] = error "impossible"
                 in loop cons
show' (Rex xa) = RS $ \ (Ex w) ->
					  let (rep,z) = w in 
					  --             rshow (xa rep) z
										 rshow (xa (Run (RS $ const "XXXX"))) z
show' (Run p) = p

t1 = (Ex ((Rep Rint Rint2), (2::Int, 3::Int)))
rt1 = (Rex (\ a -> Rtimes Rint a))

--
-- Flatten

newtype F b a = F (a -> [b])
unF (F x) = x

flatten :: R (F b) a -> a -> [b]
flatten = unF . flatten'

flatten' :: R (F b) a -> F b a
flatten' Rint = F (const [])
flatten' Runit  = F (const [])
flatten' (Rtimes xa xb) = F $ \(v1,v2) -> 
           (flatten xa v1) ++ (flatten xb v2)
flatten' (Rname string cons) =
             F $ \v -> 
             let loop (DC rep dci : rest) = 
                   case (from dci v) of  
                     Just s  -> flatten rep s
                     Nothing -> loop rest
                 loop [] = error "impossible"
                 in loop cons
flatten' (Rex xa) = F $ \ (Ex w) ->
             let (r,z) = w in
				   case r of 
                 (Rep rep1 _) -> flatten (xa rep1) z
flatten' (Run p) = p

                  
treeFlatten :: Tree a -> [a]
treeFlatten = flatten (rtree (Run (F $ \x -> [x])))

treeSize = size (rtree (Run (S $ \x -> 1)))

t :: Tree Int
t = Node (Node (Leaf (3::Int)) (Leaf 4)) (Leaf 5)

--- Map

gmap :: R2 (->) a b -> (a -> b)
gmap Rint2 = \x -> x
gmap Runit2 = \x -> x
gmap (Rtimes2 ra rb) = \(v1,v2) -> (gmap ra v1, gmap rb v2)
gmap (Rname2 str cons) = \ (v :: a) ->
  let loop (DC2 rep dci1 dci2 : rest) = 
          case (from dci1 v) of 
             Just s  -> to dci2 (gmap rep s)
             Nothing -> loop rest
      loop [] = error "impossible"
  in loop cons
gmap (Rex2 xa) = \ (Ex w) ->
   let (rep,z) = w in 
       case rep of 
        (Rep r1 r2) ->  let rb = xa (Run2 (\x -> x)) in
                          -- what if rb = xa r2?
 	                 	 Ex (rep, gmap rb z)

gmap (Run2 p) = p

map_list :: (a -> b) -> [a] -> [b]
map_list f = gmap (rlist2 (Run2 f))