Skip to content
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.

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

Attempt to repro CI failures in tactics #522

Closed
wants to merge 3 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions plugins/tactics/hls-tactics-plugin.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ library
, syb
, text
, transformers
, deepseq

default-language: Haskell2010

47 changes: 30 additions & 17 deletions plugins/tactics/src/Ide/Plugin/Tactic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import Data.Coerce
import Data.Generics.Aliases (mkQ)
import Data.Generics.Schemes (everything)
import Data.List
import qualified Data.Foldable as F
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid
Expand Down Expand Up @@ -101,6 +102,10 @@ commandProvider Auto = provide Auto ""
commandProvider Intros =
filterGoalType isFunction $
provide Intros ""
commandProvider Split =
filterGoalType (isJust . algebraicTyCon) $
foldMapGoalType (F.fold . tyDataCons) $ \dc ->
provide Split $ T.pack $ occNameString $ getOccName dc
commandProvider Destruct =
filterBindingType destructFilter $ \occ _ ->
provide Destruct $ T.pack $ occNameString occ
Expand All @@ -119,11 +124,12 @@ commandProvider HomomorphismLambdaCase =

------------------------------------------------------------------------------
-- | A mapping from tactic commands to actual tactics for refinery.
commandTactic :: TacticCommand -> OccName -> TacticsM ()
commandTactic :: TacticCommand -> String -> TacticsM ()
commandTactic Auto = const auto
commandTactic Intros = const intros
commandTactic Destruct = destruct
commandTactic Homomorphism = homo
commandTactic Split = splitDataCon' . mkDataOcc
commandTactic Destruct = destruct . mkVarOcc
commandTactic Homomorphism = homo . mkVarOcc
commandTactic DestructLambdaCase = const destructLambdaCase
commandTactic HomomorphismLambdaCase = const homoLambdaCase

Expand Down Expand Up @@ -194,6 +200,14 @@ requireExtension ext tp dflags plId uri range jdg =
False -> pure []


------------------------------------------------------------------------------
-- | Create a 'TacticProvider' for each occurance of an 'a' in the foldable container
-- extracted from the goal type. Useful instantiations for 't' include 'Maybe' or '[]'.
foldMapGoalType :: Foldable t => (Type -> t a) -> (a -> TacticProvider) -> TacticProvider
foldMapGoalType f tpa dflags plId uri range jdg =
foldMap tpa (f $ unCType $ jGoal jdg) dflags plId uri range jdg


------------------------------------------------------------------------------
-- | Restrict a 'TacticProvider', making sure it appears only when the given
-- predicate holds for the goal.
Expand Down Expand Up @@ -280,7 +294,7 @@ judgementForHole state nfp range = do



tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
tacticCmd :: (String -> TacticsM ()) -> CommandFunction TacticParams
tacticCmd tac lf state (TacticParams uri range var_name)
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
fromMaybeT (Right Null, Nothing) $ do
Expand All @@ -289,19 +303,18 @@ tacticCmd tac lf state (TacticParams uri range var_name)
pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
x <- lift $ timeout 2e8 $
case runTactic ctx jdg
$ tac
$ mkVarOcc
$ T.unpack var_name of
Left err ->
pure $ (, Nothing)
$ Left
$ ResponseError InvalidRequest (T.pack $ show err) Nothing
Right (_, ext) -> do
let g = graft (RealSrcSpan span) ext
response = transform dflags (clientCapabilities lf) uri g pm
pure $ case response of
Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
$ tac
$ T.unpack var_name of
Left err ->
pure $ (, Nothing)
$ Left
$ ResponseError InvalidRequest (T.pack $ show err) Nothing
Right (_, ext) -> do
let g = graft (RealSrcSpan span) ext
response = transform dflags (clientCapabilities lf) uri g pm
pure $ case response of
Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
pure $ case x of
Just y -> y
Nothing -> (, Nothing)
Expand Down
25 changes: 24 additions & 1 deletion plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,7 @@
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeApplications #-}

