From 95e0da3f9e093783f8aa4b45ace01befee0d4ee4 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 24 Jul 2020 15:30:16 +0200 Subject: [PATCH] adsusussu --- uds/asds.dcl | 5 +++-- uds/asds.icl | 32 +++++++++++++++++--------------- 2 files changed, 20 insertions(+), 17 deletions(-) diff --git a/uds/asds.dcl b/uds/asds.dcl index afddb15..027d9b8 100644 --- a/uds/asds.dcl +++ b/uds/asds.dcl @@ -69,11 +69,12 @@ source :: (p -> m r) (p w -> m ()) -> Source m p r w //* Combine two shares in parallel :: Par sdsl sdsr m p r w = E.p1 p2 r1 r2 w1 w2: Par (ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w) & TC r1 & TC r2 & TC w1 & TC w2 & TC p1 & TC p2 -par :: (p -> (p1, p2)) (r1 r2 -> r) (p w r1 -> m (Maybe w1)) (p w r2 -> m (Maybe 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 +par :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 w1) (p w r2 -> m (Maybe 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 :: ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w = { param :: p -> (p1, p2) , readl :: r1 r2 -> r - , writel :: p w r1 -> m (Maybe w1) + , writel :: LensWrite m p w r1 w1 +// , writel :: p w r1 -> m (Maybe w1) , writer :: p w r2 -> m (Maybe w2) , left :: sdsl m p1 r1 w1 , right :: sdsr m p2 r2 w2 diff --git a/uds/asds.icl b/uds/asds.icl index 727413a..eefe267 100644 --- a/uds/asds.icl +++ b/uds/asds.icl @@ -43,14 +43,14 @@ instance write WriteSource where write (WriteSource write) p w = Written <$> wri timeStamp :: ReadSource IO () Timestamp () timeStamp = ReadSource \_->withWorld time -par :: (p -> (p1, p2)) (r1 r2 -> r) (p w r1 -> m (Maybe w1)) (p w r2 -> m (Maybe 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 +par :: (p -> (p1, p2)) (r1 r2 -> r) (LensWrite m p w r1 w1) (p w r2 -> m (Maybe 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 par param readl writel writer left right = Par {param=param,readl=readl,writel=writel,writer=writer,left=left,right=right} (>*<) 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 -(>*<) l r = par id tuple (\p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r +(>*<) l r = par id tuple (LensWrite \p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r (>+<) infixl 6 :: (sdsl m p r1 w1) (sdsr m p r2 w2) -> Par sdsl sdsr m p (r1, r2) (w1, w2) | TC r1 & TC r2 & TC w1 & TC w2 & TC p & Monad m -(>+<) l r = par (\p->(p, p)) tuple (\p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r +(>+<) l r = par (\p->(p, p)) tuple (LensWrite \p (w1, _) r1->pure $ Just w1) (\p (_, w2) r2->pure $ Just w2) l r instance read (Par sdsl sdsr) | read sdsl & read sdsr where @@ -85,8 +85,8 @@ 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=(LensReadConst f),lens}) p = Read <$> f p - read (Lens t=:{param,mapr=(LensRead mapr),lens}) p = read lens (param p) >>= \v->case v of + read (Lens t=:{mapr=LensReadConst f}) 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 @@ -103,16 +103,18 @@ where instance write (Lens sds) | read sds & write sds where - 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 ()*/ + write (Lens t=:{param,mapw=(LensWriteConst mapw),lens}) p w = mapw p w >>= \v->case v of + Nothing = pure $ Written () + Just w = write lens (param p) w >>= \v->case v of + Writing s = pure $ Writing $ Lens {t & lens=RWPair lens s} + Written () = pure $ Written () + write (Lens t=:{param,mapw=LensWrite 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=LensWriteConst \_ _->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 (LensRead \p->f) (LensWrite \p w r->pure $ Just w) sds -- 2.20.1