From b1f24e950aaad29ca1bdb357de1e10413c80f7ed Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 24 Jul 2020 15:07:30 +0200 Subject: [PATCH] asds --- uds/asds.dcl | 13 ++++++++++--- uds/asds.icl | 40 ++++++++++++++++++++++------------------ 2 files changed, 32 insertions(+), 21 deletions(-) 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 -- 2.20.1