[ elab ] Add an ability to fail elab script with a custom FC

Author: buzden

libs/base/Language/Reflection.idr

@@ -12,7 +12,7 @@ export
 data Elab : Type -> Type where
      Pure : a -> Elab a
      Bind : Elab a -> (a -> Elab b) -> Elab b
-     Fail : String -> Elab a
+     Fail : FC -> String -> Elab a
 
      LogMsg : String -> Nat -> String -> Elab ()
      LogTerm : String -> Nat -> String -> TTImp -> Elab ()
@@ -63,7 +63,11 @@ Monad Elab where
 ||| Report an error in elaboration
 export
 fail : String -> Elab a
-fail = Fail
+fail = Fail EmptyFC
+
+export
+failAt : FC -> String -> Elab a
+failAt = Fail
 
 ||| Write a log message, if the log level is >= the given level
 export

src/TTImp/Elab/RunElab.idr

@@ -63,9 +63,12 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
                               !(sc defs (toClosure withAll env
                                               !(quote defs env act'))) exp
                   x => failWith defs $ "non-function RHS of a Bind: " ++ show x
-    elabCon defs "Fail" [_,msg]
+    elabCon defs "Fail" [_, mbfc, msg]
         = do msg' <- evalClosure defs msg
-             throw (GenericMsg fc ("Error during reflection: " ++
+             let customFC = case !(evalClosure defs mbfc >>= reify defs) of
+                               EmptyFC => fc
+                               x       => x
+             throw (GenericMsg customFC ("Error during reflection: " ++
                                       !(reify defs msg')))
     elabCon defs "LogMsg" [topic, verb, str]
         = do topic' <- evalClosure defs topic