From: Mart Lubbers <mart@martlubbers.net>
Date: Fri, 9 Oct 2020 12:26:39 +0000 (+0200)
Subject: tests
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=7675818dc8fc41eaf864dc89a8c2ce62c7dae93f;p=clean-tests.git

tests
---

diff --git a/fundeps/test.icl b/fundeps/test.icl
new file mode 100644
index 0000000..8d8fc11
--- /dev/null
+++ b/fundeps/test.icl
@@ -0,0 +1,118 @@
+module test
+
+import qualified StdEnv
+import StdEnv => qualified isEven, isOdd, class toInt(toInt), instance toInt Int
+
+:: Zero = Zero
+:: Succ a = Succ
+:: One :== Succ Zero
+One :: One
+One = undef
+:: Two :== Succ (Succ Zero)
+Two :: Two
+Two = undef
+:: Three :== Succ (Succ (Succ Zero))
+Three :: Three
+Three = undef
+:: True = Tr
+:: False = Fs
+
+class Even a ~c
+where
+	isEven :: a -> c
+	isEven _ = undef
+class Odd a ~c
+where
+	isOdd :: a -> c
+	isOdd _ = undef
+instance Even Zero True
+instance Odd Zero False
+instance Even (Succ a) b | Odd a b
+instance Odd (Succ a) b | Even a b
+
+dec :: (Succ a) -> a
+dec _ = undef
+
+class Add a b ~c
+where
+	(:+:) infixl 6  :: a b -> c
+	(:+:) _ _ = undef
+instance Add Zero b b
+instance Add (Succ a) b (Succ c) | Add a b c
+
+class Mult a b ~c
+where
+	(:*:) infixl 7 :: a b -> c
+	(:*:) _ _ = undef
+instance Mult Zero b Zero
+instance Mult (Succ a) b d | Mult a b c & Add b c d
+
+class Pow a b ~c
+where
+	(:^:) infixr 8 :: a b -> c
+	(:^:) _ _ = undef
+instance Pow a Zero One
+instance Pow a (Succ b) d | Pow a b c & Mult a c d
+
+instance +++ {!a}
+where
+	(+++) l r =
+		{  'StdEnv'._createArray (size l+size r)
+		&  [i]=l.[i], [size l+j]=r.[j]
+		\\ i<-[0..size l-1] & j <- [0..size r-1]
+		}
+
+:: Vec n a = Vec {!a}
+
+empty :: Vec Zero a
+empty = Vec {}
+
+single :: a -> Vec (Succ Zero) a
+single a = Vec {a}
+
+length :: (Vec n a) -> n
+length _ = undef
+
+nrepeat :: n a -> Vec n a | toInt n
+nrepeat _ a = repeat a
+
+repeat :: a -> Vec n a | toInt n
+repeat a = let r = Vec (createArray (toInt (length r)) a) in r
+
+append :: (Vec n a) (Vec m a) -> Vec x a | Add n m x
+append (Vec a) (Vec b) = Vec (a +++ b)
+
+class Le a b ~c
+where
+	le :: a b -> c
+	le _ _ = undef
+instance Le Zero b True
+instance Le (Succ a) Zero False
+instance Le (Succ a) (Succ b) c | Le a b c
+
+//Because toInt from StdEnv is strict in the first argument
+class toInt a :: a -> Int
+instance toInt Int where toInt i = i
+instance toInt Zero where toInt _ = 0
+instance toInt (Succ n) | toInt n where toInt a = inc (toInt (dec a))
+
+(!!) infixl 9 :: (Vec n a) i -> a | Le (Succ i) n True & toInt i
+(!!) (Vec a) i = a.[toInt i]
+
+(=.) infixl 9 :: (Vec n a) (i, a) -> Vec n a | Le (Succ i) n True & toInt i
+(=.) (Vec a) (i, x) = Vec {{e\\e<-:a} & [toInt i]=x}
+
+:: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
+:: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
+:: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
+:: Y = Y; :: Z = Z;
+:: Nul = Nul
+:: SC l r = SC
+
+Start = nrepeat (Three :*: Three) 'a'
+
+e1 :: Vec (Succ (Succ Zero)) Int
+e1 = append (single 1) (single 32)
+
+e2 :: Vec Three Int
+e2 = repeat 5
diff --git a/uds/ASDS.dcl b/uds/ASDS.dcl
index fd82537..a6cf0ea 100644
--- a/uds/ASDS.dcl
+++ b/uds/ASDS.dcl
@@ -12,28 +12,30 @@ import ASDS.Lens
 
 :: PViewT m a :== StateT [NRequest m] m a
 :: NRequest m = NRequest String (m ()) Dynamic
