diff --git a/CHANGELOG b/CHANGELOG index 1a9bc0f4b..28b8d7d60 100644 --- a/CHANGELOG +++ b/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 diff --git a/libs/neweffects/Effect/File.idr b/libs/neweffects/Effect/File.idr index 758c957d4..2b38d0aa6 100644 --- a/libs/neweffects/Effect/File.idr +++ b/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 diff --git a/libs/neweffects/Effects.idr b/libs/neweffects/Effects.idr index 663e8f730..a793a432c 100644 --- a/libs/neweffects/Effects.idr +++ b/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) diff --git a/libs/prelude/Prelude/Either.idr b/libs/prelude/Prelude/Either.idr index 38c2e55f5..46df8064a 100644 --- a/libs/prelude/Prelude/Either.idr +++ b/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 \ No newline at end of file +rightInjective refl = refl diff --git a/test/dsl002/Resimp.idr b/test/dsl002/Resimp.idr index 28399d714..2efef7d05 100644 --- a/test/dsl002/Resimp.idr +++ b/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 =>