implementation module auds

import StdEnv
import Data.Maybe
import Data.Functor
import Data.Func
import Data.Either
import Data.Tuple
import Data.List
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.Trans
import qualified Data.Map
from Data.Map import :: Map
import System.FilePath

import System.IO
import System.Time

instance MonadFail ? where fail _ = ?None
instance MonadFail [] where fail _ = []
instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s

sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
sds s = SDS s (pure ())
instance read SDS where read (SDS s _) = read s
instance write SDS where write (SDS sds _) w = write sds w

source :: (m r) (w -> m ()) -> Source m r w
source read write = RWPair (ReadSource read) (WriteSource write)

constShare :: a -> ReadSource m a b | Monad m
constShare a = ReadSource $ pure a

nullShare :: WriteSource m a b | Monad m
nullShare = WriteSource (\_->pure ())

instance read ReadSource where read (ReadSource read) = Read <$> read
instance write WriteSource where write (WriteSource write) w = Written <$> write w

timeStamp :: ReadSource IO Timestamp ()
timeStamp = ReadSource $ withWorld time

par :: (r1 r2 -> m r) (w -> m (w1, w2)) (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m r w | TC r1 & TC r2 & TC w1 & TC w2
par readl writel left right = Par {readl=readl,writel=writel,left=left,right=right}

(>*<) infixl 6 :: (sdsl m r1 w1) (sdsr m r2 w2) -> Par sdsl sdsr m (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & Monad m
(>*<) l r = par (\x y->pure (x, y)) pure l r

instance read (Par sdsl sdsr) | read sdsl & read sdsr
where
	read (Par t=:{readl,left,right}) = read left >>= \v->case v of
		Read l = read right >>= \v->case v of
			Read r = Read <$> readl l r
			Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
		Reading s = pure $ Reading $ Par {t & left=s}
instance write (Par sdsl sdsr) | write sdsl & write sdsr
where
	write (Par t=:{writel,left,right}) w
		= writel w >>= \(w1, w2)->write left w1 >>= \v->case v of
			Written _ = write right w2 >>= \v->case v of
				Written _ = pure $ Written ()
				Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=nullShare, right=s}
			Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=s}

lens :: (r1 -> m r) (w r1 -> m (? w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
lens mapr mapw lens = Lens {mapr=mapr,mapw=mapw,lens=lens}

instance read (Lens sds) | read sds
where
	read (Lens t=:{mapr,lens}) = read lens >>= \v->case v of
		Read r = Read <$> mapr r
		Reading s = pure $ Reading $ Lens {t & lens=s}

instance read (RWPair sdsr sdsw) | read sdsr
where
	read (RWPair s w) = read s >>= \v->case v of
		Read r = pure $ Read r
		Reading s = pure $ Reading (RWPair s w)
instance write (RWPair sdsr sdsw) | write sdsw
where
	write (RWPair r s) w = write s w >>= \v->case v of
		Written _ = pure $ Written ()
		Writing s = pure $ Writing $ RWPair r s

instance write (Lens sds) | read sds & write sds
where
	write (Lens t=:{mapw,lens}) w = read lens >>= \v->case v of
		Read r = mapw w r >>= \w->case w of
			?None = pure $ Written ()
			?Just w = write lens w >>= \v->case v of
				Written _ = pure $ Written ()
				Writing s = pure $ Writing $ Lens {t & mapw= \_ _->pure $ ?Just w, lens=RWPair (constShare r) s}
		Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}

mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
mapRead f sds = lens f (\_ _->pure ?None) sds

fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
fromDynStore sds = lens
	(\r->case r of
		(r :: r^) = pure r
		_ = fail "type mismatch")
	(\w _->pure $ ?Just (dynamic w))
	sds

toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
toDynStore sds = lens
	(\r->pure (dynamic r))
	(\w _->case w of
		(w :: w^) = pure $ ?Just w
		_ = fail "type mismatch")
	sds

mapWrite :: (w` r -> m (? w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
mapWrite f sds = lens pure f sds

indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
indexedStore idx sds = lens
	(\r->maybe (fail "out of range") pure (r !? idx))
	(\w->pure o ?Just o updateAt idx w)
	sds

keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
keyedStore key sds = lens
	(maybe (fail "key not present") pure o 'Data.Map'.get key)
	(\w->pure o ?Just o 'Data.Map'.put key w)
	sds

select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
select select bind = Select {select=select,bind=bind}

instance read (Select sdsl sdsr) | read sdsl & read sdsr
where
	read (Select t=:{select,bind}) = read select >>= \v->case v of
		Read r = bind r >>= read
		Reading s = pure $ Reading $ Select {t & select=s}
instance write (Select sdsl sdsr) | read sdsl & write sdsr
where
	write (Select t=:{select,bind}) w = read select >>= \v->case v of
		Read r = bind r >>= flip write w
		Reading s = pure $ Writing $ Select {t & select=s}

indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
indexedSelect l r = select l $ pure o flip indexedStore r

keyedSelect :: (sdsl m k z) (sdsr m (Map k v) (Map k v))
	-> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
keyedSelect l r = select l $ pure o flip keyedStore r

getShare :: (sds m r w) -> m r | Monad m & read sds & TC r & TC w
getShare s = read s >>= \v->case v of
	Read r = pure r
	Reading s = getShare s

setShare :: w (sds m r w) -> m () | Monad m & write sds & TC r & TC w
setShare w s = write s w >>= \v->case v of
	Written _ = pure ()
	Writing s = setShare w s

updShare :: (r -> w) (sds m r w) -> m w | Monad m & read sds & write sds & TC r & TC w
updShare f s = f <$> getShare s >>= \v->setShare v s >>| pure v

//Start :: Either String (Map String Dynamic)
Start :: Either String (Int, Map String Dynamic)
Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
where
//	t = write (42, "blurp") (astore "foo" >*< astore "bar")
//	t = write 42 (astore "blurp")
//		>>| read (astore "blurp")
	t = setShare 42 (astore "blurp")
		>>| getShare (astore "blurp")

//Start world = evalIO t world
//where
//	t = read (file "auds.icl")

astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
astore s = fromDynStore $ dstore s

dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
dstore s = keyedStore s store

store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
store = source getState put

file :: FilePath -> Source IO String String
file p = source (readFileM p) (writeFileM p)