uds/asds.dcl

   1 definition module asds
   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 p r w
  22         = Read r //* done reading
  23         | E.sds: Reading (sds m p r w) & read sds //* not done reading
  24         | ReadResultUnused (m ())
  25
  26 //* Result of a single write rewrite
  27 :: WriteResult m p r w
  28         = Written () //* done writing
  29         | E.sds: Writing (sds m p r w) & write sds //* not done writing
  30         | WriteResultUnused (m ())
  31
  32 //* Read a share with one rewrite step
  33 class read v :: (v m p r w) p -> m (ReadResult m p r w) | TC r & Monad m
  34 //* Write a share with one rewrite step
  35 class write v :: (v m p r w) p w -> m (WriteResult m p r w) | TC w & Monad m
  36 //* Read a share completely
  37 getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w
  38 //* Write a share completely
  39 setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w
  40 //* Update a share completely
  41 updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w
  42
  43 //* Box type, to get rid of a possible complex constructor of combinators
  44 :: SDS m p r w = E.sds: SDS (sds m p r w) (m ()) /*force kind*/ & read sds & write sds
  45 sds :: (sds m p r w) -> SDS m p r w | read sds & write sds & Monad m
  46
  47 instance read SDS, ReadSource
  48 instance read (RWPair sdsr sdsw) | read sdsr
  49 instance read (Par sdsl sdsr) | read sdsl & read sdsr
  50 instance read (Lens sds) | read sds
  51 //instance read (Select sdsl sdsr) | read sdsl & read sdsr
  52
  53 instance write SDS, WriteSource
  54 instance write (RWPair sdsr sdsw) | write sdsw
  55 instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr
  56 instance write (Lens sds) | read sds & write sds
  57 //instance write (Select sdsl sdsr) | read sdsl & write sdsr
  58
  59 //* Just read something
  60 :: ReadSource m p r w = ReadSource (p -> m r)
  61 //* Just write something
  62 :: WriteSource m p r w = WriteSource (p w -> m ())
  63 //* Pair a two shares to form a read/write sds that only touches one share per action
  64 :: RWPair sdsr sdsw m p r w = RWPair (sdsr m p r w) (sdsw m p r w) | RWPairUnused (m ())
  65
  66 //* Special type of RWPair that contains sds sources
  67 :: Source m p r w :== RWPair ReadSource WriteSource m p r w
  68 source :: (p -> m r) (p w -> m ()) -> Source m p r w
  69
  70 //* Combine two shares in parallel
  71 :: Par sdsl sdsr m p r w = E.p1 p2 r1 r2 w1 w2: Par (ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w) & TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2
  72 par :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 w1) (p w r2 -> m (Maybe w2)) (sdsl m p1 r1 w1) (sdsr m p2 r2 w2) -> Par sdsl sdsr m p r w | TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2
  73 :: ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w =
  74         { param  :: p -> (p1, p2)
  75         , readl  :: r1 r2 -> r
  76         , writel :: LensWrite m p w r1 w1
  77 //      , writel :: p w r1 -> m (Maybe w1)
  78         , writer :: p w r2 -> m (Maybe w2)
  79         , left   :: sdsl m p1 r1 w1
  80         , right  :: sdsr m p2 r2 w2
  81         }
  82
  83 //* Apply a lens to a share
  84 :: Lens sds m p r w = E.p1 r1 w1: Lens (LensOpts sds m p1 r1 w1 p r w) & TC r1 & TC w1 & TC p1
  85 lens :: (p -> p1) (LensRead m p r r1) (LensWrite m p w r1 w1) (sds m p1 r1 w1) -> Lens sds m p r w | TC r1 & TC w1 & TC p1
  86 :: LensOpts sds m p1 r1 w1 p r w =
  87         { param  :: p -> p1
  88         , mapr   :: LensRead m p r r1
  89         , mapw   :: LensWrite m p w r1 w1
  90         , lens   :: sds m p1 r1 w1
  91         }
  92
  93 :: LensRead m p r rs
  94         = LensRead (p rs -> m r)
  95         | LensReadConst (p -> m r)
  96 :: LensWrite m p w rs ws
  97         = LensWrite (p w rs -> m (Maybe ws))
  98         | LensWriteConst (p w -> m (Maybe ws))
  99
 100 //* Determine a share from the value read from another share
 101 :: Select sdsl sdsr m p r w = E.p1 r1 w1 p2: Select (SelectOpts sdsl sdsr m p1 r1 w1 p2 p r w) & TC r1 & TC p1 & TC p2
 102 //select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
 103 :: SelectOpts sdsl sdsr m p1 r1 w1 p2 p r w =
 104         { index  :: sdsl m p1 r1 w1
 105         , source :: sdsr m p2 r w
 106         , parami :: p -> p1
 107         , params :: p r1 -> p2
 108         , unused :: m ()
 109         }
 110
 111 //* Immediately returns the given value on a read
 112 constShare :: a -> ReadSource m p a b | Monad m
 113 //* Values written are discarded
 114 nullShare :: WriteSource m p a b | Monad m
 115
 116 //* Current time
 117 timeStamp :: ReadSource IO () Timestamp ()
 118
 119 ////* Map a function to the value read
 120 mapRead :: (r -> m r`) (sds m p r w) -> Lens sds m p r` w | TC r` & TC r & TC w & TC p & Monad m
 121 (>?@) infixl 6
 122 (>?@) :== mapRead
 123
 124 //* Map a function to the value written.
 125 mapWrite :: (w` r -> m (Maybe w)) (sds m p r w) -> Lens sds m p r w` | TC r & TC w & TC w` & TC p & Monad m
 126 (>!@) infixl 6
 127 (>!@) :== mapWrite
 128
 129 //* Translate the parameter space
 130 translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m
 131 //* focus a parameter: @type :: p (sds m p r w) -> (sds m p` r w)
 132 focus p :== translate \_->p
 133
 134 (>*<) infixl 6 :: (sdsl m p1 r1 w1) (sdsr m p2 r2 w2) -> Par sdsl sdsr m (p1, p2) (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2 & Monad m
 135
 136 fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
 137 toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
 138
 139 indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
 140 keyedStore :: (sds m p (Map k v) (Map k v)) -> Lens sds m (p, k) v v | TC v & TC k & < k & TC p & MonadFail m
 141
 142 astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
 143 dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m
 144 store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
 145
 146 file :: Source IO FilePath String String