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