definition module auds

from Control.Applicative import class Applicative, class pure, class <*>
from Control.Monad import class Monad
from Control.Monad.State import :: StateT
from Data.Either import :: Either
from Data.Functor import class Functor
from Data.Map import :: Map
from StdOverloaded import class <, class fromString
from System.FilePath import :: FilePath
from System.IO import :: IO
from System.Time import :: Timestamp

class MonadFail m | Monad m where fail :: String -> m a
instance MonadFail ?, []
instance MonadFail (Either a) | fromString a
instance MonadFail (StateT s m) | MonadFail m

//* Result of a single read rewrite
:: ReadResult m r w
	= Read r //* done reading
	| E.sds: Reading (sds m r w) & read sds //* not done reading
	| ReadResultUnused (m ())

//* Result of a single write rewrite
:: WriteResult m r w
	= Written () //* done writing
	| E.sds: Writing (sds m r w) & write sds //* not done writing
	| WriteResultUnused (m ())


class read v  :: (v m r w) -> m (ReadResult m r w) | TC r & Monad m
class write v :: (v m r w) w -> m (WriteResult m r w) | TC w & Monad m

//* Box type, to get rid of a possible complex constructor of combinators
:: SDS m r w = E.sds: SDS (sds m r w) (m ()) /*force kind*/ & read sds & write sds
sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m

instance read SDS, ReadSource
instance read (RWPair sdsr sdsw) | read sdsr
instance read (Par sdsl sdsr) | read sdsl & read sdsr
instance read (Lens sds) | read sds
instance read (Select sdsl sdsr) | read sdsl & read sdsr

instance write SDS, WriteSource
instance write (RWPair sdsr sdsw) | write sdsw
instance write (Par sdsl sdsr) | write sdsl & write sdsr
instance write (Lens sds) | read sds & write sds
instance write (Select sdsl sdsr) | read sdsl & write sdsr

//* ?Just read something
:: ReadSource m r w = ReadSource (m r)
//* ?Just write something
:: WriteSource m r w = WriteSource (w -> m ())
//* Pair a two shares to form a read/write sds that only touches one share per action
:: RWPair sdsr sdsw m r w = RWPair (sdsr m r w) (sdsw m r w) | RWPairUnused (m ())

//* Special type of RWPair that contains sds sources
:: Source m r w :== RWPair ReadSource WriteSource m r w
source :: (m r) (w -> m ()) -> Source m r w

//* Combine two shares in parallel
:: Par sdsl sdsr m r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr m r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
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
:: ParOpts sdsl sdsr m r1 r2 w1 w2 r w =
	{ readl  :: r1 r2 -> m r
	, writel :: w -> m (w1, w2)
	, left   :: sdsl m r1 w1
	, right  :: sdsr m r2 w2
	}

//* Apply a lens to a share
:: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
lens :: (r1 -> m r) (w r1 -> m (? w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
:: LensOpts sds m r1 w1 r w =
	{ mapr :: r1 -> m r
	, mapw :: w r1 -> m (? w1)
	, lens :: sds m r1 w1
	}

//* Determine a share from the value read from another share
:: Select sdsl sdsr m r w = E.r1 w1: Select (SelectOpts sdsl sdsr m r1 w1 r w) & TC r1 & TC w1
select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
:: SelectOpts sdsl sdsr m r1 w1 r w =
	{ select :: sdsl m r1 w1
	, bind   :: r1 -> m (sdsr m r w)
	}

//* Immediately returns the given value on a read
constShare :: a -> ReadSource m a b | Monad m
//* Values written are discarded
nullShare :: WriteSource m a b | Monad m

//* Current time
timeStamp :: ReadSource IO Timestamp ()

//* Map a function to the value read
mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
(>?@) infixl 6
(>?@) :== mapRead

//* Map a function to the value written.
mapWrite :: (w` r -> m (? w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
(>!@) infixl 6
(>!@) :== mapWrite

(>*<) 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

fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m

indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m

indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
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

astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m

file :: FilePath -> Source IO String String