module Data.OpenWitness
(
OpenWitness,
RealWorld,IOWitness,newIOWitness,
OW,newOpenWitnessOW,runOW,owToIO,
iowitness
) where
{
import Prelude;
import Data.Kind;
import Data.List;
import System.Random;
import Language.Haskell.TH;
import Unsafe.Coerce;
import System.IO.Unsafe (unsafePerformIO);
import Control.Concurrent.MVar;
import Control.Monad.Fix;
import Control.Monad.Trans.State;
import Data.Functor.Identity;
import Data.Traversable;
import Data.Hashable;
import Data.Witness;
import Data.Type.Heterogeneous;
unsafeSameType :: HetEq a b;
unsafeSameType = unsafeCoerce ReflH;
;
newtype OpenWitness :: * -> forall (k :: *). k -> * where
{
MkOpenWitness :: Integer -> OpenWitness s a;
};
instance Eq (OpenWitness s a) where
{
(MkOpenWitness p) == (MkOpenWitness q) = p == q;
};
instance TestHetEquality (OpenWitness s) where
{
testHetEquality (MkOpenWitness ua) (MkOpenWitness ub) =
if ua == ub then Just unsafeSameType else Nothing;
};
instance TestEquality (OpenWitness s) where
{
testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;
};
;
data RealWorld;
;
type IOWitness = OpenWitness RealWorld;
ioWitnessSource :: MVar Integer;
;
ioWitnessSource = unsafePerformIO (newMVar 0);
;
newIOWitness :: forall a. IO (IOWitness a);
newIOWitness = do
{
val <- takeMVar ioWitnessSource;
putMVar ioWitnessSource (val + 1);
return (MkOpenWitness val);
};
type OWState = Integer;
;
newtype OW s a = MkOW (State OWState a) deriving (Functor,Applicative,Monad,MonadFix);
;
runOW :: forall a. (forall s. OW s a) -> a;
runOW uw = (\(MkOW st) -> evalState st 0) uw;
;
newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);
newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val,val+1)));
;
owToIO :: OW RealWorld a -> IO a;
owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let
{
(a,count) = runState st start;
} in return (count,a));
;
unsafeIOWitnessFromInteger :: Integer -> IOWitness a;
unsafeIOWitnessFromInteger = MkOpenWitness;
;
unsafeIOWitnessFromString :: String -> IOWitness a;
unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hash;
;
iowitness :: TypeQ -> Q Exp;
iowitness qt = do
{
t <- qt;
_ <- forM (freevarsType t) (\v -> reportError ("Type variable "++(show v)++" free in iowitness type"));
l <- location;
rnd :: Integer <- runIO randomIO;
key <- return ((showLoc l) ++ "/" ++ (show rnd));
keyExpr <- return (LitE (StringL key));
untypedWitExpr <- [| unsafeIOWitnessFromString $(return keyExpr) |];
[| $(return untypedWitExpr) :: IOWitness $(return t) |];
} where
{
showLoc :: Loc -> String;
showLoc l = (loc_filename l) ++ "=" ++ (loc_package l) ++ ":" ++ (loc_module l) ++ (show (loc_start l)) ++ (show (loc_end l));
unionList :: (Eq a) => [[a]] -> [a];
unionList [] = [];
unionList (l:ls) = union l (unionList ls);
bindingvarTVB :: TyVarBndr -> Name;
bindingvarTVB (PlainTV n) = n;
bindingvarTVB (KindedTV n _) = n;
freevarsType :: Language.Haskell.TH.Type -> [Name];
freevarsType (ForallT tvbs ps t) =
(union (freevarsType t) (unionList (fmap freevarsType ps))) \\ (fmap bindingvarTVB tvbs);
freevarsType (VarT name) = [name];
freevarsType (AppT t1 t2) = union (freevarsType t1) (freevarsType t2);
freevarsType (SigT t _) = freevarsType t;
freevarsType _ = [];
};
}