
   0 | module Control.Eff.Except
   1 | 
   2 | import Control.Eff.Internal
   3 | 
   4 | %default total
   5 | 
   6 | public export
   7 | data ExceptL : (lbl : k) -> (err : Type) -> (a : Type) -> Type where
   8 |   [search lbl]
   9 |   Err : err -> ExceptL lbl err a
  10 | 
  11 | public export
  12 | Except : (err,a : Type) -> Type
  13 | Except = ExceptL ()
  14 | 
  15 | public export
  16 | FailL : (lbl : k) -> (a : Type) -> Type
  17 | FailL lbl = ExceptL lbl ()
  18 | 
  19 | public export
  20 | Fail : (a : Type) -> Type
  21 | Fail = FailL ()
  22 | 
  23 | export
  24 | throwAt : (0 lbl : k) -> Has (ExceptL lbl err) fs => err -> Eff fs a
  25 | throwAt lbl e = send $ Err {lbl} e
  26 | 
  27 | export %inline
  28 | throw : Has (Except err) fs => err -> Eff fs a
  29 | throw = throwAt ()
  30 | 
  31 | export %inline
  32 | failAt : (0 lbl : k) -> Has (FailL lbl) fs => Eff fs a
  33 | failAt lbl = throwAt lbl ()
  34 | 
  35 | export %inline
  36 | fail : Has Fail fs => Eff fs a
  37 | fail = throwAt () ()
  38 | 
  39 | export %inline
  40 | rethrowAt : (0 lbl : k) -> Has (ExceptL lbl err) fs => Either err a -> Eff fs a
  41 | rethrowAt lbl = either (throwAt lbl) pure
  42 | 
  43 | export %inline
  44 | rethrow : Has (Except err) fs => Either err a -> Eff fs a
  45 | rethrow = rethrowAt ()
  46 | 
  47 | export %inline
  48 | noteAt :
  49 |      (0 lbl : k)
  50 |   -> {auto _ : Has (ExceptL lbl err) fs}
  51 |   -> Lazy err
  52 |   -> Maybe a
  53 |   -> Eff fs a
  54 | noteAt lbl e = maybe (throwAt lbl e) pure
  55 | 
  56 | export %inline
  57 | note : Has (Except err) fs => Lazy err -> Maybe a -> Eff fs a
  58 | note = noteAt ()
  59 | 
  60 | export %inline
  61 | fromJustAt : (0 lbl : k) -> Has (FailL lbl) fs => Maybe a -> Eff fs a
  62 | fromJustAt lbl = noteAt lbl ()
  63 | 
  64 | export %inline
  65 | fromJust : Has Fail fs => Maybe a -> Eff fs a
  66 | fromJust = fromJustAt ()
  67 | 
  68 | --------------------------------------------------------------------------------
  69 | --          Handling Exceptions
  70 | --------------------------------------------------------------------------------
  71 | 
  72 | unExcept : ExceptL lbl err a -> err
  73 | unExcept (Err e) = e
  74 | 
  75 | export
  76 | catchAt :
  77 |      (0 lbl : k)
  78 |   -> {auto _ : Has (ExceptL lbl err) fs}
  79 |   -> (err -> Eff (fs - ExceptL lbl err) a)
  80 |   -> Eff fs a
  81 |   -> Eff (fs - ExceptL lbl err) a
  82 | catchAt _ f = handleRelay pure $ \v,_ => f (unExcept v)
  83 | 
  84 | export %inline
  85 | catch :
  86 |      {auto _ : Has (Except err) fs}
  87 |   -> (err -> Eff (fs - Except err) a)
  88 |   -> Eff fs a
  89 |   -> Eff (fs - Except err) a
  90 | catch = catchAt ()
  91 | 
  92 | export
  93 | runExceptAt :
  94 |      (0 lbl : k)
  95 |   -> {auto _ : Has (ExceptL lbl err) fs}
  96 |   -> Eff fs a
  97 |   -> Eff (fs - ExceptL lbl err) (Either err a)
  98 | runExceptAt _ = handleRelay (pure . Right) $ \v,_ => pure (Left $ unExcept v)
  99 | 
 100 | export %inline
 101 | runExcept :
 102 |      {auto _ : Has (Except err) fs}
 103 |   -> Eff fs a
 104 |   -> Eff (fs - Except err) (Either err a)
 105 | runExcept = runExceptAt ()
 106 | 
 107 | export
 108 | runFailAt :
 109 |      (0 lbl : k)
 110 |   -> {auto _ : Has (FailL lbl) fs}
 111 |   -> Eff fs a
 112 |   -> Eff (fs - FailL lbl) (Maybe a)
 113 | runFailAt lbl = map (either (const Nothing) Just) . runExceptAt lbl
 114 | 
 115 | export %inline
 116 | runFail : Has Fail fs => Eff fs a -> Eff (fs - Fail) (Maybe a)
 117 | runFail = runFailAt ()
 118 |