# LANGUAGE KindSignatures , RankNTypes , ScopedTypeVariables , EmptyDataDecls , MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances #

----------------------------------------------------------------------------
-- |
-- Module     : Data.Reflection
  Copyright   : 2009   , 2004   and    
-- License    : BSD3
--
  Maintainer   :   <  >
-- Stability   : experimental
  Portability : non - portable ( scoped types , MPTCs , rank - n , FFI , kinds )
--
-- Implementation of the Functional Pearl: Implicit Configurations paper by
    and     .
--
-- </~ccshan/prepose/prepose.pdf>
--
-- Packaged and updated to work with the current implementation of scoped type 
  variables by   .
--
-------------------------------------------------------------------------------

module Data.Reflection 
    ( 
    -- * Reflect Integrals
      ReflectedNum
    , reflectNum
    , reifyIntegral
    -- * Reflect Lists of Integrals
    , ReflectedNums
    , reifyIntegrals
    -- * Reflect Storables
    , ReflectedStorable
    , reflectStorable
    , reifyStorable
    -- * Reflect Anything
    , Reflects
    , reflect
    , reify
    ) where

import Foreign.C.Types
import Foreign.Marshal.Alloc
import Foreign.Marshal.Array
import Foreign.Marshal.Utils
import Foreign.Ptr
import Foreign.StablePtr
import Foreign.Storable
import System.IO.Unsafe

data Zero
data Twice s
data Succ s
data Pred s

class ReflectedNum s where
    reflectNum :: Num a => s -> a

instance ReflectedNum Zero where
    reflectNum _ = 0

instance ReflectedNum s => ReflectedNum (Twice s) where
    reflectNum _ = reflectNum (undefined :: s) * 2

instance ReflectedNum s => ReflectedNum (Succ s) where
    reflectNum _ = reflectNum (undefined :: s) + 1

instance ReflectedNum s => ReflectedNum (Pred s) where
    reflectNum _ = reflectNum (undefined :: s) - 1

reifyIntegral :: Integral a => a -> (forall s. ReflectedNum s => s -> w) -> w
reifyIntegral i k = case quotRem i 2 of
    (0, 0) -> k (undefined :: Zero)
    (j, 0) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Twice s))
    (j, 1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Succ (Twice s)))
    (j,-1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Pred (Twice s)))
    _      -> undefined

data Nil
data Cons s ss

class ReflectedNums ss where
    reflectNums :: Num a => ss -> [a]

instance ReflectedNums Nil where
    reflectNums _ = []

instance (ReflectedNum s, ReflectedNums ss) => ReflectedNums (Cons s ss) where
    reflectNums _ = reflectNum (undefined :: s) : reflectNums (undefined :: ss)

reifyIntegrals :: Integral a => [a] -> (forall ss. ReflectedNums ss => ss -> w) -> w
reifyIntegrals [] k = k (undefined :: Nil)
reifyIntegrals (i:ii) k = 
    reifyIntegral i (\(_ :: s) -> 
    reifyIntegrals ii (\(_ :: ss) -> 
    k (undefined :: Cons s ss)))

data Store s a 

class ReflectedStorable s where
    reflectStorable :: Storable a => s a -> a

instance ReflectedNums s => ReflectedStorable (Store s) where
# NOINLINE reflectStorable #
    reflectStorable _ = unsafePerformIO . alloca $ \p -> do 
            pokeArray (castPtr p) bytes
            peek p 
        where 
            bytes = reflectNums (undefined :: s) :: [CChar]

reifyStorable :: Storable a => a -> (forall s. ReflectedStorable s => s a -> w) -> w
reifyStorable a k = reifyIntegrals (bytes :: [CChar]) (\(_ :: s) -> k (undefined :: Store s a))
  where
    bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr) 
# NOINLINE reifyStorable #

class Reflects s a | s -> a where 
    reflect :: s -> a

data Stable (s :: * -> *) a


 instance ReflectedStorable s = > Reflects ( Stable s a ) a where 
     reflect = unsafePerformIO . fmap const . deRefStablePtr $ reflectStorable ( undefined : : s p ) 

 reify : : a - > ( forall s. Reflects s a = > s - > w ) - > w 
 reify ( a : : a ) k = unsafePerformIO $ do 
         p < - newStablePtr a 
         reifyStorable p ( \ ( _ : : s ( StablePtr a ) ) - > return ( k ( undefined : : Stable s a ) ) ) 

instance ReflectedStorable s => Reflects (Stable s a) a where
    reflect = unsafePerformIO . fmap const . deRefStablePtr $ reflectStorable (undefined :: s p) 

reify :: a -> (forall s. Reflects s a => s -> w) -> w
reify (a :: a) k = unsafePerformIO $ do
        p <- newStablePtr a
        reifyStorable p (\(_ :: s (StablePtr a)) -> return (k (undefined :: Stable s a)))
-}

instance ReflectedStorable s => Reflects (Stable s a) a where
    reflect = unsafePerformIO $ do
            a <- deRefStablePtr p
            freeStablePtr p
            return (const a)
        where  
            p = reflectStorable (undefined :: s p)
# NOINLINE reflect #

