From: Mart Lubbers <mart@martlubbers.net>
Date: Thu, 20 Aug 2020 13:08:29 +0000 (+0200)
Subject: cleanup gentype
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ca0986f81a4cc7ca9e9f9069fd499ad4b89a31e8;p=clean-tests.git

cleanup gentype
---

diff --git a/gengen/Data/GenType.icl b/gengen/Data/GenType.icl
index 3cdb60d..951b3f4 100644
--- a/gengen/Data/GenType.icl
+++ b/gengen/Data/GenType.icl
@@ -334,8 +334,8 @@ predef =:
 	, ("_!List!", "[!!]"), ("_!Cons!", "(:)"), ("_!Nil!", "[ !]")
 	, ("_#List", "[#]"), ("_#Cons", "(:)"), ("_#Nil", "[#]")
 	, ("_#List!", "[#!]"), ("_#Cons!", "(:)"), ("_#Nil!", "[#!]")
-	, ("_!Maybe", "?"), ("_!Just", "?Just"), ("_!None", "?None")
-	, ("_Maybe", "?^"), ("_Just", "?^Just"), ("_None", "?^None")
+	, ("_!Maybe", "?"), ("_!Just", "?Just"), ("_!Nothing", "?None")
+	, ("_Maybe", "?^"), ("_Just", "?^Just"), ("_Nothing", "?^None")
 	, ("_Array", "{}"), ("_!Array", "{!}"), ("_#Array", "{#}"), ("_32#Array", "{32#}")
 	, ("_Unit", "()")
 	:[("_Tuple" +++ toString i, "(" +++ createArray i ',' +++")")\\i<-[2..32]]]
diff --git a/gengen/Data/GenType/CType.icl b/gengen/Data/GenType/CType.icl
index c5c58ce..ec0d5fb 100644
--- a/gengen/Data/GenType/CType.icl
+++ b/gengen/Data/GenType/CType.icl
@@ -4,188 +4,183 @@ import Control.Applicative
 import Control.Monad => qualified join
 import Control.Monad.State
 import Control.Monad.Trans
+import Control.Monad.Writer
+import Control.Monad.Fail
 import Data.Either
 import Data.Func
 import Data.Functor
 import Data.Tuple
 import qualified Data.Map
-from Data.Map import :: Map(..), putList, alter, get, union, fromList
+from Data.Map import :: Map(..)
 import Data.Maybe
+import Data.List
 import StdEnv
 import Data.GenType
 import Text
 
-flatTypedef :: Type -> Either String [String]
-flatTypedef t = case ftd t 0 [] of
-	[] = Left ("Unable to flatTypedef: " +++ toString t)
-	c = Right c
+instance MonadFail (Either String) where fail s = Left s
+
+safe :: String -> String
+safe s = concat [fromMaybe {c} $ lookup c cs\\c <-:s]
 where
-	indent i c = [createArray i '\t':c]
+	cs = [('~', "Tld"), ('@', "At"), ('#', "Hsh"), ('$', "Dlr"), ('%', "Prc")
+		,('^', "Hat"), ('?', "Qtn"), ('!', "Bng"), (':', "Cln"), ('+', "Pls")
+		,('-', "Min"), ('*', "Ast"), ('<', "Les"), ('>', "Gre"), ('\\', "Bsl")
+		,('/', "Slh"), ('|', "Pip"), ('&', "Amp"), ('=', "Eq"), ('.', "Dot")]
 
-	ftd :: Type Int [String] -> [String]
-	ftd (TyRef s) i c = indent i [s:c]
-	ftd (TyBasic t) i c = case t of
-		BTInt  = indent i ["int64_t":c]
-		BTChar = indent i ["char":c]
-		BTReal = indent i ["double":c]
-		BTBool = indent i ["bool":c]
-		t = []
+:: FTMonad :== WriterT [String] (StateT [(String, [String])] (Either String)) ()
+flatTypedef :: Type -> Either String [String]
+flatTypedef t = (\(w, es)->flatten (map snd es) ++ w)
+	<$> runStateT (execWriterT (ftd t True 0)) []
+where
+	indent :: Int [String] -> FTMonad
+	indent i c = tell [createArray i '\t':c]
+
+	ftd :: Type Bool Int -> FTMonad
+	ftd (TyRef s) tl i = indent i [s]
+	ftd (TyBasic t) tl i 
+		| tl = tell []
+		 = case t of
+			BTInt  = indent i ["int64_t"]
+			BTChar = indent i ["char"]
+			BTReal = indent i ["double"]
+			BTBool = indent i ["bool"]
+			t = fail $ "cannot flatTypedef: " +++ toString t
 //	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
