@@ -20,6 +20,8 @@ import Wingman.Metaprogramming.Parser.Documentation
20
20
import Wingman.Metaprogramming.ProofState (proofState , layout )
21
21
import Wingman.Tactics
22
22
import Wingman.Types
23
+ import Development.IDE.GHC.Compat (RealSrcLoc , srcLocLine , srcLocCol , srcLocFile )
24
+ import FastString (unpackFS )
23
25
24
26
25
27
nullary :: T. Text -> TacticsM () -> Parser (TacticsM () )
@@ -420,17 +422,30 @@ wrapError :: String -> String
420
422
wrapError err = " ```\n " <> err <> " \n ```\n "
421
423
422
424
425
+ fixErrorOffset :: RealSrcLoc -> P. ParseErrorBundle a b -> P. ParseErrorBundle a b
426
+ fixErrorOffset rsl (P. ParseErrorBundle ne (P. PosState a n (P. SourcePos _ line col) pos s))
427
+ = P. ParseErrorBundle ne
428
+ $ P. PosState a n
429
+ (P. SourcePos
430
+ (unpackFS $ srcLocFile rsl)
431
+ ((<>) line $ P. mkPos $ srcLocLine rsl - 1 )
432
+ ((<>) col $ P. mkPos $ srcLocCol rsl - 1 + length @ [] " [wingman|" )
433
+ )
434
+ pos
435
+ s
436
+
423
437
------------------------------------------------------------------------------
424
438
-- | Attempt to run a metaprogram tactic, returning the proof state, or the
425
439
-- errors.
426
440
attempt_it
427
- :: Context
441
+ :: RealSrcLoc
442
+ -> Context
428
443
-> Judgement
429
444
-> String
430
445
-> IO (Either String String )
431
- attempt_it ctx jdg program =
446
+ attempt_it rsl ctx jdg program =
432
447
case P. runParser tacticProgram " <splice>" (T. pack program) of
433
- Left peb -> pure $ Left $ wrapError $ P. errorBundlePretty peb
448
+ Left peb -> pure $ Left $ wrapError $ P. errorBundlePretty $ fixErrorOffset rsl peb
434
449
Right tt -> do
435
450
res <- runTactic
436
451
ctx
0 commit comments