--- /dev/null
+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
:: 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
| 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
//* 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
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
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
// 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
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
:: 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
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
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
import StdEnv
import Data.Either
import Data.Func
+import Data.Functor
import Data.Functor.Identity
from Data.Map import :: Map(..)
import qualified Data.Map
import Control.Monad.State
import Control.Monad.Fail
import Control.Monad.Trans
+import System.IO
import ASDS
import ASDS.Source
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)
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
repositories / clean-tests.git / commitdiff