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