uds/ASDS/Select.icl

   1 implementation module ASDS.Select
   2
   3 import StdEnv
   4 import Data.Func
   5 import Data.Functor
   6 import Control.Monad
   7 import ASDS
   8
   9 select` :: (p -> p1) (p r1 -> p2) (sdsl m p1 r1 w1) (sdsr m p2 r w) -> Select sdsl sdsr m p r w | TC p & TC p1 & TC p2 & TC r1 & TC r & TC w & pure m
  10 select` parami params index source = Select {parami=parami,params=params,index=index,source=source,unused=pure ()}
  11
  12 instance read (Select sdsl sdsr) | read sdsl & read sdsr
  13 where
  14         read (Select t=:{parami,params,index,source}) p = read index (parami p) >>= \v->case v of
  15                 Reading s = pure $ Reading $ Select {t & index=s}
  16                 Read r1 = read source (params p r1) >>= \v->case v of
  17                         Reading s = pure $ Reading $ Select {t & index=constShare r1, source=s}
  18                         Read r = pure $ Read r
  19 instance write (Select sdsl sdsr) | read sdsl & write sdsr
  20 where
  21         write (Select t=:{parami,params,index,source}) p w = read index (parami p) >>= \v->case v of
  22                 Reading s = pure $ Writing $ Select {t & index=s}
  23                 Read r1 = write source (params p r1) w >>= \v->case v of
  24                         Writing s = pure $ Writing $ Select {t & index=constShare r1, source=s}
  25                         Written () = pure $ Written ()
  26
  27 selectList :: (sdss m p1 Int w1) (sdsc m p2 [a] [a]) -> Select sdss (Lens sdsc) m (p1, p2) a a | TC p1 & TC p2 & TC a & TC w1 & MonadFail m
  28 selectList sdss sdsc = select` (\(p1, p2)->p1) (\(p1, p2) i->(p2, i)) sdss (indexedStore sdsc)