asds

[clean-tests.git] / uds / asds.dcl

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