-
Notifications
You must be signed in to change notification settings - Fork 24
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit 5608d69
Showing
5 changed files
with
247 additions
and
0 deletions.
There are no files selected for viewing
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,181 @@ | ||
{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TypeOperators #-} | ||
|
||
---------------------------------------------------------------------------- | ||
-- | | ||
-- Module : Data.Reflection | ||
-- Copyright : 2009 Edward Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan | ||
-- License : BSD3 | ||
-- | ||
-- Maintainer : Edward Kmett <[email protected]> | ||
-- Stability : experimental | ||
-- Portability : non-portable (scoped types, MPTCs, rank-n, FFI, kinds) | ||
-- | ||
-- Based on the Functional Pearl: Implicit Configurations paper by | ||
-- Oleg Kiselyov and Chung-chieh Shan. | ||
-- | ||
-- <http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf> | ||
-- | ||
-- Modified to minimize extensions and work with Data.Tagged rather than | ||
-- explicit scoped type variables by Edward Kmett. | ||
-- | ||
------------------------------------------------------------------------------- | ||
|
||
module Data.Reflection | ||
( | ||
-- * Reflect Integrals | ||
ReifiesNum | ||
, reflectNum | ||
, reifyIntegral | ||
-- * Reflect Lists of Integrals | ||
, ReifiesNums | ||
, reifyIntegrals | ||
-- * Reflect Storables | ||
, ReifiesStorable | ||
, reflectStorable | ||
, reifyStorable | ||
-- * Reflect Anything | ||
, Reifies | ||
, 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 | ||
import Control.Applicative | ||
import Prelude hiding (succ, pred) | ||
import Data.Tagged | ||
|
||
class Unused t where unused :: t -> () | ||
|
||
type Retag f g = forall b. Tagged g b -> Tagged f b | ||
|
||
newtype Zero = Zero Zero deriving (Show) | ||
newtype Twice s = Twice (Twice s) deriving (Show) | ||
newtype Succ s = Succ (Succ s) deriving (Show) | ||
newtype Pred s = Pred (Pred s) deriving (Show) | ||
instance Unused Zero where unused Zero{} = () | ||
instance Unused (Twice s) where unused Twice{} = () | ||
instance Unused (Succ s) where unused Succ{} = () | ||
instance Unused (Pred s) where unused Pred{} = () | ||
|
||
pop :: Retag (f s) s | ||
pop = retag | ||
{-# INLINE pop #-} | ||
|
||
class ReifiesNum s where | ||
reflectNum :: Num a => Tagged s a | ||
|
||
instance ReifiesNum Zero where | ||
reflectNum = pure 0 | ||
|
||
instance ReifiesNum s => ReifiesNum (Twice s) where | ||
reflectNum = (2*) <$> pop reflectNum | ||
|
||
instance ReifiesNum s => ReifiesNum (Succ s) where | ||
reflectNum = (1+) <$> pop reflectNum | ||
|
||
instance ReifiesNum s => ReifiesNum (Pred s) where | ||
reflectNum = subtract 1 <$> pop reflectNum | ||
|
||
reifyIntegral :: Integral a => a -> (forall s. ReifiesNum s => Tagged s w) -> w | ||
reifyIntegral i k = case quotRem i 2 of | ||
(0, 0) -> zero k | ||
(j, 0) -> reifyIntegral j (twice k) | ||
(j, 1) -> reifyIntegral j (twice (succ k)) | ||
(j,-1) -> reifyIntegral j (twice (pred k)) | ||
_ -> undefined | ||
where | ||
twice :: Retag s (Twice s) | ||
twice = retag | ||
succ :: Retag s (Succ s) | ||
succ = retag | ||
pred :: Retag s (Pred s) | ||
pred = retag | ||
zero :: Tagged Zero a -> a | ||
zero = unTagged | ||
|
||
newtype Nil = Nil Nil | ||
newtype Cons s ss = Cons (Cons s ss) | ||
instance Unused Nil where unused Nil{} = () | ||
instance Unused (Cons s ss) where unused Cons{} = () | ||
|
||
class ReifiesNums ss where | ||
reflectNums :: Num a => Tagged ss [a] | ||
|
||
instance ReifiesNums Nil where | ||
reflectNums = pure [] | ||
|
||
instance (ReifiesNum s, ReifiesNums ss) => ReifiesNums (Cons s ss) where | ||
reflectNums = (:) <$> car reflectNum <*> cdr reflectNums where | ||
car :: Retag (Cons s ss) s | ||
car = retag | ||
cdr :: Retag (Cons s ss) ss | ||
cdr = retag | ||
|
||
reifyIntegrals :: Integral a => [a] -> (forall ss. ReifiesNums ss => Tagged ss w) -> w | ||
reifyIntegrals [] k = nil k where | ||
nil :: Tagged Nil a' -> a' | ||
nil = unTagged | ||
reifyIntegrals (i:ii) k = reifyIntegral i (reifyIntegrals ii (cons k)) where | ||
cons :: Tagged (Cons s' ss') a' -> Tagged ss' (Tagged s' a') | ||
cons = pure . retag | ||
|
||
newtype Store s a = Store (Store s a) | ||
instance Unused (Store s a) where unused Store{} = () | ||
|
||
class ReifiesStorable s where | ||
reflectStorable :: Storable a => Tagged (s a) a | ||
|
||
instance ReifiesNums s => ReifiesStorable (Store s) where | ||
reflectStorable = r where | ||
r = unsafePerformIO $ alloca $ \p -> do | ||
pokeArray (castPtr p) (bytes reflectNums r) | ||
pure <$> peek p | ||
bytes :: Tagged s' [CChar] -> Tagged (Store s' b) b -> [CChar] | ||
bytes (Tagged a) _ = a | ||
{-# NOINLINE reflectStorable #-} | ||
|
||
store :: Retag s' (Store s' c) | ||
store = retag | ||
|
||
reifyStorable :: Storable a => a -> (forall s. ReifiesStorable s => Tagged (s a) w) -> w | ||
reifyStorable a k = reifyIntegrals bytes (store k) | ||
where | ||
bytes :: [CChar] | ||
bytes = unsafePerformIO $ with a (peekArray (sizeOf a) . castPtr) | ||
{-# NOINLINE reifyStorable #-} | ||
|
||
class Reifies s a | s -> a where | ||
reflect :: Tagged s a | ||
|
||
newtype Stable s a = Stable (s (Stable s a)) | ||
instance Unused (Stable s a) where unused Stable{} = () | ||
|
||
instance ReifiesStorable s => Reifies (Stable s a) a where | ||
reflect = r where | ||
r = unsafePerformIO $ do | ||
pure <$> deRefStablePtr p <* freeStablePtr p | ||
|
||
p = pointer reflectStorable r | ||
|
||
pointer :: Tagged (s' p) p -> Tagged (Stable s' a') a' -> p | ||
pointer (Tagged a) _ = a | ||
{-# NOINLINE reflect #-} | ||
|
||
reify :: a -> (forall s. Reifies s a => Tagged s w) -> w | ||
reify a k = unsafePerformIO $ do | ||
p <- newStablePtr a | ||
reifyStorable p (stable (reflect `before` (return <$> k))) | ||
where | ||
stable :: Retag (s' (StablePtr a')) (Stable s' a') | ||
stable = retag | ||
before :: Tagged (s' a') a' -> Tagged (s' a') r -> Tagged (s' a') r | ||
before = seq | ||
{-# NOINLINE reify #-} | ||
|
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
Copyright (c) 2009 Edward Kmett | ||
Copyright (c) 2004 Oleg Kiselyov and Chung-chieh Shan | ||
All rights reserved. | ||
|
||
Redistribution and use in source and binary forms, with or without | ||
modification, are permitted provided that the following conditions are | ||
met: | ||
|
||
* Redistributions of source code must retain the above copyright | ||
notice, this list of conditions and the following disclaimer. | ||
|
||
* Redistributions in binary form must reproduce the above | ||
copyright notice, this list of conditions and the following | ||
disclaimer in the documentation and/or other materials provided | ||
with the distribution. | ||
|
||
* Neither the name of Edward Kmett nor the names of other | ||
contributors may be used to endorse or promote products derived | ||
from this software without specific prior written permission. | ||
|
||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS | ||
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT | ||
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR | ||
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT | ||
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, | ||
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT | ||
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, | ||
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY | ||
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT | ||
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE | ||
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
reflection | ||
========== | ||
|
||
Implementation of the ideas presented in the paper Functional Pearl: Implicit Configurations by Oleg Kiselyov and Chung-chieh Shan. Modified to avoid the use of scoped type variables, and to use a phantom type wrapper rather than dummy arguments. |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
#!/usr/bin/runhaskell | ||
> module Main (main) where | ||
|
||
> import Distribution.Simple | ||
|
||
> main :: IO () | ||
> main = defaultMain |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
name: reflection | ||
version: 0.3.0 | ||
license: BSD3 | ||
license-file: LICENSE | ||
author: Edward A. Kmett, Oleg Kiselyov and Chung-chieh Shan | ||
maintainer: Edward A. Kmett <[email protected]> | ||
stability: experimental | ||
homepage: http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf | ||
category: Data, Reflection, Dependent Types | ||
synopsis: Functional Pearl: Implicit Configurations | ||
copyright: 2009 Edward A. Kmett, 2004 Oleg Kiselyov and Chung-chieh Shan | ||
description: Implementation of the ideas presented in the paper "Functional Pearl: Implicit Configurations" by Oleg Kiselyov and Chung-chieh Shan. | ||
Modified to avoid the use of scoped type variables, and to use a phantom type wrapper rather than dummy arguments. | ||
build-type: Simple | ||
cabal-version: >=1.2 | ||
|
||
library | ||
build-depends: | ||
base >= 4 && < 5, | ||
tagged >= 0.0 && < 0.1 | ||
exposed-modules: | ||
Data.Reflection | ||
|
||
ghc-options: -Wall |