git.iko.soy/Idris-dev
on master help sign in
Add tryCatch as an Elab action in Language.Reflection.Elab
09fe491Joomy Korkut
libs/prelude/Language/Reflection/Elab.idr+9
compare with master
unifiedsplit
@@ -16,6 +16,7 @@ import Prelude.Maybe
16import Prelude.Monad
16import Prelude.Monad
17import Prelude.Nat
17import Prelude.Nat
18import Language.Reflection
18import Language.Reflection
19+import Language.Reflection.Errors
19
20
20%access public export
21%access public export
21
22
@@ -138,6 +139,7 @@ data Elab : Type -> Type where
138 Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
139 Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
139
140
140 Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
141 Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
142+ Prim__TryCatch : {a : Type} -> Elab a -> (Err -> Elab a) -> Elab a
141 Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
143 Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
142
144
143 Prim__Env : Elab (List (TTName, Binder TT))
145 Prim__Env : Elab (List (TTName, Binder TT))
@@ -218,6 +220,13 @@ namespace Tactics
218 implementation Monad Elab where
220 implementation Monad Elab where
219 x >>= f = Prim__BindElab x f
221 x >>= f = Prim__BindElab x f
220
222
223+ ||| `tryCatch t (\err => t')` will run `t`, and if it
224+ ||| fails, roll back the elaboration state and run `t'`,
225+ ||| but with access to the knowledge of why `t` failed.
226+ export
227+ tryCatch : Elab a -> (Err -> Elab a) -> Elab a
228+ tryCatch x f = Prim__TryCatch x f
229+
221 ||| Halt elaboration with an error
230 ||| Halt elaboration with an error
222 export
231 export
223 fail : List ErrorReportPart -> Elab a
232 fail : List ErrorReportPart -> Elab a
src/Idris/Elab/Term.hs+8
@@ -2026,6 +2026,14 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
2026 first' <- eval first
2026 first' <- eval first
2027 alt' <- eval alt
2027 alt' <- eval alt
2028 try' (runTacTm first') (runTacTm alt') True
2028 try' (runTacTm first') (runTacTm alt') True
2029+ | n == tacN "Prim__TryCatch"
2030+ = do ~[_a, first, f] <- tacTmArgs 3 tac args
2031+ first' <- eval first
2032+ f' <- eval f
2033+ tryCatch (runTacTm first') $ \err ->
2034+ do (err', _) <- checkClosed (reflectErr err)
2035+ f' <- eval (App Complete f err')
2036+ runTacTm f'
2029 | n == tacN "Prim__Fill"
2037 | n == tacN "Prim__Fill"
2030 = do ~[raw] <- tacTmArgs 1 tac args
2038 = do ~[raw] <- tacTmArgs 1 tac args
2031 raw' <- reifyRaw =<< eval raw
2039 raw' <- reifyRaw =<< eval raw