From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 24 Jul 2020 13:30:16 +0000 (+0200)
Subject: adsusussu
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=95e0da3f9e093783f8aa4b45ace01befee0d4ee4;p=clean-tests.git

adsusussu
---

diff --git a/uds/asds.dcl b/uds/asds.dcl
index afddb15..027d9b8 100644
--- 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
--- 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