reify :: a -> (forall s. (s `Reflects` a) => s -> w) -> w
reify (a :: a) k = unsafePerformIO $ do
        p <- newStablePtr a
        reifyStorable p (\(_ :: s (StablePtr a)) -> 
                let k' s = (reflect :: Stable s a -> a) `seq` return (k s) 
                in k' (undefined :: Stable s a))
# NOINLINE reify #

--------------------------------------------------------------------------
 |
 Module     : Data.Reflection
 License    : BSD3

 Stability   : experimental

 Implementation of the Functional Pearl: Implicit Configurations paper by

 </~ccshan/prepose/prepose.pdf>

 Packaged and updated to work with the current implementation of scoped type 

-----------------------------------------------------------------------------
 * Reflect Integrals
 * Reflect Lists of Integrals
 * Reflect Storables
 * Reflect Anything
# LANGUAGE KindSignatures , RankNTypes , ScopedTypeVariables , EmptyDataDecls , MultiParamTypeClasses , FunctionalDependencies , FlexibleInstances #

  Copyright   : 2009   , 2004   and    
  Maintainer   :   <  >
  Portability : non - portable ( scoped types , MPTCs , rank - n , FFI , kinds )
    and     .
  variables by   .

module Data.Reflection 
    ( 
      ReflectedNum
    , reflectNum
    , reifyIntegral
    , ReflectedNums
    , reifyIntegrals
    , ReflectedStorable
    , reflectStorable
    , reifyStorable
    , Reflects
    , reflect
    , reify
    ) where

import Foreign.C.Types
import Foreign.Marshal.Alloc
import Foreign.Marshal.Array
import Foreign.Marshal.Utils
import Foreign.Ptr
import Foreign.StablePtr
import Foreign.Storable
import System.IO.Unsafe

data Zero
data Twice s
data Succ s
data Pred s

class ReflectedNum s where
    reflectNum :: Num a => s -> a

instance ReflectedNum Zero where
    reflectNum _ = 0

instance ReflectedNum s => ReflectedNum (Twice s) where
    reflectNum _ = reflectNum (undefined :: s) * 2

instance ReflectedNum s => ReflectedNum (Succ s) where
    reflectNum _ = reflectNum (undefined :: s) + 1

instance ReflectedNum s => ReflectedNum (Pred s) where
    reflectNum _ = reflectNum (undefined :: s) - 1

reifyIntegral :: Integral a => a -> (forall s. ReflectedNum s => s -> w) -> w
reifyIntegral i k = case quotRem i 2 of
    (0, 0) -> k (undefined :: Zero)
    (j, 0) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Twice s))
    (j, 1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Succ (Twice s)))
    (j,-1) -> reifyIntegral j (\(_ :: s) -> k (undefined :: Pred (Twice s)))
    _      -> undefined

data Nil
data Cons s ss

class ReflectedNums ss where
    reflectNums :: Num a => ss -> [a]

instance ReflectedNums Nil where
    reflectNums _ = []

instance (ReflectedNum s, ReflectedNums ss) => ReflectedNums (Cons s ss) where
    reflectNums _ = reflectNum (undefined :: s) : reflectNums (undefined :: ss)

reifyIntegrals :: Integral a => [a] -> (forall ss. ReflectedNums ss => ss -> w) -> w
reifyIntegrals [] k = k (undefined :: Nil)
reifyIntegrals (i:ii) k = 
    reifyIntegral i (\(_ :: s) -> 
    reifyIntegrals ii (\(_ :: ss) -> 
    k (undefined :: Cons s ss)))

data Store s a 

class ReflectedStorable s where
    reflectStorable :: Storable a => s a -> a

instance ReflectedNums s => ReflectedStorable (Store s) where
# NOINLINE reflectStorable #
    reflectStorable _ = unsafePerformIO . alloca $ \p -> do 
            pokeArray (castPtr p) bytes
            peek p 
        where 
            bytes = reflectNums (undefined :: s) :: [CChar]

reifyStorable :: Storable a => a -> (forall s. ReflectedStorable s => s a -> w) -> w
reifyStorable a k = reifyIntegrals (bytes :: [CChar]) (\(_ :: s) -> k (undefined :: Store s a))
  where
    bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr) 
# NOINLINE reifyStorable #

class Reflects s a | s -> a where 
    reflect :: s -> a

data Stable (s :: * -> *) a


 instance ReflectedStorable s = > Reflects ( Stable s a ) a where 
     reflect = unsafePerformIO . fmap const . deRefStablePtr $ reflectStorable ( undefined : : s p ) 

 reify : : a - > ( forall s. Reflects s a = > s - > w ) - > w 
 reify ( a : : a ) k = unsafePerformIO $ do 
         p < - newStablePtr a 
         reifyStorable p ( \ ( _ : : s ( StablePtr a ) ) - > return ( k ( undefined : : Stable s a ) ) ) 

instance ReflectedStorable s => Reflects (Stable s a) a where
    reflect = unsafePerformIO . fmap const . deRefStablePtr $ reflectStorable (undefined :: s p) 

reify :: a -> (forall s. Reflects s a => s -> w) -> w
reify (a :: a) k = unsafePerformIO $ do
        p <- newStablePtr a
        reifyStorable p (\(_ :: s (StablePtr a)) -> return (k (undefined :: Stable s a)))
-}

instance ReflectedStorable s => Reflects (Stable s a) a where
    reflect = unsafePerformIO $ do
            a <- deRefStablePtr p
            freeStablePtr p
            return (const a)
        where  
            p = reflectStorable (undefined :: s p)
# NOINLINE reflect #

reify :: a -> (forall s. (s `Reflects` a) => s -> w) -> w
reify (a :: a) k = unsafePerformIO $ do
        p <- newStablePtr a
        reifyStorable p (\(_ :: s (StablePtr a)) -> 
                let k' s = (reflect :: Stable s a -> a) `seq` return (k s) 
                in k' (undefined :: Stable s a))
# NOINLINE reify #
