From ace8aee5a2518e3802cac38436505ccf80b0824f Mon Sep 17 00:00:00 2001
From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 20 Aug 2020 10:50:55 +0200
Subject: [PATCH] updates, hierarchical

---
 gengen/Data/GenType.dcl       |   1 -
 gengen/Data/GenType.icl       |   6 +-
 gengen/Data/GenType/CType.icl |   4 +-
 gengen/gengen.hs              |  12 --
 gengen/test.hs                |  10 --
 gengen/test.icl               |  86 +-------------
 prj/test.icl                  |   5 -
 test.icl                      |   4 +-
 uds/ASDS.dcl                  |  53 +++++++++
 uds/ASDS.icl                  |  28 +++++
 uds/ASDS/Lens.dcl             |  55 +++++++++
 uds/ASDS/Lens.icl             |  88 ++++++++++++++
 uds/ASDS/Parallel.dcl         |  27 +++++
 uds/ASDS/Parallel.icl         |  57 +++++++++
 uds/ASDS/Select.dcl           |  24 ++++
 uds/ASDS/Select.icl           |  28 +++++
 uds/ASDS/Source.dcl           |  29 +++++
 uds/ASDS/Source.icl           |  38 ++++++
 uds/asds.dcl                  | 146 -----------------------
 uds/asds.icl                  | 216 ----------------------------------
 uds/auds.dcl                  |  13 +-
 uds/auds.icl                  |  22 ++--
 uds/test.icl                  |  62 ++++++++++
 uds/uds.dcl                   |   3 +-
 uds/uds.icl                   |   2 +-
 25 files changed, 522 insertions(+), 497 deletions(-)
 delete mode 100644 gengen/gengen.hs
 delete mode 100644 gengen/test.hs
 delete mode 100644 prj/test.icl
 create mode 100644 uds/ASDS.dcl
 create mode 100644 uds/ASDS.icl
 create mode 100644 uds/ASDS/Lens.dcl
 create mode 100644 uds/ASDS/Lens.icl
 create mode 100644 uds/ASDS/Parallel.dcl
 create mode 100644 uds/ASDS/Parallel.icl
 create mode 100644 uds/ASDS/Select.dcl
 create mode 100644 uds/ASDS/Select.icl
 create mode 100644 uds/ASDS/Source.dcl
 create mode 100644 uds/ASDS/Source.icl
 delete mode 100644 uds/asds.dcl
 delete mode 100644 uds/asds.icl
 create mode 100644 uds/test.icl

diff --git a/gengen/Data/GenType.dcl b/gengen/Data/GenType.dcl
index aeaf7da..2230df7 100644
--- a/gengen/Data/GenType.dcl
+++ b/gengen/Data/GenType.dcl
@@ -1,7 +1,6 @@
 definition module Data.GenType
 
 import StdGeneric
-from StdMaybe import :: Maybe
 
 :: Box b a =: Box b
 derive bimap Box
diff --git a/gengen/Data/GenType.icl b/gengen/Data/GenType.icl
index aeaf5aa..3cdb60d 100644
--- a/gengen/Data/GenType.icl
+++ b/gengen/Data/GenType.icl
@@ -1,6 +1,6 @@
 implementation module Data.GenType
 
-import StdEnv, StdGeneric, StdMaybe
+import StdEnv, StdGeneric
 import Control.Applicative
 
 import Control.Monad => qualified join
@@ -334,6 +334,8 @@ predef =:
 	, ("_!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]]]
@@ -360,6 +362,6 @@ gType{|{}|} a = box $ GTyArray ALazy $ unBox a
 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 (), (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)
diff --git a/gengen/Data/GenType/CType.icl b/gengen/Data/GenType/CType.icl
index 538ce9a..c5c58ce 100644
--- a/gengen/Data/GenType/CType.icl
+++ b/gengen/Data/GenType/CType.icl
@@ -5,12 +5,12 @@ import Control.Monad => qualified join
 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
@@ -30,7 +30,7 @@ where
 		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
diff --git a/gengen/gengen.hs b/gengen/gengen.hs
deleted file mode 100644
index 7b44a72..0000000
--- a/gengen/gengen.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# 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 ""
diff --git a/gengen/test.hs b/gengen/test.hs
deleted file mode 100644
index 72985ff..0000000
--- a/gengen/test.hs
+++ /dev/null
@@ -1,10 +0,0 @@
-{-# 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 ""
diff --git a/gengen/test.icl b/gengen/test.icl
index 18fde1d..242ccbe 100644
--- a/gengen/test.icl
+++ b/gengen/test.icl
@@ -1,25 +1,25 @@
 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}}
@@ -58,82 +58,6 @@ Start =
 //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 []
