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

asds
---

diff --git a/uds/asds.dcl b/uds/asds.dcl
index 816b096..afddb15 100644
--- a/uds/asds.dcl
+++ b/uds/asds.dcl
@@ -81,14 +81,21 @@ par :: (p -> (p1, p2)) (r1 r2 -> r) (p w r1 -> m (Maybe w1)) (p w r2 -> m (Maybe
 
 //* 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
+lens :: (p -> p1) (LensRead m p r r1) (LensWrite m p w r1 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)
+	, mapr   :: LensRead m p r r1
+	, mapw   :: LensWrite m p w r1 w1
 	, lens   :: sds m p1 r1 w1
 	}
 
+:: LensRead m p r rs
+	= LensRead (p rs -> m r)
+	| LensReadConst (p -> m r)
+:: LensWrite m p w rs ws
+	= LensWrite (p w rs -> m (Maybe ws))
+	| LensWriteConst (p w -> m (Maybe ws))
+
 //* 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
diff --git a/uds/asds.icl b/uds/asds.icl
index e4351d4..727413a 100644
--- a/uds/asds.icl
+++ b/uds/asds.icl
@@ -80,12 +80,13 @@ 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 :: (p -> p1) (LensRead m p r r1) (LensWrite m p w r1 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
+	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
 		Reading s = pure $ Reading $ Lens {t & lens=s}
 		Read r = Read <$> mapr p r
 
@@ -102,50 +103,53 @@ where
 
 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 ()
+	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 ()*/
 
 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
+mapRead f sds = lens id (LensRead \p->f) (LensWrite \p w r->pure $ Just w) 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
+	(LensRead \_ r->case r of
 		(r :: r^) = pure r
 		_ = fail "type mismatch")
-	(\_ w _->pure $ Just (dynamic w))
+	(LensWrite \_ 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
+	(LensRead \_ r->pure (dynamic r))
+	(LensWrite \_ 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
+mapWrite f sds = lens id (LensRead \_->pure) (LensWrite \_ w r->f w r) 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
+translate param sds = lens param (LensRead \_->pure) (LensWrite \_ 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
+indexedStore sds = lens param (LensRead read) (LensWrite 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
+keyedStore sds = lens param (LensRead read) (LensWrite write) sds
 where
 	param (p, _) = p
 	read (_, k) r = maybe (fail "key not present") pure $ 'Data.Map'.get k r