-
-
Save nonowarn/181412 to your computer and use it in GitHub Desktop.
Trace of the paper for reflection in haskell
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- trace of http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf | |
import Foreign | |
import Foreign.Storable | |
import Foreign.C.Types | |
data Zero; data Succ n; data Pred n; data Twice n; | |
class ReflectNum s where reflectNum :: Num a => s -> a | |
instance ReflectNum Zero where reflectNum _ = 0 | |
instance ReflectNum n => | |
ReflectNum (Succ n) where reflectNum _ = reflectNum (undefined :: n) + 1 | |
instance ReflectNum n => | |
ReflectNum (Pred n) where reflectNum _ = reflectNum (undefined :: n) - 1 | |
instance ReflectNum n => | |
ReflectNum (Twice n) where reflectNum _ = reflectNum (undefined :: n) * 2 | |
reifyIntegral :: Integral a => a -> (forall s. ReflectNum s => s -> w) -> w | |
-- reifyIntegral :: (Integral a, ReflectNum s) => a -> (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))) | |
data Nil; data Cons s ss; | |
class ReflectNums ss where reflectNums :: Num a => ss -> [a] | |
instance ReflectNums Nil where reflectNums _ = [] | |
instance (ReflectNum s, ReflectNums ss) => ReflectNums (Cons s ss) where | |
reflectNums _ = reflectNum (undefined :: s) : reflectNums (undefined :: ss) | |
reifyIntegrals :: Integral a => [a] -> (forall ss. ReflectNums ss => ss -> w) -> w | |
reifyIntegrals [] k = k (undefined :: Nil) | |
reifyIntegrals (a:as) k = reifyIntegral a $ \(_::s) -> | |
reifyIntegrals as $ \(_::ss) -> | |
k (undefined :: Cons s ss) | |
type Byte = CChar | |
data Store s a | |
class ReflectStorable s where reflectStorable :: Storable a => s a -> a | |
instance ReflectNums s => ReflectStorable (Store s) where | |
reflectStorable _ = unsafePerformIO | |
$ alloca | |
$ \p -> do pokeArray (castPtr p) bytes | |
peek p | |
where bytes = reflectNums (undefined::s) :: [Byte] | |
reifyStorable :: Storable a => a -> (forall s. ReflectStorable s => s a -> w) -> w | |
reifyStorable a k = reifyIntegrals (bytes::[Byte]) (\(_::s) -> k (undefined :: Store s a)) | |
where bytes = unsafePerformIO | |
$ with a (peekArray (sizeOf a) . castPtr) | |
data Stable (s :: * -> *) a | |
class Reflect s a | s -> a where reflect :: s -> a | |
instance ReflectStorable s => Reflect (Stable s a) a where | |
reflect = unsafePerformIO | |
$ do a <- deRefStablePtr p | |
freeStablePtr p | |
return (const a) | |
where p = reflectStorable (undefined :: s p) | |
reify :: a -> (forall s. Reflect s a => s -> w) -> w | |
reify a k = unsafePerformIO | |
$ do p <- newStablePtr a | |
reifyStorable p $ \(_::s (StablePtr a)) -> k' (undefined :: Stable s a) | |
where k' s = reflect s `seq` return (k s) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment