From 02a1e882ea2e69f580336351fa4895b1b02121cd Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 3 Sep 2020 06:41:52 +0200 Subject: [PATCH] uds --- test.icl | 26 ++++++++++- uds/ASDS.dcl | 14 +++--- uds/ASDS.icl | 14 +++--- uds/ASDS/Lens.icl | 8 ++-- uds/ASDS/Parallel.icl | 8 ++-- uds/ASDS/Select.icl | 2 + uds/ASDS/Source.icl | 6 ++- uds/param/ASDS.dcl | 57 ++++++++++++++++++++++++ uds/param/ASDS.icl | 29 ++++++++++++ uds/param/ASDS/Lens.dcl | 55 +++++++++++++++++++++++ uds/param/ASDS/Lens.icl | 88 +++++++++++++++++++++++++++++++++++++ uds/param/ASDS/Parallel.dcl | 27 ++++++++++++ uds/param/ASDS/Parallel.icl | 57 ++++++++++++++++++++++++ uds/param/ASDS/Select.dcl | 24 ++++++++++ uds/param/ASDS/Select.icl | 28 ++++++++++++ uds/param/ASDS/Source.dcl | 29 ++++++++++++ uds/param/ASDS/Source.icl | 38 ++++++++++++++++ uds/param/test.icl | 80 +++++++++++++++++++++++++++++++++ uds/test.icl | 16 ++++--- 19 files changed, 578 insertions(+), 28 deletions(-) create mode 100644 uds/param/ASDS.dcl create mode 100644 uds/param/ASDS.icl create mode 100644 uds/param/ASDS/Lens.dcl create mode 100644 uds/param/ASDS/Lens.icl create mode 100644 uds/param/ASDS/Parallel.dcl create mode 100644 uds/param/ASDS/Parallel.icl create mode 100644 uds/param/ASDS/Select.dcl create mode 100644 uds/param/ASDS/Select.icl create mode 100644 uds/param/ASDS/Source.dcl create mode 100644 uds/param/ASDS/Source.icl create mode 100644 uds/param/test.icl diff --git a/test.icl b/test.icl index 367eccd..4e45f55 100644 --- a/test.icl +++ b/test.icl @@ -1,5 +1,27 @@ module test -import Data.Maybe +import iTasks -Start = isJust (?Just 42) +:: OpenWeatherResponse = + { main :: OpenWeatherResponseMain + , weather :: [OpenWeatherResponseWeather] + } + +:: OpenWeatherResponseWeather = + { id :: Int + , main :: String + , description :: String + , icon :: String + } +:: OpenWeatherResponseMain = + { temp :: Real + , pressure :: Int + , humidity :: Int + , temp_min :: Real + , temp_max :: Real + } + +derive class iTask OpenWeatherResponseMain, OpenWeatherResponseWeather, OpenWeatherResponse +Start w = doTasks (viewInformation [] v <<@ Title "Weather in Nijmegen from openweather.com") w + +v = {temp=18.4, pressure=1050, humidity=60, temp_min=12.5, temp_max=24.1} diff --git a/uds/ASDS.dcl b/uds/ASDS.dcl index 4a5f0ba..f8ea837 100644 --- a/uds/ASDS.dcl +++ b/uds/ASDS.dcl @@ -3,16 +3,20 @@ definition module ASDS from Data.Functor import class Functor from Control.Applicative import class Applicative, class <*>, class pure from Control.Monad import class Monad +from Control.Monad.State import :: StateT import ASDS.Source import ASDS.Parallel import ASDS.Select import ASDS.Lens +:: PViewT m a :== StateT [NRequest m] m a +:: NRequest m = NRequest String (m ()) Dynamic + //* Read a share with one rewrite step -class read v :: (v m p r w) p -> m (ReadResult m p r w) | TC r & Monad m +class read v :: (v m p r w) p -> PViewT m (ReadResult m p r w) | TC r & Monad m //* Write a share with one rewrite step -class write v :: (v m p r w) p w -> m (WriteResult m p r w) | TC w & Monad m +class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | TC w & Monad m //* Result of a single read rewrite :: ReadResult m p r w @@ -44,10 +48,10 @@ instance read SDS instance write SDS //* Read a share completely -getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w +getShare :: (sds m () r w) -> PViewT m r | Monad m & read sds & TC r & TC w //* Write a share completely -setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w +setShare :: w (sds m () r w) -> PViewT m () | Monad m & write sds & TC r & TC w //* Update a share completely -updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w +updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w diff --git a/uds/ASDS.icl b/uds/ASDS.icl index f8413c3..54f9334 100644 --- a/uds/ASDS.icl +++ b/uds/ASDS.icl @@ -2,6 +2,8 @@ implementation module ASDS import Data.Functor import Control.Monad +import Control.Monad.State +import Control.Monad.Trans import ASDS.Source import ASDS.Lens @@ -14,15 +16,15 @@ sds s = SDS s (pure ()) instance read SDS where read (SDS s _) p = read s p instance write SDS where write (SDS sds _) p w = write sds p w -getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w +getShare :: (sds m () r w) -> PViewT m r | Monad m & read sds & TC r & TC w getShare s = read s () >>= \v->case v of Reading s = getShare s - Read r = pure r + Read r = liftT (pure r) -setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w +setShare :: w (sds m () r w) -> PViewT m () | Monad m & write sds & TC r & TC w setShare w s = write s () w >>= \v->case v of Writing s = setShare w s - Written _ = pure () + Written _ = liftT (pure ()) -updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w -updShare f s = f <$> getShare s >>= \v->setShare v s >>| pure v +updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w +updShare f s = f <$> getShare s >>= \v->setShare v s >>| liftT (pure v) diff --git a/uds/ASDS/Lens.icl b/uds/ASDS/Lens.icl index 351e759..a5f4889 100644 --- a/uds/ASDS/Lens.icl +++ b/uds/ASDS/Lens.icl @@ -6,6 +6,8 @@ import Data.Functor import Data.List import Data.Maybe import Control.Monad +from Control.Monad.State import instance Monad (StateT st m), instance Functor (StateT st m), instance pure (StateT st m), instance <*> (StateT st m), instance MonadTrans (StateT st) +import Control.Monad.Trans import Control.Monad.Fail from Data.Map import :: Map(..), get, put @@ -16,10 +18,10 @@ lens param mapr mapw lens = Lens {param=param,mapr=mapr,mapw=mapw,lens=lens} instance read (Lens sds) | read sds where - read (Lens t=:{mapr=LensReadConst f}) p = Read <$> f p + read (Lens t=:{mapr=LensReadConst f}) p = Read <$> liftT (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 + Read r = Read <$> liftT (mapr p r) instance write (Lens sds) | read sds & write sds where @@ -28,7 +30,7 @@ where Reading s = pure $ Writing $ Lens {t & lens=rwpair s lens} Read r = write (Lens {t & mapw=LensWriteConst \p w->mapw p w r}) p w //Then do the actual writing - write (Lens t=:{param,mapw=LensWriteConst mapw,lens}) p w = mapw p w >>= \v->case v of + write (Lens t=:{param,mapw=LensWriteConst mapw,lens}) p w = liftT (mapw p w) >>= \v->case v of ?None = pure $ Written () ?Just w = write lens (param p) w >>= \v->case v of Writing s = pure $ Writing $ Lens {t & lens=rwpair lens s} diff --git a/uds/ASDS/Parallel.icl b/uds/ASDS/Parallel.icl index 735c8ba..ac9a341 100644 --- a/uds/ASDS/Parallel.icl +++ b/uds/ASDS/Parallel.icl @@ -5,6 +5,8 @@ import Data.Func 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 @@ -45,9 +47,9 @@ where // 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 diff --git a/uds/ASDS/Select.icl b/uds/ASDS/Select.icl index 14de73b..955b8cb 100644 --- a/uds/ASDS/Select.icl +++ b/uds/ASDS/Select.icl @@ -4,6 +4,8 @@ import StdEnv import Data.Func import Data.Functor import Control.Monad +import Control.Monad.State +import Control.Monad.Trans import ASDS select` :: (p -> p1) (p r1 -> p2) (sdsl m p1 r1 w1) (sdsr m p2 r w) -> Select sdsl sdsr m p r w | TC p & TC p1 & TC p2 & TC r1 & TC r & TC w & pure m diff --git a/uds/ASDS/Source.icl b/uds/ASDS/Source.icl index 5ffb97f..65c7443 100644 --- a/uds/ASDS/Source.icl +++ b/uds/ASDS/Source.icl @@ -3,6 +3,8 @@ implementation module ASDS.Source import Data.Func import Data.Functor import Control.Monad +import Control.Monad.State +import Control.Monad.Trans import ASDS rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w | pure m @@ -13,11 +15,11 @@ source read write = rwpair (ReadSource read) (WriteSource write) instance read ReadSource where - read (ReadSource read) p = Read <$> read p + read (ReadSource read) p = Read <$> liftT (read p) instance write WriteSource where - write (WriteSource write) p w = Written <$> write p w + write (WriteSource write) p w = Written <$> liftT (write p w) instance read (RWPair sdsr sdsw) | read sdsr where diff --git a/uds/param/ASDS.dcl b/uds/param/ASDS.dcl new file mode 100644 index 0000000..4a52da0 --- /dev/null +++ b/uds/param/ASDS.dcl @@ -0,0 +1,57 @@ +definition module ASDS + +from Data.Functor import class Functor +from Control.Applicative import class Applicative, class <*>, class pure +from Control.Monad import class Monad +from Control.Monad.State import :: StateT + +import ASDS.Source +import ASDS.Parallel +import ASDS.Select +import ASDS.Lens + +:: PViewT m a = PViewT (StateT [NRequest m] m a) (m ()) +:: NRequest m = NRequest String (m ()) + +//* Read a share with one rewrite step +class read v :: (v m p r w) p -> m (ReadResult m p r w) | TC r & Monad m +//* Write a share with one rewrite step +class write v :: (v m p r w) p w -> m (WriteResult m p r w) | TC w & Monad m + +//* Result of a single read rewrite +:: ReadResult m p r w + = Read r //* done reading + | E.sds: Reading (sds m p r w) & read sds //* not done reading + | ReadResultUnused (m ()) + +//* Result of a single write rewrite +:: WriteResult m p r w + = Written () //* done writing + | E.sds: Writing (sds m p r w) & write sds //* not done writing + | WriteResultUnused (m ()) + +//* Read lens, it can choose to ignore the source +:: LensRead m p r rs + = LensRead (p rs -> m r) + | LensReadConst (p -> m r) + +//* Write lens, it can choose to ignore the source, and thus not read it +:: LensWrite m p w rs ws + = LensWrite (p w rs -> m (? ws)) + | LensWriteConst (p w -> m (? ws)) + +//* Box type, to get rid of a possible complex constructor of combinators +:: SDS m p r w = E.sds: SDS (sds m p r w) (m ()) /*force kind*/ & read sds & write sds +sds :: (sds m p r w) -> SDS m p r w | read sds & write sds & Monad m + +instance read SDS +instance write SDS + +//* Read a share completely +getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w + +//* Write a share completely +setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w + +//* Update a share completely +updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w diff --git a/uds/param/ASDS.icl b/uds/param/ASDS.icl new file mode 100644 index 0000000..24de5be --- /dev/null +++ b/uds/param/ASDS.icl @@ -0,0 +1,29 @@ +implementation module ASDS + +import Data.Functor +import Control.Monad +import Control.Monad.State + +import ASDS.Source +import ASDS.Lens +import ASDS.Select +import ASDS.Parallel + +sds :: (sds m p r w) -> SDS m p r w | read sds & write sds & Monad m +sds s = SDS s (pure ()) + +instance read SDS where read (SDS s _) p = read s p +instance write SDS where write (SDS sds _) p w = write sds p w + +getShare :: (sds m () r w) -> m r | Monad m & read sds & TC r & TC w +getShare s = read s () >>= \v->case v of + Reading s = getShare s + Read r = pure r + +setShare :: w (sds m () r w) -> m () | Monad m & write sds & TC r & TC w +setShare w s = write s () w >>= \v->case v of + Writing s = setShare w s + Written _ = pure () + +updShare :: (r -> w) (sds m () r w) -> m w | Monad m & read sds & write sds & TC r & TC w +updShare f s = f <$> getShare s >>= \v->setShare v s >>| pure v diff --git a/uds/param/ASDS/Lens.dcl b/uds/param/ASDS/Lens.dcl new file mode 100644 index 0000000..3a66a34 --- /dev/null +++ b/uds/param/ASDS/Lens.dcl @@ -0,0 +1,55 @@ +definition module ASDS.Lens + +from ASDS import class read, class write, :: LensWrite, :: LensRead + +from StdOverloaded import class < +from StdClass import class Eq +from Control.Monad import class Monad +from Control.Monad.Fail import class MonadFail +from Control.Applicative import class Applicative, class <*>, class pure +from Data.Functor import class Functor +from Data.Map import :: Map + +//* 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 +:: LensOpts sds m p1 r1 w1 p r w = + { param :: p -> p1 + , mapr :: LensRead m p r r1 + , mapw :: LensWrite m p w r1 w1 + , lens :: sds m p1 r1 w1 + } +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 + +instance read (Lens sds) | read sds +instance write (Lens sds) | read sds & write sds + +//* Map a function to the value read +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 +(>?@) infixl 6 +(>?@) :== mapRead + +//* Map a function to the value written. +mapWrite :: (w` r -> m (? w)) (sds m p r w) -> Lens sds m p r w` | TC r & TC w & TC w` & TC p & Monad m +(>!@) infixl 6 +(>!@) :== mapWrite + +//* Translate the parameter space +translate :: (p -> ps) (sds m ps r w) -> Lens sds m p r w | TC r & TC w & TC p & TC ps & Monad m + +//* focus a parameter: @type :: p (sds m p r w) -> (sds m p` r w) +focus p :== translate \_->p + +//* Deserialize from a dynamic store +fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m + +//* Serialize to a dynamic store +toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m + +//* Focus on a single element in a list +indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m + +//* Focus on a single element in an associative list +assocStore :: (sds m p [(k, v)] [(k, v)]) -> Lens sds m (p, k) v v | TC v & TC k & Eq k & TC p & MonadFail m + +//* Focus on a value in a map +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 diff --git a/uds/param/ASDS/Lens.icl b/uds/param/ASDS/Lens.icl new file mode 100644 index 0000000..351e759 --- /dev/null +++ b/uds/param/ASDS/Lens.icl @@ -0,0 +1,88 @@ +implementation module ASDS.Lens + +import StdEnv +import Data.Func +import Data.Functor +import Data.List +import Data.Maybe +import Control.Monad +import Control.Monad.Fail +from Data.Map import :: Map(..), get, put + +import ASDS, ASDS.Source + +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=:{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 + +instance write (Lens sds) | read sds & write sds +where + //First read the child when necessary + 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 = write (Lens {t & mapw=LensWriteConst \p w->mapw p w r}) p w + //Then do the actual writing + write (Lens t=:{param,mapw=LensWriteConst mapw,lens}) p w = mapw p w >>= \v->case v of + ?None = 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 () + +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 + +mapWrite :: (w` r -> m (? 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 (LensRead \p r->pure r) (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 (LensRead \p r->pure r) (LensWriteConst \p w->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 (LensRead read) (LensWriteConst write) sds +where + read p (r :: r^) = pure r + read p r = fail $ "fromDynStore: " +++ typeMismatchError r (dynamic undef :: r^) + write p w = pure $ ?Just (dynamic w) + +toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m +toDynStore sds = lens id (LensRead read) (LensWriteConst write) sds +where + read p r = pure (dynamic r) + write p (w :: w^) = pure $ ?Just w + write p w = fail $ "toDynStore: " +++ typeMismatchError w (dynamic undef :: w^) + +typeMismatchError :: Dynamic Dynamic -> String +typeMismatchError a b = "type mismatch " +++ toString (typeCodeOfDynamic a) +++ " and" +++ toString (typeCodeOfDynamic b) + +indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m +indexedStore sds = lens param (LensRead read) (LensWrite write) sds +where + param (p, _) = p + read (_, idx) r = case r !? idx of + ?None = fail "indexedStore: index out of range" + ?Just a = pure a + write (_, idx) w r = pure $ ?Just $ updateAt idx w r + +assocStore :: (sds m p [(k, v)] [(k, v)]) -> Lens sds m (p, k) v v | TC v & TC k & Eq k & TC p & MonadFail m +assocStore sds = lens param (LensRead read) (LensWrite write) sds +where + param (p, _) = p + read (_, k) r = case lookup k r of + ?None = fail "assocStore: key not present" + ?Just a = pure a + write (_, k) w r = pure $ ?Just [(k, w):filter ((<>) k o fst) 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 (LensRead read) (LensWrite write) sds +where + param (p, _) = p + read (_, k) r = case get k r of + ?None = fail "keyedStore: key not present" + ?Just a = pure a + write (_, k) w r = pure $ ?Just $ put k w r diff --git a/uds/param/ASDS/Parallel.dcl b/uds/param/ASDS/Parallel.dcl new file mode 100644 index 0000000..91d61c1 --- /dev/null +++ b/uds/param/ASDS/Parallel.dcl @@ -0,0 +1,27 @@ +definition module ASDS.Parallel + +from ASDS import class read, class write, :: LensWrite, :: LensRead +from Control.Monad import class Monad +from Control.Applicative import class Applicative, class <*>, class pure +from Data.Functor import class Functor + +//* 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 +:: ParOpts sdsl sdsr m p1 p2 r1 r2 w1 w2 p r w = + { param :: p -> (p1, p2) + , readl :: r1 r2 -> r + , writel :: LensWrite m p w r1 w1 + , writer :: LensWrite m p w r2 w2 + , left :: sdsl m p1 r1 w1 + , right :: sdsr m p2 r2 w2 + } +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 + +instance read (Par sdsl sdsr) | read sdsl & read sdsr +instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr + +//* Product of two shares +(>*<) 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 + +//* Product of two shares that have the same the parameter +(>+<) 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 diff --git a/uds/param/ASDS/Parallel.icl b/uds/param/ASDS/Parallel.icl new file mode 100644 index 0000000..735c8ba --- /dev/null +++ b/uds/param/ASDS/Parallel.icl @@ -0,0 +1,57 @@ +implementation module ASDS.Parallel + +import StdEnv +import Data.Func +import Data.Functor +import Data.Tuple +import Control.Monad +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 +par param readl writel writer left right = Par {param=param,readl=readl,writel=writel,writer=writer,left=left,right=right} + +instance read (Par sdsl sdsr) | read sdsl & read sdsr +where + read (Par t=:{param,readl,left,right}) p + = read left p1 >>= \v->case v of + Reading s = pure $ Reading $ Par {t & left=s} + Read l = read right p2 >>= \v->case v of + Reading s = pure $ Reading $ Par {t & left=constShare l, right=s} + Read r = pure $ Read $ readl l r + where (p1, p2) = param p + +instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr +where + //First read the lhs if necessary + write (Par t=:{param,writel=LensWrite writel,left}) p w + = read left p1 >>= \v->case v of + Reading s = pure $ Writing $ Par {t & left=rwpair s left} + Read r1 = write (Par {t & writel=LensWriteConst \p w->writel p w r1}) p w + where (p1, p2) = param p + //Then read the rhs if necessary + write (Par t=:{param,writer=LensWrite writer,right}) p w + = read right p2 >>= \v->case v of + Reading s = pure $ Writing $ Par {t & right=rwpair s right} + Read r2 = write (Par {t & writer=LensWriteConst \p w->writer p w r2}) p w + where (p1, p2) = param p + //Then do the actual writing + write (Par t=:{param,writel=LensWriteConst writel,writer=LensWriteConst writer,left,right}) p w + = write` left p1 (writel p w) >>= \v->case v of + Writing s = pure $ Writing $ Par {t & left=rwpair left s} + Written () = write` right p2 (writer p w) >>= \v->case v of + Writing s = pure $ Writing $ Par {t & left=rwpair left nullShare, right=rwpair right s} + Written () = pure $ Written () + where (p1, p2) = param p + +// 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 () + ?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 +(>*<) l r = par id tuple (LensWriteConst \p (w1, _)->pure $ ?Just w1) (LensWriteConst \p (_, w2)->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 (LensWriteConst \p (w1, _)->pure $ ?Just w1) (LensWriteConst \p (_, w2)->pure $ ?Just w2) l r diff --git a/uds/param/ASDS/Select.dcl b/uds/param/ASDS/Select.dcl new file mode 100644 index 0000000..bf5bc88 --- /dev/null +++ b/uds/param/ASDS/Select.dcl @@ -0,0 +1,24 @@ +definition module ASDS.Select + +from ASDS import class read, class write +from ASDS.Lens import :: Lens +from Control.Monad import class Monad +from Control.Monad.Fail import class MonadFail +from Control.Applicative import class Applicative, class <*>, class pure +from Data.Functor import class Functor + +//* 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 +:: SelectOpts sdsl sdsr m p1 r1 w1 p2 p r w = + { index :: sdsl m p1 r1 w1 + , source :: sdsr m p2 r w + , parami :: p -> p1 + , params :: p r1 -> p2 + , unused :: m () + } +select` :: (p -> p1) (p r1 -> p2) (sdsl m p1 r1 w1) (sdsr m p2 r w) -> Select sdsl sdsr m p r w | TC p & TC p1 & TC p2 & TC r1 & TC r & TC w & pure m + +instance read (Select sdsl sdsr) | read sdsl & read sdsr +instance write (Select sdsl sdsr) | read sdsl & write sdsr + +selectList :: (sdss m p1 Int w1) (sdsc m p2 [a] [a]) -> Select sdss (Lens sdsc) m (p1, p2) a a | TC p1 & TC p2 & TC a & TC w1 & MonadFail m diff --git a/uds/param/ASDS/Select.icl b/uds/param/ASDS/Select.icl new file mode 100644 index 0000000..14de73b --- /dev/null +++ b/uds/param/ASDS/Select.icl @@ -0,0 +1,28 @@ +implementation module ASDS.Select + +import StdEnv +import Data.Func +import Data.Functor +import Control.Monad +import ASDS + +select` :: (p -> p1) (p r1 -> p2) (sdsl m p1 r1 w1) (sdsr m p2 r w) -> Select sdsl sdsr m p r w | TC p & TC p1 & TC p2 & TC r1 & TC r & TC w & pure m +select` parami params index source = Select {parami=parami,params=params,index=index,source=source,unused=pure ()} + +instance read (Select sdsl sdsr) | read sdsl & read sdsr +where + read (Select t=:{parami,params,index,source}) p = read index (parami p) >>= \v->case v of + Reading s = pure $ Reading $ Select {t & index=s} + Read r1 = read source (params p r1) >>= \v->case v of + Reading s = pure $ Reading $ Select {t & index=constShare r1, source=s} + Read r = pure $ Read r +instance write (Select sdsl sdsr) | read sdsl & write sdsr +where + write (Select t=:{parami,params,index,source}) p w = read index (parami p) >>= \v->case v of + Reading s = pure $ Writing $ Select {t & index=s} + Read r1 = write source (params p r1) w >>= \v->case v of + Writing s = pure $ Writing $ Select {t & index=constShare r1, source=s} + Written () = pure $ Written () + +selectList :: (sdss m p1 Int w1) (sdsc m p2 [a] [a]) -> Select sdss (Lens sdsc) m (p1, p2) a a | TC p1 & TC p2 & TC a & TC w1 & MonadFail m +selectList sdss sdsc = select` (\(p1, p2)->p1) (\(p1, p2) i->(p2, i)) sdss (indexedStore sdsc) diff --git a/uds/param/ASDS/Source.dcl b/uds/param/ASDS/Source.dcl new file mode 100644 index 0000000..ab3446b --- /dev/null +++ b/uds/param/ASDS/Source.dcl @@ -0,0 +1,29 @@ +definition module ASDS.Source + +from ASDS import class read, class write +from Control.Monad import class Monad +from Control.Applicative import class Applicative, class <*>, class pure +from Data.Functor import class Functor + +//* Just read something +:: ReadSource m p r w = ReadSource (p -> m r) + +//* Just write something +:: WriteSource m p r w = WriteSource (p w -> m ()) + +//* Pair a two shares to form a read/write sds that only touches one share per action +:: RWPair sdsr sdsw m p r w = RWPair (sdsr m p r w) (sdsw m p r w) (m ()) +rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w | pure m + +//* Special type of RWPair that contains sds sources +:: Source m p r w :== RWPair ReadSource WriteSource m p r w +source :: (p -> m r) (p w -> m ()) -> Source m p r w | pure m + +instance read ReadSource, (RWPair sdsr sdsw) | read sdsr +instance write WriteSource, (RWPair sdsr sdsw) | write sdsw + +//* Immediately returns the given value on a read +constShare :: a -> ReadSource m p a b | pure m + +//* Values written are discarded +nullShare :: WriteSource m p a b | pure m diff --git a/uds/param/ASDS/Source.icl b/uds/param/ASDS/Source.icl new file mode 100644 index 0000000..5ffb97f --- /dev/null +++ b/uds/param/ASDS/Source.icl @@ -0,0 +1,38 @@ +implementation module ASDS.Source + +import Data.Func +import Data.Functor +import Control.Monad +import ASDS + +rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w | pure m +rwpair l r = RWPair l r (pure ()) + +source :: (p -> m r) (p w -> m ()) -> Source m p r w | pure m +source read write = rwpair (ReadSource read) (WriteSource write) + +instance read ReadSource +where + read (ReadSource read) p = Read <$> read p + +instance write WriteSource +where + write (WriteSource write) p w = Written <$> write p w + +instance read (RWPair sdsr sdsw) | read sdsr +where + read (RWPair s w _) p = read s p >>= \v->case v of + Reading s = pure $ Reading (rwpair s w) + Read r = pure $ Read r + +instance write (RWPair sdsr sdsw) | write sdsw +where + write (RWPair r s _) p w = write s p w >>= \v->case v of + Writing s = pure $ Writing $ rwpair r s + Written _ = pure $ Written () + +constShare :: a -> ReadSource m p a b | pure m +constShare a = ReadSource \_->pure a + +nullShare :: WriteSource m p a b | pure m +nullShare = WriteSource \_ _->pure () diff --git a/uds/param/test.icl b/uds/param/test.icl new file mode 100644 index 0000000..0431427 --- /dev/null +++ b/uds/param/test.icl @@ -0,0 +1,80 @@ +module test + +import StdEnv +import Data.Either +import Data.Func +from Data.Map import :: Map(..) +import qualified Data.Map +import Control.Monad +import Control.Monad.State +import Control.Monad.Fail + +import ASDS +import ASDS.Source +import ASDS.Lens +import ASDS.Select +import ASDS.Parallel + +instance MonadFail (Either String) where fail s = Left s + + +readwrite :: r w (sds m () r w) -> m () | MonadFail m & read sds & write sds & TC r & TC w & == r +readwrite r w sds = equal r (setShare w sds >>| getShare sds) + +equal :: a (m a) -> m () | MonadFail m & == a +equal expected mon = mon >>= \v->if (v == expected) (pure ()) (fail "Not equal") + +Start :: Either String ((), Map String Dynamic) +Start = runStateT (sequence_ $ map test tests) 'Data.Map'.newMap +where + test t = put 'Data.Map'.newMap >>| t + + tests = flatten + [ [readwrite i i sh \\ i<-[-1, 0, -100, 100]] + , [setShare [0..10] sh >>| equal i (getShare (focus ((), i) (indexedStore sh)))\\i<-[0..10]] + , [setShare [0..10] sh >>| setShare 42 (focus ((), i) (indexedStore sh)) >>| equal 42 (getShare (focus ((), i) (indexedStore sh)))\\i<-[0..10]] + , [setShare [(i, i)\\i<-[0..10]] sh >>| equal i (getShare (focus ((), i) (assocStore sh)))\\i<-[0..10]] + , [setShare ('Data.Map'.fromList [(i, i)\\i<-[0..10]]) sh >>| equal i (getShare (focus ((), i) (keyedStore sh)))\\i<-[0..10]] + , [setShare [0..10] sh >>| setShare 4 (focus "idx" astore) >>| equal 4 (getShare $ focus ((), ()) $ selectList (focus "idx" astore) sh)] + , [setShare 38 sh >>| equal 38 (getShare (After 100 sh (pure ())))] + , [testpar (focus "foo" astore) (focus "bar" astore)] + , [testpar (after 100 $ focus "foo" astore) (after 100 $ focus "bar" astore)] + , [testpar (after 100 $ focus "foo" astore) (focus "bar" astore)] + , [testpar (focus "foo" astore) (after 100 $ focus "bar" astore)] +//selectList :: (sdss m p1 Int w1) (sdsc m p2 [a] [a]) -> Select sdss (Lens sdsc) m (p1, p2) a a | TC p1 & TC p2 & TC a & TC w1 & MonadFail m + ] + + sh :: Lens (Lens (Lens (Lens (RWPair ReadSource WriteSource)))) (StateT (Map String Dynamic) m) () a a | MonadFail m & TC a + sh = focus "foo" astore + +testpar :: (A.a: sds1 m () a a | TC, == a) (A.a: sds2 m () a a | TC, == a) -> m () | MonadFail m & read, write sds1 & read, write sds2 +testpar l r = + setShare (42, 'a') (l >+< r) + >>| equal (42, 'a') (getShare $ l >+< r) >>| equal 42 (getShare l) >>| equal 'a' (getShare r) + >>| setShare 38 l + >>| equal (38, 'a') (getShare $ l >+< r) >>| equal 38 (getShare l) >>| equal 'a' (getShare r) + >>| setShare 'b' r + >>| equal (38, 'b') (getShare $ l >+< r) >>| equal 38 (getShare l) >>| equal 'b' (getShare r) + +:: After sds m p r w = After Int (sds m p r w) (m ()) +after :: Int (sds m p r w) -> After sds m p r w | pure m +after i sds = After i sds $ pure () + +instance read (After sds) | read sds +where + read (After 0 sds _) p = read sds p + read (After n sds m) p = pure (Reading (After (n-1) sds m)) + +instance write (After sds) | write sds +where + write (After 0 sds _) p w = write sds p w + write (After n sds m) p w = pure (Writing (After (n-1) sds m)) + +astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a +astore = fromDynStore dstore + +dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m +dstore = translate (\i->((), i)) $ keyedStore store + +store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m +store = source (\_->getState) \_->put diff --git a/uds/test.icl b/uds/test.icl index 0431427..4d8049e 100644 --- a/uds/test.icl +++ b/uds/test.icl @@ -8,6 +8,7 @@ import qualified Data.Map import Control.Monad import Control.Monad.State import Control.Monad.Fail +import Control.Monad.Trans import ASDS import ASDS.Source @@ -18,17 +19,19 @@ import ASDS.Parallel instance MonadFail (Either String) where fail s = Left s -readwrite :: r w (sds m () r w) -> m () | MonadFail m & read sds & write sds & TC r & TC w & == r +readwrite :: r w (sds m () r w) -> PViewT m () | MonadFail m & read sds & write sds & TC r & TC w & == r readwrite r w sds = equal r (setShare w sds >>| getShare sds) -equal :: a (m a) -> m () | MonadFail m & == a +equal :: a (PViewT m a) -> PViewT m () | MonadFail m & == a equal expected mon = mon >>= \v->if (v == expected) (pure ()) (fail "Not equal") -Start :: Either String ((), Map String Dynamic) -Start = runStateT (sequence_ $ map test tests) 'Data.Map'.newMap +//Start :: Either String ((), Map String Dynamic) +Start = runStateT (runStateT (sequence_ $ map test tests) []) 'Data.Map'.newMap where - test t = put 'Data.Map'.newMap >>| t + test t = liftT (put 'Data.Map'.newMap) >>| t +// tests :: [StateT [NRequest (StateT (Map String Dynamic) (Either String))] (StateT (Map String Dynamic) (Either String)) ()] + tests :: [PViewT (StateT (Map String Dynamic) (Either String)) ()] tests = flatten [ [readwrite i i sh \\ i<-[-1, 0, -100, 100]] , [setShare [0..10] sh >>| equal i (getShare (focus ((), i) (indexedStore sh)))\\i<-[0..10]] @@ -41,13 +44,12 @@ where , [testpar (after 100 $ focus "foo" astore) (after 100 $ focus "bar" astore)] , [testpar (after 100 $ focus "foo" astore) (focus "bar" astore)] , [testpar (focus "foo" astore) (after 100 $ focus "bar" astore)] -//selectList :: (sdss m p1 Int w1) (sdsc m p2 [a] [a]) -> Select sdss (Lens sdsc) m (p1, p2) a a | TC p1 & TC p2 & TC a & TC w1 & MonadFail m ] sh :: Lens (Lens (Lens (Lens (RWPair ReadSource WriteSource)))) (StateT (Map String Dynamic) m) () a a | MonadFail m & TC a sh = focus "foo" astore -testpar :: (A.a: sds1 m () a a | TC, == a) (A.a: sds2 m () a a | TC, == a) -> m () | MonadFail m & read, write sds1 & read, write sds2 +testpar :: (A.a: sds1 m () a a | TC, == a) (A.a: sds2 m () a a | TC, == a) -> PViewT m () | MonadFail m & read, write sds1 & read, write sds2 testpar l r = setShare (42, 'a') (l >+< r) >>| equal (42, 'a') (getShare $ l >+< r) >>| equal 42 (getShare l) >>| equal 'a' (getShare r) -- 2.20.1