[ elab ] Print script's FC in the bad elaboration script error

This commit is contained in:
Denis Buzdalov 2023-09-21 12:29:08 +03:00 committed by G. Allais
parent f6c000e27e
commit a643e3af62
4 changed files with 42 additions and 0 deletions

View File

@ -603,6 +603,10 @@ perrorRaw (BadRunElab fc env script desc)
= pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script)
<++> parens (pretty0 desc) <+> dot)
<+> line <+> !(ploc fc)
<+> !(let scriptFC = getLoc script in
if isJust (isNonEmptyFC scriptFC)
then pure $ line <+> reflow "Stuck place in the script:" <+> line <+> !(ploc scriptFC)
else pure emptyDoc)
perrorRaw (RunElabFail e)
= pure $ reflow "Error during reflection" <+> colon <++> !(perrorRaw e)
perrorRaw (GenericMsg fc str) = pure $ pretty0 str <+> line <+> !(ploc fc)

View File

@ -0,0 +1,14 @@
module BadElabScript
import Language.Reflection
%language ElabReflection
x : Elab Nat
x = do
ignore $ check {expected=Type} `(Nat)
?someHole
check `(%search)
y : Nat
y = %runElab x

View File

@ -0,0 +1,21 @@
1/1: Building BadElabScript (BadElabScript.idr)
Error: While processing right hand side of y. Bad elaborator script ?someHole [no locals in scope] (script is not a data value).
BadElabScript:14:5--14:15
10 | ?someHole
11 | check `(%search)
12 |
13 | y : Nat
14 | y = %runElab x
^^^^^^^^^^
Stuck place in the script:
BadElabScript:10:3--10:12
06 |
07 | x : Elab Nat
08 | x = do
09 | ignore $ check {expected=Type} `(Nat)
10 | ?someHole
^^^^^^^^^

View File

@ -0,0 +1,3 @@
. ../../../testutils.sh
check BadElabScript.idr