diff --git a/prj/test.icl b/prj/test.icl
deleted file mode 100644
index bd20f3d..0000000
--- a/prj/test.icl
+++ /dev/null
@@ -1,5 +0,0 @@
-module test
-
-import iTasks
-
-Start w = doTasks (return ()) w
diff --git a/test.icl b/test.icl
index 21d4a89..367eccd 100644
--- a/test.icl
+++ b/test.icl
@@ -1,3 +1,5 @@
 module test
-class C m :: u:m -> v:m
 
+import Data.Maybe
+
+Start = isJust (?Just 42)
diff --git a/uds/ASDS.dcl b/uds/ASDS.dcl
new file mode 100644
index 0000000..4a5f0ba
--- /dev/null
+++ b/uds/ASDS.dcl
@@ -0,0 +1,53 @@
+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
diff --git a/uds/ASDS.icl b/uds/ASDS.icl
new file mode 100644
index 0000000..f8413c3
--- /dev/null
+++ b/uds/ASDS.icl
@@ -0,0 +1,28 @@
+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
diff --git a/uds/ASDS/Lens.dcl b/uds/ASDS/Lens.dcl
new file mode 100644
index 0000000..3a66a34
--- /dev/null
+++ b/uds/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/ASDS/Lens.icl b/uds/ASDS/Lens.icl
new file mode 100644
index 0000000..351e759
--- /dev/null
+++ b/uds/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/ASDS/Parallel.dcl b/uds/ASDS/Parallel.dcl
new file mode 100644
index 0000000..91d61c1
--- /dev/null
+++ b/uds/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/ASDS/Parallel.icl b/uds/ASDS/Parallel.icl
new file mode 100644
index 0000000..735c8ba
--- /dev/null
+++ b/uds/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/ASDS/Select.dcl b/uds/ASDS/Select.dcl
new file mode 100644
index 0000000..bf5bc88
--- /dev/null
+++ b/uds/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/ASDS/Select.icl b/uds/ASDS/Select.icl
new file mode 100644
index 0000000..14de73b
--- /dev/null
+++ b/uds/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/ASDS/Source.dcl b/uds/ASDS/Source.dcl
new file mode 100644
index 0000000..ab3446b
--- /dev/null
+++ b/uds/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/ASDS/Source.icl b/uds/ASDS/Source.icl
new file mode 100644
index 0000000..5ffb97f
--- /dev/null
+++ b/uds/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/asds.dcl b/uds/asds.dcl
deleted file mode 100644
index 027d9b8..0000000
--- a/uds/asds.dcl
+++ /dev/null
@@ -1,146 +0,0 @@
-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
diff --git a/uds/asds.icl b/uds/asds.icl
deleted file mode 100644
index eefe267..0000000
--- a/uds/asds.icl
+++ /dev/null
@@ -1,216 +0,0 @@
-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
diff --git a/uds/auds.dcl b/uds/auds.dcl
index 176d1e6..0476022 100644
--- a/uds/auds.dcl
+++ b/uds/auds.dcl
@@ -6,14 +6,13 @@ 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 ?, []
 instance MonadFail (Either a) | fromString a
 instance MonadFail (StateT s m) | MonadFail m
 
@@ -49,9 +48,9 @@ instance write (Par sdsl 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
+//* ?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 ())
@@ -72,10 +71,10 @@ par :: (r1 r2 -> m r) (w -> m (w1, w2)) (sdsl m r1 w1) (sdsr m r2 w2) -> Par sds
 
 //* 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
 	}
 
@@ -101,7 +100,7 @@ mapRead :: (r -> m r`) (sds m r w) -> Lens sds m r` w | TC r` & TC r & TC w & Mo
 (>?@) :== 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
 
diff --git a/uds/auds.icl b/uds/auds.icl
index adb7c32..a7c37ed 100644
--- a/uds/auds.icl
+++ b/uds/auds.icl
@@ -18,7 +18,7 @@ import System.FilePath
 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
@@ -65,7 +65,7 @@ where
 				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
@@ -89,44 +89,44 @@ instance write (Lens sds) | read sds & write 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
diff --git a/uds/test.icl b/uds/test.icl
new file mode 100644
index 0000000..76a5a53
--- /dev/null
+++ b/uds/test.icl
@@ -0,0 +1,62 @@
+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
diff --git a/uds/uds.dcl b/uds/uds.dcl
index 8c3e495..6f3abd4 100644
--- a/uds/uds.dcl
+++ b/uds/uds.dcl
@@ -6,14 +6,13 @@ 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 ?, []
 instance MonadFail (Either a) | fromString a
 instance MonadFail (StateT s m) | MonadFail m
 
diff --git a/uds/uds.icl b/uds/uds.icl
index 57be2eb..cb12a39 100644
--- a/uds/uds.icl
+++ b/uds/uds.icl
@@ -17,7 +17,7 @@ import System.FilePath
 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
-- 
2.20.1