From 2311c1b9daf0216995ffcbab5cffbbb4a7997cbf Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 26 Jul 2021 09:13:08 -0700 Subject: [PATCH 1/3] Simplify TacticError --- .../src/Wingman/Machinery.hs | 2 +- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 2 +- .../hls-tactics-plugin/src/Wingman/Types.hs | 33 ++++--------------- 3 files changed, 9 insertions(+), 28 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index 499a1b48bc..9eb6e1dc62 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index c582b2c729..db980dfacd 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/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 ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index d15893f3b1..edd7ec1487 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -366,15 +366,10 @@ instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where data TacticError = UndefinedHypothesis OccName | 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 @@ -389,36 +384,20 @@ instance Show TacticError where , " 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 ------------------------------------------------------------------------------ @@ -563,16 +542,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 From 00897a19c8a9d51f09bb113e524c8fb58b5a2a0a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 26 Jul 2021 09:13:21 -0700 Subject: [PATCH 2/3] OutOfGas machinery --- plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs | 1 + plugins/hls-tactics-plugin/src/Wingman/Plugin.hs | 8 +++++++- plugins/hls-tactics-plugin/src/Wingman/Tactics.hs | 2 +- plugins/hls-tactics-plugin/src/Wingman/Types.hs | 6 +++--- 4 files changed, 12 insertions(+), 5 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs index 2c95db5d61..02e9da6a87 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs b/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs index abec9914a0..8cd6fa1c9d 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Plugin.hs +++ b/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) -> diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index db980dfacd..8829b5cfb6 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs index edd7ec1487..679e97a58a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs @@ -364,7 +364,7 @@ instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where ------------------------------------------------------------------------------ -- | Reasons a tactic might fail. data TacticError - = UndefinedHypothesis OccName + = OutOfGas | GoalMismatch String CType | NoProgress | NoApplicableTactic @@ -373,10 +373,10 @@ data TacticError | 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 " From df7f96b579b8f4c4ff0e349611da2da9e357f167 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 26 Jul 2021 09:24:25 -0700 Subject: [PATCH 3/3] Not enough gas test --- .../hls-tactics-plugin/test/CodeAction/AutoSpec.hs | 5 +++-- .../test/golden/MessageNotEnoughGas.hs | 13 +++++++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/MessageNotEnoughGas.hs diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index c776e2015a..94d266554e 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/test/golden/MessageNotEnoughGas.hs b/plugins/hls-tactics-plugin/test/golden/MessageNotEnoughGas.hs new file mode 100644 index 0000000000..9156cc0053 --- /dev/null +++ b/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 = _ +