@@ -0,0 +1,38 @@
1+module Control.ST.ImplicitCall
4+import Control.Catchable
5+import Control.IOExcept
8+interface Exception (m : Type -> Type) errorType | m where
9+ throw : errorType -> STrans m a ctxt (const ctxt)
11+ catch : STrans m a in_res (const out_res) ->
12+ (errorType -> STrans m a out_res (const out_res)) ->
13+ STrans m a in_res (const out_res)
16+Exception (Either errorType) errorType where
17+ throw err = lift (Left err)
18+ catch prog f = do res <- runAs prog
24+Exception Maybe () where
25+ throw err = lift Nothing
26+ catch prog f = do res <- runAs prog
32+Exception (IOExcept errorType) errorType where
33+ throw err = lift (ioe_fail err)
34+ catch prog f = do io_res <- runAs prog
35+ res <- lift (catch (do r <- io_res
37+ (\err => pure (Left err)))
38+ either (\err => f err) (\ok => pure ok) res