module test

import StdEnv
import Data.Maybe
import Data.Functor
import Data.Func
import Data.Tuple
import Data.List
import Control.Applicative
import Control.Monad
import qualified Data.Map

class get v ~st :: (v r w) .st -> .(Maybe r, .st) | TC r
class put v ~st :: w (v r w) .st -> .(Maybe (), .st) | TC w

:: SDS sds a :== sds a a

:: Source r w = Source String
:: St :== 'Data.Map'.Map String Dynamic

instance get Source St
where
	get (Source n) st = case 'Data.Map'.get n st of
		Just (a :: a^) = (Just a, st)
		_ = (Nothing, st)

instance put Source St
where
	put w (Source n) st = (Just (), 'Data.Map'.put n (dynamic w) st)

:: Par sdsl sdsr r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
:: ParOpts sdsl sdsr r1 r2 w1 w2 r w =
	{ read  :: r1 r2 -> Maybe r
	, write :: w -> Maybe (w1, w2)
	, left  :: sdsl r1 w1
	, right :: sdsr r2 w2
	}
(>*<) infixl 6 :: (sdsl r1 w1) (sdsr r2 w2) -> Par sdsl sdsr (r1, r2) (w1, w2) | get sdsl St & put sdsr St & TC r1 & TC r2 & TC w1 & TC w2
(>*<) l r = Par {read= \x y->Just (x, y), write=Just, left=l, right=r}

instance get (Par sdsl sdsr) St | get sdsl St & get sdsr St
where
	get (Par {read,left,right}) st
		# (ml, st) = get left st
		# (mr, st) = get right st
		= (join $ read <$> ml <*> mr, st)
instance put (Par sdsl sdsr) St | put sdsl St & put sdsr St
where
	put w (Par {write,left,right}) st
		= case write w of
			Just (w1, w2)
				# (ml, st) = put w1 left st
				# (mr, st) = put w2 right st
				= (ml *> mr, st)
			Nothing = (Nothing, st)

:: Lens sds r w = E.r1 w1: Lens (LensOpts sds r1 w1 r w) & TC r1 & TC w1
:: LensOpts sds r1 w1 r w =
	{ mapr :: r1   -> Maybe r
	, mapw :: w r1 -> Maybe w1
	, lens :: sds r1 w1
	}

instance get (Lens sds) St | get sds St
where
	get (Lens {mapr,lens}) st = appFst ((=<<) mapr) $ get lens st
instance put (Lens sds) St | get sds St & put sds St
where
	put w (Lens {mapw,lens}) st
		# (mv, st) = get lens st
		= case mv of
			Just r = case mapw w r of
				Just w = put w lens st
				Nothing = (Nothing, st)
			Nothing = (Nothing, st)

:: Select sdsl sdsr r w = E.r1 w1: Select (SelectOpts sdsl sdsr r1 w1 r w) & TC r1 & TC w1
:: SelectOpts sdsl sdsr r1 w1 r w =
	{ select :: sdsl r1 w1
	, bind   :: r1 -> (sdsr r w)
	}

instance get (Select sdsl sdsr) St | get sdsl St & get sdsr St
where
	get (Select {select,bind}) st
		= case get select st of
			(Just r, st)  = get (bind r) st
			(Nothing, st) = (Nothing, st)
instance put (Select sdsl sdsr) St | get sdsl St & put sdsr St
where
	put w (Select {select,bind}) st
		= case get select st of
			(Just r, st) = put w (bind r) st
			(Nothing, st) = (Nothing, st)

mapRead :: (r -> r`) (sds r w) -> Lens sds r` w | TC r` & TC r & TC w
mapRead f sds = Lens {mapr=Just o f, mapw=const o Just, lens=sds}
(>?@) infixl 6
(>?@) :== mapRead

mapWrite :: (w` r -> Maybe w) (sds r w) -> Lens sds r w` | TC r & TC w & TC w`
mapWrite f sds = Lens {mapr=Just, mapw=f, lens=sds}
(>!@) infixl 6
(>!@) :== mapWrite

indexedStore :: Int (SDS sds [a]) -> SDS (Lens sds) a | TC a
indexedStore idx sds
	= Lens
		{ mapr = \r->r !? idx
		, mapw = \w->Just o updateAt idx w
		, lens = sds
		}

indexedSelect :: (sdsl Int z) (SDS sdsr [a]) -> SDS (Select sdsl (Lens sdsr)) a | TC a & TC z
indexedSelect l r = Select {select=l, bind=flip indexedStore r}

keyedSelect :: (sdsl k z) (SDS sdsr ('Data.Map'.Map k v)) -> SDS (Select sdsl (Lens sdsr)) v | TC z & TC v & TC k & < k
keyedSelect l r = Select {select=l, bind=flip keyedStore r}

keyedStore :: k (SDS sds ('Data.Map'.Map k v)) -> SDS (Lens sds) v | TC v & TC k & < k
keyedStore key sds
	= Lens
		{ mapr = 'Data.Map'.get key
		, mapw = \r->Just o 'Data.Map'.put key r
		, lens = sds
		}

Start = appSnd 'Data.Map'.toList
	$ put (42, "blurp") (store "foo" >*< store "bar") 'Data.Map'.newMap

store :: (String -> Source a a) | TC a
store = Source