{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-incoherent-instances #-}

module MonadicRegions where

{-
  NOTE ABOUT EXTENSIONS

The overlapping instance extension is used ONLY for the type equality
testing. To be more precise, we use a subset of that extension
as implemented in GHC 6.3 and above. Given a set of instances
  class C a where op:: a -> Int
  instance C a where ...
  instance C Bool where ...
  data W  = forall a. W a
the expression
  case W () of W x -> op x 
is well-typed with the "instance C a" chosen. In the context of TypeEq,
that behavior guarantees that a quantified variable is equal only to itself
and nothing else. So, the use of overlapping instances in this code
is well-defined and sound.

The existence of this remarkable feature has been pointed out by Simon
Peyton-Jones, who also implemented it.

As it turns out, with -fallow-incoherent-instances, the code runs
(and gives errors, where expected) even with GHC 6.2.1

So, this code tested on GHC 6.2.1 and GHC ghc-6.3.20041106 snapshot
and GHC 6.4
-}

import Control.Monad.ST
import Data.STRef

testr1 = runST (do a <- (runRGN (do return ()))
		   return a)

testr2 = let vf = runRGN (do r1 <- getRGN
			     a  <- newRGNVar (1::Int) r1
			     readRGNVar a)
	 in runST vf

-- try to allocate RGNVar in a bad scope
-- It gives an error, as expected
{-
testrw = let vf = runRGN (do r1 <- badgetRGN
			     a  <- newRGNVar (1::Int) r1
			     readRGNVar a)
	 in runST vf
-}

testr3 = let vf = runRGN (do r1 <- getRGN
			     a  <- newRGNVar (1::Int) r1
			     c <- newRGN (do v <- readRGNVar a
					     r2 <- getRGN
					     b <- newRGNVar (2::Int) r2
					     v' <- readRGNVar b
					     newRGNVar (v+v') r1)
			     readRGNVar c)
	 in runST vf

-- Note the inferred type of gpair!
gpair v w = do
	    a <- readRGNVar v
	    b <- readRGNVar w
	    l <- getRGN
	    newRGNVar (a,b) l

testr4 = let vf = runRGN (do r1 <- getRGN
			     v  <- newRGNVar (1::Int) r1
			     newRGN (do r2 <- getRGN
				        w  <- newRGNVar (2::Int) r2
				        newRGN (do
						p1 <- gpair v w 
						p2 <- gpair w v
						a1 <- readRGNVar p1
					        a2 <- readRGNVar p2
					        return (a1,a2))))
	 in runST vf

-- Indeed, gpair is polymorphic to the desired extent...
testr5 = let vf = runRGN (do r1 <- getRGN
			     v  <- newRGNVar (1::Int) r1
			     newRGN (do p <- gpair v v 
				        readRGNVar p))
	 in runST vf

------------------------------------------------------------------------
-- The RGN monad
-- RGN r p s a
-- r is the region's unique label
-- p is the HList of region's labels in scope (it is treated like a SET)
-- s is the thread id of the underlying ST monad, in term of which
--      we emulate everything
-- a is the type of the value

newtype RGN r p s a = RGN (ST s a)

unRGN (RGN a) = a

instance Monad (RGN r p s) where
    return = RGN . return
    (RGN m) >>= f = RGN $ m >>= (unRGN . f)

runRGN::(forall r. RGN r (HCons r HNil) s a) -> ST s a
runRGN = unRGN

newRGN::(forall r'. RGN r' (HCons r' p) s a) -> RGN r p s a
newRGN = RGN . unRGN

-- Get our own label
data RGNLab r = RGNLab
getRGN:: RGN r p s (RGNLab r)
getRGN = return RGNLab

-- used for testing
badgetRGN:: RGN r p s (RGNLab r')
badgetRGN = return RGNLab


newtype RGNVar r s a = RGNVar (STRef s a)
--newRGNVar:: a -> (RGNLab rv) -> RGN r p s (RGNVar rv s a)
newRGNVar:: HOccurs rv p => a -> (RGNLab rv) -> RGN r p s (RGNVar rv s a)
newRGNVar v _ = RGN $ newSTRef v >>= return . RGNVar

readRGNVar::HOccurs rv p => RGNVar rv s a -> RGN r p s a
--readRGNVar::RGNVar rv s a -> RGN r p s a
readRGNVar (RGNVar r) = RGN $ readSTRef r


------------------------------------------------------------------------

-- Testing for occurrence of a type in a HList
-- The constraint `HOccurs a l' holds if type `a' occurs in the type list l

data HCons a b = HCons a b
data HNil = HNil

class HOccurs a l
instance HOccurs a  (HCons a l)
instance HOccurs a l => HOccurs a (HCons a' l)


-- some tests
test1:: HOccurs a l => l -> a; test1 = undefined
_ = test1 (HCons True (HCons () HNil)) :: Bool
_ = test1 (HCons True (HCons () HNil)) :: ()
-- The latter should be a type error
-- _ = test1 (HCons True (HCons () HNil)) :: Int


data W  = forall a. W a
test2::HOccurs a l => l -> a -> (); test2 _ _ = ()

_ = case W True of W x -> test2 (HCons x (HCons 'a' HNil)) 'b'
_ = case W True of W x -> test2 (HCons 'z' (HCons x HNil)) 'b'
_ = case W True of W x -> test2 (HCons () (HCons x (HCons 'a' HNil))) 'b'
_ = case W True of W x -> test2 (HCons () (HCons x (HCons 'a' HNil))) ()
_ = case W True of W x -> test2 (HCons x (HCons 'a' HNil)) x
_ = case W True of
      W x -> 
	  case W 'a' of W y -> 
			    test2 (HCons x (HCons 'a' (HCons y HNil))) x

_ = case W True of
      W x -> 
	  case W 'a' of W y -> 
			    test2 (HCons x (HCons 'a' (HCons y HNil))) y

{-
  But the following is error:
    No instance for (HOccurs a HNil)
      arising from use of `test2' at /tmp/m.hs:111:28-32

_ = case W True of
      W x -> 
	  case W 'a' of W y -> 
			    test2 (HCons x (HCons 'a' (HCons x HNil))) y

-}