definition module Data.GenType
import StdGeneric
-from StdMaybe import :: Maybe
:: Box b a =: Box b
derive bimap Box
implementation module Data.GenType
-import StdEnv, StdGeneric, StdMaybe
+import StdEnv, StdGeneric
import Control.Applicative
import Control.Monad => qualified join
, ("_!List!", "[!!]"), ("_!Cons!", "(:)"), ("_!Nil!", "[ !]")
, ("_#List", "[#]"), ("_#Cons", "(:)"), ("_#Nil", "[#]")
, ("_#List!", "[#!]"), ("_#Cons!", "(:)"), ("_#Nil!", "[#!]")
+ , ("_!Maybe", "?"), ("_!Just", "?Just"), ("_!None", "?None")
+ , ("_Maybe", "?^"), ("_Just", "?^Just"), ("_None", "?^None")
, ("_Array", "{}"), ("_!Array", "{!}"), ("_#Array", "{#}"), ("_32#Array", "{32#}")
, ("_Unit", "()")
:[("_Tuple" +++ toString i, "(" +++ createArray i ',' +++")")\\i<-[2..32]]]
gType{|{!}|} a = box $ GTyArray AStrict $ unBox a
gType{|{#}|} a = box $ GTyArray AUnboxed $ unBox a
gType{|{32#}|} a = box $ GTyArray APacked $ unBox a
-derive gType ?#, ?, ?^
+derive gType ?, ?^
derive gType [], [! ], [ !], [!!]
derive gType (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
import Control.Monad.State
import Control.Monad.Trans
import Data.Either
-import Data.Maybe
import Data.Func
import Data.Functor
import Data.Tuple
import qualified Data.Map
from Data.Map import :: Map(..), putList, alter, get, union, fromList
+import Data.Maybe
import StdEnv
import Data.GenType
import Text
BTReal = indent i ["double":c]
BTBool = indent i ["bool":c]
t = []
- ftd (TyArrow l r) i c = indent i ["*":ftd a i c]
+// ftd (TyArrow l r) i c = indent i ["*":ftd a i c]
ftd (TyArray _ a) i c = indent i ["*":ftd a i c]
ftd (TyNewType ti ci a) i c = ftd a i c
ftd (TyRecord ti fs) i c
+++ /dev/null
-{-# LANGUAGE GADTs, DeriveGeneric, DefaultSignatures, TypeOperators #-}
-module Main where
-
-import GHC.Generics
-
-data GType a where
- Unit :: GType (U1 p)
- Product :: (GType a) (GType b) -> GType ((a :*: b) p)
- Sum :: (GType a) (GType b) -> GType (a :+: b)
-
-
-main = putStrLn ""
+++ /dev/null
-{-# LANGUAGE GADTs #-}
-module Main where
-
-data GType
-data GType a where
- Unit :: GType UNIT
- Add :: (Num a, Eq a) => Expr a -> Expr a -> Expr a
- Ext :: (Eval v, Print v, Opt v, Typeable v) => v a -> Expr a
-
-main = putStrLn ""
module test
-import StdEnv, StdGeneric, StdMaybe
+import StdEnv, StdGeneric
import Data.Func
import Data.Functor
import Data.List
import Data.Tuple
import Data.Bifunctor
-import Control.GenBimap
import Data.Maybe
+import Control.GenBimap
import Data.Either
import Data.GenType
import Data.GenType.CType
-derive gType Either, Maybe, T, R, Frac, Tr, Fix, Odd, Even, SR, List, Enum, NT, Blurp, EnumList
+derive gType Either, T, R, Frac, Tr, Fix, Odd, Even, SR, List, Enum, NT, Blurp, EnumList
:: T a =: T2 a
:: NT =: NT Int
:: SR = {f1 :: Int, f2 :: Bool, f3 :: Tr Either Bool, f4 :: Enum}
-:: R a = {f1 :: Maybe (R a), f2 :: Bool, f3 :: T a, f4 :: Char -> Dynamic,
+:: R a = {f1 :: ? (R a), f2 :: Bool, f3 :: T a, f4 :: Char -> Dynamic,
f5 :: [([#Int], [#Int!], [!Int!], [!Int], [Int!])],
f6 :: ({!Int}, {R Bool}, {#Char}, {32#Int}),/*({!Int}, {#Char}, {R Bool})*/
f7 :: {!Int}}
//t :: Box GType (Maybe [Maybe (Either Bool String)])
//t :: Box GType ([SR], Enum, T Int, NT, Blurp Int)
//t :: Box GType [EnumList]
-t :: Box GType (Int -> SR)
+t :: Box GType (?(?(?Int)))
//t :: Box GType (Odd Int, (), [Either (R (T *World)) (Frac Real)], Tr Either Bool, Fix Maybe)
t = gType{|*|}
-
-//Start = toString t
-//
-//t :: GGType [Int]
-//t = ggType{|*|}
-//
-//:: BM a b =
-// { ab :: a -> b
-// , ba :: b -> a
-//// , mab :: A.m: (m a) -> m b
-//// , mba :: A.m: (m b) -> m a
-// }
-//bm :: BM a a
-//bm = {ab=id, ba=id}//, mab=id, mba=id}
-//
-//:: GGType a
-// = GGBasicType BasicType
-// | GGTyRef String
-// | GGUnit
-// | E.e: GGObject (BM a (OBJECT e)) GenericTypeDefDescriptor (GGType e)
-// | E.e: GGRecord (BM a (RECORD e)) GenericRecordDescriptor (GGType e)
-// | E.e: GGCons (BM a (CONS e)) GenericConsDescriptor (GGType e)
-// | E.e: GGField (BM a (FIELD e)) GenericFieldDescriptor (GGType e)
-// | E.l r: GGEither (BM a (EITHER l r)) (GGType l) (GGType r)
-// | E.l r: GGPair (BM a (PAIR l r)) (GGType l) (GGType r)
-// | E.l r: GGArrow (BM a (l -> r)) (GGType l) (GGType r)
-//
-//instance toString (GGType a)
-//where
-// toString (GGBasicType t) = toString t
-// toString GGUnit = "UNIT"
-// toString (GGObject bm i e) = "(OBJECT " +++ i.gtd_name +++ " " +++ toString e +++ ")"
-// toString (GGRecord bm i e) = "(RECORD " +++ i.grd_name +++ " " +++ toString e +++ ")"
-// toString (GGCons bm i e) = "(CONS " +++ i.gcd_name +++ " " +++ toString e +++ ")"
-// toString (GGField bm i e) = "(FIELD " +++ i.gfd_name +++ " " +++ toString e +++ ")"
-// toString (GGEither bm l r) = "(EITHER " +++ toString l +++ " " +++ toString r +++ ")"
-// toString (GGPair bm l r) = "(PAIR " +++ toString l +++ " " +++ toString r +++ ")"
-//
-//ggtypemap :: (.a -> .b) (.b -> .a) u:(GGType .a) -> u:GGType .b
-//ggtypemap ab ba (GGBasicType t) = (GGBasicType t)
-//ggtypemap ab ba GGUnit = GGUnit
-//ggtypemap ab ba (GGObject bm i a) = GGObject {bm & ab=bm.ab o ba, ba=ab o bm.ba} i a
-//ggtypemap ab ba (GGRecord bm i a) = GGRecord {bm & ab=bm.ab o ba, ba=ab o bm.ba} i a
-//ggtypemap ab ba (GGCons bm i a) = GGCons {bm & ab=bm.ab o ba, ba=ab o bm.ba} i a
-//ggtypemap ab ba (GGField bm i a) = GGField {bm & ab=bm.ab o ba, ba=ab o bm.ba} i a
-//ggtypemap ab ba (GGEither bm l r) = GGEither {bm & ab=bm.ab o ba, ba=ab o bm.ba} l r
-//ggtypemap ab ba (GGPair bm l r) = GGPair {bm & ab=bm.ab o ba, ba=ab o bm.ba} l r
-//ggtypemap ab ba (GGArrow bm l r) = GGArrow {bm & ab=bm.ab o ba, ba=ab o bm.ba} l r
-//
-//bimap{|GGType|} ab ba t = ggtypemap ab ba t
-//
-//generic ggType a :: GGType a
-//ggType{|UNIT|} = GGUnit
-//ggType{|OBJECT of gtd|} f = GGObject bm gtd f
-//ggType{|CONS of gcd|} f = GGCons bm gcd f
-//ggType{|RECORD of grd|} f = GGRecord bm grd f
-//ggType{|FIELD of gfd|} f = GGField bm gfd f
-//ggType{|EITHER|} fl fr = GGEither bm fl fr
-//ggType{|PAIR|} fl fr = GGPair bm fl fr
-//
-//ggType{|Int|} = GGBasicType BTInt
-//ggType{|Bool|} = GGBasicType BTBool
-//ggType{|Real|} = GGBasicType BTReal
-//ggType{|Char|} = GGBasicType BTChar
-//ggType{|World|} = GGBasicType BTWorld
-//ggType{|Dynamic|} = GGBasicType BTDynamic
-//ggType{|File|} = GGBasicType BTFile
-//
-//ggType{|(->)|} fl fr = GGArrow bm fl fr
-////ggType{|[#]|} f = GGUList ULLazy f
-////ggType{|[#!]|} f = GGUList ULStrict f
-////ggType{|{}|} f = GGArray ALazy f
-////ggType{|{!}|} f = GGAray AStrict f
-////ggType{|{#}|} f = GGArray AUnboxed f
-////ggType{|{32#}|} f = GGArray APacked f
-//derive ggType []
+++ /dev/null
-module test
-
-import iTasks
-
-Start w = doTasks (return ()) w
module test
-class C m :: u:m -> v:m
+import Data.Maybe
+
+Start = isJust (?Just 42)
--- /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
+
+import ASDS.Source
+import ASDS.Parallel
+import ASDS.Select
+import ASDS.Lens
+
+//* 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 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
-definition module asds
-
-from Control.Applicative import class Applicative, class pure, class <*>
-from Control.Monad import class Monad
-from Control.Monad.State import :: StateT
-from Data.Either import :: Either
-from Data.Functor import class Functor
-from Data.Map import :: Map
-from StdMaybe import :: Maybe
-from StdOverloaded import class <, class fromString
-from System.FilePath import :: FilePath
-from System.IO import :: IO
-from System.Time import :: Timestamp
-
-class MonadFail m | Monad m where fail :: String -> m a
-instance MonadFail Maybe, []
-instance MonadFail (Either a) | fromString a
-instance MonadFail (StateT s m) | MonadFail 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 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
-//* 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
-
-//* 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, ReadSource
-instance read (RWPair sdsr sdsw) | read sdsr
-instance read (Par sdsl sdsr) | read sdsl & read sdsr
-instance read (Lens sds) | read sds
-//instance read (Select sdsl sdsr) | read sdsl & read sdsr
-
-instance write SDS, WriteSource
-instance write (RWPair sdsr sdsw) | write sdsw
-instance write (Par sdsl sdsr) | read sdsl & read sdsr & write sdsl & write sdsr
-instance write (Lens sds) | read sds & write sds
-//instance write (Select sdsl sdsr) | read sdsl & write sdsr
-
-//* 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) | RWPairUnused (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
-
-//* 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) (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 :: 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
- }
-
-//* 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) (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 :: 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
-:: 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 ()
- }
-
-//* Immediately returns the given value on a read
-constShare :: a -> ReadSource m p a b | Monad m
-//* Values written are discarded
-nullShare :: WriteSource m p a b | Monad m
-
-//* Current time
-timeStamp :: ReadSource IO () Timestamp ()
-
-////* 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 (Maybe 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
-
-(>*<) 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
-
-fromDynStore :: (sds m p Dynamic Dynamic) -> Lens sds m p r w | TC r & TC w & TC p & MonadFail m
-toDynStore :: (sds m p r w) -> Lens sds m p Dynamic Dynamic | TC r & TC w & TC p & MonadFail m
-
-indexedStore :: (sds m p [a] [a]) -> Lens sds m (p, Int) a a | TC a & TC p & MonadFail m
-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
-
-astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
-dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynamic) m) String Dynamic Dynamic | MonadFail m
-store :: Source (StateT (Map String Dynamic) m) () (Map String Dynamic) (Map String Dynamic) | Monad m
-
-file :: Source IO FilePath String String
+++ /dev/null
-implementation module asds
-
-import StdEnv
-import Data.Maybe
-import Data.Functor
-import Data.Func
-import Data.Either
-import Data.Tuple
-import Data.List
-import Control.Applicative
-import Control.Monad
-import Control.Monad.State
-import Control.Monad.Trans
-import qualified Data.Map
-from Data.Map import :: Map
-import System.FilePath
-
-import System.IO
-import System.Time
-
-instance MonadFail Maybe where fail _ = Nothing
-instance MonadFail [] where fail _ = []
-instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
-instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
-
-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
-
-source :: (p -> m r) (p w -> m ()) -> Source m p r w
-source read write = RWPair (ReadSource read) (WriteSource write)
-
-constShare :: a -> ReadSource m p a b | Monad m
-constShare a = ReadSource \_->pure a
-
-nullShare :: WriteSource m p a b | Monad m
-nullShare = WriteSource \_ _->pure ()
-
-instance read ReadSource where read (ReadSource read) p = Read <$> read p
-instance write WriteSource where write (WriteSource write) p w = Written <$> write p w
-
-timeStamp :: ReadSource IO () Timestamp ()
-timeStamp = ReadSource \_->withWorld time
-
-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 (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 (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
- 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
- write (Par t=:{param,writel,writer,left,right}) p w
- = read left p1 >>= \v->case v of
- Reading s = pure $ Writing $ Par {t & left=RWPair s left}
- Read r1 = write` left p1 (writel p w r1) >>= \v->case v of
- Writing s = pure $ Writing $ Par {t & left=RWPair (constShare r1) left}
- Written () = read right p2 >>= \v->case v of
- Reading s = pure $ Writing $ Par {t & left=RWPair (constShare r1) nullShare, right=RWPair s right}
- Read r2 = write` right p2 (writer p w r2) >>= \v->case v of
- Writing s = pure $ Writing $ Par {t & left=RWPair (constShare r1) nullShare, right=RWPair (constShare r2) right}
- Written () = pure $ Written ()
- where (p1, p2) = param p
-
-write` :: (sds m p r w) p (m (Maybe w)) -> m (WriteResult m p r w) | TC w & Monad m & write sds
-write` sds p mmv = mmv >>= \mv->case mv of
- Nothing = pure $ Written ()
- Just v = write sds p v
-
-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 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 ()
-
-instance write (Lens sds) | read sds & write sds
-where
- 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
-
-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 \_ r->case r of
- (r :: r^) = pure r
- _ = fail "type mismatch")
- (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
- (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 (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 (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 (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 (LensRead read) (LensWrite write) sds
-where
- param (p, _) = p
- read (_, k) r = maybe (fail "key not present") pure $ 'Data.Map'.get k r
- write (_, k) w r = pure $ Just $ 'Data.Map'.put k w r
-
-//select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad 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
-select parami params index source = Select {parami=parami,params=params,index=index,source=source,unused=undef}
-
-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 ()
-
-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
-
-//Start :: Either String (Map String Dynamic)
-Start :: Either String ((), Map String Dynamic)
-Start = runStateT t $ 'Data.Map'.singleton "blurp" (dynamic 38)
-where
- t = setShare (42, "blurp") (focus "foo" astore >+< focus "bar" astore)
-// t = write 42 (astore "blurp")
-// >>| read (astore "blurp")
-// t = setShare 42 (focus "blurp" astore)
-// >>| getShare (focus "blurp" astore)
-
-//Start world = evalIO t world
-//where
-// t = getShare (focus "auds.icl" file)
-
-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
-
-file :: Source IO FilePath String String
-file = source readFileM writeFileM
from Data.Either import :: Either
from Data.Functor import class Functor
from Data.Map import :: Map
-from StdMaybe import :: Maybe
from StdOverloaded import class <, class fromString
from System.FilePath import :: FilePath
from System.IO import :: IO
from System.Time import :: Timestamp
class MonadFail m | Monad m where fail :: String -> m a
-instance MonadFail Maybe, []
+instance MonadFail ?, []
instance MonadFail (Either a) | fromString a
instance MonadFail (StateT s m) | MonadFail m
instance write (Lens sds) | read sds & write sds
instance write (Select sdsl sdsr) | read sdsl & write sdsr
-//* Just read something
+//* ?Just read something
:: ReadSource m r w = ReadSource (m r)
-//* Just write something
+//* ?Just write something
:: WriteSource m r w = WriteSource (w -> m ())
//* Pair a two shares to form a read/write sds that only touches one share per action
:: RWPair sdsr sdsw m r w = RWPair (sdsr m r w) (sdsw m r w) | RWPairUnused (m ())
//* Apply a lens to a share
:: Lens sds m r w = E.r1 w1: Lens (LensOpts sds m r1 w1 r w) & TC r1 & TC w1
-lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+lens :: (r1 -> m r) (w r1 -> m (? w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
:: LensOpts sds m r1 w1 r w =
{ mapr :: r1 -> m r
- , mapw :: w r1 -> m (Maybe w1)
+ , mapw :: w r1 -> m (? w1)
, lens :: sds m r1 w1
}
(>?@) :== mapRead
//* Map a function to the value written.
-mapWrite :: (w` r -> m (Maybe w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+mapWrite :: (w` r -> m (? w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
(>!@) infixl 6
(>!@) :== mapWrite
import System.IO
import System.Time
-instance MonadFail Maybe where fail _ = Nothing
+instance MonadFail ? where fail _ = ?None
instance MonadFail [] where fail _ = []
instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=nullShare, right=s}
Writing s = pure $ Writing $ Par {t & writel= \_->pure (w1, w2), left=s}
-lens :: (r1 -> m r) (w r1 -> m (Maybe w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
+lens :: (r1 -> m r) (w r1 -> m (? w1)) (sds m r1 w1) -> Lens sds m r w | TC r1 & TC w1
lens mapr mapw lens = Lens {mapr=mapr,mapw=mapw,lens=lens}
instance read (Lens sds) | read sds
where
write (Lens t=:{mapw,lens}) w = read lens >>= \v->case v of
Read r = mapw w r >>= \w->case w of
- Nothing = pure $ Written ()
- Just w = write lens w >>= \v->case v of
+ ?None = pure $ Written ()
+ ?Just w = write lens w >>= \v->case v of
Written _ = pure $ Written ()
- Writing s = pure $ Writing $ Lens {t & mapw= \_ _->pure $ Just w, lens=RWPair (constShare r) s}
+ Writing s = pure $ Writing $ Lens {t & mapw= \_ _->pure $ ?Just w, lens=RWPair (constShare r) s}
Reading s = pure $ Writing $ Lens {t & lens=RWPair s lens}
mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Monad m
-mapRead f sds = lens f (\_ _->pure Nothing) sds
+mapRead f sds = lens f (\_ _->pure ?None) sds
fromDynStore :: (sds m Dynamic Dynamic) -> Lens sds m r w | TC r & TC w & MonadFail m
fromDynStore sds = lens
(\r->case r of
(r :: r^) = pure r
_ = fail "type mismatch")
- (\w _->pure $ Just (dynamic w))
+ (\w _->pure $ ?Just (dynamic w))
sds
toDynStore :: (sds m r w) -> Lens sds m Dynamic Dynamic | TC r & TC w & MonadFail m
toDynStore sds = lens
(\r->pure (dynamic r))
(\w _->case w of
- (w :: w^) = pure $ Just w
+ (w :: w^) = pure $ ?Just w
_ = fail "type mismatch")
sds
-mapWrite :: (w` r -> m (Maybe w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
+mapWrite :: (w` r -> m (? w)) (sds m r w) -> Lens sds m r w` | TC r & TC w & TC w` & Monad m
mapWrite f sds = lens pure f sds
indexedStore :: Int (sds m [a] [a]) -> Lens sds m a a | TC a & MonadFail m
indexedStore idx sds = lens
(\r->maybe (fail "out of range") pure (r !? idx))
- (\w->pure o Just o updateAt idx w)
+ (\w->pure o ?Just o updateAt idx w)
sds
keyedStore :: k (sds m (Map k v) (Map k v)) -> Lens sds m v v | TC v & TC k & < k & MonadFail m
keyedStore key sds = lens
(maybe (fail "key not present") pure o 'Data.Map'.get key)
- (\w->pure o Just o 'Data.Map'.put key w)
+ (\w->pure o ?Just o 'Data.Map'.put key w)
sds
select :: (sdsl m r1 w1) (r1 -> m (sdsr m r w)) -> Select sdsl sdsr m r w | TC r1 & TC w1 & Monad m
--- /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 (42, 'a') $ focus "foo" astore >+< focus "bar" astore]
+ ]
+
+ sh :: Lens (Lens (Lens (Lens (RWPair ReadSource WriteSource)))) (StateT (Map String Dynamic) m) () a a | MonadFail m & TC a
+ sh = focus "foo" astore
+
+
+// t = setShare (42, "blurp") (focus "foo" astore >+< focus "bar" astore)
+// t = write 42 (astore "blurp")
+// >>| read (astore "blurp")
+// t = setShare 42 (focus "blurp" astore)
+// >>| getShare (focus "blurp" astore)
+
+//Start world = evalIO t world
+//where
+// t = getShare (focus "auds.icl" file)
+
+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
from Data.Either import :: Either
from Data.Functor import class Functor
from Data.Map import :: Map
-from StdMaybe import :: Maybe
from StdOverloaded import class <, class fromString
from System.FilePath import :: FilePath
from System.IO import :: IO
from System.Time import :: Timestamp
class MonadFail m | Monad m where fail :: String -> m a
-instance MonadFail Maybe, []
+instance MonadFail ?, []
instance MonadFail (Either a) | fromString a
instance MonadFail (StateT s m) | MonadFail m
import System.IO
import System.Time
-instance MonadFail Maybe where fail _ = Nothing
+instance MonadFail ? where fail _ = ?None
instance MonadFail [] where fail _ = []
instance MonadFail (Either a) | fromString a where fail s = Left $ fromString s
instance MonadFail (StateT s m) | MonadFail m where fail s = liftT $ fail s
repositories / clean-tests.git / commitdiff