Stick judgment and context into the RTR

Author: isovector

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs

@@ -182,7 +182,7 @@ tacticCmd tac state (TacticParams uri range var_name)
             Left err ->
               Left $ mkErr InvalidRequest $ T.pack $ show err
             Right rtr ->
-              mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm
+              mkWorkspaceEdits rtr span dflags clientCapabilities uri pm
         pure $ joinNote (mkErr InvalidRequest "timed out") x
 
       case res of
@@ -206,8 +206,8 @@ joinNote _ (Just a) = a
 ------------------------------------------------------------------------------
 -- | Turn a 'RunTacticResults' into concrete edits to make in the source
 -- document.
-mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm = do
-  let g = graftHole jdg (RealSrcSpan span) ctx rtr
+mkWorkspaceEdits rtr span dflags clientCapabilities uri pm = do
+  let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags clientCapabilities uri g pm
    in case response of
         Right res -> Right $ Just res
@@ -219,25 +219,22 @@ mkWorkspaceEdits rtr jdg span ctx dflags clientCapabilities uri pm = do
 -- deals with top-level holes, in which we might need to fiddle with the
 -- 'Match's that bind variables.
 graftHole
-  :: Judgement' a2
-  -> SrcSpan
-  -> Context
-  -> RunTacticResults
-  -> Graft (Either String) ParsedSource
-graftHole jdg span ctx rtr
-  | _jIsTopHole jdg
+    :: SrcSpan
+    -> RunTacticResults
+    -> Graft (Either String) ParsedSource
+graftHole span rtr
+  | _jIsTopHole (rtr_jdg rtr)
       = graftSmallestDeclsWithM span
-      $ graftDecl span
-      $ \pats ->
-        splitToDecl (fst $ last $ ctxDefiningFuncs ctx)
+      $ graftDecl span $ \pats ->
+        splitToDecl (fst $ last $ ctxDefiningFuncs $ rtr_ctx rtr)
       $ iterateSplit
       $ mkFirstAgda (fmap unXPat pats)
       $ unLoc
       $ rtr_extract rtr
-graftHole jdg span _ rtr
+graftHole span rtr
   = graftWithoutParentheses span
     -- Parenthesize the extract iff we're not in a top level hole
-  $ bool maybeParensAST id (_jIsTopHole jdg)
+  $ bool maybeParensAST id (_jIsTopHole $ rtr_jdg rtr)
   $ rtr_extract rtr
 
 

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs

@@ -97,11 +97,14 @@ runTactic ctx jdg t =
                 Down $ scoreSolution ext jdg holes
         case sorted of
           (((tr, ext), _) : _) ->
-            Right
-              . RunTacticResults tr (simplify ext)
-              . reverse
-              . fmap fst
-              $ take 5 sorted
+            Right $
+              RunTacticResults
+                { rtr_trace = tr
+                , rtr_extract = simplify ext
+                , rtr_other_solns = reverse . fmap fst $ take 5 sorted
+                , rtr_jdg = jdg
+                , rtr_ctx = ctx
+                }
           -- guaranteed to not be empty
           _ -> Left []
 

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs

@@ -337,7 +337,7 @@ data Context = Context
   , ctxModuleFuncs :: [(OccName, CType)]
     -- ^ Everything defined in the current module
   }
-  deriving stock (Eq, Ord)
+  deriving stock (Eq, Ord, Show)
 
 
 ------------------------------------------------------------------------------
@@ -374,6 +374,8 @@ data RunTacticResults = RunTacticResults
   { rtr_trace       :: Trace
   , rtr_extract     :: LHsExpr GhcPs
   , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]
+  , rtr_jdg         :: Judgement
+  , rtr_ctx         :: Context
   } deriving Show