+implementation module auds
+
+import StdEnv
+import Data.Maybe
+import Data.Functor
+import Data.Func
+import Data.Either
+import Data.Tuple
+import Data.List
+import Control.Applicative
+import Control.Monad
+import Control.Monad.State
+import Control.Monad.Trans
+import qualified Data.Map
+from Data.Map import :: Map
+import System.FilePath
+
+import System.IO
+import System.Time
+
+instance MonadFail Maybe where fail _ = Nothing
+instance MonadFail [] where fail _ = []
+instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
+instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
+
+sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
+sds s = SDS s (pure ())
+instance read SDS where read (SDS s _) = read s
+instance write SDS where write w (SDS sds _) = write w sds
+
+source :: (m r) (w -> m ()) -> Source m r w
+source read write = RWPair (ReadSource read) (WriteSource write)
+
+constShare :: a -> ReadSource m a b | Monad m
+constShare a = ReadSource $ pure a
+
+nullShare :: WriteSource m a b | Monad m
+nullShare = WriteSource (\_->pure ())
+
+instance read ReadSource where read (ReadSource read) = Read <$> read
+instance write WriteSource where write w (WriteSource write) = Written <$> write w
+
+//upd :: (r -> w) (v m r w) -> m w | TC r & TC w & read, write v & Monad m
+//upd fun sds = read sds >>= \r
+// # w = fun r
+// = write w sds >>| pure w
+//
+timeStamp :: ReadSource IO Timestamp ()
+timeStamp = ReadSource $ withWorld time
+
+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
+par readl writel left right = Par {readl=readl,writel=writel,left=left,right=right}
+
+(>*<) 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
+(>*<) l r = par (\x y->pure (x, y)) pure l r
+
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+where
+ read (Par t=:{readl,left,right}) = read left >>= \v->case v of
+ Read l = read right >>= \v->case v of
+ Read r = Read <$> readl l r
+ Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
+ Reading s = pure $ Reading $ Par {t & left=s}
+instance write (Par sdsl sdsr) | write sdsl & write sdsr
+where
+ write w (Par t=:{writel,left,right})
+ = writel w >>= \(w1, w2)->write w1 left >>= \v->case v of
+ Written _ = write w2 right >>= \v->case v of
+ Written _ = pure $ Written ()
+ Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=nullShare, right=s}
+ Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=s}
+
+lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+lens mapr mapw lens = Lens {mapr=mapr,mapw=mapw,lens=lens}
+
+instance read (Lens sds) | read sds
+where
+ read (Lens t=:{mapr,lens}) = read lens >>= \v->case v of
+ Read r = Read <$> mapr r
+ Reading s = pure $ Reading $ Lens {t & lens=s}
+
+instance read (RWPair sdsr sdsw) | read sdsr
+where
+ read (RWPair s w) = read s >>= \v->case v of
+ Read r = pure $ Read r
+ Reading s = pure $ Reading (RWPair s w)
+instance write (RWPair sdsr sdsw) | write sdsw
+where
+ write w (RWPair r s) = write w s >>= \v->case v of
+ Written _ = pure $ Written ()
+ Writing s = pure $ Writing $ RWPair r s
+
+instance write (Lens sds) | read sds & write sds
+where
+ write w (Lens t=:{mapw,lens}) = read lens >>= \v->case v of
+ Read r = mapw w r >>= \w->case w of
+ Nothing = pure $ Written ()
+ Just w = write w lens >>= \v->case v of
+ Written _ = pure $ Written ()
+ Writing s = pure $ Writing $ Lens {t & mapw= \_ _->pure $ Just w, lens=RWPair (constShare r) s}
+ Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
+
+mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+mapRead f sds = lens f (\_ _->pure Nothing) sds
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+fromDynStore sds = lens
+ (\r->case r of
+ (r :: r^) = pure r
+ _ = fail "type mismatch")
+ (\w _->pure $ Just (dynamic w))
+ sds
+
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+toDynStore sds = lens
+ (\r->pure (dynamic r))
+ (\w _->case w of
+ (w :: w^) = pure $ Just w
+ _ = fail "type mismatch")
+ sds
+
+mapWrite :: (w` r -> m (Maybe w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+mapWrite f sds = lens pure f sds
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+indexedStore idx sds = lens
+ (\r->maybe (fail "out of range") pure (r !? idx))
+ (\w->pure o Just o updateAt idx w)
+ sds
+
+keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+keyedStore key sds = lens
+ (maybe (fail "key not present") pure o 'Data.Map'.get key)
+ (\w->pure o Just o 'Data.Map'.put key w)
+ sds
+
+select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+select select bind = Select {select=select,bind=bind}
+
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+where
+ read (Select t=:{select,bind}) = read select >>= \v->case v of
+ Read r = bind r >>= read
+ Reading s = pure $ Reading $ Select {t & select=s}
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+where
+ write w (Select t=:{select,bind}) = read select >>= \v->case v of
+ Read r = bind r >>= write w
+ Reading s = pure $ Writing $ Select {t & select=s}
+
+indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
+indexedSelect l r = select l $ pure o flip indexedStore r
+
+keyedSelect :: (sdsl m k z) (sdsr m (Map k v) (Map k v))
+ -> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
+keyedSelect l r = select l $ pure o flip keyedStore r
+
+getShare :: (sds m r w) -> m r | Monad m & read sds & TC r & TC w
+getShare s = read s >>= \v->case v of
+ Read r = pure r
+ Reading s = getShare s
+
+setShare :: w (sds m r w) -> m () | Monad m & write sds & TC r & TC w
+setShare w s = write w s >>= \v->case v of
+ Written _ = pure ()
+ Writing s = setShare w s
+
+updShare :: (r -> w) (sds m r w) -> m w | Monad m & read sds & write sds & TC r & TC w
+updShare f s = f <$> getShare s >>= \v->setShare v s >>| pure v
+
+//Start :: Either String (Map String Dynamic)
+Start :: Either String (Int, Map String Dynamic)
+Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
+where
+// t = write (42, "blurp") (astore "foo" >*< astore "bar")
+// t = write 42 (astore "blurp")
+// >>| read (astore "blurp")
+ t = setShare 42 (astore "blurp")
+ >>| getShare (astore "blurp")
+
+//Start world = evalIO t world
+//where
+// t = read (file "auds.icl")
+
+astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
+astore s = fromDynStore $ dstore s
+
+dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+dstore s = keyedStore s store
+
+store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
+store = source getState put
+
+file :: FilePath -> Source IO String String
+file p = source (readFileM p) (writeFileM p)