diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 39efc51..450e42c 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -12,7 +12,7 @@ on:
env:
SCHEME: scheme
IDRIS2_TESTS_CG: chez
- IDRIS2_COMMIT: "0bc18bd34a53824cafa5a72d7790ca380648636a"
+ IDRIS2_COMMIT: "bf87b623ef64244451d10c4b5460e8fc2f88c99a"
jobs:
build:
diff --git a/README.md b/README.md
index 2f064be..3cca658 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,8 @@
[![](https://github.com/Russoul/Idris2-Effect/workflows/Ubuntu/badge.svg)](https://github.com/Russoul/Idris2-Effect/actions?query=workflow%3A"Ubuntu")
Experimental effects library for Idris 2
-
Tested against [Idris 2, version 0.5.1-0bc18bd34](https://github.com/idris-lang/Idris2/tree/0bc18bd34a53824cafa5a72d7790ca380648636a)
+
Tested against [Idris 2, version 0.5.1-bf87b623e](https://github.com/idris-lang/Idris2/tree/bf87b623ef64244451d10c4b5460e8fc2f88c99a)
+
For an introduction, see [writing a parser via effects](/docs/example-parser.md)
diff --git a/src/Control/Effect/NonDet.idr b/src/Control/Effect/NonDet.idr
index 3e91737..7ceb36a 100644
--- a/src/Control/Effect/NonDet.idr
+++ b/src/Control/Effect/NonDet.idr
@@ -31,7 +31,7 @@ namespace Algebra
-- hdl : Handler ctx n (ListT m)
-- hdl' : Handler (List m) (ListT m) m
-- ? : Handler (List m . ctx) n m
- EffectAlgebra.alg {f = Functor.Compose @{(ListM, %search)}}
+ EffectAlgebra.alg {f = Functor.Compose @{ListM}}
{ctx = ListM m . ctx}
{m} (ctxx :: pure [])
((~<~) @{%search} @{Functor.ListM} { ctx1 = ListM m
diff --git a/src/Control/Effect/Writer.idr b/src/Control/Effect/Writer.idr
index 00a0114..c2fffe9 100644
--- a/src/Control/Effect/Writer.idr
+++ b/src/Control/Effect/Writer.idr
@@ -25,7 +25,7 @@ namespace Algebra
alg ctx hdl (Inl (Tell s)) = MkWriterT $ \_ => pure (ctx, s)
alg ctxx hdl (Inr x) = MkWriterT $ \r => do
res <- alg
- {f = Functor.Compose @{(Functor.LeftPair, %search)}}
+ {f = Functor.Compose @{Functor.LeftPair}}
(ctxx, r) h x
pure res
where
@@ -45,7 +45,7 @@ namespace Algebra
-- h : Handler (,s) (WriterT s m) m
-- h ~<~ hdl : Handler ((, s) . ctx) n m
res <- alg
- {f = Functor.Compose @{(Functor.LeftPair, %search)}}
+ {f = Functor.Compose @{Functor.LeftPair}}
(ctxx, r) h x
pure res
where
diff --git a/tests/Main.idr b/tests/Main.idr
index 2b6c0d4..51adf55 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -14,4 +14,4 @@ main = runner
[ testPaths "effect" allTests
] where
testPaths : String -> TestPool -> TestPool
- testPaths dir = record { testCases $= map ((dir ++ "/") ++) }
+ testPaths dir = { testCases $= map ((dir ++ "/") ++) }