git.iko.soy/Idris-dev
on master help sign in
Add tryCatch as an Elab action in Language.Reflection.Elab
commit09fe4917058955f47d23ea59244d1d0729608f1a authorJoomy Korkut <joomy@cattheory.com> dateSun 11 Mar 2018, 18:25 (9 years ago) parent007ef39
2 files changed+17
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+9 src/Idris/Elab/Term.hs+8
libs/prelude/Language/Reflection/Elab.idr+9
@@ -16,6 +16,7 @@ import Prelude.Maybe
1616import Prelude.Monad
1717import Prelude.Nat
1818import Language.Reflection
19+import Language.Reflection.Errors
1920
2021%access public export
2122
@@ -138,6 +139,7 @@ data Elab : Type -> Type where
138139 Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b
139140
140141 Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
142+ Prim__TryCatch : {a : Type} -> Elab a -> (Err -> Elab a) -> Elab a
141143 Prim__Fail : {a : Type} -> List ErrorReportPart -> Elab a
142144
143145 Prim__Env : Elab (List (TTName, Binder TT))
@@ -218,6 +220,13 @@ namespace Tactics
218220 implementation Monad Elab where
219221 x >>= f = Prim__BindElab x f
220222
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+
221230 ||| Halt elaboration with an error
222231 export
223232 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
20262026 first' <- eval first
20272027 alt' <- eval alt
20282028 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'
20292037 | n == tacN "Prim__Fill"
20302038 = do ~[raw] <- tacTmArgs 1 tac args
20312039 raw' <- reifyRaw =<< eval raw