{-# OPTIONS -fglasgow-exts #-}

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

data Ex a = forall b. Ex (forall c. (R c 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) 









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

-- 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

--
-- 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 Rbool Rbool) = S $ (\(v1,v2) -> if v1 then 1 else if v2 then 3 else 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 
--                      let rz = (xa (Run (S $ \x -> 0))) in
--                      let rz = xa rep in
                        let rz = xa (Run (size' rep))  in
			 size rz z
size' (Run t)  = t

-- size :: (forall c. R c a) -> a -> Int
size :: R Size a -> a -> Int
size = unS . size'  

real_size :: (forall c. R c a) -> a -> Int
real_size = 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 s) = s

t1 = (Ex (Rint, (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 (rep,z) = w in 
             flatten (xa rep) z

                  
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)

{-

-- cast  -- doesn't work! Need "closed" reps...

icast:: R ((->) Int) b -> Int -> b
icast Rint = (\x -> x) 
icast _    = error "Can't cast"

ucast :: R ((->)()) b -> () -> b
ucast Runit = (\x -> x)
ucast _     = error "Can't cast"

pcast :: R Cast a1 -> R Cast a2 -> R ((->)(a1,a2)) b -> (a1,a2) -> b
pcast ra1 ra2 (Rtimes rb1 rb2) = (\(x1,x2) -> (cast ra1 rb1 x1, cast ra2 rb2 x2))
pcast _ _ _              = error "Can't cast"

ncast :: [DC Cast a1] -> R ((->) a1) b -> a1 -> b
ncast cons1 (Rname str cons2) = \v -> 
    let loop (DC rep1 dci1 : rest1) (DC rep2 dci2 : rest2) = 
           case (from dci1 v) of 
             Just s -> to dci2 (cast rep1 rep2 s)
             Nothing -> loop rest1 rest2
        loop [] _ = error "impossible"
    in loop cons1 cons2
ncast _ = error "Can't cast"

xcast :: (forall b. R Cast b -> R Cast (a b)) -> R ((->) (Ex a)) b -> (Ex a) -> b
xcast ra (Rex rb) = \(Ex w) ->
   let (rep,z) = w in 
     Ex (rep, cast (ra rep) (rb rep) z)
xcast _ = error "Can't cast"


newtype Cast a = C (forall b. R ((->)a) b -> a -> b)
unC (C x) = x

cast' :: R Cast a -> Cast a
cast' Rint = C icast
cast' Runit = C ucast
cast' (Rtimes r1 r2) = C (pcast r1 r2)
cast' (Rname str1 cons1) = C (ncast cons1)
cast' (Rex r1) = C (xcast r1)

cast :: R Cast a -> R ((->) a) b -> a -> b
cast = unC . cast'
-}