@@ -0,0 +1,38 @@
1+module Control.ST.ImplicitCall
2+
3+import Control.ST
4+import Control.Catchable
5+import Control.IOExcept
6+
7+public export
8+interface Exception (m : Type -> Type) errorType | m where
9+ throw : errorType -> STrans m a ctxt (const ctxt)
10+
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)
14+
15+export
16+Exception (Either errorType) errorType where
17+ throw err = lift (Left err)
18+ catch prog f = do res <- runAs prog
19+ case res of
20+ Left err => f err
21+ Right ok => pure ok
22+
23+export
24+Exception Maybe () where
25+ throw err = lift Nothing
26+ catch prog f = do res <- runAs prog
27+ case res of
28+ Nothing => f ()
29+ Just ok => pure ok
30+
31+export
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
36+ pure (Right r))
37+ (\err => pure (Left err)))
38+ either (\err => f err) (\ok => pure ok) res