Wingman: Low gas warning (#2038)

* Simplify TacticError

* OutOfGas machinery

* Not enough gas test

Co-authored-by: Javier Neira <[email protected]>

Author: isovector

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

@@ -485,6 +485,7 @@ isRhsHole (unTrack -> rss) (unTrack -> tcs) =
 
 
 ufmSeverity :: UserFacingMessage -> MessageType
+ufmSeverity NotEnoughGas            = MtInfo
 ufmSeverity TacticErrors            = MtError
 ufmSeverity TimedOut                = MtInfo
 ufmSeverity NothingToDo             = MtInfo

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

@@ -225,7 +225,7 @@ unify goal inst = do
   case tryUnifyUnivarsButNotSkolems skolems goal inst of
     Just subst ->
       modify $ updateSubst subst
-    Nothing -> cut -- failure (UnificationError inst goal)
+    Nothing -> cut
 
 cut :: RuleT jdg ext err s m a
 cut = RuleT Empty

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

@@ -100,6 +100,12 @@ showUserFacingMessage ufm = do
   pure $ Left $ mkErr InternalError $ T.pack $ show ufm
 
 
+mkUserFacingMessage :: [TacticError] -> UserFacingMessage
+mkUserFacingMessage errs
+  | elem OutOfGas errs = NotEnoughGas
+mkUserFacingMessage _ = TacticErrors
+
+
 tacticCmd
     :: (T.Text -> TacticsM ())
     -> PluginId
@@ -122,7 +128,7 @@ tacticCmd tac pId state (TacticParams uri range var_name)
           pure $ join $ case res of
             Left errs ->  do
               traceMX "errs" errs
-              Left TacticErrors
+              Left $ mkUserFacingMessage errs
             Right rtr ->
               case rtr_extract rtr of
                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->

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

@@ -65,7 +65,7 @@ assume name = rule $ \jdg -> do
           { syn_trace = tracePrim $ "assume " <> occNameString name
           , syn_used_vals = S.singleton name
           }
-    Nothing -> cut -- failure $ UndefinedHypothesis name
+    Nothing -> cut
 
 
 ------------------------------------------------------------------------------
@@ -432,7 +432,7 @@ refine = intros <%> splitSingle
 
 
 auto' :: Int -> TacticsM ()
-auto' 0 = failure NoProgress
+auto' 0 = failure OutOfGas
 auto' n = do
   let loop = auto' (n - 1)
   try intros

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

@@ -361,61 +361,40 @@ instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where
 ------------------------------------------------------------------------------
 -- | Reasons a tactic might fail.
 data TacticError
-  = UndefinedHypothesis OccName
+  = OutOfGas
   | GoalMismatch String CType
-  | UnsolvedSubgoals [Judgement]
-  | UnificationError CType CType
   | NoProgress
   | NoApplicableTactic
-  | IncorrectDataCon DataCon
-  | RecursionOnWrongParam OccName Int OccName
   | UnhelpfulRecursion
   | UnhelpfulDestruct OccName
-  | UnhelpfulSplit OccName
   | TooPolymorphic
   | NotInScope OccName
   | TacticPanic String
+  deriving (Eq)
 
 instance Show TacticError where
-    show (UndefinedHypothesis name) =
-      occNameString name <> " is not available in the hypothesis."
+    show OutOfGas = "Auto ran out of gas"
     show (GoalMismatch tac (CType typ)) =
       mconcat
         [ "The tactic "
         , tac
         , " doesn't apply to goal type "
         , unsafeRender typ
         ]
-    show (UnsolvedSubgoals _) =
-      "There were unsolved subgoals"
-    show (UnificationError (CType t1) (CType t2)) =
-        mconcat
-          [ "Could not unify "
-          , unsafeRender t1
-          , " and "
-          , unsafeRender t2
-          ]
     show NoProgress =
       "Unable to make progress"
     show NoApplicableTactic =
       "No tactic could be applied"
-    show (IncorrectDataCon dcon) =
-      "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"
-    show (RecursionOnWrongParam call p arg) =
-      "Recursion on wrong param (" <> show call <> ") on arg"
-        <> show p <> ": " <> show arg
     show UnhelpfulRecursion =
       "Recursion wasn't productive"
     show (UnhelpfulDestruct n) =
       "Destructing patval " <> show n <> " leads to no new types"
-    show (UnhelpfulSplit n) =
-      "Splitting constructor " <> show n <> " leads to no new goals"
     show TooPolymorphic =
       "The tactic isn't applicable because the goal is too polymorphic"
     show (NotInScope name) =
       "Tried to do something with the out of scope name " <> show name
     show (TacticPanic err) =
-      "PANIC: " <> err
+      "Tactic panic: " <> err
 
 
 ------------------------------------------------------------------------------
@@ -560,16 +539,18 @@ data AgdaMatch = AgdaMatch
 
 
 data UserFacingMessage
-  = TacticErrors
+  = NotEnoughGas
+  | TacticErrors
   | TimedOut
   | NothingToDo
   | InfrastructureError Text
   deriving Eq
 
 instance Show UserFacingMessage where
-  show TacticErrors            = "Wingman couldn't find a solution"
-  show TimedOut                = "Wingman timed out while trying to find a solution"
-  show NothingToDo             = "Nothing to do"
+  show NotEnoughGas = "Wingman ran out of gas when trying to find a solution.  \nTry increasing the `auto_gas` setting."
+  show TacticErrors = "Wingman couldn't find a solution"
+  show TimedOut     = "Wingman timed out while trying to find a solution"
+  show NothingToDo  = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
 

plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs

@@ -83,6 +83,7 @@ spec = do
 
 
   describe "messages" $ do
-    mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors
-    mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors
+    mkShowMessageTest Auto ""  2 8 "MessageForallA"      TacticErrors
+    mkShowMessageTest Auto ""  7 8 "MessageCantUnify"    TacticErrors
+    mkShowMessageTest Auto "" 12 8 "MessageNotEnoughGas" NotEnoughGas
 

plugins/hls-tactics-plugin/test/golden/MessageNotEnoughGas.hs

@@ -0,0 +1,13 @@
+test
+   :: (a1 -> a2)
+   -> (a2 -> a3)
+   -> (a3 -> a4)
+   -> (a4 -> a5)
+   -> (a5 -> a6)
+   -> (a6 -> a7)
+   -> (a7 -> a8)
+   -> (a8 -> a9)
+   -> (a9 -> a10)
+   -> a1 -> a10
+test = _
+