asds

diff --git a/uds/asds.dcl b/uds/asds.dcl
index 816b096..afddb15 100644 (file)
--- 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 (file)
--- 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