uds/auds.dcl

   1 definition module auds
   2
   3 from Control.Applicative import class Applicative, class pure, class <*>
   4 from Control.Monad import class Monad
   5 from Control.Monad.State import :: StateT
   6 from Data.Either import :: Either
   7 from Data.Functor import class Functor
   8 from Data.Map import :: Map
   9 from StdOverloaded import class <, class fromString
  10 from System.FilePath import :: FilePath
  11 from System.IO import :: IO
  12 from System.Time import :: Timestamp
  13
  14 class MonadFail m | Monad m where fail :: String -> m a
  15 instance MonadFail ?, []
  16 instance MonadFail (Either a) | fromString a
  17 instance MonadFail (StateT s m) | MonadFail m
  18
  19 //* Result of a single read rewrite
  20 :: ReadResult m r w
  21         = Read r //* done reading
  22         | E.sds: Reading (sds m r w) & read sds //* not done reading
  23         | ReadResultUnused (m ())
  24
  25 //* Result of a single write rewrite
  26 :: WriteResult m r w
  27         = Written () //* done writing
  28         | E.sds: Writing (sds m r w) & write sds //* not done writing
  29         | WriteResultUnused (m ())
  30
  31
  32 class read v  :: (v m r w) -> m (ReadResult m r w) | TC r & Monad m
  33 class write v :: (v m r w) w -> m (WriteResult m r w) | TC w & Monad m
  34
  35 //* Box type, to get rid of a possible complex constructor of combinators
  36 :: SDS m r w = E.sds: SDS (sds m r w) (m ()) /*force kind*/ & read sds & write sds
  37 sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
  38
  39 instance read SDS, ReadSource
  40 instance read (RWPair sdsr sdsw) | read sdsr
  41 instance read (Par sdsl sdsr) | read sdsl & read sdsr
  42 instance read (Lens sds) | read sds
  43 instance read (Select sdsl sdsr) | read sdsl & read sdsr
  44
  45 instance write SDS, WriteSource
  46 instance write (RWPair sdsr sdsw) | write sdsw
  47 instance write (Par sdsl sdsr) | write sdsl & write sdsr
  48 instance write (Lens sds) | read sds & write sds
  49 instance write (Select sdsl sdsr) | read sdsl & write sdsr
  50
  51 //* ?Just read something
  52 :: ReadSource m r w = ReadSource (m r)
  53 //* ?Just write something
  54 :: WriteSource m r w = WriteSource (w -> m ())
  55 //* Pair a two shares to form a read/write sds that only touches one share per action
  56 :: RWPair sdsr sdsw m r w = RWPair (sdsr m r w) (sdsw m r w) | RWPairUnused (m ())
  57
  58 //* Special type of RWPair that contains sds sources
  59 :: Source m r w :== RWPair ReadSource WriteSource m r w
  60 source :: (m r) (w -> m ()) -> Source m r w
  61
  62 //* Combine two shares in parallel
  63 :: 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
  64 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
  65 :: ParOpts sdsl sdsr m r1 r2 w1 w2 r w =
  66         { readl  :: r1 r2 -> m r
  67         , writel :: w -> m (w1, w2)
  68         , left   :: sdsl m r1 w1
  69         , right  :: sdsr m r2 w2
  70         }
  71
  72 //* Apply a lens to a share
  73 :: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
  74 lens :: (r1 -> m r) (w r1 -> m (? w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
  75 :: LensOpts sds m r1 w1 r w =
  76         { mapr :: r1 -> m r
  77         , mapw :: w r1 -> m (? w1)
  78         , lens :: sds m r1 w1
  79         }
  80
  81 //* Determine a share from the value read from another share
  82 :: Select sdsl sdsr m r w = E.r1 w1: Select (SelectOpts sdsl sdsr m r1 w1 r w) & TC r1 & TC w1
  83 select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
  84 :: SelectOpts sdsl sdsr m r1 w1 r w =
  85         { select :: sdsl m r1 w1
  86         , bind   :: r1 -> m (sdsr m r w)
  87         }
  88
  89 //* Immediately returns the given value on a read
  90 constShare :: a -> ReadSource m a b | Monad m
  91 //* Values written are discarded
  92 nullShare :: WriteSource m a b | Monad m
  93
  94 //* Current time
  95 timeStamp :: ReadSource IO Timestamp ()
  96
  97 //* Map a function to the value read
  98 mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
  99 (>?@) infixl 6
 100 (>?@) :== mapRead
 101
 102 //* Map a function to the value written.
 103 mapWrite :: (w` r -> m (? w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
 104 (>!@) infixl 6
 105 (>!@) :== mapWrite
 106
 107 (>*<) 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
 108
 109 fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
 110 toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
 111
 112 indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
 113 keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
 114
 115 indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
 116 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
 117
 118 astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
 119 dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
 120 store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
 121
 122 file :: FilePath -> Source IO String String