Ticket #2820: RepSmall.hs

{-# LANGUAGE TemplateHaskell, UndecidableInstances #-}
-- {-# OPTIONS -fglasgow-exts #-}
{-# 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
--
--
--
-----------------------------------------------------------------------------

-- options for deletion. tuple commands, cast commands, Rep SYB ops.

module Data.RepLib.RepCombined (

  -- ** Operations for heterogeneous lists 
  findCon, Val(..), foldl_l, foldr_l, map_l, mapQ_l, mapM_l, 

  -- Tuple ops
  fromTup, fromTupM, toList,

  -- ** SYB style operations (Rep)
  Traversal, Query, MapM, 
  gmapT, gmapQ, gmapM,

  -- ** SYB style operations (Rep1)
  Traversal1, Query1, MapM1,
  gmapT1, gmapQ1, gmapM1,

  -- ** SYB Reloaded

  Typed(..),Spine(..), toSpine, fromSpine


) where

import Data.List
-- import GHC.Base (unsafeCoerce#)


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



-- Parameterized rep
data R1 ctx a where
    Int1      :: R1 ctx Int
    Char1     :: R1 ctx Char
    Integer1  :: R1 ctx Integer
    Float1    :: R1 ctx Float
    Double1   :: R1 ctx Double
    Rational1 :: R1 ctx Rational
    IOError1  :: R1 ctx IOError
    IO1       :: (Rep a) => ctx a -> R1 ctx (IO a)
    Arrow1    :: (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a -> b)
    Data1     :: DT -> [Con ctx a] -> R1 ctx a

class Sat a where dict :: a 

class Rep a => Rep1 ctx a where rep1 :: R1 ctx a

instance Show (R1 c a) where
    show Int1           = "Int1"
    show Char1          = "Char1"
    show Integer1       = "Integer1"
    show Float1         = "Float1"
    show Double1        = "Double1"
    show Rational1      = "Rational1"
    show IOError1       = "IOError1"
    show (IO1 cb)       = "(IO1 " ++ show (getRep cb) ++ ")"
    show (Arrow1 cb cc) = "(Arrow1 " ++ show (getRep cb) ++ " " ++ show (getRep cc) ++ ")" 
    show (Data1 dt _)   = "(Data1 " ++ show dt ++ ")"

-- | Access a representation, given a proxy
getRep :: Rep b => c b -> R b
getRep cb = rep 

-- | Transform a parameterized rep to a vanilla rep
toR :: R1 c a -> R a
toR Int1            = Int
toR Char1           = Char
toR Integer1        = Integer
toR Float1          = Float
toR Double1         = Double
toR Rational1       = Rational
toR IOError1        = IOError
toR (Arrow1 t1 t2)  = Arrow (getRep t1) (getRep t2)
toR (IO1 t1)        = IO (getRep t1)
toR (Data1 dt cons) = (Data dt (map toCon cons))
  where toCon (Con emb rec) = Con emb (toRs rec)
        toRs           :: MTup c a -> MTup R a 
        toRs MNil      = MNil
        toRs (c :+: l) = (getRep c :+: toRs l)

---------------  Representations of Prelude types

instance Rep1 ctx Int      where rep1 = Int1
instance Rep1 ctx Char     where rep1 = Char1
instance Rep1 ctx Integer  where rep1 = Integer1
instance Rep1 ctx Float    where rep1 = Float1
instance Rep1 ctx Double   where rep1 = Double1
instance Rep1 ctx IOError  where rep1 = IOError1
instance Rep1 ctx Rational where rep1 = Rational1
instance (Rep a, Sat (ctx a)) => 
         Rep1 ctx (IO a)   where rep1 = IO1 dict
instance (Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => 
         Rep1 ctx (a -> b) where rep1 = Arrow1 dict dict


-- Data structures

-- unit
instance Rep1 ctx ()   where 
 rep1 = Data1 (DT "()" MNil)
        [Con rUnitEmb MNil]

-- pairs
rTup2_1 :: forall a b ctx. (Rep a, Rep b) => ctx a -> ctx b -> R1 ctx (a,b)
rTup2_1 ca cb = 
  case (rep :: R (a,b)) of 
     Data rdt _ -> Data1 rdt 
       [Con rPairEmb (ca :+: cb :+: MNil)]
     
instance (Rep a, Sat (ctx a), Rep b, Sat (ctx b)) => Rep1 ctx (a,b) where
  rep1 = rTup2_1 dict dict


-- Lists
rList1 :: forall a ctx. 
  Rep a => ctx a -> ctx [a] -> R1 ctx [a]
rList1 ca cl = Data1 (DT "[]" ((rep :: R a) :+: MNil))
                  [ rCons1 ca cl, rNil1 ]

rNil1  :: Con ctx [a]
rNil1  = Con rNilEmb MNil

rCons1 :: Rep a => ctx a -> ctx [a] -> Con ctx [a]
rCons1 ca cl = Con rConsEmb (ca :+: cl :+: MNil)

instance (Rep a, Sat (ctx a), Sat (ctx [a])) => Rep1 ctx [a] where
  rep1 = rList1 dict dict








--------- Basic instances and library operations for heterogeneous lists ---------------

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

-- | A fold right operation for heterogeneous lists, that folds a function 
-- expecting a type type representation across each element of the list.
foldr_l :: (forall a. Rep a => ctx a -> a -> b -> b) -> b 
            -> (MTup ctx l) -> l -> b
foldr_l f b MNil Nil = b
foldr_l f b (ca :+: cl) (a :*: l) = f ca a (foldr_l f b cl l ) 

-- | A fold left for heterogeneous lists
foldl_l :: (forall a. Rep a => ctx a -> b -> a -> b) -> b 
            -> (MTup ctx l) ->  l -> b
foldl_l f b MNil Nil = b
foldl_l f b (ca :+: cl) (a :*: l) = foldl_l f (f ca b a) cl l 

-- | A map for heterogeneous lists
map_l :: (forall a. Rep a => ctx a -> a -> a) 
           -> (MTup ctx l) ->  l ->  l
map_l f MNil Nil = Nil
map_l f (ca :+: cl) (a :*: l) = (f ca a) :*: (map_l f cl l)

-- | Transform a heterogeneous list in to a standard list
mapQ_l :: (forall a. Rep a => ctx a -> a -> r) -> MTup ctx l -> l -> [r]
mapQ_l q MNil Nil = []
mapQ_l q (r :+: rs) (a :*: l) = q r a : mapQ_l q rs l

-- | mapM for heterogeneous lists
mapM_l :: (Monad m) => (forall a. Rep a => ctx a -> a -> m a) -> MTup ctx l -> l -> m l
mapM_l f MNil Nil = return Nil
mapM_l f (ca :+: cl) (a :*: l) = do 
  x1 <- f ca a
  x2 <- mapM_l f cl l
  return (x1 :*: x2)



-- | Generate a heterogeneous list from metadata
fromTup :: (forall a. Rep a => ctx a -> a) -> MTup ctx l -> l
fromTup f MNil = Nil
fromTup f (b :+: l) = (f b) :*: (fromTup f l)

-- | Generate a heterogeneous list from metadata, in a monad
fromTupM :: (Monad m) => (forall a. Rep a => ctx a -> m a) -> MTup ctx l -> m l
fromTupM f MNil = return Nil
fromTupM f (b :+: l) = do hd <- f b
                          tl <- fromTupM f l
                          return (hd :*: tl)

-- | Generate a normal lists from metadata
toList :: (forall a. Rep a => ctx a -> b) -> MTup ctx l -> [b]
toList f MNil = []
toList f (b :+: l) = f b : toList f l


---------------------  SYB style operations --------------------------

-- | A SYB style traversal
type Traversal = forall a. Rep a => a -> a

-- | Map a traversal across the kids of a data structure 
gmapT :: forall a. Rep a => Traversal -> a -> a
gmapT t = 
  case (rep :: R a) of 
   (Data dt cons) -> \x -> 
     case (findCon cons x) of 
      Val emb reps ys -> to emb (map_l (const t) reps ys)
   _ -> id


-- | SYB style query type
type Query r = forall a. Rep a => a -> r 

gmapQ :: forall a r. Rep a => Query r -> a -> [r]
gmapQ q =
  case (rep :: R a) of 
    (Data dt cons) -> \x -> case (findCon cons x) of 
                Val emb reps ys -> mapQ_l (const q) reps ys
    _ -> const []


-- | SYB style monadic map type
type MapM m = forall a. Rep a => a -> m a

gmapM   :: forall a m. (Rep a, Monad m) => MapM m -> a -> m a
gmapM m = case (rep :: R a) of
   (Data dt cons) -> \x -> case (findCon cons x) of 
     Val emb reps ys -> do l <- mapM_l (const m) reps ys
                           return (to emb l)
   _ -> return 


-------------- Generalized  SYB ops ---------------------------

type Traversal1 ctx = forall a. Rep a => ctx a -> a -> a
gmapT1 :: forall a ctx. (Rep1 ctx a) => Traversal1 ctx -> a -> a 
gmapT1 t = 
  case (rep1 :: R1 ctx a) of 
   (Data1 dt cons) -> \x -> 
     case (findCon cons x) of 
      Val emb recs kids -> to emb (map_l t recs kids)
   _ -> id

type Query1 ctx r = forall a. Rep a => ctx a -> a -> r
gmapQ1 :: forall a ctx r. (Rep1 ctx a) => Query1 ctx r -> a -> [r]
gmapQ1 q  =
  case (rep1 :: R1 ctx a) of 
    (Data1 dt cons) -> \x -> case (findCon cons x) of 
                Val emb recs kids -> mapQ_l q recs kids
    _ -> const []

type MapM1 ctx m = forall a. Rep a => ctx a -> a -> m a
gmapM1  :: forall a ctx m. (Rep1 ctx a, Monad m) => MapM1 ctx m -> a -> m a
gmapM1 m = case (rep1 :: R1 ctx a) of
   (Data1 dt cons) -> \x -> case (findCon cons x) of 
     Val emb rec ys -> do l <- mapM_l m rec ys
                          return (to emb l)
   _ -> return 

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

toSpineR :: R a -> a -> Spine a
toSpineR (Data _ cons) a = 
         case (findCon cons a) of 
            Val emb reps kids -> 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)

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

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