Skip to content

Wingman: Add the correct file offset to metaprogram parse errors #1967

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Jun 25, 2021
Merged

Wingman: Add the correct file offset to metaprogram parse errors #1967

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ca60a81
Add the correct file offset to metaprogram parse errors
isovector Jun 22, 2021
6e3bcef
Merge branch 'master' into parser-offset
mergify[bot] Jun 23, 2021
bb0f924
Merge branch 'master' into parser-offset
mergify[bot] Jun 23, 2021
0a73ea5
Merge branch 'master' into parser-offset
mergify[bot] Jun 23, 2021
e1e6002
Merge branch 'master' into parser-offset
isovector Jun 24, 2021
9f1a5c4
Merge branch 'master' into parser-offset
mergify[bot] Jun 25, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ import Development.IDE.Core.RuleTypes
import Development.IDE.Core.Shake (IdeState (..))
import Development.IDE.Core.UseStale
import Development.IDE.GHC.Compat
import GhcPlugins (containsSpan, realSrcLocSpan)
import GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart)
import Ide.Types
import Language.LSP.Types
import Prelude hiding (span)
Expand Down Expand Up @@ -50,8 +50,9 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
Just (trss, program) -> do
let tr_range = fmap realSrcSpanToRange trss
rsl = realSrcSpanStart $ unTrack trss
HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
z <- liftIO $ attempt_it ctx jdg $ T.unpack program
z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program
pure $ Hover
{ _contents = HoverContents
$ MarkupContent MkMarkdown
Expand Down
21 changes: 18 additions & 3 deletions plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ import Wingman.Metaprogramming.Parser.Documentation
import Wingman.Metaprogramming.ProofState (proofState, layout)
import Wingman.Tactics
import Wingman.Types
import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
import FastString (unpackFS)


nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
Expand Down Expand Up @@ -421,17 +423,30 @@ wrapError :: String -> String
wrapError err = "```\n" <> err <> "\n```\n"


fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b
fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s))
= P.ParseErrorBundle ne
$ P.PosState a n
(P.SourcePos
(unpackFS $ srcLocFile rsl)
((<>) line $ P.mkPos $ srcLocLine rsl - 1)
((<>) col $ P.mkPos $ srcLocCol rsl - 1 + length @[] "[wingman|")
)
pos
s

------------------------------------------------------------------------------
-- | Attempt to run a metaprogram tactic, returning the proof state, or the
-- errors.
attempt_it
:: Context
:: RealSrcLoc
-> Context
-> Judgement
-> String
-> IO (Either String String)
attempt_it ctx jdg program =
attempt_it rsl ctx jdg program =
case P.runParser tacticProgram "<splice>" (T.pack program) of
Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty peb
Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb
Right tt -> do
res <- runTactic
ctx
Expand Down