From: Mart Lubbers 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