adsusussu

diff --git a/uds/asds.dcl b/uds/asds.dcl
index afddb15..027d9b8 100644 (file)
--- a/uds/asds.dcl
+++ b/uds/asds.dcl
@@ -69,11 +69,12 @@ 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
+par :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 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)
+       , writel :: LensWrite m p w r1 w1
+//     , 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

diff --git a/uds/asds.icl b/uds/asds.icl
index 727413a..eefe267 100644 (file)
--- a/uds/asds.icl
+++ b/uds/asds.icl
@@ -43,14 +43,14 @@ instance write WriteSource where write (WriteSource write) p w = Written <$> wri
 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 :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 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
+(>*<) l r = par id tuple (LensWrite \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
+(>+<) l r = par (\p->(p, p)) tuple (LensWrite \p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r
 
 instance read (Par sdsl sdsr) | read sdsl & read sdsr
 where
@@ -85,8 +85,8 @@ 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=(LensReadConst f),lens}) p = Read <$> f p
-       read (Lens t=:{param,mapr=(LensRead mapr),lens}) p = read lens (param p) >>= \v->case v of
+       read (Lens t=:{mapr=LensReadConst f}) p = Read <$> f p
+       read (Lens t=:{param,mapr=LensRead 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
 
@@ -103,16 +103,18 @@ where
 
 instance write (Lens sds) | read sds & write sds
 where
-       write (Lens t=:{param,mapw=(LensWriteConst f),lens}) p w = write` lens (param p) (f p w) >>= \v->case v of
-               Writing s = pure $ Writing $ Lens {t & lens=s}
-               Written () = pure $ Written ()
-//     write (Lens t=:{param,mapw,lens}) p w = undef/*read lens (param p) >>= \v->case v of
-//             Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
-//             Read r = mapw p w (pure 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 ()*/
+       write (Lens t=:{param,mapw=(LensWriteConst mapw),lens}) p w = mapw p w >>= \v->case v of
+               Nothing = pure $ Written ()
+               Just w = write lens (param p) w >>= \v->case v of
+                       Writing s = pure $ Writing $ Lens {t & lens=RWPair lens s}
+                       Written () = pure $ Written ()
+       write (Lens t=:{param,mapw=LensWrite 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=LensWriteConst \_ _->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 (LensRead \p->f) (LensWrite \p w r->pure $ Just w) sds