uds/auds.icl

   1 implementation module auds
   2
   3 import StdEnv
   4 import Data.Maybe
   5 import Data.Functor
   6 import Data.Func
   7 import Data.Either
   8 import Data.Tuple
   9 import Data.List
  10 import Control.Applicative
  11 import Control.Monad
  12 import Control.Monad.State
  13 import Control.Monad.Trans
  14 import qualified Data.Map
  15 from Data.Map import :: Map
  16 import System.FilePath
  17
  18 import System.IO
  19 import System.Time
  20
  21 instance MonadFail Maybe where fail _ = Nothing
  22 instance MonadFail [] where fail _ = []
  23 instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
  24 instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
  25
  26 sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
  27 sds s = SDS s (pure ())
  28 instance read SDS where read (SDS s _) = read s
  29 instance write SDS where write (SDS sds _) w = write sds w
  30
  31 source :: (m r) (w -> m ()) -> Source m r w
  32 source read write = RWPair (ReadSource read) (WriteSource write)
  33
  34 constShare :: a -> ReadSource m a b | Monad m
  35 constShare a = ReadSource $ pure a
  36
  37 nullShare :: WriteSource m a b | Monad m
  38 nullShare = WriteSource (\_->pure ())
  39
  40 instance read ReadSource where read (ReadSource read) = Read <$> read
  41 instance write WriteSource where write (WriteSource write) w = Written <$> write w
  42
  43 timeStamp :: ReadSource IO Timestamp ()
  44 timeStamp = ReadSource $ withWorld time
  45
  46 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
  47 par readl writel left right = Par {readl=readl,writel=writel,left=left,right=right}
  48
  49 (>*<) 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
  50 (>*<) l r = par (\x y->pure (x, y)) pure l r
  51
  52 instance read (Par sdsl sdsr) | read sdsl & read sdsr
  53 where
  54         read (Par t=:{readl,left,right}) = read left >>= \v->case v of
  55                 Read l = read right >>= \v->case v of
  56                         Read r = Read <$> readl l r
  57                         Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
  58                 Reading s = pure $ Reading $ Par {t & left=s}
  59 instance write (Par sdsl sdsr) | write sdsl & write sdsr
  60 where
  61         write (Par t=:{writel,left,right}) w
  62                 = writel w >>= \(w1, w2)->write left w1 >>= \v->case v of
  63                         Written _ = write right w2 >>= \v->case v of
  64                                 Written _ = pure $ Written ()
  65                                 Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=nullShare, right=s}
  66                         Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=s}
  67
  68 lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
  69 lens mapr mapw lens = Lens {mapr=mapr,mapw=mapw,lens=lens}
  70
  71 instance read (Lens sds) | read sds
  72 where
  73         read (Lens t=:{mapr,lens}) = read lens >>= \v->case v of
  74                 Read r = Read <$> mapr r
  75                 Reading s = pure $ Reading $ Lens {t & lens=s}
  76
  77 instance read (RWPair sdsr sdsw) | read sdsr
  78 where
  79         read (RWPair s w) = read s >>= \v->case v of
  80                 Read r = pure $ Read r
  81                 Reading s = pure $ Reading (RWPair s w)
  82 instance write (RWPair sdsr sdsw) | write sdsw
  83 where
  84         write (RWPair r s) w = write s w >>= \v->case v of
  85                 Written _ = pure $ Written ()
  86                 Writing s = pure $ Writing $ RWPair r s
  87
  88 instance write (Lens sds) | read sds & write sds
  89 where
  90         write (Lens t=:{mapw,lens}) w = read lens >>= \v->case v of
  91                 Read r = mapw w r >>= \w->case w of
  92                         Nothing = pure $ Written ()
  93                         Just w = write lens w >>= \v->case v of
  94                                 Written _ = pure $ Written ()
  95                                 Writing s = pure $ Writing $ Lens {t & mapw= \_ _->pure $ Just w, lens=RWPair (constShare r) s}
  96                 Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
  97
  98 mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
  99 mapRead f sds = lens f (\_ _->pure Nothing) sds
 100
 101 fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
 102 fromDynStore sds = lens
 103         (\r->case r of
 104                 (r :: r^) = pure r
 105                 _ = fail "type mismatch")
 106         (\w _->pure $ Just (dynamic w))
 107         sds
 108
 109 toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
 110 toDynStore sds = lens
 111         (\r->pure (dynamic r))
 112         (\w _->case w of
 113                 (w :: w^) = pure $ Just w
 114                 _ = fail "type mismatch")
 115         sds
 116
 117 mapWrite :: (w` r -> m (Maybe w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
 118 mapWrite f sds = lens pure f sds
 119
 120 indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
 121 indexedStore idx sds = lens
 122         (\r->maybe (fail "out of range") pure (r !? idx))
 123         (\w->pure o Just o updateAt idx w)
 124         sds
 125
 126 keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
 127 keyedStore key sds = lens
 128         (maybe (fail "key not present") pure o 'Data.Map'.get key)
 129         (\w->pure o Just o 'Data.Map'.put key w)
 130         sds
 131
 132 select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
 133 select select bind = Select {select=select,bind=bind}
 134
 135 instance read (Select sdsl sdsr) | read sdsl & read sdsr
 136 where
 137         read (Select t=:{select,bind}) = read select >>= \v->case v of
 138                 Read r = bind r >>= read
 139                 Reading s = pure $ Reading $ Select {t & select=s}
 140 instance write (Select sdsl sdsr) | read sdsl & write sdsr
 141 where
 142         write (Select t=:{select,bind}) w = read select >>= \v->case v of
 143                 Read r = bind r >>= flip write w
 144                 Reading s = pure $ Writing $ Select {t & select=s}
 145
 146 indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
 147 indexedSelect l r = select l $ pure o flip indexedStore r
 148
 149 keyedSelect :: (sdsl m k z) (sdsr m (Map k v) (Map k v))
 150         -> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
 151 keyedSelect l r = select l $ pure o flip keyedStore r
 152
 153 getShare :: (sds m r w) -> m r | Monad m & read sds & TC r & TC w
 154 getShare s = read s >>= \v->case v of
 155         Read r = pure r
 156         Reading s = getShare s
 157
 158 setShare :: w (sds m r w) -> m () | Monad m & write sds & TC r & TC w
 159 setShare w s = write s w >>= \v->case v of
 160         Written _ = pure ()
 161         Writing s = setShare w s
 162
 163 updShare :: (r -> w) (sds m r w) -> m w | Monad m & read sds & write sds & TC r & TC w
 164 updShare f s = f <$> getShare s >>= \v->setShare v s >>| pure v
 165
 166 //Start :: Either String (Map String Dynamic)
 167 Start :: Either String (Int, Map String Dynamic)
 168 Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
 169 where
 170 //      t = write (42, "blurp") (astore "foo" >*< astore "bar")
 171 //      t = write 42 (astore "blurp")
 172 //              >>| read (astore "blurp")
 173         t = setShare 42 (astore "blurp")
 174                 >>| getShare (astore "blurp")
 175
 176 //Start world = evalIO t world
 177 //where
 178 //      t = read (file "auds.icl")
 179
 180 astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
 181 astore s = fromDynStore $ dstore s
 182
 183 dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
 184 dstore s = keyedStore s store
 185
 186 store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
 187 store = source getState put
 188
 189 file :: FilePath -> Source IO String String
 190 file p = source (readFileM p) (writeFileM p)