git.iko.soy/Idris-dev
on master help sign in
Remove Threading effect (on account of it not working :))
abb2c24Edwin Brady
CHANGELOG+1
compare with master
unifiedsplit
@@ -4,6 +4,7 @@ New in 0.9.7:
4User visible changes:
4User visible changes:
5
5
6* 'implicit' keyword, for implicit type conversion
6* 'implicit' keyword, for implicit type conversion
7+* Added Effects package
7* Primitives for 8,16,32 and 64 bit integers
8* Primitives for 8,16,32 and 64 bit integers
8
9
9Internal changes:
10Internal changes:
effects/Effect/Threads.idrdeleted−68
@@ -1,68 +0,0 @@
1−module Main
2−
3−import Eff
4−import State
5−
6−mutual
7− Thunk : (Type -> Type) -> Type
8− Thunk m = (t : Type) -> Threads m ->
9− (Threads m -> () -> m t) -> m t
10−
11− data Threads : (Type -> Type) -> Type where
12− MkThreads : List (Thunk m) -> List (Thunk m) -> Threads m
13−
14−initThreads : Monad m => Threads m
15−initThreads = MkThreads [] []
16−
17−data Threading : (Type -> Type) -> Effect where
18− Yield : Threading m (Threads m) (Threads m) ()
19− Fork : Threading m (Threads m) (Threads m) Bool
20−
21−instance Monad m => Effective (Threading m) m where
22− runEffect (MkThreads ds []) Yield k
23− = k (MkThreads [] (reverse ds)) ()
24− runEffect (MkThreads ds (q :: qs)) Yield k
25− = q _ (MkThreads (newThread :: ds) qs) k
26− where newThread _ st k' = do k st ()
27− k' st ()
28−
29− runEffect (MkThreads ds qs) Fork k
30− = k (MkThreads ds (newThread :: qs)) False
31− where newThread t st k' = do t <- k st True
32− k' st ()
33−
34−THREADING : (Type -> Type) -> EFF
35−THREADING m = MkEff (Threads m) (Threading m)
36−
37−fork : Monad m => (EffT m [THREADING m] ()) -> EffT m [THREADING m] ()
38−fork prog = do branch <- effect Fork
39− if branch then prog else return ()
40−
41−yield : Monad m => EffT m [THREADING m] ()
42−yield = effect Yield
43−
44−printA : Int -> Eff [THREADING m, STATE String] ()
45−printA 0 = return ()
46−printA n = do s <- lift get
47− lift (put (s ++ "A"))
48− lift yield
49− printA (n - 1)
50−
51−printB : Int -> Eff [THREADING m, STATE String] ()
52−printB 0 = return ()
53−printB n = do s <- lift get
54− lift (put (s ++ "B"))
55− lift yield
56− printB (n - 1)
57−
58−printAB : Int -> Eff [THREADING m, STATE String] String
59−printAB n = do branch <- effect Fork
60− if branch then printA n
61− else printB n
62− lift get
63−
64−
65−main : IO ()
66−main = print $ runPure [initThreads, ""] (printAB 10)
67−
68−