+//* @type :: String (m ()) p [NRequest] -> [NRequest] | TC p
+nrequestc p id hnd s :== [NRequest id hnd (dynamic p):s]
+
+//* Used to force kinds of variables in a
+:: KindHelper a b :== b
 
 //* Read a share with one rewrite step
 class read v :: (v m p r w) p -> PViewT m (ReadResult m p r w) | Monad m
 //* Write a share with one rewrite step
-class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | Monad m
+class write v :: (v m p r w) p w -> PViewT m (WriteResult m p r w) | Monad m & TC p
+//* Generate a unique name
+class identity v :: (v m p r w) (KindHelper (m ()) [String]) -> [String]
 //* Observe a share and get notified when it happens
-class observe v
-where
-	identity :: (v m p r w) [String] -> [String]
-	observe :: (v m p r w) p String (m ()) -> PViewT m () | Monad m & TC p
+class observe v :: (v m p r w) p String (m ()) -> PViewT m () | Monad m & TC p
 
 //* Result of a single read rewrite
 :: ReadResult m p r w
-	= Read r //* done reading
+	= Read (KindHelper (m ()) 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
+	= Written (KindHelper (m ()) ()) //* 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
@@ -46,11 +48,12 @@ where
 	| 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, write, observe sds
-sds :: (sds m p r w) -> SDS m p r w | read, write, observe sds & Monad m
+:: SDS m p r w = E.sds: SDS (KindHelper (m ()) (sds m p r w)) & read, write, identity, observe sds
+sds :: (sds m p r w) -> SDS m p r w | read, write, identity, observe sds & Monad m
 
 instance read SDS
 instance write SDS
+instance identity SDS
 instance observe SDS
 
 //* Read a share completely
@@ -61,3 +64,6 @@ setShare :: w (sds m () r w) -> PViewT m () | Monad m & write sds & TC r & TC w
 
 //* Update a share completely
 updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w
+
+//* Trigger observing tasks
+trigger :: (v m p r w) (p -> Bool) -> PViewT m () | identity v & TC p & Monad m
diff --git a/uds/ASDS.icl b/uds/ASDS.icl
index 4da3be4..77dd23f 100644
--- a/uds/ASDS.icl
+++ b/uds/ASDS.icl
@@ -6,21 +6,20 @@ import Data.Functor
 import Control.Monad
 import Control.Monad.State
 import Control.Monad.Trans
+from Text import class Text(concat), instance Text String
 
 import ASDS.Source
 import ASDS.Lens
 import ASDS.Select
 import ASDS.Parallel
 
-sds :: (sds m p r w) -> SDS m p r w | read, write, observe sds & Monad m
-sds s = SDS s (pure ())
+sds :: (sds m p r w) -> SDS m p r w | read, write, identity, observe sds & Monad m
+sds s = SDS s
 
-instance read SDS where read (SDS s _) p = read s p
-instance write SDS where write (SDS sds _) p w = write sds p w
-instance observe SDS
-where
-	identity (SDS sds _) c = identity sds c
-	observe (SDS sds _) p oid handle = observe sds p oid handle
+instance read SDS where read (SDS s) p = read s p
+instance write SDS where write (SDS sds) p w = write sds p w
+instance identity SDS where identity (SDS sds) c = identity sds c
+instance observe SDS where observe (SDS sds) p oid handle = observe sds p oid handle
 
 getShare :: (sds m () r w) -> PViewT m r | Monad m & read sds & TC r & TC w
 getShare s = read s () >>= \v->case v of
@@ -35,12 +34,12 @@ setShare w s = write s () w >>= \v->case v of
 updShare :: (r -> w) (sds m () r w) -> PViewT m w | Monad m & read sds & write sds & TC r & TC w
 updShare f s = f <$> getShare s >>= \v->setShare v s >>| liftT (pure v)
 
-trigger :: (p -> Bool) -> PViewT m () | TC p & Monad m
-trigger inv = gets (filter (match inv)) >>= mapM_ run
+trigger :: (v m p r w) (p -> Bool) -> PViewT m () | identity v & TC p & Monad m
+trigger sds inv = gets (filter (match (concat (identity sds [])) inv)) >>= mapM_ run
 where
-	match :: (p -> Bool) (NRequest m) -> Bool | TC p
-	match inv (NRequest oid ohnd (a :: p^)) = inv a
-	match _ _ = False
+	match :: String (p -> Bool) (NRequest m) -> Bool | TC p
+	match id inv (NRequest oid ohnd (a :: p^)) = id == oid && inv a
+	match _ _ _ = False
 
 	run :: (NRequest m) -> PViewT m () | Monad m
 	run (NRequest oid ohnd _) = liftT ohnd
diff --git a/uds/ASDS/Parallel.icl b/uds/ASDS/Parallel.icl
index ac9a341..877ff68 100644
--- a/uds/ASDS/Parallel.icl
+++ b/uds/ASDS/Parallel.icl
@@ -47,7 +47,7 @@ where
 
 // Write the share but only if the given value is a Just.
 // If it is None, pretend that the value was written
-write` :: (sds m p r w) p (m (? w)) -> PViewT m (WriteResult m p r w) | TC w & Monad m & write sds
+write` :: (sds m p r w) p (m (? w)) -> PViewT m (WriteResult m p r w) | TC w & Monad m & write sds & TC p
 write` sds p mmv = liftT mmv >>= \mv->case mv of
 	?None = liftT $ pure $ Written ()
 	?Just v = write sds p v
diff --git a/uds/ASDS/Source.dcl b/uds/ASDS/Source.dcl
index 3838e0e..1e7d988 100644
--- a/uds/ASDS/Source.dcl
+++ b/uds/ASDS/Source.dcl
@@ -1,6 +1,6 @@
 definition module ASDS.Source
 
-from ASDS import class read, class write, class observe
+from ASDS import class read, class write, class observe, class identity, :: KindHelper
 from Control.Monad import class Monad
 from Control.Applicative import class Applicative, class <*>, class pure
 from Data.Functor import class Functor
@@ -9,18 +9,19 @@ from Data.Functor import class Functor
 :: ReadSource m p r w = ReadSource (p -> m r)
 
 //* Just write something
-:: WriteSource m p r w = WriteSource (p w -> m ())
+:: WriteSource m p r w = WriteSource String (p w -> m (p -> Bool))
 
 //* 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
+:: RWPair sdsr sdsw m p r w = RWPair (KindHelper (m ()) (sdsr m p r w)) (sdsw m p r w)
+rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w
 
 //* 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
+source :: String (p -> m r) (p w -> m (p -> Bool)) -> Source m p r w
 
 instance read ReadSource, (RWPair sdsr sdsw) | read sdsr
 instance write WriteSource, (RWPair sdsr sdsw) | write sdsw
+instance identity WriteSource, (RWPair sdsr sdsw) | identity sdsw
 instance observe WriteSource, (RWPair sdsr sdsw) | observe sdsw
 
 //* Immediately returns the given value on a read
diff --git a/uds/ASDS/Source.icl b/uds/ASDS/Source.icl
index b84aeba..991dd19 100644
--- a/uds/ASDS/Source.icl
+++ b/uds/ASDS/Source.icl
@@ -8,11 +8,11 @@ import Control.Monad.State
 import Control.Monad.Trans
 import ASDS
 
-rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w | pure m
-rwpair l r = RWPair l r (pure ())
+rwpair :: (sdsr m p r w) (sdsw m p r w) -> RWPair sdsr sdsw m p r w
+rwpair l r = RWPair l r
 
-source :: (p -> m r) (p w -> m ()) -> Source m p r w | pure m
-source read write = rwpair (ReadSource read) (WriteSource write)
+source :: String (p -> m r) (p w -> m (p -> Bool)) -> Source m p r w
+source name read write = rwpair (ReadSource read) (WriteSource name write)
 
 instance read ReadSource
 where
@@ -20,30 +20,39 @@ where
 
 instance write WriteSource
 where
-	write (WriteSource write) p w = Written <$> liftT (write p w)
+	write s=:(WriteSource _ write) p w = liftT (write p w)
+		>>= trigger s >>| pure (Written ())
+
+instance identity WriteSource
+where
+	identity (WriteSource n _) c = [n:c]
 
 instance observe WriteSource
 where
-	observe sds p oid hnd = modify \s->[NRequest oid hnd (dynamic p):s]
+	observe sds p oid hnd = modify (nrequestc p oid hnd)
 
 instance read (RWPair sdsr sdsw) | read sdsr
 where
-	read (RWPair s w _) p = read s p >>= \v->case v of
+	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
+	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 identity (RWPair sdsr sdsw) | identity sdsw
+where
+	identity (RWPair r w) c = identity w c
+
 instance observe (RWPair sdsr sdsw) | observe sdsw
 where
-	observe (RWPair r s _) p oid hnd = observe s p oid hnd
+	observe (RWPair r s) p oid hnd = observe s p oid hnd
 
 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 ()
+nullShare = WriteSource "null" \_ _->pure \_->False
diff --git a/uds/test.icl b/uds/test.icl
index aceaab3..f294e8e 100644
--- a/uds/test.icl
+++ b/uds/test.icl
@@ -3,6 +3,7 @@ module test
 import StdEnv
 import Data.Either
 import Data.Func
+import Data.Functor
 import Data.Functor.Identity
 from Data.Map import :: Map(..)
 import qualified Data.Map
@@ -10,6 +11,7 @@ import Control.Monad
 import Control.Monad.State
 import Control.Monad.Fail
 import Control.Monad.Trans
+import System.IO
 
 import ASDS
 import ASDS.Source
@@ -26,10 +28,12 @@ equal :: a (PViewT m a) -> PViewT m () | MonadFail m & == a
 equal expected mon = mon >>= \v->if (v == expected) (pure ()) (fail "Not equal")
 
 //Start :: Either String (((), [NRequest Identity)]), Map String Dynamic)
-Start = runIdentity (runStateT (observe intsource () "observeid" (pure ()) >>| setShare 42 intsource) [])
+Start w = /*eval*/execIO (runStateT (observe intsource () "int" (putStrLn "blurp" >>| pure ()) >>| setShare 42 intsource) []) w
+
+import Debug.Trace
 
 intsource :: Source m () Int Int | pure m
-intsource = source (\_->pure 42) (\_ _->pure ())
+intsource = source "int" (\_->pure 42) (\_ _->pure (\_->True))
 
 /*
 //Start :: Either String ((), Map String Dynamic)
@@ -87,4 +91,4 @@ dstore :: Lens (Lens (RWPair ReadSource WriteSource)) (StateT (Map String Dynami
 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
+store = source "store" (\p->getState) \p w->(\p->True) <$ put w