git.iko.soy/Idris-dev
on master help sign in
Change argument order for 'either'

For consistency with maybe (and indeed Haskell!). Sorry if this breaks anything...

commit0a9653baf08cba1f693da1dd67782e90785d4067 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 3 Feb 2014, 13:37 (13 years ago) parent1f0e676
5 files changed+12−7
compare with master
unifiedsplit
CHANGELOG+3 libs/neweffects/Effect/File.idr+1−1 libs/neweffects/Effects.idr+2 libs/prelude/Prelude/Either.idr+4−4 test/dsl002/Resimp.idr+2−2
CHANGELOG+3
@@ -26,6 +26,9 @@ New in 0.9.11:
2626 be total, e.g "assert_total (tail (x :: xs))".
2727* Terminal width is automatically detected if Idris is compiled with curses
2828 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.
2932
3033Internal changes
3134
libs/neweffects/Effect/File.idr+1−1
@@ -12,7 +12,7 @@ openOK m False = ()
1212
1313data FileIO : Effect where
1414 Open : String -> (m : Mode) ->
15− {() ==> if result then OpenFile m else ()} FileIO Bool
15+ {() ==> {res} if res then OpenFile m else ()} FileIO Bool
1616 Close : {OpenFile m ==> ()} FileIO ()
1717
1818 ReadLine : {OpenFile Read} FileIO String
libs/neweffects/Effects.idr+2
@@ -22,6 +22,8 @@ class Handler (e : Effect) (m : Type -> Type) where
2222-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
2323-- up to a small number of parameters...)
2424
25+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
26+ = eff inst (\b => outst)
2527syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
2628syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
2729
libs/prelude/Prelude/Either.idr+4−4
@@ -29,9 +29,9 @@ choose : (b : Bool) -> Either (so b) (so (not b))
2929choose True = Left oh
3030choose False = Right oh
3131
32−either : Either a b -> (a -> c) -> (b -> c) -> c
33−either (Left x) l r = l x
34−either (Right x) l r = r x
32+either : (a -> c) -> (b -> c) -> Either a b -> c
33+either l r (Left x) = l x
34+either l r (Right x) = r x
3535
3636lefts : List (Either a b) -> List a
3737lefts [] = []
@@ -84,4 +84,4 @@ leftInjective refl = refl
8484
8585total rightInjective : {a : Type} -> {x : b} -> {y : b}
8686 -> (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)
135135 interp env (Lift io) k
136136 = k env io
137137 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)
140139 (\b => interp (envUpdate x b env) right k)
140+ (envLookup x env)
141141 interp env (While test body) k
142142 = interp env test
143143 (\env', result =>