git.iko.soy/Idris-dev
on master help sign in
Rename EFF to EFFECT (for more consistent naming rules)
5593697Edwin Brady
CHANGELOG+8
compare with master
unifiedsplit
@@ -1,3 +1,11 @@
1+New in 0.9.8:
2+-------------
3+
4+User visible changes:
5+
6+* Renamed EFF to EFFECT in Effect package
7+* Experimental Java backend
8+
1New in 0.9.7:
9New in 0.9.7:
2-------------
10-------------
3
11
effects/Effect/Exception.idr+1−1
@@ -17,7 +17,7 @@ instance Show a => Handler (Exception a) IO where
17instance Handler (Exception a) (IOExcept a) where
17instance Handler (Exception a) (IOExcept a) where
18 handle _ (Raise e) k = ioM (return (Left e))
18 handle _ (Raise e) k = ioM (return (Left e))
19
19
20−EXCEPTION : Type -> EFF
20+EXCEPTION : Type -> EFFECT
21EXCEPTION t = MkEff () (Exception t)
21EXCEPTION t = MkEff () (Exception t)
22
22
23raise : a -> Eff m [EXCEPTION a] b
23raise : a -> Eff m [EXCEPTION a] b
effects/Effect/File.idr+1−1
@@ -40,7 +40,7 @@ instance Handler FileIO (IOExcept String) where
40 handle (FH h) EOF k = do e <- ioe_lift (feof h)
40 handle (FH h) EOF k = do e <- ioe_lift (feof h)
41 k (FH h) e
41 k (FH h) e
42
42
43−FILE_IO : Type -> EFF
43+FILE_IO : Type -> EFFECT
44FILE_IO t = MkEff t FileIO
44FILE_IO t = MkEff t FileIO
45
45
46open : Handler FileIO e =>
46open : Handler FileIO e =>
effects/Effect/Random.idr+1−1
@@ -11,7 +11,7 @@ using (m : Type -> Type)
11 = let seed' = 1664525 * seed + 1013904223 in
11 = let seed' = 1664525 * seed + 1013904223 in
12 k seed' seed'
12 k seed' seed'
13
13
14−RND : EFF
14+RND : EFFECT
15RND = MkEff Int Random
15RND = MkEff Int Random
16
16
17rndInt : Int -> Int -> Eff m [RND] Int
17rndInt : Int -> Int -> Eff m [RND] Int
effects/Effect/Select.idr+1−1
@@ -15,7 +15,7 @@ instance Handler Selection Maybe where
15instance Handler Selection List where
15instance Handler Selection List where
16 handle r (Select xs) k = concatMap (k r) xs
16 handle r (Select xs) k = concatMap (k r) xs
17
17
18−SELECT : EFF
18+SELECT : EFFECT
19SELECT = MkEff () Selection
19SELECT = MkEff () Selection
20
20
21select : List a -> Eff m [SELECT] a
21select : List a -> Eff m [SELECT] a
effects/Effect/State.idr+1−1
@@ -13,7 +13,7 @@ using (m : Type -> Type)
13 handle st Get k = k st st
13 handle st Get k = k st st
14 handle st (Put n) k = k n ()
14 handle st (Put n) k = k n ()
15
15
16−STATE : Type -> EFF
16+STATE : Type -> EFFECT
17STATE t = MkEff t State
17STATE t = MkEff t State
18
18
19get : Eff m [STATE x] x
19get : Eff m [STATE x] x
effects/Effect/StdIO.idr+1−1
@@ -38,7 +38,7 @@ instance Handler StdIO IOStream where
38
38
39--- The Effect and associated functions
39--- The Effect and associated functions
40
40
41−STDIO : EFF
41+STDIO : EFFECT
42STDIO = MkEff () StdIO
42STDIO = MkEff () StdIO
43
43
44putStr : Handler StdIO e => String -> Eff e [STDIO] ()
44putStr : Handler StdIO e => String -> Eff e [STDIO] ()
effects/Effects.idr+10−10
@@ -10,8 +10,8 @@ import Control.Catchable
10Effect : Type
10Effect : Type
11Effect = Type -> Type -> Type -> Type
11Effect = Type -> Type -> Type -> Type
12
12
13−data EFF : Type where
13+data EFFECT : Type where
14− MkEff : Type -> Effect -> EFF
14+ MkEff : Type -> Effect -> EFFECT
15
15
16class Handler (e : Effect) (m : Type -> Type) where
16class Handler (e : Effect) (m : Type -> Type) where
17 handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a
17 handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a
@@ -28,12 +28,12 @@ using (xs : List a, ys : List a)
28 subListId {xs = Nil} = SubNil
28 subListId {xs = Nil} = SubNil
29 subListId {xs = x :: xs} = Keep subListId
29 subListId {xs = x :: xs} = Keep subListId
30
30
31−data Env : (m : Type -> Type) -> List EFF -> Type where
31+data Env : (m : Type -> Type) -> List EFFECT -> Type where
32 Nil : Env m Nil
32 Nil : Env m Nil
33 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
33 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
34
34
35data EffElem : (Type -> Type -> Type -> Type) -> Type ->
35data EffElem : (Type -> Type -> Type -> Type) -> Type ->
36− List EFF -> Type where
36+ List EFFECT -> Type where
37 Here : EffElem x a (MkEff a x :: xs)
37 Here : EffElem x a (MkEff a x :: xs)
38 There : EffElem x a xs -> EffElem x a (y :: xs)
38 There : EffElem x a xs -> EffElem x a (y :: xs)
39
39
@@ -73,8 +73,8 @@ findSubList (S n)
73 ((Try (Refine "Keep" `Seq` Solve)
73 ((Try (Refine "Keep" `Seq` Solve)
74 (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))
74 (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))
75
75
76−updateResTy : (xs : List EFF) -> EffElem e a xs -> e a b t ->
76+updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
77− List EFF
77+ List EFFECT
78updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
78updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
79updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
79updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
80
80
@@ -83,7 +83,7 @@ infix 5 :::, :-, :=
83data LRes : lbl -> Type -> Type where
83data LRes : lbl -> Type -> Type where
84 (:=) : (x : lbl) -> res -> LRes x res
84 (:=) : (x : lbl) -> res -> LRes x res
85
85
86−(:::) : lbl -> EFF -> EFF
86+(:::) : lbl -> EFFECT -> EFFECT
87(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
87(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
88
88
89private
89private
@@ -97,7 +97,7 @@ relabel {x = MkEff a eff} l [v] = [l := v]
97-- the language of Effects
97-- the language of Effects
98
98
99data EffM : (m : Type -> Type) ->
99data EffM : (m : Type -> Type) ->
100− List EFF -> List EFF -> Type -> Type where
100+ List EFFECT -> List EFFECT -> Type -> Type where
101 value : a -> EffM m xs xs a
101 value : a -> EffM m xs xs a
102 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
102 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
103 effect : {a, b: _} -> {e : Effect} ->
103 effect : {a, b: _} -> {e : Effect} ->
@@ -114,7 +114,7 @@ data EffM : (m : Type -> Type) ->
114 EffM m xs xs' a
114 EffM m xs xs' a
115 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
115 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
116
116
117−-- Eff : List (EFF m) -> Type -> Type
117+-- Eff : List (EFFECT m) -> Type -> Type
118
118
119implicit
119implicit
120lift' : {default tactics { reflect findSubList 10; solve; }
120lift' : {default tactics { reflect findSubList 10; solve; }
@@ -192,7 +192,7 @@ runPure env prog = eff env prog (\env, r => r)
192runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
192runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
193runWith inj env prog = eff env prog (\env, r => inj r)
193runWith inj env prog = eff env prog (\env, r => inj r)
194
194
195−Eff : (Type -> Type) -> List EFF -> Type -> Type
195+Eff : (Type -> Type) -> List EFFECT -> Type -> Type
196Eff m xs t = EffM m xs xs t
196Eff m xs t = EffM m xs xs t
197
197
198-- some higher order things
198-- some higher order things