uds/ASDS/Source.dcl

   1 definition module ASDS.Source
   2
   3 from ASDS import class read, class write, class observe, class identity, :: KindHelper
   4 from Control.Monad import class Monad
   5 from Control.Applicative import class Applicative, class <*>, class pure
   6 from Data.Functor import class Functor
   7
   8 //* Just read something
   9 :: ReadSource m p r w = ReadSource (p -> m r)
  10
  11 //* Just write something
  12 :: WriteSource m p r w = WriteSource String (p w -> m (p -> Bool))
  13
  14 //* Pair a two shares to form a read/write sds that only touches one share per action
  15 :: RWPair sdsr sdsw m p r w = RWPair (KindHelper (m ()) (sdsr m p r w)) (sdsw m p r w)
  16 rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w
  17
  18 //* Special type of RWPair that contains sds sources
  19 :: Source m p r w :== RWPair ReadSource WriteSource m p r w
  20 source :: String (p -> m r) (p w -> m (p -> Bool)) -> Source m p r w
  21
  22 instance read ReadSource, (RWPair sdsr sdsw) | read sdsr
  23 instance write WriteSource, (RWPair sdsr sdsw) | write sdsw
  24 instance identity WriteSource, (RWPair sdsr sdsw) | identity sdsw
  25 instance observe WriteSource, (RWPair sdsr sdsw) | observe sdsw
  26
  27 //* Immediately returns the given value on a read
  28 constShare :: a -> ReadSource m p a b | pure m
  29
  30 //* Values written are discarded
  31 nullShare :: WriteSource m p a b | pure m