import Data.Functor
import Data.Tuple
import Control.Monad
+import Control.Monad.State
+import Control.Monad.Trans
import ASDS
par :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 w1) (LensWrite m p w r2 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
// Write the share but only if the given value is a Just.
// If it is None, pretend that the value was written
-write` :: (sds m p r w) p (m (? w)) -> m (WriteResult m p r w) | TC w & Monad m & write sds
-write` sds p mmv = mmv >>= \mv->case mv of
- ?None = pure $ Written ()
+write` :: (sds m p r w) p (m (? w)) -> PViewT m (WriteResult m p r w) | TC w & Monad m & write sds
+write` sds p mmv = liftT mmv >>= \mv->case mv of
+ ?None = liftT $ pure $ Written ()
?Just v = write sds p v
(>*<) 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