module Ide.Plugin.Tactic.Debug
( unsafeRender
, unsafeRender'
Expand All @@ -9,17 +13,36 @@ module Ide.Plugin.Tactic.Debug
, traceMX
) where

import Control.DeepSeq
import Control.Exception
import Debug.Trace
import DynFlags (unsafeGlobalDynFlags)
import Outputable hiding ((<>))
import System.IO.Unsafe (unsafePerformIO)

#if __GLASGOW_HASKELL__ >= 808
import PlainPanic (PlainGhcException)
type GHC_EXCEPTION = PlainGhcException
#else
import Panic (GhcException)
type GHC_EXCEPTION = GhcException
#endif


------------------------------------------------------------------------------
-- | Print something
unsafeRender :: Outputable a => a -> String
unsafeRender = unsafeRender' . ppr


unsafeRender' :: SDoc -> String
unsafeRender' = showSDoc unsafeGlobalDynFlags
unsafeRender' sdoc = unsafePerformIO $ do
let z = showSDoc unsafeGlobalDynFlags sdoc
-- We might not have unsafeGlobalDynFlags (like during testing), in which
-- case GHC panics. Instead of crashing, let's just fail to print.
!res <- try @GHC_EXCEPTION $ evaluate $ deepseq z z
pure $ either (const "<unsafeRender'>") id res
{-# NOINLINE unsafeRender' #-}

traceMX :: (Monad m, Show a) => String -> a -> m ()
traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
Expand Down
8 changes: 8 additions & 0 deletions plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module Ide.Plugin.Tactic.GHC where
import Data.Maybe (isJust)
import Development.IDE.GHC.Compat
import OccName
import DataCon
import TcType
import TyCoRep
import Type
Expand Down Expand Up @@ -106,3 +107,10 @@ getPatName (fromPatCompat -> p0) =
#endif
_ -> Nothing

------------------------------------------------------------------------------
-- | What data-constructor, if any, does the type have?
tyDataCons :: Type -> Maybe [DataCon]
tyDataCons g = do
(tc, _) <- splitTyConApp_maybe g
pure $ tyConDataCons tc

23 changes: 19 additions & 4 deletions plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -194,10 +194,9 @@ split :: TacticsM ()
split = tracing "split(user)" $ do
jdg <- goal
let g = jGoal jdg
case splitTyConApp_maybe $ unCType g of
Nothing -> throwError $ GoalMismatch "split" g
Just (tc, _) -> do
let dcs = tyConDataCons tc
case tyDataCons $ unCType g of
Nothing -> throwError $ GoalMismatch "split(user)" g
Just dcs -> do
choice $ fmap splitDataCon dcs


Expand Down Expand Up @@ -235,6 +234,22 @@ splitDataCon dc = tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
Nothing -> throwError $ GoalMismatch "splitDataCon" g


------------------------------------------------------------------------------
-- | Attempt to instantiate the named data constructor to solve the goal.
splitDataCon' :: OccName -> TacticsM ()
splitDataCon' dcn = do
let tacname = "splitDataCon'(" ++ unsafeRender dcn ++ ")"
jdg <- goal
let g = jGoal jdg
case tyDataCons $ unCType g of
Nothing -> throwError $ GoalMismatch tacname g
Just dcs -> do
let mdc = find ((== dcn) . getOccName) dcs
case mdc of
Nothing -> throwError $ GoalMismatch tacname g
Just dc -> splitDataCon dc


------------------------------------------------------------------------------
-- | @matching f@ takes a function from a judgement to a @Tactic@, and
-- then applies the resulting @Tactic@.
Expand Down
2 changes: 2 additions & 0 deletions plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import qualified Data.Text as T
data TacticCommand
= Auto
| Intros
| Split
| Destruct
| Homomorphism
| DestructLambdaCase
Expand All @@ -21,6 +22,7 @@ data TacticCommand
tacticTitle :: TacticCommand -> T.Text -> T.Text
tacticTitle Auto _ = "Attempt to fill hole"
tacticTitle Intros _ = "Introduce lambda"
tacticTitle Split cname = "Introduce constructor " <> cname
tacticTitle Destruct var = "Case split on " <> var
tacticTitle Homomorphism var = "Homomorphic case split on " <> var
tacticTitle DestructLambdaCase _ = "Lambda case split"
Expand Down
1 change: 1 addition & 0 deletions stack.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ packages:
- .
- ./ghcide/
- ./hls-plugin-api
- ./plugins/tactics

ghc-options:
"$everything": -haddock
Expand Down
26 changes: 26 additions & 0 deletions test/functional/Tactic.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumDecimals #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
Expand All @@ -21,9 +22,11 @@ import Language.Haskell.LSP.Types (ApplyWorkspaceEditRequest, Position
import Test.Hls.Util
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.ExpectedFailure (ignoreTestBecause)
import System.FilePath
import System.Directory (doesFileExist)
import Control.Monad (unless)
import Control.Concurrent (threadDelay)


------------------------------------------------------------------------------
Expand Down Expand Up @@ -80,6 +83,27 @@ tests = testGroup
"T3.hs" 7 13
[ (id, DestructLambdaCase, "")
]
, ignoreTestBecause "Not implemented, see isovector/haskell-language-server#31" $ mkTest
"Splits Int with I# when -XMagicHash is enabled"
"T3.hs" 10 14
[ (id, Split, "I#")
]
, mkTest
"Produces datatype split action for single-constructor types"
"T2.hs" 16 14
[ (id, Split, "T")
]
, mkTest
"Produces datatype split action for multiple constructors"
"T2.hs" 21 15
[ (id, Split, "T21")
, (id, Split, "T22")
]
, mkTest
"Doesn't suggest MagicHash constructors without -XMagicHash"
"T2.hs" 24 14
[ (not, Split, "I#")
]
, mkTest
"Doesn't suggest lambdacase without -XLambdaCase"
"T2.hs" 11 25
Expand All @@ -101,6 +125,7 @@ tests = testGroup
, goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt"
, goldenTest "GoldenGADTAuto.hs" 7 13 Auto ""
, goldenTest "GoldenSwapMany.hs" 2 12 Auto ""
, goldenTest "GoldenSplitPair.hs" 2 11 Split "(,)"
]


Expand Down Expand Up @@ -134,6 +159,7 @@ goldenTest :: FilePath -> Int -> Int -> TacticCommand -> Text -> TestTree
goldenTest input line col tc occ =
testCase (input <> " (golden)") $ do
runSession hlsCommand fullCaps tacticPath $ do
liftIO $ threadDelay (length input * 1e6)
doc <- openDoc input "haskell"
actions <- getCodeActions doc $ pointRange line col
Just (CACodeAction (CodeAction {_command = Just c}))
Expand Down
2 changes: 2 additions & 0 deletions test/testdata/tactic/GoldenSplitPair.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
thePair :: (Int, Int)
thePair = _
2 changes: 2 additions & 0 deletions test/testdata/tactic/GoldenSplitPair.hs.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
thePair :: (Int, Int)
thePair = (_, _)
12 changes: 12 additions & 0 deletions test/testdata/tactic/T2.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,15 @@ foo = _
dontSuggestLambdaCase :: Either a b -> Int
dontSuggestLambdaCase = _

data T = T !(Int, Int)

suggestCon :: T
suggestCon = _

data T2 = T21 Int | T22 Int Int

suggestCons :: T2
suggestCons = _

suggestInt :: Int
suggestInt = _
4 changes: 3 additions & 1 deletion test/testdata/tactic/T3.hs
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LambdaCase, MagicHash #-}

suggestHomomorphicLC :: Either a b -> Either a b
suggestHomomorphicLC = _

suggestLC :: Either a b -> Int
suggestLC = _

suggestInt :: Int
suggestInt = _