uds/asds.icl

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