5593697 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Rename EFF to EFFECT (for more consistent naming rules)

commit559369785e4d7426fae334e604347e96e9c017f7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 Mar 2013, 11:53 (14 years ago) parentedfe5b3

8 files changed+24−16

compare with master

unifiedsplit

CHANGELOG+8 effects/Effect/Exception.idr+1−1 effects/Effect/File.idr+1−1 effects/Effect/Random.idr+1−1 effects/Effect/Select.idr+1−1 effects/Effect/State.idr+1−1 effects/Effect/StdIO.idr+1−1 effects/Effects.idr+10−10

CHANGELOG+8

@@ -1,3 +1,11 @@

1+New in 0.9.8:

2+-------------

4+User visible changes:

6+* Renamed EFF to EFFECT in Effect package

7+* Experimental Java backend

19New in 0.9.7:

210-------------

311

effects/Effect/Exception.idr+1−1

@@ -17,7 +17,7 @@ instance Show a => Handler (Exception a) IO where

1717instance Handler (Exception a) (IOExcept a) where

1818 handle _ (Raise e) k = ioM (return (Left e))

1919

20−EXCEPTION : Type -> EFF

20+EXCEPTION : Type -> EFFECT

2121EXCEPTION t = MkEff () (Exception t)

2222

2323raise : a -> Eff m [EXCEPTION a] b

effects/Effect/File.idr+1−1

@@ -40,7 +40,7 @@ instance Handler FileIO (IOExcept String) where

4040 handle (FH h) EOF k = do e <- ioe_lift (feof h)

4141 k (FH h) e

4242

43−FILE_IO : Type -> EFF

43+FILE_IO : Type -> EFFECT

4444FILE_IO t = MkEff t FileIO

4545

4646open : Handler FileIO e =>

effects/Effect/Random.idr+1−1

@@ -11,7 +11,7 @@ using (m : Type -> Type)

1111 = let seed' = 1664525 * seed + 1013904223 in

1212 k seed' seed'

1313

14−RND : EFF

14+RND : EFFECT

1515RND = MkEff Int Random

1616

1717rndInt : Int -> Int -> Eff m [RND] Int

effects/Effect/Select.idr+1−1

@@ -15,7 +15,7 @@ instance Handler Selection Maybe where

1515instance Handler Selection List where

1616 handle r (Select xs) k = concatMap (k r) xs

1717

18−SELECT : EFF

18+SELECT : EFFECT

1919SELECT = MkEff () Selection

2020

2121select : List a -> Eff m [SELECT] a

effects/Effect/State.idr+1−1

@@ -13,7 +13,7 @@ using (m : Type -> Type)

1313 handle st Get k = k st st

1414 handle st (Put n) k = k n ()

1515

16−STATE : Type -> EFF

16+STATE : Type -> EFFECT

1717STATE t = MkEff t State

1818

1919get : Eff m [STATE x] x

effects/Effect/StdIO.idr+1−1

@@ -38,7 +38,7 @@ instance Handler StdIO IOStream where

3838

3939--- The Effect and associated functions

4040

41−STDIO : EFF

41+STDIO : EFFECT

4242STDIO = MkEff () StdIO

4343

4444putStr : Handler StdIO e => String -> Eff e [STDIO] ()

effects/Effects.idr+10−10

@@ -10,8 +10,8 @@ import Control.Catchable

1010Effect : Type

1111Effect = Type -> Type -> Type -> Type

1212

13−data EFF : Type where

14− MkEff : Type -> Effect -> EFF

13+data EFFECT : Type where

14+ MkEff : Type -> Effect -> EFFECT

1515

1616class Handler (e : Effect) (m : Type -> Type) where

1717 handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a

@@ -28,12 +28,12 @@ using (xs : List a, ys : List a)

2828 subListId {xs = Nil} = SubNil

2929 subListId {xs = x :: xs} = Keep subListId

3030

31−data Env : (m : Type -> Type) -> List EFF -> Type where

31+data Env : (m : Type -> Type) -> List EFFECT -> Type where

3232 Nil : Env m Nil

3333 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

3434

3535data EffElem : (Type -> Type -> Type -> Type) -> Type ->

36− List EFF -> Type where

36+ List EFFECT -> Type where

3737 Here : EffElem x a (MkEff a x :: xs)

3838 There : EffElem x a xs -> EffElem x a (y :: xs)

3939

@@ -73,8 +73,8 @@ findSubList (S n)

7373 ((Try (Refine "Keep" `Seq` Solve)

7474 (Refine "Drop" `Seq` Solve)) `Seq` findSubList n))

7575

76−updateResTy : (xs : List EFF) -> EffElem e a xs -> e a b t ->

77− List EFF

76+updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->

77+ List EFFECT

7878updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs

7979updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n

8080

@@ -83,7 +83,7 @@ infix 5 :::, :-, :=

8383data LRes : lbl -> Type -> Type where

8484 (:=) : (x : lbl) -> res -> LRes x res

8585

86−(:::) : lbl -> EFF -> EFF

86+(:::) : lbl -> EFFECT -> EFFECT

8787(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff

8888

8989private

@@ -97,7 +97,7 @@ relabel {x = MkEff a eff} l [v] = [l := v]

9797-- the language of Effects

9898

9999data EffM : (m : Type -> Type) ->

100− List EFF -> List EFF -> Type -> Type where

100+ List EFFECT -> List EFFECT -> Type -> Type where

101101 value : a -> EffM m xs xs a

102102 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

103103 effect : {a, b: _} -> {e : Effect} ->

@@ -114,7 +114,7 @@ data EffM : (m : Type -> Type) ->

114114 EffM m xs xs' a

115115 (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t

116116

117−-- Eff : List (EFF m) -> Type -> Type

117+-- Eff : List (EFFECT m) -> Type -> Type

118118

119119implicit

120120lift' : {default tactics { reflect findSubList 10; solve; }

@@ -192,7 +192,7 @@ runPure env prog = eff env prog (\env, r => r)

192192runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a

193193runWith inj env prog = eff env prog (\env, r => inj r)

194194

195−Eff : (Type -> Type) -> List EFF -> Type -> Type

195+Eff : (Type -> Type) -> List EFFECT -> Type -> Type

196196Eff m xs t = EffM m xs xs t

197197

198198-- some higher order things