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}
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
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
import Data.Functor
import Control.Monad
+import Control.Monad.State
+import Control.Monad.Trans
import ASDS.Source
import ASDS.Lens
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)
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
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
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}
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
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
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
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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+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)
--- /dev/null
+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
--- /dev/null
+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 ()
--- /dev/null
+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
import Control.Monad
import Control.Monad.State
import Control.Monad.Fail
+import Control.Monad.Trans
import ASDS
import ASDS.Source
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]]
, [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)
repositories / clean-tests.git / commitdiff