{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExistentialQuantification, TypeOperators, GADTs #-}
{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances  #-}
{-# LANGUAGE TypeSynonymInstances, ScopedTypeVariables  #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.RepLib.R
-- Copyright   :  (c) The University of Pennsylvania, 2006
-- License     :  BSD
-- 
-- Maintainer  :  sweirich@cis.upenn.edu
-- Stability   :  experimental
-- Portability :  non-portable
--
--
-----------------------------------------------------------------------------

module Data.RepLib.RepCombined (

  -- ** Operations for heterogeneous lists 
  findCon, Val(..), 

  -- ** SYB Reloaded
  Typed(..), Spine(..), 

  -- these seem to 'cause' the problem.
  -- toSpine, 
  badFunction

) 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

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

-- | A datastructure to store the results of findCon
data Val ctx a = forall l.  Val (Emb l a) (MTup ctx l) l

-- | Given a list of constructor representations for a datatype, 
-- determine which constructor formed the datatype.
findCon :: [Con ctx a] -> a -> Val ctx a
findCon (Con rcd rec : rest) x = case (from rcd x) of 
       Just ys -> Val rcd rec ys
       Nothing -> findCon rest x


-------------- Spine from SYB Reloaded ---------------------------

data Typed a = a ::: R a 
infixr 7 :::

data Spine a where
	 Constr :: a -> Spine a
	 (:<>:)  :: Spine (a -> b) -> Typed a -> Spine b

{- 

toSpine :: Rep a => a -> Spine a 
toSpine = toSpineR rep

toSpineR :: R a -> a -> Spine a
toSpineR (Data _ cons) a = 
	 case (findCon cons a) of 
	    Val emb reps kids -> Constr toSpineRl reps kids (to emb)
toSpineR _ a = Constr a

toSpineRl :: MTup R l -> l -> (l -> a) -> Spine a 
toSpineRl MNil Nil into = Constr (into Nil)
toSpineRl (ra :+: rs) (a :*: l) into = 
	 (toSpineRl rs l into') :<>: (a ::: ra)
		  where into' tl1 x1 = into (x1 :*: tl1)

fromSpine :: Spine a -> a
fromSpine (Constr x) = x
fromSpine (x :<> (y:::_)) = fromSpine x y

-}

-- toSpineRl function causes problem
badFunction :: MTup R l -> l -> (l -> a) -> Spine a 
badFunction MNil Nil into = Constr (into Nil)
badFunction (ra :+: rs) (a :*: l) into = 
	 (badFunction rs l into') :<>: (a ::: ra)
		  where into' tl1 x1 = into (x1 :*: tl1)