
  0 | module Control.Eff.Choose
  1 | 
  2 | import Control.Eff.Internal
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | data Choose : (a : Type) -> Type where
  8 |   Empty : Choose a
  9 |   Alt   : (lft, rgt : a) -> Choose a
 10 | 
 11 | export %inline
 12 | empty : Has Choose fs => Eff fs a
 13 | empty = send Empty
 14 | 
 15 | export %inline
 16 | alt : Has Choose fs => Eff fs a -> Eff fs a -> Eff fs a
 17 | alt x y = join $ send (Alt x y)
 18 | 
 19 | export %inline
 20 | guard : Has Choose fs => Bool -> Eff fs ()
 21 | guard False = empty
 22 | guard True  = pure ()
 23 | 
 24 | --------------------------------------------------------------------------------
 25 | --          Running Choose
 26 | --------------------------------------------------------------------------------
 27 | 
 28 | export
 29 | runChoose :
 30 |      {auto _ : Alternative f}
 31 |   -> {auto _ : Has Choose fs}
 32 |   -> Eff fs a
 33 |   -> Eff (fs - Choose) (f a)
 34 | runChoose fr = case toView fr of
 35 |   Pure val => pure (pure val)
 36 |   Bind x g => case handle (id {a = Choose _}) x of
 37 |     Left y  => assert_total $ lift y >>= runChoose . g
 38 |     Right Empty         => pure empty
 39 |     Right (Alt lft rgt) => assert_total $ do
 40 |       x <- runChoose (g lft)
 41 |       y <- runChoose (g rgt)
 42 |       pure (x <|> y)
 43 |