uds/ASDS/Parallel.icl

   1 implementation module ASDS.Parallel
   2
   3 import StdEnv
   4 import Data.Func
   5 import Data.Functor
   6 import Data.Tuple
   7 import Control.Monad
   8 import Control.Monad.State
   9 import Control.Monad.Trans
  10 import ASDS
  11
  12 par :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 w1) (LensWrite m p w r2 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
  13 par param readl writel writer left right = Par {param=param,readl=readl,writel=writel,writer=writer,left=left,right=right}
  14
  15 instance read (Par sdsl sdsr) | read sdsl & read sdsr
  16 where
  17         read (Par t=:{param,readl,left,right}) p
  18                 = read left p1 >>= \v->case v of
  19                         Reading s = pure $ Reading $ Par {t & left=s}
  20                         Read l = read right p2 >>= \v->case v of
  21                                 Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
  22                                 Read r = pure $ Read $ readl l r
  23         where (p1, p2) = param p
  24
  25 instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr
  26 where
  27         //First read the lhs if necessary
  28         write (Par t=:{param,writel=LensWrite writel,left}) p w
  29                 = read left p1 >>= \v->case v of
  30                         Reading s = pure $ Writing $ Par {t & left=rwpair s left}
  31                         Read r1 = write (Par {t & writel=LensWriteConst \p w->writel p w r1}) p w
  32                 where (p1, p2) = param p
  33         //Then read the rhs if necessary
  34         write (Par t=:{param,writer=LensWrite writer,right}) p w
  35                 = read right p2 >>= \v->case v of
  36                         Reading s = pure $ Writing $ Par {t & right=rwpair s right}
  37                         Read r2 = write (Par {t & writer=LensWriteConst \p w->writer p w r2}) p w
  38                 where (p1, p2) = param p
  39         //Then do the actual writing
  40         write (Par t=:{param,writel=LensWriteConst writel,writer=LensWriteConst writer,left,right}) p w
  41                 = write` left p1 (writel p w) >>= \v->case v of
  42                         Writing s = pure $ Writing $ Par {t & left=rwpair left s}
  43                         Written () = write` right p2 (writer p w) >>= \v->case v of
  44                                 Writing s = pure $ Writing $ Par {t & left=rwpair left nullShare, right=rwpair right s}
  45                                 Written () = pure $ Written ()
  46                 where (p1, p2) = param p
  47
  48 // Write the share but only if the given value is a Just.
  49 // If it is None, pretend that the value was written
  50 write` :: (sds m p r w) p (m (? w)) -> PViewT m (WriteResult m p r w) | TC w & Monad m & write sds & TC p
  51 write` sds p mmv = liftT mmv >>= \mv->case mv of
  52         ?None = liftT $ pure $ Written ()
  53         ?Just v = write sds p v
  54
  55 (>*<) 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
  56 (>*<) l r = par id tuple (LensWriteConst \p (w1, _)->pure $ ?Just w1) (LensWriteConst \p (_, w2)->pure $ ?Just w2) l r
  57
  58 (>+<) infixl 6 :: (sdsl m p r1 w1) (sdsr m p r2 w2) -> Par sdsl sdsr m p (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & TC p & Monad m
  59 (>+<) l r = par (\p->(p, p)) tuple (LensWriteConst \p (w1, _)->pure $ ?Just w1) (LensWriteConst \p (_, w2)->pure $ ?Just w2) l r