git.iko.soy/Idris-dev
on master help sign in
Change argument order for 'either'
0a9653bEdwin Brady
CHANGELOG+3
compare with master
unifiedsplit
@@ -26,6 +26,9 @@ New in 0.9.11:
26 be total, e.g "assert_total (tail (x :: xs))".
26 be total, e.g "assert_total (tail (x :: xs))".
27* Terminal width is automatically detected if Idris is compiled with curses
27* Terminal width is automatically detected if Idris is compiled with curses
28 support. If curses is not available, automatic mode assumes 80 columns.
28 support. If curses is not available, automatic mode assumes 80 columns.
29+* Changed argument order for Prelude.Either.either.
30+* Experimental 'neweffects' library, intended to replace 'effects' in the
31+ next release.
29
32
30Internal changes
33Internal changes
31
34
libs/neweffects/Effect/File.idr+1−1
@@ -12,7 +12,7 @@ openOK m False = ()
12
12
13data FileIO : Effect where
13data FileIO : Effect where
14 Open : String -> (m : Mode) ->
14 Open : String -> (m : Mode) ->
15− {() ==> if result then OpenFile m else ()} FileIO Bool
15+ {() ==> {res} if res then OpenFile m else ()} FileIO Bool
16 Close : {OpenFile m ==> ()} FileIO ()
16 Close : {OpenFile m ==> ()} FileIO ()
17
17
18 ReadLine : {OpenFile Read} FileIO String
18 ReadLine : {OpenFile Read} FileIO String
libs/neweffects/Effects.idr+2
@@ -22,6 +22,8 @@ class Handler (e : Effect) (m : Type -> Type) where
22-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
22-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
23-- up to a small number of parameters...)
23-- up to a small number of parameters...)
24
24
25+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
26+ = eff inst (\b => outst)
25syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
27syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
26syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
28syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
27
29
libs/prelude/Prelude/Either.idr+4−4
@@ -29,9 +29,9 @@ choose : (b : Bool) -> Either (so b) (so (not b))
29choose True = Left oh
29choose True = Left oh
30choose False = Right oh
30choose False = Right oh
31
31
32−either : Either a b -> (a -> c) -> (b -> c) -> c
32+either : (a -> c) -> (b -> c) -> Either a b -> c
33−either (Left x) l r = l x
33+either l r (Left x) = l x
34−either (Right x) l r = r x
34+either l r (Right x) = r x
35
35
36lefts : List (Either a b) -> List a
36lefts : List (Either a b) -> List a
37lefts [] = []
37lefts [] = []
@@ -84,4 +84,4 @@ leftInjective refl = refl
84
84
85total rightInjective : {a : Type} -> {x : b} -> {y : b}
85total rightInjective : {a : Type} -> {x : b} -> {y : b}
86 -> (Right {a = a} x = Right {a = a} y) -> (x = y)
86 -> (Right {a = a} x = Right {a = a} y) -> (x = y)
87−rightInjective refl = refl
87+rightInjective refl = refl
test/dsl002/Resimp.idr+2−2
@@ -135,9 +135,9 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
135 interp env (Lift io) k
135 interp env (Lift io) k
136 = k env io
136 = k env io
137 interp env (Check x left right) k =
137 interp env (Check x left right) k =
138− either (envLookup x env)
139− (\a => interp (envUpdate x a env) left k)
138+ either (\a => interp (envUpdate x a env) left k)
140 (\b => interp (envUpdate x b env) right k)
139 (\b => interp (envUpdate x b env) right k)
140+ (envLookup x env)
141 interp env (While test body) k
141 interp env (While test body) k
142 = interp env test
142 = interp env test
143 (\env', result =>
143 (\env', result =>