--- /dev/null
+definition module asds
+
+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 p r w
+ = Read r //* done reading
+ | E.sds: Reading (sds m p r w) & read sds //* not done reading
+ | ReadResultUnused (m ())
+
+//* Result of a single write rewrite
+:: WriteResult m p r w
+ = Written () //* done writing
+ | E.sds: Writing (sds m p r w) & write sds //* not done writing
+ | WriteResultUnused (m ())
+
+//* Read a share with one rewrite step
+class read v :: (v m p r w) p -> m (ReadResult m p r w) | TC r & Monad m
+//* Write a share with one rewrite step
+class write v :: (v m p r w) p w -> m (WriteResult m p r w) | TC w & Monad m
+//* Read a share completely
+getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w
+//* Write a share completely
+setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w
+//* Update a share completely
+updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w
+
+//* Box type, to get rid of a possible complex constructor of combinators
+:: SDS m p r w = E.sds: SDS (sds m p r w) (m ()) /*force kind*/ & read sds & write sds
+sds :: (sds m p r w) -> SDS m p 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) | read sdsl & read 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 p r w = ReadSource (p -> m r)
+//* Just write something
+:: WriteSource m p r w = WriteSource (p w -> m ())
+//* Pair a two shares to form a read/write sds that only touches one share per action
+:: RWPair sdsr sdsw m p r w = RWPair (sdsr m p r w) (sdsw m p r w) | RWPairUnused (m ())
+
+//* Special type of RWPair that contains sds sources
+:: Source m p r w :== RWPair ReadSource WriteSource m p r w
+source :: (p -> m r) (p w -> m ()) -> Source m p r w
+
+//* Combine two shares in parallel
+:: Par sdsl sdsr m p r w = E.p1 p2 r1 r2 w1 w2: Par (ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w) & TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2
+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
+:: ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w =
+ { param :: p -> (p1, p2)
+ , readl :: r1 r2 -> r
+ , writel :: p w r1 -> m (Maybe w1)
+ , writer :: p w r2 -> m (Maybe w2)
+ , left :: sdsl m p1 r1 w1
+ , right :: sdsr m p2 r2 w2
+ }
+
+//* Apply a lens to a share
+:: Lens sds m p r w = E.p1 r1 w1: Lens (LensOpts sds m p1 r1 w1 p r w) & TC r1 & TC w1 & TC p1
+lens :: (p -> p1) (p r1 -> m r) (p w r1 -> m (Maybe w1)) (sds m p1 r1 w1) -> Lens sds m p r w | TC r1 & TC w1 & TC p1
+:: LensOpts sds m p1 r1 w1 p r w =
+ { param :: p -> p1
+ , mapr :: p r1 -> m r
+ , mapw :: p w r1 -> m (Maybe w1)
+ , lens :: sds m p1 r1 w1
+ }
+
+//* Determine a share from the value read from another share
+:: Select sdsl sdsr m p r w = E.p1 r1 w1 p2: Select (SelectOpts sdsl sdsr m p1 r1 w1 p2 p r w) & TC r1 & TC p1 & TC p2
+//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 p1 r1 w1 p2 p r w =
+ { index :: sdsl m p1 r1 w1
+ , source :: sdsr m p2 r w
+ , parami :: p -> p1
+ , params :: p r1 -> p2
+ , unused :: m ()
+ }
+
+//* Immediately returns the given value on a read
+constShare :: a -> ReadSource m p a b | Monad m
+//* Values written are discarded
+nullShare :: WriteSource m p a b | Monad m
+
+//* Current time
+timeStamp :: ReadSource IO () Timestamp ()
+
+////* Map a function to the value read
+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
+(>?@) infixl 6
+(>?@) :== mapRead
+
+//* Map a function to the value written.
+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
+(>!@) infixl 6
+(>!@) :== mapWrite
+
+//* Translate the parameter space
+translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m
+//* focus a parameter: @type :: p (sds m p r w) -> (sds m p` r w)
+focus p :== translate \_->p
+
+(>*<) 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
+
+fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
+toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
+
+indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
+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
+
+astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
+dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m
+store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
+
+file :: Source IO FilePath String String
--- /dev/null
+implementation module asds
+
+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 p r w) -> SDS m p r w | read sds & write sds & Monad m
+sds s = SDS s (pure ())
+instance read SDS where read (SDS s _) p = read s p
+instance write SDS where write (SDS sds _) p w = write sds p w
+
+source :: (p -> m r) (p w -> m ()) -> Source m p r w
+source read write = RWPair (ReadSource read) (WriteSource write)
+
+constShare :: a -> ReadSource m p a b | Monad m
+constShare a = ReadSource \_->pure a
+
+nullShare :: WriteSource m p a b | Monad m
+nullShare = WriteSource \_ _->pure ()
+
+instance read ReadSource where read (ReadSource read) p = Read <$> read p
+instance write WriteSource where write (WriteSource write) p w = Written <$> write p w
+
+timeStamp :: ReadSource IO () Timestamp ()
+timeStamp = ReadSource \_->withWorld time
+
+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
+par param readl writel writer left right = Par {param=param,readl=readl,writel=writel,writer=writer,left=left,right=right}
+
+(>*<) 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
+(>*<) l r = par id tuple (\p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r
+
+(>+<) 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
+(>+<) l r = par (\p->(p, p)) tuple (\p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r
+
+instance read (Par sdsl sdsr) | read sdsl & read sdsr
+where
+ read (Par t=:{param,readl,left,right}) p
+ = read left p1 >>= \v->case v of
+ Reading s = pure $ Reading $ Par {t & left=s}
+ Read l = read right p2 >>= \v->case v of
+ Reading s = pure $ Reading $ Par {t & left=constShare l, right=s}
+ Read r = pure $ Read $ readl l r
+ where (p1, p2) = param p
+instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr
+where
+ write (Par t=:{param,writel,writer,left,right}) p w
+ = read left p1 >>= \v->case v of
+ Reading s = pure $ Writing $ Par {t & left=RWPair s left}
+ Read r1 = write` left p1 (writel p w r1) >>= \v->case v of
+ Writing s = pure $ Writing $ Par {t & left=RWPair (constShare r1) left}
+ Written () = read right p2 >>= \v->case v of
+ Reading s = pure $ Writing $ Par {t & left=RWPair (constShare r1) nullShare, right=RWPair s right}
+ Read r2 = write` right p2 (writer p w r2) >>= \v->case v of
+ Writing s = pure $ Writing $ Par {t & left=RWPair (constShare r1) nullShare, right=RWPair (constShare r2) right}
+ Written () = pure $ Written ()
+ where (p1, p2) = param p
+
+write` :: (sds m p r w) p (m (Maybe w)) -> m (WriteResult m p r w) | TC w & Monad m & write sds
+write` sds p mmv = mmv >>= \mv->case mv of
+ Nothing = pure $ Written ()
+ Just v = write sds p v
+
+lens :: (p -> p1) (p r1 -> m r) (p w r1 -> m (Maybe w1)) (sds m p1 r1 w1) -> Lens sds m p r w | TC r1 & TC w1 & TC p1
+lens param mapr mapw lens = Lens {param=param,mapr=mapr,mapw=mapw,lens=lens}
+
+instance read (Lens sds) | read sds
+where
+ read (Lens t=:{param,mapr,lens}) p = read lens (param p) >>= \v->case v of
+ Reading s = pure $ Reading $ Lens {t & lens=s}
+ Read r = Read <$> mapr p r
+
+instance read (RWPair sdsr sdsw) | read sdsr
+where
+ read (RWPair s w) p = read s p >>= \v->case v of
+ Reading s = pure $ Reading (RWPair s w)
+ Read r = pure $ Read r
+instance write (RWPair sdsr sdsw) | write sdsw
+where
+ write (RWPair r s) p w = write s p w >>= \v->case v of
+ Writing s = pure $ Writing $ RWPair r s
+ Written _ = pure $ Written ()
+
+instance write (Lens sds) | read sds & write sds
+where
+ write (Lens t=:{param,mapw,lens}) p w = read lens (param p) >>= \v->case v of
+ Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
+ Read r = mapw p w r >>= \v->case v of
+ Nothing = pure $ Written ()
+ Just w = write lens (param p) w >>= \v->case v of
+ Writing s = pure $ Writing $ Lens {t & mapw= \_ _ _->pure $ Just w, lens=RWPair (constShare r) s}
+ Written _ = pure $ Written ()
+
+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
+mapRead f sds = lens id (\p r->f r) (\p w r->pure Nothing) sds
+
+fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
+fromDynStore sds = lens
+ id
+ (\_ r->case r of
+ (r :: r^) = pure r
+ _ = fail "type mismatch")
+ (\_ w _->pure $ Just (dynamic w))
+ sds
+
+toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
+toDynStore sds = lens
+ id
+ (\_ 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 p r w) -> Lens sds m p r w` | TC r & TC w & TC w` & TC p & Monad m
+mapWrite f sds = lens id (\_->pure) (\_->f) sds
+
+translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m
+translate param sds = lens param (\_ r->pure r) (\_ w _->pure $ Just w) sds
+
+indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
+indexedStore sds = lens param read write sds
+where
+ param (p, _) = p
+ read (_, idx) r = maybe (fail "out of range") pure (r !? idx)
+ write (_, idx) w r = pure $ Just $ updateAt idx w r
+
+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
+keyedStore sds = lens param read write sds
+where
+ param (p, _) = p
+ read (_, k) r = maybe (fail "key not present") pure $ 'Data.Map'.get k r
+ write (_, k) w r = pure $ Just $ 'Data.Map'.put k w r
+
+//select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
+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
+select parami params index source = Select {parami=parami,params=params,index=index,source=source,unused=undef}
+
+instance read (Select sdsl sdsr) | read sdsl & read sdsr
+where
+ read (Select t=:{parami,params,index,source}) p = read index (parami p) >>= \v->case v of
+ Reading s = pure $ Reading $ Select {t & index=s}
+ Read r1 = read source (params p r1) >>= \v->case v of
+ Reading s = pure $ Reading $ Select {t & index=constShare r1, source=s}
+ Read r = pure $ Read r
+instance write (Select sdsl sdsr) | read sdsl & write sdsr
+where
+ write (Select t=:{parami,params,index,source}) p w = read index (parami p) >>= \v->case v of
+ Reading s = pure $ Writing $ Select {t & index=s}
+ Read r1 = write source (params p r1) w >>= \v->case v of
+ Writing s = pure $ Writing $ Select {t & index=constShare r1, source=s}
+ Written () = pure $ Written ()
+
+getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w
+getShare s = read s () >>= \v->case v of
+ Reading s = getShare s
+ Read r = pure r
+
+setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w
+setShare w s = write s () w >>= \v->case v of
+ Writing s = setShare w s
+ Written _ = pure ()
+
+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 ((), Map String Dynamic)
+Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
+where
+ t = setShare (42, "blurp") (focus "foo" astore >+< focus "bar" astore)
+// t = write 42 (astore "blurp")
+// >>| read (astore "blurp")
+// t = setShare 42 (focus "blurp" astore)
+// >>| getShare (focus "blurp" astore)
+
+//Start world = evalIO t world
+//where
+// t = getShare (focus "auds.icl" file)
+
+astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
+astore = fromDynStore dstore
+
+dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m
+dstore = translate (\i->((), i)) $ keyedStore store
+
+store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
+store = source (\_->getState) \_->put
+
+file :: Source IO FilePath String String
+file = source readFileM writeFileM
| 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
+class read v :: (v m r w) -> m (ReadResult m r w) | TC r & Monad m
+class write v :: (v m r w) 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
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
+instance write SDS where write (SDS sds _) w = write sds w
source :: (m r) (w -> m ()) -> Source m r w
source read write = RWPair (ReadSource read) (WriteSource write)
nullShare = WriteSource (\_->pure ())
instance read ReadSource where read (ReadSource read) = Read <$> read
-instance write WriteSource where write w (WriteSource write) = Written <$> write w
+instance write WriteSource where write (WriteSource write) w = 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
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
+ write (Par t=:{writel,left,right}) w
+ = writel w >>= \(w1, w2)->write left w1 >>= \v->case v of
+ Written _ = write right w2 >>= \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}
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
+ write (RWPair r s) w = write s w >>= \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
+ write (Lens t=:{mapw,lens}) w = 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
+ Just w = write lens w >>= \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}
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
+ write (Select t=:{select,bind}) w = read select >>= \v->case v of
+ Read r = bind r >>= flip 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
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
+setShare w s = write s w >>= \v->case v of
Written _ = pure ()
Writing s = setShare w s
repositories / clean-tests.git / commitdiff