-		= indent i ["struct ", safe ti.grd_name, " {\n"
-		: foldr (fmtField $ i+1) (indent i ["}\n":c])
-			[(fi.gfd_name, ty)\\(fi, ty)<-fs]
-		]
+	ftd (TyNewType ti ci a) tl i = ftd a tl i
+	ftd (TyArray _ a) tl i = indent i ["*"] >>| ftd a tl i
+	ftd (TyRecord ti fs) tl i
+		= indent i ["struct ", if tl (safe ti.grd_name) "", " {\n"
+		] >>| mapM_ (fmtField $ i+1) [(fi.gfd_name, ty)\\(fi, ty)<-fs]
+		>>| indent i ["}\n"]
 	//Enumeration
-	ftd (TyObject ti fs) i c
+	ftd (TyObject ti fs) tl i
 		| and [t =: [] \\ (_, t)<-fs]
-			= indent i ["enum ", safe ti.gtd_name, " {"
-				, join ", " [safe ci.gcd_name\\(ci, _)<-fs], "}":c]
+			| tl = tell []
+			= indent i [] >>| enum ti fs
 	//Single constructor, single field (box)
-	ftd (TyObject ti [(ci, [ty])]) i c = ftd ty i c
+	ftd (TyObject ti [(ci, [ty])]) tl i = ftd ty tl i
 	//Single constructor
