Change argument order for 'either'

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

CHANGELOG

@@ -26,6 +26,9 @@ New in 0.9.11:
   be total, e.g "assert_total (tail (x :: xs))".
 * Terminal width is automatically detected if Idris is compiled with curses
   support. If curses is not available, automatic mode assumes 80 columns.
+* Changed argument order for Prelude.Either.either.
+* Experimental 'neweffects' library, intended to replace 'effects' in the
+  next release.
 
 Internal changes
 

libs/neweffects/Effect/File.idr

@@ -12,7 +12,7 @@ openOK m False = ()
 
 data FileIO : Effect where
      Open  : String -> (m : Mode) -> 
-             {() ==> if result then OpenFile m else ()} FileIO Bool
+             {() ==> {res} if res then OpenFile m else ()} FileIO Bool
      Close : {OpenFile m ==> ()}               FileIO () 
 
      ReadLine  :           {OpenFile Read}  FileIO String 

libs/neweffects/Effects.idr

@@ -22,6 +22,8 @@ class Handler (e : Effect) (m : Type -> Type) where
 -- A bit of syntactic sugar ('syntax' is not very flexible so we only go
 -- up to a small number of parameters...)
 
+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff] 
+       = eff inst (\b => outst)
 syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
 syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
 

libs/prelude/Prelude/Either.idr

@@ -29,9 +29,9 @@ choose : (b : Bool) -> Either (so b) (so (not b))
 choose True  = Left oh
 choose False = Right oh
 
-either : Either a b -> (a -> c) -> (b -> c) -> c
-either (Left x)  l r = l x
-either (Right x) l r = r x
+either : (a -> c) -> (b -> c) -> Either a b -> c
+either l r (Left x)  = l x
+either l r (Right x) = r x
 
 lefts : List (Either a b) -> List a
 lefts []      = []
@@ -84,4 +84,4 @@ leftInjective refl = refl
 
 total rightInjective : {a : Type} -> {x : b} -> {y : b}
                      -> (Right {a = a} x = Right {a = a} y) -> (x = y)
-rightInjective refl = refl
+rightInjective refl = refl

test/dsl002/Resimp.idr

@@ -135,9 +135,9 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
   interp env (Lift io) k
      = k env io
   interp env (Check x left right) k =
-     either (envLookup x env)
-            (\a => interp (envUpdate x a env) left k)
+     either (\a => interp (envUpdate x a env) left k)
             (\b => interp (envUpdate x b env) right k)
+            (envLookup x env)
   interp env (While test body) k
      = interp env test
           (\env', result =>