-- lambda R with data types

data Either a b = Inl a | Inr b

-- representation of a data constructor
data RepCon a = forall b. RC (a -> Maybe b) (b -> a) String (() -> Rep b) 

data Rep :: *0 ~> *0 where
   Runit :: Rep ()
   Rint  :: Rep Int
   Rbool :: Rep Bool
   Rpair :: Rep a -> Rep b -> Rep (a,b)
   Rarr  :: Rep a -> Rep b -> Rep (a -> b)
   Rsum  :: Rep a -> Rep b -> Rep (Either a b)
   Rcon  :: String -> [RepCon a] -> Rep a	


data Age = Age Int
rage = Rcon "Age" [RC (\(Age x) -> Just x) Age "Age" (\x -> Rint)]

data Phone = Phone Int
rphone = Rcon "Phone" [RC (\(Phone x) -> Just x) Phone "Phone" (\x -> Rint)]


data Tree a = Leaf a | Node (Tree a) (Tree a)
deLeaf (Leaf x) = Just x
deLeaf _ = Nothing  
deNode (Node x y) = Just (x,y)
deNode _ = Nothing

rtree :: Rep a -> Rep (Tree a)
rtree ra = Rcon ("Tree " ++ (pt ra)) 
	     [RC deLeaf Leaf "Leaf" (\_ -> ra),
              RC deNode (\(x,y) -> Node x y) "Node" (\_ -> Rpair (rtree ra) (rtree ra))]

deJust x = x 
deNothing Nothing = Just ()
deNothing _ = Nothing

deNil :: [a] -> Maybe ()
deNil [] = Just ()
deNil _  = Nothing 

deCons :: [a] -> Maybe (a,[a])
deCons (hd:tl) = Just (hd,tl)
deCons _        = Nothing

rlist ::  Rep a -> Rep [a] 
rlist ra = Rcon ("["++ (pt ra) ++ "]") 
	        [RC deNil (\x -> []) "[]" (\_ -> Runit),
	         RC deCons (\(x,y) -> x:y) ":" (\_ -> Rpair ra (rlist ra))]


-- invariant --- no empty types.
zero :: Rep a -> a
zero Rint = 0
zero Rbool = False
zero (Rpair t1 t2) = (zero t1, zero t2)
zero (Rarr t1 t2)  = \x -> zero t2
zero (Rsum t1 t2) = Inl (zero t1)
zero (Rcon s (c:cs))  = 
   case c of 
     RC out inn name rep -> inn (zero (rep ()))
	 













-- print type
pt :: Rep a -> String
pt Rint = "Int"
pt Rbool = "Bool"
pt (Rpair t1 t2) = "(" ++ pt t1 ++ "," ++ pt t2 ++ ")"
pt (Rarr t1 t2) = "(" ++ pt t1 ++ "->" ++ pt t2 ++ ")"
pt (Rsum t1 t2) = "(" ++ pt t1 ++ ":+:" ++ pt t2 ++ ")"
pt (Rcon s _)  = s













-- casting between two types
cast :: Rep a -> Rep b -> Maybe (a -> b)
cast Rint Rint =  (\x -> x)
cast Rbool Rbool =  (\x -> x)
cast (Rpair t1 t2) (Rpair s1 s2) = 
    case (cast t1 s1, cast t2 s2) of 
            ( f,  g) ->  (\(x,y) -> (f x,g y))
cast (Rsum t1 t2) (Rsum s1 s2) = 
    case (cast t1 s1, cast t2 s2) of 
            (f,  g) ->  (\x -> case x of Inl y -> Inl (f y)
	                                 Inr y -> Inr (g y))
cast (Rarr t1 t2) (Rarr s1 s2) = 
    case (cast s1 t1, cast t2 s2) of 
            (f, g) ->  (\h -> g . h . f)
cast (Rcon s1 cons1) (Rcon s2 cons2) = \x -> 
    let loop [] [] = error "impossible"
        loop (rc1 : rest1) (rc2 : rest2) = 
            case (rc1, rc2) of 
               (RC out1 inn1 name1 rep1, RC out2 inn2 name2 rep2) -> 
                  case (out1 x) of 
                     Just y -> inn2 (cast (rep1 ()) (rep2 ()) y)
                     Nothing -> loop rest1 rest2 
    in loop cons1 cons2


cast r1 r2 = error ("Invalid cast " ++ (pt r1) ++ " and " ++ (pt r2)  )