-	ftd (TyObject ti [(ci, ts)]) i c
-		= indent i ["struct ", safe ti.gtd_name, " {\n"
-		: flip (foldr (fmtField $ i+1)) [("f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
-		$ indent i ["}":c]]
+	ftd (TyObject ti [(ci, ts)]) tl i
+		=   indent i ["struct ", if tl (safe ti.gtd_name) "", " {\n"]
+		>>| mapM_ (fmtField $ i+1) [("f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
+		>>| indent i ["}"]
 	//Complex adt
-	ftd (TyObject ti fs) i c
-		= indent i ["struct ", safe ti.gtd_name, " {\n"
-		: indent (i+1) ["enum {", join ", " [safe ci.gcd_name\\(ci, _)<-fs], "} cons;\n"
-		: indent (i+1) ["struct {\n"
-		: flip (foldr (fmtCons $ i + 2)) fs
-		$ indent (i+1) ["} data;\n"
-		: indent i ["}":c]
-		]]]]
+	ftd (TyObject ti fs) tl i
+		=   indent i ["struct ", if tl (safe ti.gtd_name) "", " {\n"]
+		>>| indent (i+1) [] >>| enum ti fs >>| tell [" cons;\n"]
+		>>| indent (i+1) ["struct {\n"]
+		>>| mapM_ (fmtCons $ i+2) fs
+		>>| indent (i+1) ["} data;\n"]
+		>>| indent i ["}", if tl ";" ""]
 	where
-		fmtCons i (ci, []) c = c
-		fmtCons i (ci, [t]) c = ftd t i [" ", safe ci.gcd_name, ";\n":c]
-		fmtCons i (ci, ts) c
-			= indent i ["struct {\n"
-			: flip (foldr (fmtField (i+1))) [("f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
-			$ indent i ["} ", safe ci.gcd_name, ";\n":c]
-			]
-	ftd t i c = []
-
-	fmtField i (name, ty) c = ftd ty i [" ", name, ";\n":c]
-
-typedefs :: [[Type]] -> Either String [String]
-typedefs ts = flatten <$> evalStateT (mapM typedefgroup ts) 'Data.Map'.newMap
+		fmtCons i (ci, []) = pure ()
+		fmtCons i (ci, [t]) = ftd t False i >>| tell [" ", safe ci.gcd_name, ";\n"]
+		fmtCons i (ci, ts)
+			=   indent i ["struct {\n"]
+			>>| mapM_ (fmtField $ i+1) [("f" +++ toString i, ty)\\i<-[0..] & ty<-ts]
+			>>| indent i ["} ", safe ci.gcd_name, ";\n"]
+	ftd t tl i = fail $ "cannot flatTypedef: " +++ toString t
+
+	
+	enum :: GenericTypeDefDescriptor [(GenericConsDescriptor, [Type])] -> FTMonad
+	enum ti fs = liftT (gets (lookup ti.gtd_name)) >>= \e->case e of
+		?None = liftT (modify \s->[(ti.gtd_name, ["enum ", safe ti.gtd_name, "_cons {", join ", " [safe ci.gcd_name\\(ci, _)<-fs], "};\n"]):s]) >>| enum ti fs
+		?Just _ = tell ["enum ", safe ti.gtd_name, "_cons"]
+
+	fmtField :: Int (String, Type) -> FTMonad
+	fmtField i (name, ty) = ftd ty False i >>| tell [" ", name, ";\n"]
 
 :: TDMonad :== StateT TDState (Either String) [String]
 :: TDState :== 'Data.Map'.Map String (String, Bool)
-
-typedefgroup :: [Type] -> TDMonad
-typedefgroup ts
-	=   flatten
-	<$  modify (putList [(typeName ty, (prefix ty, True))\\ty<-ts])
-	<*> mapM (\t->typedef t >>= post ["\n"]) ts
-	<*  modify (flip (foldr $ alter (fmap (fmap \_->False)) o typeName) ts)
-	>>= \c->case ts of
-		[_] = pure c
-		ts = mapM (\x->printTypeName x >>= post [";\n"]) (map typeName ts)
-			>>= post c o flatten
-where
-	prefix :: Type -> String
-	prefix (TyRecord _ _) = "struct "
-	prefix (TyObject _ fs)
-		| and [t =: [] \\ (_, t)<-fs] = "enum "
-		| fs =: [(_, [_])] = ""
-		| fs =: [_] = "struct "
-		= "struct "
-	prefix  _ = ""
-
-printTypeName :: String -> TDMonad
-printTypeName tname
-	= gets $ maybe [safe tname, " "] (\(p, b)->[p, safe tname, if b " *" " "]) o get tname
-
-safe s = concat [sf c\\c <-:s]
+typedefs :: [[Type]] -> Either String [String]
+typedefs ts = flatten <$> evalStateT (mapM typedefgroup ts) 'Data.Map'.newMap
 where
-	sf '~' = "Tld"
-	sf '@' = "At"
-	sf '#' = "Hsh"
-	sf '$' = "Dlr"
-	sf '%' = "Prc"
-	sf '^' = "Hat"
-	sf '?' = "Qtn"
-	sf '!' = "Bng"
-	sf ':' = "Cln"
-	sf '+' = "Pls"
-	sf '-' = "Min"
-	sf '*' = "Ast"
-	sf '<' = "Les"
-	sf '>' = "Gre"
-	sf '\\' = "Bsl"
-	sf '/' = "Slh"
-	sf '|' = "Pip"
-	sf '&' = "Amp"
-	sf '=' = "Eq"
-	sf '.' = "Dot"
-	sf c = toString c
-
-pre :: [String] (m [String]) -> m [String] | Monad m
-pre t s = ((++)t) <$> s
-
-post :: [String] [String] -> m [String] | pure m
-post t s = pure (s ++ t)
-
-header t c = pre ["// ", toString (replaceBuiltins t), "\n":c]
-
-typedef :: Type -> TDMonad
-typedef (TyRef s) = printTypeName s
-typedef (TyBasic t) = case t of
-	BTInt = printTypeName "int64_t"
-	BTChar = printTypeName "char"
-	BTReal = printTypeName "double"
-	BTBool = printTypeName "bool"
-	t = pure []//liftT $ Left $ "basic type: " +++ toString t +++ " not implemented"
-typedef (TyArray _ a) = pre ["*"] $ typedef a
-typedef t=:(TyNewType ti ci a)
-	= header t [] $ tydef ti.gtd_name ci.gcd_type
-typedef t=:(TyRecord ti fs) = header t ["struct ", safe ti.grd_name, " {\n"]
-	$ fmtFields 1 ti.grd_type [fi.gfd_name\\(fi, _)<-fs] >>= post ["};\n"]
-//Enumeration
-typedef t=:(TyObject ti fs)
-	| and [t =: [] \\ (_, t)<-fs] = header t
-		["enum ", safe ti.gtd_name, " {"
-			, join ", " [safe ci.gcd_name\\(ci, _)<-fs], "};\n"] $ pure []
-//Single constructor, single field (box)
-typedef t=:(TyObject ti [(ci, [ty])]) = header t [] $ tydef ti.gtd_name ci.gcd_type
-//Single constructor
-typedef t=:(TyObject ti [(ci, ts)]) = header t ["struct ", safe ti.gtd_name, " {\n"]
-	$ fmtFields 1 ci.gcd_type ["f" +++ toString i\\i<-indexList ts] >>= post ["};\n"]
-//Complex adt
-typedef t=:(TyObject ti fs) = header t
-	["struct ", safe ti.gtd_name, " {\n"
+	typedefgroup :: [Type] -> TDMonad
+	typedefgroup ts
+		=   flatten
+		<$  modify ('Data.Map'.putList [(typeName ty, (prefix ty, True))\\ty<-ts])
+		<*> mapM (\t->typedef t >>= post ["\n"]) ts
+		<*  modify (flip (foldr $ 'Data.Map'.alter (fmap (fmap \_->False)) o typeName) ts)
+		>>= \c->case ts of
+			[_] = pure c
+			ts = mapM (\x->printTypeName x >>= post [";\n"]) (map typeName ts)
+				>>= post c o flatten
+	where
+		prefix :: Type -> String
+		prefix (TyRecord _ _) = "struct "
+		prefix (TyObject _ fs)
+			| and [t =: [] \\ (_, t)<-fs] = "enum "
+			| fs =: [(_, [_])] = ""
+			| fs =: [_] = "struct "
+			= "struct "
+		prefix  _ = ""
+
+	printTypeName :: String -> TDMonad
+	printTypeName tname
+		= gets $ maybe [safe tname, " "] (\(p, b)->[p, safe tname, if b " *" " "]) o 'Data.Map'.get tname
+
+	pre :: [String] (m [String]) -> m [String] | Monad m
+	pre t s = ((++)t) <$> s
+	
+	post :: [String] [String] -> m [String] | pure m
+	post t s = pure (s ++ t)
+	
+	header t c = pre ["// ", toString (replaceBuiltins t), "\n":c]
+	
+	typedef :: Type -> TDMonad
+	typedef (TyRef s) = printTypeName s
+	typedef (TyBasic t) = case t of
+		BTInt = printTypeName "int64_t"
+		BTChar = printTypeName "char"
+		BTReal = printTypeName "double"
+		BTBool = printTypeName "bool"
+		t = pure []//liftT $ Left $ "basic type: " +++ toString t +++ " not implemented"
+	typedef (TyArray _ a) = pre ["*"] $ typedef a
+	typedef t=:(TyNewType ti ci a)
+		= header t [] $ tydef ti.gtd_name ci.gcd_type
+	typedef t=:(TyRecord ti fs) = header t ["struct ", safe ti.grd_name, " {\n"]
+		$ fmtFields 1 ti.grd_type [fi.gfd_name\\(fi, _)<-fs] >>= post ["};\n"]
+	//Enumeration
+	typedef t=:(TyObject ti fs)
+		| and [t =: [] \\ (_, t)<-fs] = header t
+			["enum ", safe ti.gtd_name, " {"
+				, join ", " [safe ci.gcd_name\\(ci, _)<-fs], "};\n"] $ pure []
+	//Single constructor, single field (box)
+	typedef t=:(TyObject ti [(ci, [ty])]) = header t [] $ tydef ti.gtd_name ci.gcd_type
+	//Single constructor
+	typedef t=:(TyObject ti [(ci, ts)]) = header t ["struct ", safe ti.gtd_name, " {\n"]
+		$ fmtFields 1 ci.gcd_type ["f" +++ toString i\\i<-indexList ts] >>= post ["};\n"]
+	//Complex adt
+	typedef t=:(TyObject ti fs) = header t
+		["struct ", safe ti.gtd_name, " {\n"
 		, "\tenum {", join ", " [safe ci.gcd_name\\(ci, _)<-fs], "} cons;\n"
 		, "\tstruct {\n"]
-	$ mapM fmtCons fs
-	>>= post ["\t} data;\n};\n"] o flatten
-where
-	fmtCons :: (GenericConsDescriptor, [Type]) -> TDMonad
-	fmtCons (ci, []) = pure []
-	fmtCons (ci, [t]) = fmtFields 2 ci.gcd_type [safe ci.gcd_name]
-	fmtCons (ci, ts) = pre ["\t\tstruct {\n"]
-		$ fmtFields 3 ci.gcd_type ["f" +++ toString i\\i<-indexList ts]
-		>>= post ["\t\t} ", safe ci.gcd_name, ";\n"]
-typedef t = liftT $ Left $ toString t +++ " not implemented"
-
-tydef :: String GenType -> TDMonad
-tydef name (GenTypeArrow l r) = pre ["typedef "] $ fmtField "" l >>= post [safe name,";\n"]
-
-fmtFields :: Int GenType [String] -> TDMonad
-fmtFields i _ [] = pure []
-fmtFields i (GenTypeArrow l r) [x:xs] = pre [createArray i '\t'] $ fmtField x l >>= \c->pre (c ++ [";\n"]) $ fmtFields i r xs
-
-fmtField :: String GenType -> TDMonad
-fmtField x (GenTypeCons a) = printTypeName a >>= post [x]
-fmtField x (GenTypeVar a) = pure ["void *",x]
-fmtField x (GenTypeApp l r) = fmtField x l
-fmtField x t=:(GenTypeArrow _ r)
-	= map concat <$> mapM (fmtField "") (collectArgs t [])
-		>>= \[r:as]->pure [r, " (*",x,")(",join ", " as, ")"]
-where
-	collectArgs (GenTypeArrow l r) c = collectArgs r (c ++ [l])
-	collectArgs t c = [t:c]
+		$ mapM fmtCons fs
+		>>= post ["\t} data;\n};\n"] o flatten
+	where
+		fmtCons :: (GenericConsDescriptor, [Type]) -> TDMonad
+		fmtCons (ci, []) = pure []
+		fmtCons (ci, [t]) = fmtFields 2 ci.gcd_type [safe ci.gcd_name]
+		fmtCons (ci, ts) = pre ["\t\tstruct {\n"]
+			$ fmtFields 3 ci.gcd_type ["f" +++ toString i\\i<-indexList ts]
+			>>= post ["\t\t} ", safe ci.gcd_name, ";\n"]
+	typedef t = liftT $ Left $ toString t +++ " not implemented"
+	
+	tydef :: String GenType -> TDMonad
+	tydef name (GenTypeArrow l r) = pre ["typedef "] $ fmtField "" l >>= post [safe name,";\n"]
+	
+	fmtFields :: Int GenType [String] -> TDMonad
+	fmtFields i _ [] = pure []
+	fmtFields i (GenTypeArrow l r) [x:xs] = pre [createArray i '\t'] $ fmtField x l >>= \c->pre (c ++ [";\n"]) $ fmtFields i r xs
+	
+	fmtField :: String GenType -> TDMonad
+	fmtField x (GenTypeCons a) = printTypeName a >>= post [x]
+	fmtField x (GenTypeVar a) = pure ["void *",x]
+	fmtField x (GenTypeApp l r) = fmtField x l
+	fmtField x t=:(GenTypeArrow _ r)
+		= map concat <$> mapM (fmtField "") (collectArgs t [])
+			>>= \[r:as]->pure [r, " (*",x,")(",join ", " as, ")"]
+	where
+		collectArgs (GenTypeArrow l r) c = collectArgs r (c ++ [l])
+		collectArgs t c = [t:c]
diff --git a/gengen/test.icl b/gengen/test.icl
index 242ccbe..12169c2 100644
--- a/gengen/test.icl
+++ b/gengen/test.icl
@@ -45,6 +45,7 @@ Start =
 	( flatTypedef $ gTypeToType $ unBox t
 	, typedefs $ map (map gTypeToType) $ map (filter (not o isBasic)) $ flattenGType $ unBox t
 	)
+
 //Start = typedefs //$ (\x->[[gTypeToType x]])
 //	$ map (/*filter (not o isBuiltin) o*/ catMaybes o map gTypeToType)
 //	$ (\x->[[x]])
@@ -58,6 +59,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)))
+t :: Box GType (?(?(?(?^Enum))))
 //t :: Box GType (Odd Int, (), [Either (R (T *World)) (Frac Real)], Tr Either Bool, Fix Maybe)
 t = gType{|*|}
diff --git a/uds/test.icl b/uds/test.icl
index 76a5a53..0431427 100644
--- a/uds/test.icl
+++ b/uds/test.icl
@@ -35,22 +35,40 @@ where
 		, [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]
+		, [setShare [0..10] sh >>| setShare 4 (focus "idx" astore) >>| equal 4 (getShare $ focus ((), ()) $ selectList (focus "idx" astore) sh)]
+		, [setShare 38 sh >>| equal 38 (getShare (After 100 sh (pure ())))]
+		, [testpar (focus "foo" astore) (focus "bar" astore)]
+		, [testpar (after 100 $ focus "foo" astore) (after 100 $ focus "bar" astore)]
+		, [testpar (after 100 $ focus "foo" astore) (focus "bar" astore)]
+		, [testpar (focus "foo" astore) (after 100 $ focus "bar" astore)]
+//selectList :: (sdss m p1 Int w1) (sdsc m p2 [a] [a]) -> Select sdss (Lens sdsc) m (p1, p2) a a | TC p1 & TC p2 & TC a & TC w1 & MonadFail m
 		]
 
 	sh :: Lens (Lens (Lens (Lens (RWPair ReadSource WriteSource)))) (StateT (Map String Dynamic) m) () a a | MonadFail m & TC a
 	sh = focus "foo" astore
 
-	
-//	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)
+testpar :: (A.a: sds1 m () a a | TC, == a) (A.a: sds2 m () a a | TC, == a) -> m () | MonadFail m & read, write sds1 & read, write sds2
+testpar l r =
+	    setShare (42, 'a') (l >+< r)
+	>>| equal (42, 'a') (getShare $ l >+< r) >>| equal 42 (getShare l) >>| equal 'a' (getShare r)
+	>>| setShare 38 l
+	>>| equal (38, 'a') (getShare $ l >+< r) >>| equal 38 (getShare l) >>| equal 'a' (getShare r)
+	>>| setShare 'b' r
+	>>| equal (38, 'b') (getShare $ l >+< r) >>| equal 38 (getShare l) >>| equal 'b' (getShare r)
 
-//Start world = evalIO t world
-//where
-//	t = getShare (focus "auds.icl" file)
+:: After sds m p r w = After Int (sds m p r w) (m ())
+after :: Int (sds m p r w) -> After sds m p r w | pure m
+after i sds = After i sds $ pure ()
+
+instance read (After sds) | read sds
+where
+	read (After 0 sds _) p = read sds p
+	read (After n sds m) p = pure (Reading (After (n-1) sds m))
+
+instance write (After sds) | write sds
+where
+	write (After 0 sds _) p w = write sds p w
+	write (After n sds m) p w = pure (Writing (After (n-1) sds m))
 
 astore :: Lens (Lens (Lens (RWPair ReadSource WriteSource))) (StateT (Map String Dynamic) m) String a a | MonadFail m & TC a
 astore = fromDynStore dstore