definition module ASDS

from Data.Functor import class Functor
from Control.Applicative import class Applicative, class <*>, class pure
from Control.Monad import class Monad
from Control.Monad.State import :: StateT

import ASDS.Source
import ASDS.Parallel
import ASDS.Select
import ASDS.Lens

:: PViewT m a :== StateT [NRequest m] m a
:: NRequest m = NRequest String (m ()) Dynamic
//* @type :: String (m ()) p [NRequest] -> [NRequest] | TC p
nrequestc p id hnd s :== [NRequest id hnd (dynamic p):s]

//* Used to force kinds of variables in a
:: KindHelper a b :== b

//* Read a share with one rewrite step
class read v :: (v m p r w) p -> PViewT m (ReadResult m p r w) | Monad m
//* Write a share with one rewrite step
class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | Monad m & TC p
//* Generate a unique name
class identity v :: (v m p r w) (KindHelper (m ()) [String]) -> [String]
//* Observe a share and get notified when it happens
class observe v :: (v m p r w) p String (m ()) -> PViewT m () | Monad m & TC p

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

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

//* Read lens, it can choose to ignore the source
:: LensRead m p r rs
	= LensRead (p rs -> m r)
	| LensReadConst (p -> m r)

//* Write lens, it can choose to ignore the source, and thus not read it
:: LensWrite m p w rs ws
	= LensWrite (p w rs -> m (? ws))
	| LensWriteConst (p w -> m (? ws))

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

instance read SDS
instance write SDS
instance identity SDS
instance observe SDS

//* Read a share completely
getShare :: (sds m () r w) -> PViewT m r | Monad m & read sds & TC r & TC w

//* Write a share completely
setShare :: w (sds m () r w) -> PViewT m () | Monad m & write sds & TC r & TC w

//* Update a share completely
updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w

//* Trigger observing tasks
trigger :: (v m p r w) (p -> Bool) -> PViewT m () | identity v & TC p & Monad m