```{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,
ScopedTypeVariables
#-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.RepLib.R
-- Copyright   :  (c) The University of Pennsylvania, 2006
--
-- Maintainer  :  sweirich@cis.upenn.edu
-- Stability   :  experimental
-- Portability :  non-portable
--
--
--
-----------------------------------------------------------------------------

module Data.RepLib.R where

import Data.List

data R a where
Int     :: R Int
Char    :: R Char
Integer :: R Integer
Float   :: R Float
Double  :: R Double
Rational:: R Rational
IOError :: R IOError
IO      :: (Rep a) => R a -> R (IO a)
Arrow   :: (Rep a, Rep b) => R a -> R b -> R (a -> b)
Data    :: DT -> [Con R a] -> R a

data Emb l a  = Emb { to     :: l -> a,
from   :: a -> Maybe l,
labels :: Maybe [String],
name   :: String,
fixity :: Fixity
}

data Fixity =  Nonfix
| Infix      { prec      :: Int }
| Infixl     { prec      :: Int }
| Infixr     { prec      :: Int }

data DT       = forall l. DT String (MTup R l)
data Con r a  = forall l. Con (Emb l a) (MTup r l)

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

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

infixr 7 :+:

class Rep a where rep :: R a

------ Showing representations  (rewrite this with showsPrec?)

instance Show (R a) where
show Int     = "Int"
show Char    = "Char"
show Integer = "Integer"
show Float   = "Float"
show Double  = "Double"
show Rational= "Rational"
show (IO t)  = "(IO " ++ show t ++ ")"
show IOError = "IOError"
show (Arrow r1 r2) =
"(" ++ (show r1) ++ " -> " ++ (show r2) ++ ")"
show (Data dt _) =
"(Data" ++ show dt ++ ")"

instance Show DT where
show (DT str reps) = str ++ show reps

instance Show (MTup R l) where
show MNil         = ""
show (r :+: MNil) = show r
show (r :+: rs)   = " " ++ show r ++ show rs

instance Eq (R a) where
r1 == r2 = True

--- Representations for Haskell Prelude types

instance Rep Int where rep = Int
instance Rep Char where rep = Char
instance Rep Double where rep = Double
instance Rep Rational where rep = Rational
instance Rep Float where rep = Float
instance Rep Integer where rep = Integer
instance Rep a => Rep (IO a) where rep = IO rep
instance Rep IOError where rep = IOError
instance (Rep a, Rep b) => Rep (a -> b) where rep = Arrow rep rep

-- Booleans
{-
rTrueEmb :: Emb Nil Bool
rTrueEmb =  Emb { to = \Nil -> True,
from = \x -> if x then Just Nil else Nothing,
labels = Nothing,
name = "True",
fixity = Nonfix
}

rFalseEmb :: Emb Nil Bool
rFalseEmb =  Emb { to = \Nil -> False,
from = \x -> if x then Nothing else Just Nil,
labels = Nothing,
name = "False",
fixity = Nonfix
}

rBool :: R Bool
rBool = Data (DT "Bool" MNil) [Con rTrueEmb, Con rFalseEmb]

instance Rep Bool where rep = rBool
-}

-- Unit

rUnitEmb :: Emb Nil ()
rUnitEmb = Emb { to = \Nil -> (),
from = \() -> Just Nil,
labels = Nothing,
name = "()",
fixity = Nonfix }

rUnit :: R ()
rUnit = Data (DT "()" MNil)
[Con rUnitEmb MNil]

instance Rep () where rep = rUnit

-- Tuples

instance (Rep a, Rep b) => Rep (a,b) where
rep = rTup2

rTup2 :: forall a b. (Rep a, Rep b) => R (a,b)
rTup2 = let args =  ((rep :: R a) :+: (rep :: R b) :+: MNil) in
Data (DT "," args) [ Con rPairEmb args ]

rPairEmb :: Emb (a :*: b :*: Nil) (a,b)
rPairEmb =
Emb { to = \( t1 :*: t2 :*: Nil) -> (t1,t2),
from = \(a,b) -> Just (a :*: b :*: Nil),
labels = Nothing,
name = "(,)",
fixity = Nonfix -- ???
}

-- Lists
rList :: forall a. Rep a => R [a]
rList = Data (DT "[]" ((rep :: R a) :+: MNil))
[ Con rNilEmb MNil, Con rConsEmb ((rep :: R a) :+: rList :+: MNil) ]

rNilEmb :: Emb Nil [a]
rNilEmb = Emb {   to   = \Nil -> [],
from  = \x -> case x of
(x:xs) -> Nothing
[]     ->  Just Nil,
labels = Nothing,
name = "[]",
fixity = Nonfix

}

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,
labels = Nothing,
name = ":",
fixity = Nonfix -- ???
}

instance Rep a => Rep [a] where
rep = rList

{-
-- Maybe representation

rJust :: Rep a => Con (Maybe a)
rJust = Con (rJustEmb)

rJustEmb :: Emb (a :*: Nil) (Maybe a)
rJustEmb = Emb
{ to   = (\(x :*: Nil) -> Just x),
from  = \x -> case x of
(Just y) -> Just (y :*: Nil)
Nothing  -> Nothing,
labels = Nothing,
name = "Just"
}

rNothing :: Con (Maybe a)
rNothing = Con rNothingEmb

rNothingEmb :: Emb Nil (Maybe a)
rNothingEmb = Emb
{ to   = \Nil -> Nothing,
from  = \x -> case x of
Nothing -> Just Nil
_       -> Nothing,
labels = Nothing,
name = "Nothing"
}

rMaybe :: forall a. Rep a => R (Maybe a)
rMaybe = Data (DT "Maybe" ((rep :: R a) :+: MNil))
[rJust, rNothing]

instance Rep a => Rep (Maybe a) where
rep = rMaybe
-}
-- Ordering
-- Either

```