--- /dev/null
+definition module auds
+
+from Control.Applicative import class Applicative, class pure, class <*>
+from Control.Monad import class Monad
+from Control.Monad.State import :: StateT
+from Data.Either import :: Either
+from Data.Functor import class Functor
+from Data.Map import :: Map
+from StdMaybe import :: Maybe
+from StdOverloaded import class <, class fromString
+from System.FilePath import :: FilePath
+from System.IO import :: IO
+from System.Time import :: Timestamp
+
+class MonadFail m | Monad m where fail :: String -> m a
+instance MonadFail Maybe, []
+instance MonadFail (Either a) | fromString a
+instance MonadFail (StateT s m) | MonadFail m
+
+//* Result of a single read rewrite
+:: ReadResult m r w
+ = Read r //* done reading
+ | E.sds: Reading (sds m r w) & read sds //* not done reading
+ | ReadResultUnused (m ())
+
+//* Result of a single write rewrite
+:: WriteResult m r w
+ = Written () //* done writing
+ | E.sds: Writing (sds m r w) & write sds //* not done writing
+ | WriteResultUnused (m ())
+
+
+class read v :: (v m r w) -> m (ReadResult m r w) | TC r & Monad m
+class write v :: w (v m r w) -> m (WriteResult m r w) | TC w & Monad m
+
+//* Box type, to get rid of a possible complex constructor of combinators
+:: SDS m r w = E.sds: SDS (sds m r w) (m ()) /*force kind*/ & read sds & write sds
+sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
+
+instance read SDS, ReadSource
+instance read (RWPair sdsr sdsw) | read sdsr
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+instance read (Lens sds) | read sds
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+
+instance write SDS, WriteSource
+instance write (RWPair sdsr sdsw) | write sdsw
+instance write (Par sdsl sdsr) | write sdsl & write sdsr
+instance write (Lens sds) | read sds & write sds
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+
+//* Just read something
+:: ReadSource m r w = ReadSource (m r)
+//* Just write something
+:: WriteSource m r w = WriteSource (w -> m ())
+//* Pair a two shares to form a read/write sds that only touches one share per action
+:: RWPair sdsr sdsw m r w = RWPair (sdsr m r w) (sdsw m r w) | RWPairUnused (m ())
+
+//* Special type of RWPair that contains sds sources
+:: Source m r w :== RWPair ReadSource WriteSource m r w
+source :: (m r) (w -> m ()) -> Source m r w
+
+//* Combine two shares in parallel
+:: Par sdsl sdsr m r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr m r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
+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
+:: ParOpts sdsl sdsr m r1 r2 w1 w2 r w =
+ { readl :: r1 r2 -> m r
+ , writel :: w -> m (w1, w2)
+ , left :: sdsl m r1 w1
+ , right :: sdsr m r2 w2
+ }
+
+//* Apply a lens to a share
+:: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
+lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+:: LensOpts sds m r1 w1 r w =
+ { mapr :: r1 -> m r
+ , mapw :: w r1 -> m (Maybe w1)
+ , lens :: sds m r1 w1
+ }
+
+//* Determine a share from the value read from another share
+:: Select sdsl sdsr m r w = E.r1 w1: Select (SelectOpts sdsl sdsr m r1 w1 r w) & TC r1 & TC w1
+select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+:: SelectOpts sdsl sdsr m r1 w1 r w =
+ { select :: sdsl m r1 w1
+ , bind :: r1 -> m (sdsr m r w)
+ }
+
+//* Immediately returns the given value on a read
+constShare :: a -> ReadSource m a b | Monad m
+//* Values written are discarded
+nullShare :: WriteSource m a b | Monad m
+
+//* Current time
+timeStamp :: ReadSource IO Timestamp ()
+
+//* Map a function to the value read
+mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+(>?@) infixl 6
+(>?@) :== mapRead
+
+//* Map a function to the value written.
+mapWrite :: (w` r -> m (Maybe w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+(>!@) infixl 6
+(>!@) :== mapWrite
+
+(>*<) 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
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+
+indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
+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
+
+astore :: String -> Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
+dstore :: String -> Lens (RWPair ReadSource WriteSource) (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+store :: Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic) | Monad m
+
+file :: FilePath -> Source IO String String
--- /dev/null
+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)
+++ /dev/null
-module test
-
-import StdEnv
-import Data.Maybe
-import Data.Functor
-import Data.Func
-import Data.Tuple
-import Data.List
-import Control.Applicative
-import Control.Monad
-import qualified Data.Map
-
-class get v ~st :: (v r w) .st -> .(Maybe r, .st) | TC r
-class put v ~st :: w (v r w) .st -> .(Maybe (), .st) | TC w
-
-:: SDS sds a :== sds a a
-
-:: Source r w = Source String
-:: St :== 'Data.Map'.Map String Dynamic
-
-instance get Source St
-where
- get (Source n) st = case 'Data.Map'.get n st of
- Just (a :: a^) = (Just a, st)
- _ = (Nothing, st)
-
-instance put Source St
-where
- put w (Source n) st = (Just (), 'Data.Map'.put n (dynamic w) st)
-
-:: Par sdsl sdsr r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
-:: ParOpts sdsl sdsr r1 r2 w1 w2 r w =
- { read :: r1 r2 -> Maybe r
- , write :: w -> Maybe (w1, w2)
- , left :: sdsl r1 w1
- , right :: sdsr r2 w2
- }
-(>*<) infixl 6 :: (sdsl r1 w1) (sdsr r2 w2) -> Par sdsl sdsr (r1, r2) (w1, w2) | get sdsl St & put sdsr St & TC r1 & TC r2 & TC w1 & TC w2
-(>*<) l r = Par {read= \x y->Just (x, y), write=Just, left=l, right=r}
-
-instance get (Par sdsl sdsr) St | get sdsl St & get sdsr St
-where
- get (Par {read,left,right}) st
- # (ml, st) = get left st
- # (mr, st) = get right st
- = (join $ read <$> ml <*> mr, st)
-instance put (Par sdsl sdsr) St | put sdsl St & put sdsr St
-where
- put w (Par {write,left,right}) st
- = case write w of
- Just (w1, w2)
- # (ml, st) = put w1 left st
- # (mr, st) = put w2 right st
- = (ml *> mr, st)
- Nothing = (Nothing, st)
-
-:: Lens sds r w = E.r1 w1: Lens (LensOpts sds r1 w1 r w) & TC r1 & TC w1
-:: LensOpts sds r1 w1 r w =
- { mapr :: r1 -> Maybe r
- , mapw :: w r1 -> Maybe w1
- , lens :: sds r1 w1
- }
-
-instance get (Lens sds) St | get sds St
-where
- get (Lens {mapr,lens}) st = appFst ((=<<) mapr) $ get lens st
-instance put (Lens sds) St | get sds St & put sds St
-where
- put w (Lens {mapw,lens}) st
- # (mv, st) = get lens st
- = case mv of
- Just r = case mapw w r of
- Just w = put w lens st
- Nothing = (Nothing, st)
- Nothing = (Nothing, st)
-
-:: Select sdsl sdsr r w = E.r1 w1: Select (SelectOpts sdsl sdsr r1 w1 r w) & TC r1 & TC w1
-:: SelectOpts sdsl sdsr r1 w1 r w =
- { select :: sdsl r1 w1
- , bind :: r1 -> (sdsr r w)
- }
-
-instance get (Select sdsl sdsr) St | get sdsl St & get sdsr St
-where
- get (Select {select,bind}) st
- = case get select st of
- (Just r, st) = get (bind r) st
- (Nothing, st) = (Nothing, st)
-instance put (Select sdsl sdsr) St | get sdsl St & put sdsr St
-where
- put w (Select {select,bind}) st
- = case get select st of
- (Just r, st) = put w (bind r) st
- (Nothing, st) = (Nothing, st)
-
-mapRead :: (r -> r`) (sds r w) -> Lens sds r` w | TC r` & TC r & TC w
-mapRead f sds = Lens {mapr=Just o f, mapw=const o Just, lens=sds}
-(>?@) infixl 6
-(>?@) :== mapRead
-
-mapWrite :: (w` r -> Maybe w) (sds r w) -> Lens sds r w` | TC r & TC w & TC w`
-mapWrite f sds = Lens {mapr=Just, mapw=f, lens=sds}
-(>!@) infixl 6
-(>!@) :== mapWrite
-
-indexedStore :: Int (SDS sds [a]) -> SDS (Lens sds) a | TC a
-indexedStore idx sds
- = Lens
- { mapr = \r->r !? idx
- , mapw = \w->Just o updateAt idx w
- , lens = sds
- }
-
-indexedSelect :: (sdsl Int z) (SDS sdsr [a]) -> SDS (Select sdsl (Lens sdsr)) a | TC a & TC z
-indexedSelect l r = Select {select=l, bind=flip indexedStore r}
-
-keyedSelect :: (sdsl k z) (SDS sdsr ('Data.Map'.Map k v)) -> SDS (Select sdsl (Lens sdsr)) v | TC z & TC v & TC k & < k
-keyedSelect l r = Select {select=l, bind=flip keyedStore r}
-
-keyedStore :: k (SDS sds ('Data.Map'.Map k v)) -> SDS (Lens sds) v | TC v & TC k & < k
-keyedStore key sds
- = Lens
- { mapr = 'Data.Map'.get key
- , mapw = \r->Just o 'Data.Map'.put key r
- , lens = sds
- }
-
-Start = appSnd 'Data.Map'.toList
- $ put (42, "blurp") (store "foo" >*< store "bar") 'Data.Map'.newMap
-
-store :: (String -> Source a a) | TC a
-store = Source
--- /dev/null
+definition module uds
+
+from Control.Applicative import class Applicative, class pure, class <*>
+from Control.Monad import class Monad
+from Control.Monad.State import :: StateT
+from Data.Either import :: Either
+from Data.Functor import class Functor
+from Data.Map import :: Map
+from StdMaybe import :: Maybe
+from StdOverloaded import class <, class fromString
+from System.FilePath import :: FilePath
+from System.IO import :: IO
+from System.Time import :: Timestamp
+
+class MonadFail m | Monad m where fail :: String -> m a
+instance MonadFail Maybe, []
+instance MonadFail (Either a) | fromString a
+instance MonadFail (StateT s m) | MonadFail m
+
+class read v :: (v m r w) -> m r | TC r & Monad m
+class write v :: w (v m r w) -> m () | TC w & Monad m
+upd :: (r -> w) (v m r w) -> m w | TC r & TC w & read, write v & Monad m
+
+sds :: (sds m r w) -> SDS m r w | read sds & write sds & Monad m
+:: SDS m r w = E.sds: SDS (sds m r w) (m ()) /*force kind*/ & read sds & write sds
+
+instance read SDS, ReadSource, Source
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+instance read (Lens sds) | read sds
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+
+instance write SDS, WriteSource, Source
+instance write (Par sdsl sdsr) | write sdsl & write sdsr
+instance write (Lens sds) | read sds & write sds
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+
+:: ReadSource m r w = ReadSource (m r)
+:: WriteSource m r w = WriteSource (w -> m ())
+
+source :: (m r) (w -> m ()) -> Source m r w
+:: Source m r w = Source (ReadSource m r w) (WriteSource m r w)
+
+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 sdsl sdsr m r w = E.r1 r2 w1 w2: Par (ParOpts sdsl sdsr m r1 r2 w1 w2 r w) & TC r1 & TC r2 & TC w1 & TC w2
+:: ParOpts sdsl sdsr m r1 r2 w1 w2 r w =
+ { readl :: r1 r2 -> m r
+ , writel :: w -> m (w1, w2)
+ , left :: sdsl m r1 w1
+ , right :: sdsr m r2 w2
+ }
+
+lens :: (r1 -> m r) (w r1 -> m w1) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+:: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
+:: LensOpts sds m r1 w1 r w =
+ { mapr :: r1 -> m r
+ , mapw :: w r1 -> m w1
+ , lens :: sds m r1 w1
+ }
+
+select :: (sdsl m r1 w1) (r1 -> sdsr m r w) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+:: Select sdsl sdsr m r w = E.r1 w1: Select (SelectOpts sdsl sdsr m r1 w1 r w) & TC r1 & TC w1
+:: SelectOpts sdsl sdsr m r1 w1 r w =
+ { select :: sdsl m r1 w1
+ , bind :: r1 -> sdsr m r w
+ , unused :: m () //* to force correct kinds
+ }
+
+constShare :: a -> ReadSource m a () | Monad m
+nullShare :: WriteSource m () a | Monad m
+
+timeStamp :: ReadSource IO Timestamp ()
+
+mapRead :: (r -> r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+(>?@) infixl 6
+(>?@) :== mapRead
+mapWrite :: (w` r -> m w) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+(>!@) infixl 6
+(>!@) :== mapWrite
+
+(>*<) 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
+
+fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
+toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
+
+indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
+keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
+
+indexedSelect :: (sdsl m Int z) (sdsr m [a] [a]) -> Select sdsl (Lens sdsr) m a a | TC a & TC z & MonadFail m
+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
+
+astore :: String -> Lens (Lens Source) (StateT (Map String Dynamic) m) a a | MonadFail m & TC a
+dstore :: String -> Lens Source (StateT (Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+store :: (Source (StateT (Map String Dynamic) m) (Map String Dynamic) (Map String Dynamic)) | Monad m
+
+file :: FilePath -> Source IO String String
--- /dev/null
+implementation module uds
+
+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
+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 sds _) = read sds
+instance write SDS where write w (SDS sds _) = write w sds
+
+source :: (m r) (w -> m ()) -> Source m r w
+source read write = Source (ReadSource read) (WriteSource write)
+
+constShare :: a -> ReadSource m a () | Monad m
+constShare a = ReadSource (pure a)
+
+nullShare :: WriteSource m () a | Monad m
+nullShare = WriteSource (\_->pure ())
+
+instance read ReadSource where read (ReadSource read) = read
+instance write WriteSource where write w (WriteSource write) = write w
+instance read Source where read (Source s _) = read s
+instance write Source where write w (Source _ s) = write w s
+
+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 {readl,left,right}) = join $ readl <$> read left <*> read right
+instance write (Par sdsl sdsr) | write sdsl & write sdsr
+where
+ write w (Par {writel,left,right})
+ = writel w >>= \(w1, w2)->write w1 left >>| write w2 right
+
+lens :: (r1 -> m r) (w r1 -> m 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 {mapr,lens}) = read lens >>= mapr
+instance write (Lens sds) | read sds & write sds
+where
+ write w (Lens {mapw,lens}) = read lens >>= mapw w >>= flip write lens
+
+mapRead :: (r -> r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
+mapRead f sds = lens (pure o f) (const o pure) 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 (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 w
+ _ = fail "type mismatch")
+ sds
+
+mapWrite :: (w` r -> m 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))
+ ((o) pure o updateAt idx)
+// (\w->pure o updateAt idx w)
+ sds
+
+keyedStore :: k (sds m ('Data.Map'.Map k v) ('Data.Map'.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)
+ ((o) pure o 'Data.Map'.put key)
+// (\w->pure o 'Data.Map'.put key w)
+ sds
+
+select :: (sdsl m r1 w1) (r1 -> sdsr m r w) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+select select bind = Select {select=select,bind=bind,unused=pure ()}
+
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+where
+ read (Select {select,bind}) = read select >>= read o bind
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+where
+ write w (Select {select,bind}) = read select >>= write w o bind
+
+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 $ flip indexedStore r
+
+keyedSelect :: (sdsl m k z) (sdsr m ('Data.Map'.Map k v) ('Data.Map'.Map k v))
+ -> Select sdsl (Lens sdsr) m v v | TC z & TC v & TC k & < k & MonadFail m
+keyedSelect l r = select l $ flip keyedStore r
+
+//Start :: Either String ('Data.Map'.Map String Dynamic)
+//Start :: Either String (Int, 'Data.Map'.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")
+
+//Start world = evalIO t world
+//where
+// t = read (file "test.icl")
+
+astore :: String -> Lens (Lens Source) (StateT ('Data.Map'.Map String Dynamic) m) a a | MonadFail m & TC a
+astore s = fromDynStore $ dstore s
+
+dstore :: String -> Lens Source (StateT ('Data.Map'.Map String Dynamic) m) Dynamic Dynamic | MonadFail m
+dstore s = keyedStore s store
+
+store :: (Source (StateT ('Data.Map'.Map String Dynamic) m) ('Data.Map'.Map String Dynamic) ('Data.Map'.Map String Dynamic)) | Monad m
+store = Source (ReadSource getState) (WriteSource put)
+
+file :: FilePath -> Source IO String String
+file p = source (readFileM p) (writeFileM p)
+
+Start = 42
repositories / clean-tests.git / commitdiff