Track remaining subgoals for interactive proofstate

Author: isovector

plugins/hls-tactics-plugin/src/Wingman/Machinery.hs

@@ -82,11 +82,12 @@ runTactic ctx jdg t =
               flip sortBy solns $ comparing $ \(ext, (_, holes)) ->
                 Down $ scoreSolution ext jdg holes
         case sorted of
-          ((syn, _) : _) ->
+          ((syn, (_, subgoals)) : _) ->
             Right $
               RunTacticResults
-                { rtr_trace = syn_trace syn
-                , rtr_extract = simplify $ syn_val syn
+                { rtr_trace    = syn_trace syn
+                , rtr_extract  = simplify $ syn_val syn
+                , rtr_subgoals = subgoals
                 , rtr_other_solns = reverse . fmap fst $ sorted
                 , rtr_jdg = jdg
                 , rtr_ctx = ctx

plugins/hls-tactics-plugin/src/Wingman/Types.hs

@@ -476,6 +476,7 @@ rose a rs = Rose $ Node a $ coerce rs
 data RunTacticResults = RunTacticResults
   { rtr_trace       :: Trace
   , rtr_extract     :: LHsExpr GhcPs
+  , rtr_subgoals    :: [Judgement]
   , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
   , rtr_jdg         :: Judgement
   , rtr_ctx         :: Context