uds/ASDS.dcl

   1 definition module ASDS
   2
   3 from Data.Functor import class Functor
   4 from Control.Applicative import class Applicative, class <*>, class pure
   5 from Control.Monad import class Monad
   6 from Control.Monad.State import :: StateT
   7
   8 import ASDS.Source
   9 import ASDS.Parallel
  10 import ASDS.Select
  11 import ASDS.Lens
  12
  13 :: PViewT m a :== StateT [NRequest m] m a
  14 :: NRequest m = NRequest String (m ()) Dynamic
  15 //* @type :: String (m ()) p [NRequest] -> [NRequest] | TC p
  16 nrequestc p id hnd s :== [NRequest id hnd (dynamic p):s]
  17
  18 //* Used to force kinds of variables in a
  19 :: KindHelper a b :== b
  20
  21 //* Read a share with one rewrite step
  22 class read v :: (v m p r w) p -> PViewT m (ReadResult m p r w) | Monad m
  23 //* Write a share with one rewrite step
  24 class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | Monad m & TC p
  25 //* Generate a unique name
  26 class identity v :: (v m p r w) (KindHelper (m ()) [String]) -> [String]
  27 //* Observe a share and get notified when it happens
  28 class observe v :: (v m p r w) p String (m ()) -> PViewT m () | Monad m & TC p
  29
  30 //* Result of a single read rewrite
  31 :: ReadResult m p r w
  32         = Read (KindHelper (m ()) r) //* done reading
  33         | E.sds: Reading (sds m p r w) & read sds //* not done reading
  34
  35 //* Result of a single write rewrite
  36 :: WriteResult m p r w
  37         = Written (KindHelper (m ()) ()) //* done writing
  38         | E.sds: Writing (sds m p r w) & write sds //* not done writing
  39
  40 //* Read lens, it can choose to ignore the source
  41 :: LensRead m p r rs
  42         = LensRead (p rs -> m r)
  43         | LensReadConst (p -> m r)
  44
  45 //* Write lens, it can choose to ignore the source, and thus not read it
  46 :: LensWrite m p w rs ws
  47         = LensWrite (p w rs -> m (? ws))
  48         | LensWriteConst (p w -> m (? ws))
  49
  50 //* Box type, to get rid of a possible complex constructor of combinators
  51 :: SDS m p r w = E.sds: SDS (KindHelper (m ()) (sds m p r w)) & read, write, identity, observe sds
  52 sds :: (sds m p r w) -> SDS m p r w | read, write, identity, observe sds & Monad m
  53
  54 instance read SDS
  55 instance write SDS
  56 instance identity SDS
  57 instance observe SDS
  58
  59 //* Read a share completely
  60 getShare :: (sds m () r w) -> PViewT m r | Monad m & read sds & TC r & TC w
  61
  62 //* Write a share completely
  63 setShare :: w (sds m () r w) -> PViewT m () | Monad m & write sds & TC r & TC w
  64
  65 //* Update a share completely
  66 updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w
  67
  68 //* Trigger observing tasks
  69 trigger :: (v m p r w) (p -> Bool) -> PViewT m () | identity v & TC p & Monad m