Add test from the pull request for Elab.tryCatch
commit9fc97f9b4ec2a75bc576c52994299037a606cc74
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 18 Mar 2018, 00:41 (9 years ago)
parent09fe491
test/meta003/Catch.idrnew file+17
@@ -0,0 +1,17 @@
1+import Language.Reflection.Elab
2+
3+%language ElabReflection
4+
5+f : Err -> Elab ()
6+f (Msg _) = fill `("message error")
7+f (CantUnify _ _ _ _ _ _) = fill `("unification error")
8+f _ = fill `("other")
9+
10+s1 : String
11+s1 = %runElab (do tryCatch (fail []) f ; solve)
12+
13+s2 : String
14+s2 = %runElab (do tryCatch (fill `(True)) f ; solve)
15+
16+main : IO ()
17+main = do putStrLn s1 ; putStrLn s2
test/meta003/expected+2
@@ -8,3 +8,5 @@ Type mismatch between
88and
99 String
1010
11+message error
12+unification error
test/meta003/run+3−1
@@ -1,3 +1,5 @@
11#!/usr/bin/env bash
22${IDRIS:-idris} $@ --nocolour --check --consolewidth 70 BadDef.idr
3−rm -f *.ibc
3+${IDRIS:-idris} $@ --nocolour --consolewidth 70 -o meta003 Catch.idr
4+./meta003
5+rm -f meta003 *.ibc