
  0 | module Util.Eff
  1 | 
  2 | import Control.Eff
  3 | import Control.Eff.Except
  4 | import Control.Eff.Choose
  5 | 
  6 | ||| 'Reduce' a labled exception to an unlabled one by tagging it with its label
  7 | export
  8 | tagAt : Show label =>
  9 |      (lbl : label)
 10 |   -> {auto _ : Has (ExceptL lbl String) ((ExceptL lbl String) :: fs)}
 11 |   -> {auto _ : Has (Except String) fs}
 12 |   -> {auto _ : Subset ((ExceptL lbl String :: fs) - ExceptL lbl String) fs}
 13 |   -> Eff ((ExceptL lbl String) :: fs) a
 14 |   -> Eff fs a
 15 | tagAt lbl x =
 16 |   let f : (String -> Eff fs a) =
 17 |         \e => throw "\{show lbl}: \{e}"
 18 |   in do
 19 |     out <- lift . runExceptAt lbl $ x
 20 |     either f pure out
 21 | 
 22 | ||| Lifts any foldable data structure into the Choose effect, enabling the
 23 | ||| style of nondeterministic programming from the list monad
 24 | export
 25 | oneOf : Has (Choose) fs => Foldable f =>
 26 |     f a -> Eff fs a
 27 | oneOf x = foldl oneOf' empty x
 28 |   where
 29 |   oneOf' : Eff fs a -> a -> Eff fs a
 30 |   oneOf' acc val = pure val `alt` acc
 31 |