diff --git a/hls-tactics-plugin.cabal b/hls-tactics-plugin.cabal --- a/hls-tactics-plugin.cabal +++ b/hls-tactics-plugin.cabal @@ -1,7 +1,7 @@ cabal-version: 2.4 category: Development name: hls-tactics-plugin -version: 1.3.0.0 +version: 1.4.0.0 synopsis: Wingman plugin for Haskell Language Server description: Please see the README on GitHub at @@ -28,6 +28,10 @@ hs-source-dirs: src exposed-modules: Ide.Plugin.Tactic + Refinery.Future + Wingman.AbstractLSP + Wingman.AbstractLSP.TacticActions + Wingman.AbstractLSP.Types Wingman.Auto Wingman.CaseSplit Wingman.CodeGen @@ -91,6 +95,7 @@ , refinery ^>=0.4 , retrie >=0.1.1.0 , syb + , unagi-chan , text , transformers , unordered-containers @@ -130,6 +135,7 @@ CodeAction.DestructPunSpec CodeAction.DestructSpec CodeAction.IntrosSpec + CodeAction.IntroDestructSpec CodeAction.RefineSpec CodeAction.RunMetaprogramSpec CodeAction.UseDataConSpec diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,9 +1,5 @@ -- | A plugin that uses tactics to synthesize code -module Ide.Plugin.Tactic - ( descriptor - , tacticTitle - , TacticCommand (..) - ) where +module Ide.Plugin.Tactic (descriptor) where import Wingman.Plugin diff --git a/src/Refinery/Future.hs b/src/Refinery/Future.hs new file mode 100644 --- /dev/null +++ b/src/Refinery/Future.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE RankNTypes #-} + +------------------------------------------------------------------------------ +-- | Things that belong in the future release of refinery v5. +module Refinery.Future + ( runStreamingTacticT + , hoistListT + , consume + ) where + +import Control.Applicative +import Control.Monad (ap, (>=>)) +import Control.Monad.State.Lazy (runStateT) +import Control.Monad.Trans +import Data.Either (isRight) +import Data.Functor ((<&>)) +import Data.Tuple (swap) +import Refinery.ProofState +import Refinery.Tactic.Internal + + + +hoistElem :: Functor m => (forall x. m x -> n x) -> Elem m a -> Elem n a +hoistElem _ Done = Done +hoistElem f (Next a lt) = Next a $ hoistListT f lt + + +hoistListT :: Functor m => (forall x. m x -> n x) -> ListT m a -> ListT n a +hoistListT f t = ListT $ f $ fmap (hoistElem f) $ unListT t + + +consume :: Monad m => ListT m a -> (a -> m ()) -> m () +consume lt f = unListT lt >>= \case + Done -> pure () + Next a lt' -> f a >> consume lt' f + + +newHole :: MonadExtract meta ext err s m => s -> m (s, (meta, ext)) +newHole = fmap swap . runStateT hole + +runStreamingTacticT :: (MonadExtract meta ext err s m) => TacticT jdg ext err s m () -> jdg -> s -> ListT m (Either err (Proof s meta jdg ext)) +runStreamingTacticT t j s = streamProofs s $ fmap snd $ proofState t j + +data Elem m a + = Done + | Next a (ListT m a) + deriving stock Functor + + +point :: Applicative m => a -> Elem m a +point a = Next a $ ListT $ pure Done + +newtype ListT m a = ListT { unListT :: m (Elem m a) } + +cons :: (Applicative m) => a -> ListT m a -> ListT m a +cons x xs = ListT $ pure $ Next x xs + +instance Functor m => Functor (ListT m) where + fmap f (ListT xs) = ListT $ xs <&> \case + Done -> Done + Next a xs -> Next (f a) (fmap f xs) + +instance (Monad m) => Applicative (ListT m) where + pure = return + (<*>) = ap + +instance (Monad m) => Alternative (ListT m) where + empty = ListT $ pure Done + (ListT xs) <|> (ListT ys) = + ListT $ xs >>= \case + Done -> ys + Next x xs -> pure (Next x (xs <|> ListT ys)) + +instance (Monad m) => Monad (ListT m) where + return a = cons a empty + (ListT xs) >>= k = + ListT $ xs >>= \case + Done -> pure Done + Next x xs -> unListT $ k x <|> (xs >>= k) + + +instance MonadTrans ListT where + lift m = ListT $ fmap (\x -> Next x empty) m + + +interleaveT :: (Monad m) => Elem m a -> Elem m a -> Elem m a +interleaveT xs ys = + case xs of + Done -> ys + Next x xs -> Next x $ ListT $ fmap (interleaveT ys) $ unListT xs + +-- ys <&> \case +-- Done -> Next x xs +-- Next y ys -> Next x (cons y (interleaveT xs ys)) + +force :: (Monad m) => Elem m a -> m [a] +force = \case + Done -> pure [] + Next x xs' -> (x:) <$> (unListT xs' >>= force) + +ofList :: Monad m => [a] -> Elem m a +ofList [] = Done +ofList (x:xs) = Next x $ ListT $ pure $ ofList xs + +streamProofs :: forall ext err s m goal meta. (MonadExtract meta ext err s m) => s -> ProofStateT ext ext err s m goal -> ListT m (Either err (Proof s meta goal ext)) +streamProofs s p = ListT $ go s [] pure p + where + go :: s -> [(meta, goal)] -> (err -> m err) -> ProofStateT ext ext err s m goal -> m (Elem m (Either err (Proof s meta goal ext))) + go s goals _ (Subgoal goal k) = do + (s', (meta, h)) <- newHole s + -- Note [Handler Reset]: + -- We reset the handler stack to avoid the handlers leaking across subgoals. + -- This would happen when we had a handler that wasn't followed by an error call. + -- pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error" + -- We would see the "Handling a" message when solving for b. + (go s' (goals ++ [(meta, goal)]) pure $ k h) + go s goals handlers (Effect m) = m >>= go s goals handlers + go s goals handlers (Stateful f) = + let (s', p) = f s + in go s' goals handlers p + go s goals handlers (Alt p1 p2) = + unListT $ ListT (go s goals handlers p1) <|> ListT (go s goals handlers p2) + go s goals handlers (Interleave p1 p2) = + interleaveT <$> (go s goals handlers p1) <*> (go s goals handlers p2) + go s goals handlers (Commit p1 p2) = do + solns <- force =<< go s goals handlers p1 + if (any isRight solns) then pure $ ofList solns else go s goals handlers p2 + go _ _ _ Empty = pure Done + go _ _ handlers (Failure err _) = do + annErr <- handlers err + pure $ point $ Left annErr + go s goals handlers (Handle p h) = + -- Note [Handler ordering]: + -- If we have multiple handlers in scope, then we want the handlers closer to the error site to + -- run /first/. This allows the handlers up the stack to add their annotations on top of the + -- ones lower down, which is the behavior that we desire. + -- IE: for @handler f >> handler g >> failure err@, @g@ ought to be run before @f@. + go s goals (h >=> handlers) p + go s goals _ (Axiom ext) = pure $ point $ Right (Proof ext s goals) + diff --git a/src/Wingman/AbstractLSP.hs b/src/Wingman/AbstractLSP.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/AbstractLSP.hs @@ -0,0 +1,270 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} + +{-# LANGUAGE NoMonoLocalBinds #-} + +{-# OPTIONS_GHC -Wno-orphans #-} + +module Wingman.AbstractLSP (installInteractions) where + +import Control.Monad (void) +import Control.Monad.IO.Class +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (MaybeT, mapMaybeT) +import qualified Data.Aeson as A +import Data.Coerce +import Data.Foldable (traverse_) +import Data.Monoid (Last (..)) +import qualified Data.Text as T +import Data.Traversable (for) +import Data.Tuple.Extra (uncurry3) +import Development.IDE (IdeState) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.ExactPrint (GetAnnotatedParsedSource(GetAnnotatedParsedSource)) +import qualified Ide.Plugin.Config as Plugin +import Ide.Types +import Language.LSP.Server (LspM, sendRequest, getClientCapabilities) +import qualified Language.LSP.Types as LSP +import Language.LSP.Types hiding (CodeLens, CodeAction) +import Wingman.AbstractLSP.Types +import Wingman.EmptyCase (fromMaybeT) +import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde, showLspMessage, mkShowMessageParams) +import Wingman.Types + + +------------------------------------------------------------------------------ +-- | Attact the 'Interaction's to a 'PluginDescriptor'. Interactions are +-- self-contained request/response pairs that abstract over the LSP, and +-- provide a unified interface for doing interesting things, without needing to +-- dive into the underlying API too directly. +installInteractions + :: [Interaction] + -> PluginDescriptor IdeState + -> PluginDescriptor IdeState +installInteractions is desc = + let plId = pluginId desc + in desc + { pluginCommands = pluginCommands desc <> fmap (buildCommand plId) is + , pluginHandlers = pluginHandlers desc <> buildHandlers is + } + + +------------------------------------------------------------------------------ +-- | Extract 'PluginHandlers' from 'Interaction's. +buildHandlers + :: [Interaction] + -> PluginHandlers IdeState +buildHandlers cs = + flip foldMap cs $ \(Interaction (c :: Continuation sort target b)) -> + case c_makeCommand c of + SynthesizeCodeAction k -> + mkPluginHandler STextDocumentCodeAction $ codeActionProvider @target (c_sort c) k + SynthesizeCodeLens k -> + mkPluginHandler STextDocumentCodeLens $ codeLensProvider @target (c_sort c) k + + +------------------------------------------------------------------------------ +-- | Extract a 'PluginCommand' from an 'Interaction'. +buildCommand + :: PluginId + -> Interaction + -> PluginCommand IdeState +buildCommand plId (Interaction (c :: Continuation sort target b)) = + PluginCommand + { commandId = toCommandId $ c_sort c + , commandDesc = T.pack "" + , commandFunc = runContinuation plId c + } + + +------------------------------------------------------------------------------ +-- | Boilerplate for running a 'Continuation' as part of an LSP command. +runContinuation + :: forall sort a b + . IsTarget a + => PluginId + -> Continuation sort a b + -> CommandFunction IdeState (FileContext, b) +runContinuation plId cont state (fc, b) = do + fromMaybeT + (Left $ ResponseError + { _code = InternalError + , _message = T.pack "TODO(sandy)" + , _xdata = Nothing + } ) $ do + env@LspEnv{..} <- buildEnv state plId fc + let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a + args <- fetchTargetArgs @a env + res <- c_runCommand cont env args fc b + + -- This block returns a maybe error. + fmap (maybe (Right $ A.Null) Left . coerce . foldMap Last) $ + for res $ \case + ErrorMessages errs -> do + traverse_ showUserFacingMessage errs + pure Nothing + RawEdit edits -> do + sendEdits edits + pure Nothing + GraftEdit gr -> do + ccs <- lift getClientCapabilities + TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of + Left errs -> + pure $ Just $ ResponseError + { _code = InternalError + , _message = T.pack $ show errs + , _xdata = Nothing + } + Right edits -> do + sendEdits edits + pure $ Nothing + + +------------------------------------------------------------------------------ +-- | Push a 'WorkspaceEdit' to the client. +sendEdits :: WorkspaceEdit -> MaybeT (LspM Plugin.Config) () +sendEdits edits = + void $ lift $ + sendRequest + SWorkspaceApplyEdit + (ApplyWorkspaceEditParams Nothing edits) + (const $ pure ()) + + +------------------------------------------------------------------------------ +-- | Push a 'UserFacingMessage' to the client. +showUserFacingMessage + :: UserFacingMessage + -> MaybeT (LspM Plugin.Config) () +showUserFacingMessage ufm = + void $ lift $ showLspMessage $ mkShowMessageParams ufm + + +------------------------------------------------------------------------------ +-- | Build an 'LspEnv', which contains the majority of things we need to know +-- in a 'Continuation'. +buildEnv + :: IdeState + -> PluginId + -> FileContext + -> MaybeT (LspM Plugin.Config) LspEnv +buildEnv state plId fc = do + cfg <- lift $ getTacticConfig plId + dflags <- mapMaybeT liftIO $ getIdeDynflags state $ fc_nfp fc + pure $ LspEnv + { le_ideState = state + , le_pluginId = plId + , le_dflags = dflags + , le_config = cfg + , le_fileContext = fc + } + + +------------------------------------------------------------------------------ +-- | Lift a 'Continuation' into an LSP CodeAction. +codeActionProvider + :: forall target sort b + . (IsContinuationSort sort, A.ToJSON b, IsTarget target) + => sort + -> ( LspEnv + -> TargetArgs target + -> MaybeT (LspM Plugin.Config) [(Metadata, b)] + ) + -> PluginMethodHandler IdeState TextDocumentCodeAction +codeActionProvider sort k state plId + (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + fromMaybeT (Right $ List []) $ do + let fc = FileContext + { fc_uri = uri + , fc_nfp = nfp + , fc_range = Just $ unsafeMkCurrent range + } + env <- buildEnv state plId fc + args <- fetchTargetArgs @target env + actions <- k env args + pure + $ Right + $ List + $ fmap (InR . uncurry (makeCodeAction plId fc sort)) actions +codeActionProvider _ _ _ _ _ = pure $ Right $ List [] + + +------------------------------------------------------------------------------ +-- | Lift a 'Continuation' into an LSP CodeLens. +codeLensProvider + :: forall target sort b + . (IsContinuationSort sort, A.ToJSON b, IsTarget target) + => sort + -> ( LspEnv + -> TargetArgs target + -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] + ) + -> PluginMethodHandler IdeState TextDocumentCodeLens +codeLensProvider sort k state plId + (CodeLensParams _ _ (TextDocumentIdentifier uri)) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + fromMaybeT (Right $ List []) $ do + let fc = FileContext + { fc_uri = uri + , fc_nfp = nfp + , fc_range = Nothing + } + env <- buildEnv state plId fc + args <- fetchTargetArgs @target env + actions <- k env args + pure + $ Right + $ List + $ fmap (uncurry3 $ makeCodeLens plId sort fc) actions +codeLensProvider _ _ _ _ _ = pure $ Right $ List [] + + +------------------------------------------------------------------------------ +-- | Build a 'LSP.CodeAction'. +makeCodeAction + :: (A.ToJSON b, IsContinuationSort sort) + => PluginId + -> FileContext + -> sort + -> Metadata + -> b + -> LSP.CodeAction +makeCodeAction plId fc sort (Metadata title kind preferred) b = + let cmd_id = toCommandId sort + cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON (fc, b)] + in LSP.CodeAction + { _title = title + , _kind = Just kind + , _diagnostics = Nothing + , _isPreferred = Just preferred + , _disabled = Nothing + , _edit = Nothing + , _command = Just cmd + , _xdata = Nothing + } + + +------------------------------------------------------------------------------ +-- | Build a 'LSP.CodeLens'. +makeCodeLens + :: (A.ToJSON b, IsContinuationSort sort) + => PluginId + -> sort + -> FileContext + -> Range + -> Metadata + -> b + -> LSP.CodeLens +makeCodeLens plId sort fc range (Metadata title _ _) b = + let fc' = fc { fc_range = Just $ unsafeMkCurrent range } + cmd_id = toCommandId sort + cmd = mkLspCommand plId cmd_id title $ Just [A.toJSON (fc', b)] + in LSP.CodeLens + { _range = range + , _command = Just cmd + , _xdata = Nothing + } + diff --git a/src/Wingman/AbstractLSP/TacticActions.hs b/src/Wingman/AbstractLSP/TacticActions.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/AbstractLSP/TacticActions.hs @@ -0,0 +1,173 @@ +{-# LANGUAGE RecordWildCards #-} + +{-# LANGUAGE NoMonoLocalBinds #-} + +module Wingman.AbstractLSP.TacticActions where + +import Control.Monad (when) +import Control.Monad.IO.Class (liftIO) +import Control.Monad.Trans (lift) +import Control.Monad.Trans.Maybe (mapMaybeT) +import Data.Foldable +import Data.Maybe (listToMaybe) +import Data.Proxy +import Development.IDE hiding (rangeToRealSrcSpan) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.Compat +import Development.IDE.GHC.ExactPrint +import Generics.SYB.GHC (mkBindListT, everywhereM') +import GhcPlugins (occName) +import System.Timeout (timeout) +import Wingman.AbstractLSP.Types +import Wingman.CaseSplit +import Wingman.GHC (liftMaybe, isHole, pattern AMatch, unXPat) +import Wingman.Judgements (jNeedsToBindArgs) +import Wingman.LanguageServer (runStaleIde) +import Wingman.LanguageServer.TacticProviders +import Wingman.Machinery (runTactic, scoreSolution) +import Wingman.Range +import Wingman.Types + + +------------------------------------------------------------------------------ +-- | An 'Interaction' for a 'TacticCommand'. +makeTacticInteraction + :: TacticCommand + -> Interaction +makeTacticInteraction cmd = + Interaction $ Continuation @_ @HoleTarget cmd + (SynthesizeCodeAction $ \env@LspEnv{..} hj -> do + pure $ commandProvider cmd $ + TacticProviderData + { tpd_lspEnv = env + , tpd_jdg = hj_jdg hj + , tpd_hole_sort = hj_hole_sort hj + } + ) + $ \LspEnv{..} HoleJudgment{..} FileContext{..} var_name -> do + let stale a = runStaleIde "tacticCmd" le_ideState fc_nfp a + + let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath fc_nfp)) hj_range + TrackedStale _ pmmap <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + pm_span <- liftMaybe $ mapAgeFrom pmmap span + let t = commandTactic cmd var_name + + liftIO $ runTactic (cfg_timeout_seconds le_config * seconds) hj_ctx hj_jdg t >>= \case + Left err -> + pure + $ pure + $ ErrorMessages + $ pure + $ mkUserFacingMessage err + Right rtr -> + case rtr_extract rtr of + L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> + pure + $ addTimeoutMessage rtr + $ pure + $ ErrorMessages + $ pure NothingToDo + _ -> do + for_ (rtr_other_solns rtr) $ \soln -> do + traceMX "other solution" $ syn_val soln + traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] + traceMX "solution" $ rtr_extract rtr + pure + $ addTimeoutMessage rtr + $ pure + $ GraftEdit + $ graftHole (RealSrcSpan $ unTrack pm_span) rtr + + +addTimeoutMessage :: RunTacticResults -> [ContinuationResult] -> [ContinuationResult] +addTimeoutMessage rtr = mappend + [ ErrorMessages $ pure TimedOut + | rtr_timed_out rtr + ] + + +------------------------------------------------------------------------------ +-- | The number of microseconds in a second +seconds :: Num a => a +seconds = 1e6 + + +------------------------------------------------------------------------------ +-- | Transform some tactic errors into a 'UserFacingMessage'. +mkUserFacingMessage :: [TacticError] -> UserFacingMessage +mkUserFacingMessage errs + | elem OutOfGas errs = NotEnoughGas +mkUserFacingMessage [] = NothingToDo +mkUserFacingMessage _ = TacticErrors + + +------------------------------------------------------------------------------ +-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly +-- deals with top-level holes, in which we might need to fiddle with the +-- 'Match's that bind variables. +graftHole + :: SrcSpan + -> RunTacticResults + -> Graft (Either String) ParsedSource +graftHole span rtr + | _jIsTopHole (rtr_jdg rtr) + = genericGraftWithSmallestM + (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span + $ \dflags matches -> + everywhereM' + $ mkBindListT $ \ix -> + graftDecl dflags span ix $ \name pats -> + splitToDecl + (case not $ jNeedsToBindArgs (rtr_jdg rtr) of + -- If the user has explicitly bound arguments, use the + -- fixity they wrote. + True -> matchContextFixity . m_ctxt . unLoc + =<< listToMaybe matches + -- Otherwise, choose based on the name of the function. + False -> Nothing + ) + (occName name) + $ iterateSplit + $ mkFirstAgda (fmap unXPat pats) + $ unLoc + $ rtr_extract rtr +graftHole span rtr + = graft span + $ rtr_extract rtr + + +------------------------------------------------------------------------------ +-- | Keep a fixity if one was present in the 'HsMatchContext'. +matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity +matchContextFixity (FunRhs _ l _) = Just l +matchContextFixity _ = Nothing + + +------------------------------------------------------------------------------ +-- | Helper function to route 'mergeFunBindMatches' into the right place in an +-- AST --- correctly dealing with inserting into instance declarations. +graftDecl + :: DynFlags + -> SrcSpan + -> Int + -> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs) + -> LMatch GhcPs (LHsExpr GhcPs) + -> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)] +graftDecl dflags dst ix make_decl (L src (AMatch (FunRhs (L _ name) _ _) pats _)) + | dst `isSubspanOf` src = do + L _ dec <- annotateDecl dflags $ make_decl name pats + case dec of + ValD _ (FunBind { fun_matches = MG { mg_alts = L _ alts@(first_match : _)} + }) -> do + -- For whatever reason, ExactPrint annotates newlines to the ends of + -- case matches and type signatures, but only allows us to insert + -- them at the beginning of those things. Thus, we need want to + -- insert a preceeding newline (done in 'annotateDecl') on all + -- matches, except for the first one --- since it gets its newline + -- from the line above. + when (ix == 0) $ + setPrecedingLinesT first_match 0 0 + pure alts + _ -> lift $ Left "annotateDecl didn't produce a funbind" +graftDecl _ _ _ _ x = pure $ pure x + diff --git a/src/Wingman/AbstractLSP/Types.hs b/src/Wingman/AbstractLSP/Types.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/AbstractLSP/Types.hs @@ -0,0 +1,171 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -Wno-orphans #-} + +module Wingman.AbstractLSP.Types where + +import Control.Monad.IO.Class +import Control.Monad.Trans.Maybe (MaybeT (MaybeT), mapMaybeT) +import qualified Data.Aeson as A +import Data.Text (Text) +import Development.IDE (IdeState) +import Development.IDE.GHC.ExactPrint (Graft) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.Compat hiding (Target) +import GHC.Generics (Generic) +import qualified Ide.Plugin.Config as Plugin +import Ide.Types +import Language.LSP.Server (LspM) +import Language.LSP.Types hiding (CodeLens, CodeAction) +import Wingman.LanguageServer (judgementForHole) +import Wingman.Types + + +------------------------------------------------------------------------------ +-- | An 'Interaction' is an existential 'Continuation', which handles both +-- sides of the request/response interaction for LSP. +data Interaction where + Interaction + :: (IsTarget target, IsContinuationSort sort, A.ToJSON b, A.FromJSON b) + => Continuation sort target b + -> Interaction + + +------------------------------------------------------------------------------ +-- | Metadata for a command. Used by both code actions and lenses, though for +-- lenses, only 'md_title' is currently used. +data Metadata + = Metadata + { md_title :: Text + , md_kind :: CodeActionKind + , md_preferred :: Bool + } + deriving stock (Eq, Show) + + +------------------------------------------------------------------------------ +-- | Whether we're defining a CodeAction or CodeLens. +data SynthesizeCommand a b + = SynthesizeCodeAction + ( LspEnv + -> TargetArgs a + -> MaybeT (LspM Plugin.Config) [(Metadata, b)] + ) + | SynthesizeCodeLens + ( LspEnv + -> TargetArgs a + -> MaybeT (LspM Plugin.Config) [(Range, Metadata, b)] + ) + + +------------------------------------------------------------------------------ +-- | Transform a "continuation sort" into a 'CommandId'. +class IsContinuationSort a where + toCommandId :: a -> CommandId + +instance IsContinuationSort CommandId where + toCommandId = id + +instance IsContinuationSort Text where + toCommandId = CommandId + + +------------------------------------------------------------------------------ +-- | Ways a 'Continuation' can resolve. +data ContinuationResult + = -- | Produce some error messages. + ErrorMessages [UserFacingMessage] + -- | Produce an explicit 'WorkspaceEdit'. + | RawEdit WorkspaceEdit + -- | Produce a 'Graft', corresponding to a transformation of the current + -- AST. + | GraftEdit (Graft (Either String) ParsedSource) + + +------------------------------------------------------------------------------ +-- | A 'Continuation' is a single object corresponding to an action that users +-- can take via LSP. It generalizes codeactions and codelenses, allowing for +-- a significant amount of code reuse. +-- +-- Given @Continuation sort target payload@: +-- +-- the @sort@ corresponds to a 'CommandId', allowing you to namespace actions +-- rather than working directly with text. This functionality is driven via +-- 'IsContinuationSort'. +-- +-- the @target@ is used to fetch data from LSP on both sides of the +-- request/response barrier. For example, you can use it to resolve what node +-- in the AST the incoming range refers to. This functionality is driven via +-- 'IsTarget'. +-- +-- the @payload@ is used for data you'd explicitly like to send from the +-- request to the response. It's like @target@, but only gets computed once. +-- This is beneficial if you can do it, but requires that your data is +-- serializable via JSON. +data Continuation sort target payload = Continuation + { c_sort :: sort + , c_makeCommand :: SynthesizeCommand target payload + , c_runCommand + :: LspEnv + -> TargetArgs target + -> FileContext + -> payload + -> MaybeT (LspM Plugin.Config) [ContinuationResult] + } + + +------------------------------------------------------------------------------ +-- | What file are we looking at, and what bit of it? +data FileContext = FileContext + { fc_uri :: Uri + , fc_nfp :: NormalizedFilePath + , fc_range :: Maybe (Tracked 'Current Range) + -- ^ For code actions, this is 'Just'. For code lenses, you'll get + -- a 'Nothing' in the request, and a 'Just' in the response. + } + deriving stock (Eq, Ord, Show, Generic) + deriving anyclass (A.ToJSON, A.FromJSON) + +deriving anyclass instance A.ToJSON NormalizedFilePath +deriving anyclass instance A.ToJSON NormalizedUri +deriving anyclass instance A.FromJSON NormalizedFilePath +deriving anyclass instance A.FromJSON NormalizedUri + + +------------------------------------------------------------------------------ +-- | Everything we need to resolve continuations. +data LspEnv = LspEnv + { le_ideState :: IdeState + , le_pluginId :: PluginId + , le_dflags :: DynFlags + , le_config :: Config + , le_fileContext :: FileContext + } + + +------------------------------------------------------------------------------ +-- | Extract some information from LSP, so it can be passed to the requests and +-- responses of a 'Continuation'. +class IsTarget t where + type TargetArgs t + fetchTargetArgs + :: LspEnv + -> MaybeT (LspM Plugin.Config) (TargetArgs t) + +------------------------------------------------------------------------------ +-- | A 'HoleTarget' is a target (see 'IsTarget') which succeeds if the given +-- range is an HsExpr hole. It gives continuations access to the resulting +-- tactic judgement. +data HoleTarget = HoleTarget + deriving stock (Eq, Ord, Show, Enum, Bounded) + +instance IsTarget HoleTarget where + type TargetArgs HoleTarget = HoleJudgment + fetchTargetArgs LspEnv{..} = do + let FileContext{..} = le_fileContext + range <- MaybeT $ pure fc_range + mapMaybeT liftIO $ judgementForHole le_ideState fc_nfp range le_config + diff --git a/src/Wingman/CodeGen.hs b/src/Wingman/CodeGen.hs --- a/src/Wingman/CodeGen.hs +++ b/src/Wingman/CodeGen.hs @@ -15,6 +15,7 @@ import Control.Monad.Except import Control.Monad.Reader (ask) import Control.Monad.State +import Data.Bifunctor (second) import Data.Bool (bool) import Data.Functor ((<&>)) import Data.Generics.Labels () @@ -225,7 +226,6 @@ $ disallowing AlreadyDestructed (S.singleton term) jdg pure $ ext & #syn_trace %~ rose ("destruct " <> show term) . pure - & #syn_used_vals %~ S.insert term & #syn_val %~ noLoc . case' (var' term) @@ -315,4 +315,24 @@ matches = fmap (fmap (\(occ, expr) -> valBind (occNameToStr occ) expr)) terms g <- fmap (fmap unLoc) $ newSubgoal $ introduce ctx (userHypothesis hy') jdg pure $ fmap noLoc $ let' <$> matches <*> g + + +------------------------------------------------------------------------------ +-- | Let-bind the given occname judgement pairs. +nonrecLet + :: [(OccName, Judgement)] + -> Judgement + -> RuleM (Synthesized (LHsExpr GhcPs)) +nonrecLet occjdgs jdg = do + occexts <- traverse newSubgoal $ fmap snd occjdgs + ctx <- ask + ext <- newSubgoal + $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs) + $ jdg + pure $ fmap noLoc $ + let' + <$> traverse + (\(occ, ext) -> valBind (occNameToStr occ) <$> fmap unLoc ext) + (zip (fmap fst occjdgs) occexts) + <*> fmap unLoc ext diff --git a/src/Wingman/EmptyCase.hs b/src/Wingman/EmptyCase.hs --- a/src/Wingman/EmptyCase.hs +++ b/src/Wingman/EmptyCase.hs @@ -1,4 +1,6 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE NoMonoLocalBinds #-} @@ -9,7 +11,6 @@ import Control.Monad.Except (runExcept) import Control.Monad.Trans import Control.Monad.Trans.Maybe -import Data.Aeson import Data.Generics.Aliases (mkQ, GenericQ) import Data.Generics.Schemes (everything) import Data.Maybe @@ -31,6 +32,7 @@ import Prelude hiding (span) import Prelude hiding (span) import TcRnTypes (tcg_binds) +import Wingman.AbstractLSP.Types import Wingman.CodeGen (destructionFor) import Wingman.GHC import Wingman.Judgements @@ -38,59 +40,51 @@ import Wingman.Types ------------------------------------------------------------------------------- --- | The 'CommandId' for the empty case completion. -emptyCaseLensCommandId :: CommandId -emptyCaseLensCommandId = CommandId "wingman.emptyCase" - +data EmptyCaseT = EmptyCaseT ------------------------------------------------------------------------------- --- | A command function that just applies a 'WorkspaceEdit'. -workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit -workspaceEditHandler _ideState wedit = do - _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ()) - return $ Right Null +instance IsContinuationSort EmptyCaseT where + toCommandId _ = CommandId "wingman.emptyCase" +instance IsTarget EmptyCaseT where + type TargetArgs EmptyCaseT = () + fetchTargetArgs _ = pure () ------------------------------------------------------------------------------- --- | Provide the "empty case completion" code lens -codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens -codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri)) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - let stale a = runStaleIde "codeLensProvider" state nfp a +emptyCaseInteraction :: Interaction +emptyCaseInteraction = Interaction $ + Continuation @EmptyCaseT @EmptyCaseT @WorkspaceEdit EmptyCaseT + (SynthesizeCodeLens $ \LspEnv{..} _ -> do + let FileContext{..} = le_fileContext - ccs <- getClientCapabilities - liftIO $ fromMaybeT (Right $ List []) $ do - dflags <- getIdeDynflags state nfp - TrackedStale pm _ <- stale GetAnnotatedParsedSource - TrackedStale binds bind_map <- stale GetBindings - holes <- emptyCaseScrutinees state nfp + let stale a = runStaleIde "codeLensProvider" le_ideState fc_nfp a - fmap (Right . List) $ for holes $ \(ss, ty) -> do - binds_ss <- liftMaybe $ mapAgeFrom bind_map ss - let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss - range = realSrcSpanToRange $ unTrack ss - matches <- - liftMaybe $ - destructionFor - (foldMap (hySingleton . occName . fst) bindings) - ty - edits <- liftMaybe $ hush $ - mkWorkspaceEdits dflags ccs uri (unTrack pm) $ - graftMatchGroup (RealSrcSpan $ unTrack ss) $ - noLoc matches + ccs <- lift getClientCapabilities + TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource + TrackedStale binds bind_map <- mapMaybeT liftIO $ stale GetBindings + holes <- mapMaybeT liftIO $ emptyCaseScrutinees le_ideState fc_nfp - pure $ - CodeLens range - (Just - $ mkLspCommand - plId - emptyCaseLensCommandId - (mkEmptyCaseLensDesc ty) - $ Just $ pure $ toJSON $ edits - ) - Nothing -codeLensProvider _ _ _ = pure $ Right $ List [] + for holes $ \(ss, ty) -> do + binds_ss <- liftMaybe $ mapAgeFrom bind_map ss + let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss + range = realSrcSpanToRange $ unTrack ss + matches <- + liftMaybe $ + destructionFor + (foldMap (hySingleton . occName . fst) bindings) + ty + edits <- liftMaybe $ hush $ + mkWorkspaceEdits le_dflags ccs fc_uri (unTrack pm) $ + graftMatchGroup (RealSrcSpan $ unTrack ss) $ + noLoc matches + pure + ( range + , Metadata + (mkEmptyCaseLensDesc ty) + (CodeActionUnknown "refactor.wingman.completeEmptyCase") + False + , edits + ) + ) + $ (\ _ _ _ we -> pure $ pure $ RawEdit we) scrutinzedType :: EmptyCaseSort Type -> Maybe Type diff --git a/src/Wingman/GHC.hs b/src/Wingman/GHC.hs --- a/src/Wingman/GHC.hs +++ b/src/Wingman/GHC.hs @@ -309,13 +309,18 @@ ------------------------------------------------------------------------------ -- | Should make sure it's a fun bind -pattern TopLevelRHS :: OccName -> [PatCompat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc) -pattern TopLevelRHS name ps body <- +pattern TopLevelRHS + :: OccName + -> [PatCompat GhcTc] + -> LHsExpr GhcTc + -> HsLocalBindsLR GhcTc GhcTc + -> Match GhcTc (LHsExpr GhcTc) +pattern TopLevelRHS name ps body where_binds <- Match _ (FunRhs (L _ (occName -> name)) _ _) ps (GRHSs _ - [L _ (GRHS _ [] body)] _) + [L _ (GRHS _ [] body)] (L _ where_binds)) dataConExTys :: DataCon -> [TyCoVar] diff --git a/src/Wingman/LanguageServer.hs b/src/Wingman/LanguageServer.hs --- a/src/Wingman/LanguageServer.hs +++ b/src/Wingman/LanguageServer.hs @@ -273,7 +273,7 @@ mkFirstJudgement ctx (local_hy <> cls_hy) - (isRhsHole tcg_rss tcs) + (isRhsHoleWithoutWhere tcg_rss tcs) g , ctx ) @@ -341,6 +341,7 @@ TopLevelRHS name ps (L (RealSrcSpan span) -- body with no guards and a single defn (HsVar _ (L _ hole))) + _ | containsSpan rss span -- which contains our span , isHole $ occName hole -- and the span is a hole -> flip evalState 0 $ buildTopLevelHypothesis name ps @@ -478,12 +479,25 @@ ------------------------------------------------------------------------------ --- | Is this hole immediately to the right of an equals sign? -isRhsHole :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Bool -isRhsHole (unTrack -> rss) (unTrack -> tcs) = +-- | Is this hole immediately to the right of an equals sign --- and is there +-- no where clause attached to it? +-- +-- It's important that there is no where clause because otherwise it gets +-- clobbered. See #2183 for an example. +-- +-- This isn't a perfect check, and produces some ugly code. But it's much much +-- better than the alternative, which is to destructively modify the user's +-- AST. +isRhsHoleWithoutWhere + :: Tracked age RealSrcSpan + -> Tracked age TypecheckedSource + -> Bool +isRhsHoleWithoutWhere (unTrack -> rss) (unTrack -> tcs) = everything (||) (mkQ False $ \case - TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span - _ -> False + TopLevelRHS _ _ + (L (RealSrcSpan span) _) + (EmptyLocalBinds _) -> containsSpan rss span + _ -> False ) tcs diff --git a/src/Wingman/LanguageServer/TacticProviders.hs b/src/Wingman/LanguageServer/TacticProviders.hs --- a/src/Wingman/LanguageServer/TacticProviders.hs +++ b/src/Wingman/LanguageServer/TacticProviders.hs @@ -1,38 +1,29 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Wingman.LanguageServer.TacticProviders ( commandProvider , commandTactic - , tcCommandId - , TacticParams (..) , TacticProviderData (..) - , useNameFromHypothesis ) where import Control.Monad -import Data.Aeson import Data.Bool (bool) import Data.Coerce import Data.Maybe import Data.Monoid import qualified Data.Set as S import qualified Data.Text as T -import Data.Traversable import DataCon (dataConName) -import Development.IDE.Core.UseStale (Tracked, Age(..)) import Development.IDE.GHC.Compat -import GHC.Generics import GHC.LanguageExtensions.Type (Extension (LambdaCase)) -import Ide.PluginUtils import Ide.Types -import Language.LSP.Types hiding - (SemanticTokenAbsolute (length, line), - SemanticTokenRelative (length), - SemanticTokensEdit (_start)) +import Language.LSP.Types hiding (SemanticTokenAbsolute (..), SemanticTokenRelative (..)) import OccName import Prelude hiding (span) +import Wingman.AbstractLSP.Types import Wingman.Auto import Wingman.GHC import Wingman.Judgements @@ -47,6 +38,7 @@ commandTactic :: TacticCommand -> T.Text -> TacticsM () commandTactic Auto = const auto commandTactic Intros = const intros +commandTactic IntroAndDestruct = const introAndDestruct commandTactic Destruct = useNameFromHypothesis destruct . mkVarOcc . T.unpack commandTactic DestructPun = useNameFromHypothesis destructPun . mkVarOcc . T.unpack commandTactic Homomorphism = useNameFromHypothesis homo . mkVarOcc . T.unpack @@ -64,6 +56,7 @@ tacticKind :: TacticCommand -> T.Text tacticKind Auto = "fillHole" tacticKind Intros = "introduceLambda" +tacticKind IntroAndDestruct = "introduceAndDestruct" tacticKind Destruct = "caseSplit" tacticKind DestructPun = "caseSplitPun" tacticKind Homomorphism = "homomorphicCaseSplit" @@ -82,9 +75,10 @@ tacticPreferred :: TacticCommand -> Bool tacticPreferred Auto = True tacticPreferred Intros = True +tacticPreferred IntroAndDestruct = True tacticPreferred Destruct = True tacticPreferred DestructPun = False -tacticPreferred Homomorphism = False +tacticPreferred Homomorphism = True tacticPreferred DestructLambdaCase = False tacticPreferred HomomorphismLambdaCase = False tacticPreferred DestructAll = True @@ -110,6 +104,10 @@ requireHoleSort (== Hole) $ filterGoalType isFunction $ provide Intros "" +commandProvider IntroAndDestruct = + requireHoleSort (== Hole) $ + filterGoalType (liftLambdaCase False (\_ -> isJust . algebraicTyCon)) $ + provide IntroAndDestruct "" commandProvider Destruct = requireHoleSort (== Hole) $ filterBindingType destructFilter $ \occ _ -> @@ -185,40 +183,27 @@ -- UI. type TacticProvider = TacticProviderData - -> IO [Command |? CodeAction] + -> [(Metadata, T.Text)] data TacticProviderData = TacticProviderData - { tpd_dflags :: DynFlags - , tpd_config :: Config - , tpd_plid :: PluginId - , tpd_uri :: Uri - , tpd_range :: Tracked 'Current Range + { tpd_lspEnv :: LspEnv , tpd_jdg :: Judgement , tpd_hole_sort :: HoleSort } -data TacticParams = TacticParams - { tp_file :: Uri -- ^ Uri of the file to fill the hole in - , tp_range :: Tracked 'Current Range -- ^ The range of the hole - , tp_var_name :: T.Text - } - deriving stock (Show, Eq, Generic) - deriving anyclass (ToJSON, FromJSON) - - requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider requireHoleSort p tp tpd = case p $ tpd_hole_sort tpd of True -> tp tpd - False -> pure [] + False -> [] withMetaprogram :: (T.Text -> TacticProvider) -> TacticProvider withMetaprogram tp tpd = case tpd_hole_sort tpd of Metaprogram mp -> tp mp tpd - _ -> pure [] + _ -> [] ------------------------------------------------------------------------------ @@ -226,9 +211,9 @@ -- predicate holds for the goal. requireExtension :: Extension -> TacticProvider -> TacticProvider requireExtension ext tp tpd = - case xopt ext $ tpd_dflags tpd of + case xopt ext $ le_dflags $ tpd_lspEnv tpd of True -> tp tpd - False -> pure [] + False -> [] ------------------------------------------------------------------------------ @@ -238,7 +223,7 @@ filterGoalType p tp tpd = case p $ unCType $ jGoal $ tpd_jdg tpd of True -> tp tpd - False -> pure [] + False -> [] ------------------------------------------------------------------------------ @@ -259,11 +244,11 @@ let jdg = tpd_jdg tpd hy = jLocalHypothesis jdg g = jGoal jdg - in fmap join $ for (unHypothesis hy) $ \hi -> + in unHypothesis hy >>= \hi -> let ty = unCType $ hi_type hi in case p (unCType g) ty of True -> tp (hi_name hi) ty tpd - False -> pure [] + False -> [] ------------------------------------------------------------------------------ @@ -274,37 +259,22 @@ -> (a -> TacticProvider) -> TacticProvider filterTypeProjection p tp tpd = - fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a -> + (p $ unCType $ jGoal $ tpd_jdg tpd) >>= \a -> tp a tpd ------------------------------------------------------------------------------ -- | Get access to the 'Config' when building a 'TacticProvider'. withConfig :: (Config -> TacticProvider) -> TacticProvider -withConfig tp tpd = tp (tpd_config tpd) tpd +withConfig tp tpd = tp (le_config $ tpd_lspEnv tpd) tpd ------------------------------------------------------------------------------ -- | Terminal constructor for providing context-sensitive tactics. Tactics -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider -provide tc name TacticProviderData{..} = do - let title = tacticTitle tc name - params = TacticParams { tp_file = tpd_uri , tp_range = tpd_range , tp_var_name = name } - cmd = mkLspCommand tpd_plid (tcCommandId tc) title (Just [toJSON params]) - pure - $ pure - $ InR - $ CodeAction - { _title = title - , _kind = Just $ mkTacticKind tc - , _diagnostics = Nothing - , _isPreferred = Just $ tacticPreferred tc - , _disabled = Nothing - , _edit = Nothing - , _command = Just cmd - , _xdata = Nothing - } +provide tc name _ = + pure $ (Metadata (tacticTitle tc name) (mkTacticKind tc) (tacticPreferred tc), name) ------------------------------------------------------------------------------ @@ -338,7 +308,7 @@ -- algebraic types. destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True -destructFilter _ _ = False +destructFilter _ _ = False ------------------------------------------------------------------------------ @@ -347,5 +317,9 @@ destructPunFilter :: Type -> Type -> Bool destructPunFilter _ (algebraicTyCon -> Just tc) = any (not . null . dataConFieldLabels) $ tyConDataCons tc -destructPunFilter _ _ = False +destructPunFilter _ _ = False + + +instance IsContinuationSort TacticCommand where + toCommandId = tcCommandId diff --git a/src/Wingman/Machinery.hs b/src/Wingman/Machinery.hs --- a/src/Wingman/Machinery.hs +++ b/src/Wingman/Machinery.hs @@ -1,9 +1,11 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} module Wingman.Machinery where import Control.Applicative (empty) +import Control.Concurrent.Chan.Unagi.NoBlocking (newChan, writeChan, OutChan, tryRead, tryReadChan) import Control.Lens ((<>~)) import Control.Monad.Reader import Control.Monad.State.Class (gets, modify, MonadState) @@ -16,7 +18,7 @@ import Data.Generics.Product (field') import Data.List (sortBy) import qualified Data.Map as M -import Data.Maybe (mapMaybe) +import Data.Maybe (mapMaybe, isJust) import Data.Monoid (getSum) import Data.Ord (Down (..), comparing) import qualified Data.Set as S @@ -24,13 +26,16 @@ import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType) +import Refinery.Future import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal +import System.Timeout (timeout) import TcType import Type (tyCoVarsOfTypeWellScoped) +import TysPrim (alphaTyVar, alphaTy) import Wingman.Context (getInstance) -import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons) +import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types @@ -71,15 +76,24 @@ tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom +consumeChan :: OutChan (Maybe a) -> IO [a] +consumeChan chan = do + tryReadChan chan >>= tryRead >>= \case + Nothing -> pure [] + Just (Just a) -> (:) <$> pure a <*> consumeChan chan + Just Nothing -> pure [] + + ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. runTactic - :: Context + :: Int -- ^ Timeout + -> Context -> Judgement - -> TacticsM () -- ^ Tactic to use + -> TacticsM () -- ^ Tactic to use -> IO (Either [TacticError] RunTacticResults) -runTactic ctx jdg t = do +runTactic duration ctx jdg t = do let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ (:) (jGoal jdg) @@ -91,33 +105,36 @@ defaultTacticState { ts_skolems = skolems } - res <- flip runReaderT ctx - . unExtractM - $ runTacticT t jdg tacticState - pure $ case res of - (Left errs) -> Left $ take 50 errs - (Right solns) -> do - let sorted = - flip sortBy solns $ comparing $ \(Proof ext _ holes) -> - Down $ scoreSolution ext jdg $ fmap snd holes - case sorted of - ((Proof syn _ subgoals) : _) -> - Right $ - RunTacticResults - { rtr_trace = syn_trace syn - , rtr_extract = simplify $ syn_val syn - , rtr_subgoals = fmap snd subgoals - , rtr_other_solns = reverse . fmap pf_extract $ sorted - , rtr_jdg = jdg - , rtr_ctx = ctx - } - -- guaranteed to not be empty - _ -> Left [] -assoc23 :: (a, b, c) -> (a, (b, c)) -assoc23 (a, b, c) = (a, (b, c)) + let stream = hoistListT (flip runReaderT ctx . unExtractM) + $ runStreamingTacticT t jdg tacticState + (in_proofs, out_proofs) <- newChan + (in_errs, out_errs) <- newChan + timed_out <- + fmap (not. isJust) $ timeout duration $ consume stream $ \case + Left err -> writeChan in_errs $ Just err + Right proof -> writeChan in_proofs $ Just proof + writeChan in_proofs Nothing + solns <- consumeChan out_proofs + let sorted = + flip sortBy solns $ comparing $ \(Proof ext _ holes) -> + Down $ scoreSolution ext jdg $ fmap snd holes + case sorted of + ((Proof syn _ subgoals) : _) -> + pure $ Right $ + RunTacticResults + { rtr_trace = syn_trace syn + , rtr_extract = simplify $ syn_val syn + , rtr_subgoals = fmap snd subgoals + , rtr_other_solns = reverse . fmap pf_extract $ sorted + , rtr_jdg = jdg + , rtr_ctx = ctx + , rtr_timed_out = timed_out + } + _ -> fmap Left $ consumeChan out_errs + tracePrim :: String -> Trace tracePrim = flip rose [] @@ -213,6 +230,12 @@ deriving (Eq, Ord, Show) via a +------------------------------------------------------------------------------ +-- | Generate a unique unification variable. +newUnivar :: MonadState TacticState m => m Type +newUnivar = do + freshTyvars $ + mkInvForAllTys [alphaTyVar] alphaTy ------------------------------------------------------------------------------ diff --git a/src/Wingman/Metaprogramming/Parser.hs b/src/Wingman/Metaprogramming/Parser.hs --- a/src/Wingman/Metaprogramming/Parser.hs +++ b/src/Wingman/Metaprogramming/Parser.hs @@ -76,7 +76,7 @@ ]) (pure . \case [] -> intros - names -> intros' $ Just names + names -> intros' $ IntroduceOnlyNamed names ) [ Example Nothing @@ -100,7 +100,7 @@ , command "intro" Deterministic (Bind One) "Construct a lambda expression, binding an argument with the given name." - (pure . intros' . Just . pure) + (pure . intros' . IntroduceOnlyNamed . pure) [ Example Nothing ["aye"] @@ -348,6 +348,22 @@ "(_ :: a -> a -> a -> a) a1 a2 a3" ] + , command "let" Deterministic (Bind Many) + "Create let-bindings for each binder given to this tactic." + (pure . letBind) + [ Example + Nothing + ["a", "b", "c"] + [ ] + (Just "x") + $ T.pack $ unlines + [ "let a = _1 :: a" + , " b = _2 :: b" + , " c = _3 :: c" + , " in (_4 :: x)" + ] + ] + , command "try" Nondeterministic Tactic "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states." (pure . R.try) @@ -447,10 +463,7 @@ case P.runParser tacticProgram "" (T.pack program) of Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb Right tt -> do - res <- runTactic - ctx - jdg - tt + res <- runTactic 2e6 ctx jdg tt pure $ case res of Left tes -> Left $ wrapError $ show tes Right rtr -> Right diff --git a/src/Wingman/Plugin.hs b/src/Wingman/Plugin.hs --- a/src/Wingman/Plugin.hs +++ b/src/Wingman/Plugin.hs @@ -2,255 +2,34 @@ {-# LANGUAGE RecordWildCards #-} -- | A plugin that uses tactics to synthesize code -module Wingman.Plugin - ( descriptor - , tacticTitle - , TacticCommand (..) - ) where +module Wingman.Plugin where import Control.Monad -import Control.Monad.Trans -import Control.Monad.Trans.Maybe -import Data.Aeson -import Data.Data -import Data.Foldable (for_) -import Data.Maybe -import qualified Data.Text as T import Development.IDE.Core.Shake (IdeState (..)) -import Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent) -import Development.IDE.GHC.Compat -import Development.IDE.GHC.ExactPrint -import Generics.SYB.GHC import Ide.Types -import Language.LSP.Server import Language.LSP.Types -import Language.LSP.Types.Capabilities -import OccName import Prelude hiding (span) -import System.Timeout -import Wingman.CaseSplit +import Wingman.AbstractLSP +import Wingman.AbstractLSP.TacticActions (makeTacticInteraction) import Wingman.EmptyCase -import Wingman.GHC -import Wingman.Judgements (jNeedsToBindArgs) import Wingman.LanguageServer import Wingman.LanguageServer.Metaprogram (hoverProvider) -import Wingman.LanguageServer.TacticProviders -import Wingman.Machinery (scoreSolution) -import Wingman.Range import Wingman.StaticPlugin -import Wingman.Tactics -import Wingman.Types descriptor :: PluginId -> PluginDescriptor IdeState -descriptor plId = (defaultPluginDescriptor plId) - { pluginCommands - = mconcat - [ fmap (\tc -> - PluginCommand - (tcCommandId tc) - (tacticDesc $ tcCommandName tc) - (tacticCmd (commandTactic tc) plId)) - [minBound .. maxBound] - , pure $ - PluginCommand - emptyCaseLensCommandId - "Complete the empty case" - workspaceEditHandler - ] - , pluginHandlers = mconcat - [ mkPluginHandler STextDocumentCodeAction codeActionProvider - , mkPluginHandler STextDocumentCodeLens codeLensProvider - , mkPluginHandler STextDocumentHover hoverProvider - ] - , pluginRules = wingmanRules plId - , pluginConfigDescriptor = - defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties} - , pluginModifyDynflags = staticPlugin - } - - -codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction -codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) (unsafeMkCurrent -> range) _ctx) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - cfg <- getTacticConfig plId - liftIO $ fromMaybeT (Right $ List []) $ do - HoleJudgment{..} <- judgementForHole state nfp range cfg - actions <- lift $ - -- This foldMap is over the function monoid. - foldMap commandProvider [minBound .. maxBound] $ TacticProviderData - { tpd_dflags = hj_dflags - , tpd_config = cfg - , tpd_plid = plId - , tpd_uri = uri - , tpd_range = range - , tpd_jdg = hj_jdg - , tpd_hole_sort = hj_hole_sort +descriptor plId + = installInteractions + ( emptyCaseInteraction + : fmap makeTacticInteraction [minBound .. maxBound] + ) + $ (defaultPluginDescriptor plId) + { pluginHandlers = mkPluginHandler STextDocumentHover hoverProvider + , pluginRules = wingmanRules plId + , pluginConfigDescriptor = + defaultConfigDescriptor + { configCustomConfig = mkCustomConfig properties } - pure $ Right $ List actions -codeActionProvider _ _ _ = pure $ Right $ List [] - - -showUserFacingMessage - :: MonadLsp cfg m - => UserFacingMessage - -> m (Either ResponseError a) -showUserFacingMessage ufm = do - showLspMessage $ mkShowMessageParams ufm - pure $ Left $ mkErr InternalError $ T.pack $ show ufm - - -mkUserFacingMessage :: [TacticError] -> UserFacingMessage -mkUserFacingMessage errs - | elem OutOfGas errs = NotEnoughGas -mkUserFacingMessage _ = TacticErrors - - -tacticCmd - :: (T.Text -> TacticsM ()) - -> PluginId - -> CommandFunction IdeState TacticParams -tacticCmd tac pId state (TacticParams uri range var_name) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - let stale a = runStaleIde "tacticCmd" state nfp a - - ccs <- getClientCapabilities - cfg <- getTacticConfig pId - res <- liftIO $ runMaybeT $ do - HoleJudgment{..} <- judgementForHole state nfp range cfg - let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range - TrackedStale pm pmmap <- stale GetAnnotatedParsedSource - pm_span <- liftMaybe $ mapAgeFrom pmmap span - let t = tac var_name - - timingOut (cfg_timeout_seconds cfg * seconds) $ do - res <- liftIO $ runTactic hj_ctx hj_jdg t - pure $ join $ case res of - Left errs -> do - traceMX "errs" errs - Left $ mkUserFacingMessage errs - Right rtr -> - case rtr_extract rtr of - L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> - Left NothingToDo - _ -> pure $ mkTacticResultEdits pm_span hj_dflags ccs uri pm rtr - - case res of - Nothing -> do - showUserFacingMessage TimedOut - Just (Left ufm) -> do - showUserFacingMessage ufm - Just (Right edit) -> do - _ <- sendRequest - SWorkspaceApplyEdit - (ApplyWorkspaceEditParams Nothing edit) - (const $ pure ()) - pure $ Right Null -tacticCmd _ _ _ _ = - pure $ Left $ mkErr InvalidRequest "Bad URI" - - ------------------------------------------------------------------------------- --- | The number of microseconds in a second -seconds :: Num a => a -seconds = 1e6 - - -timingOut - :: Int -- ^ Time in microseconds - -> IO a -- ^ Computation to run - -> MaybeT IO a -timingOut t m = MaybeT $ timeout t m - - -mkErr :: ErrorCode -> T.Text -> ResponseError -mkErr code err = ResponseError code err Nothing - - ------------------------------------------------------------------------------- --- | Turn a 'RunTacticResults' into concrete edits to make in the source --- document. -mkTacticResultEdits - :: Tracked age RealSrcSpan - -> DynFlags - -> ClientCapabilities - -> Uri - -> Tracked age (Annotated ParsedSource) - -> RunTacticResults - -> Either UserFacingMessage WorkspaceEdit -mkTacticResultEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do - for_ (rtr_other_solns rtr) $ \soln -> do - traceMX "other solution" $ syn_val soln - traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] - traceMX "solution" $ rtr_extract rtr - mkWorkspaceEdits dflags ccs uri pm $ graftHole (RealSrcSpan span) rtr - - ------------------------------------------------------------------------------- --- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly --- deals with top-level holes, in which we might need to fiddle with the --- 'Match's that bind variables. -graftHole - :: SrcSpan - -> RunTacticResults - -> Graft (Either String) ParsedSource -graftHole span rtr - | _jIsTopHole (rtr_jdg rtr) - = genericGraftWithSmallestM - (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span - $ \dflags matches -> - everywhereM' - $ mkBindListT $ \ix -> - graftDecl dflags span ix $ \name pats -> - splitToDecl - (case not $ jNeedsToBindArgs (rtr_jdg rtr) of - -- If the user has explicitly bound arguments, use the - -- fixity they wrote. - True -> matchContextFixity . m_ctxt . unLoc - =<< listToMaybe matches - -- Otherwise, choose based on the name of the function. - False -> Nothing - ) - (occName name) - $ iterateSplit - $ mkFirstAgda (fmap unXPat pats) - $ unLoc - $ rtr_extract rtr -graftHole span rtr - = graft span - $ rtr_extract rtr - - -matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity -matchContextFixity (FunRhs _ l _) = Just l -matchContextFixity _ = Nothing - - ------------------------------------------------------------------------------- --- | Helper function to route 'mergeFunBindMatches' into the right place in an --- AST --- correctly dealing with inserting into instance declarations. -graftDecl - :: DynFlags - -> SrcSpan - -> Int - -> (RdrName -> [Pat GhcPs] -> LHsDecl GhcPs) - -> LMatch GhcPs (LHsExpr GhcPs) - -> TransformT (Either String) [LMatch GhcPs (LHsExpr GhcPs)] -graftDecl dflags dst ix make_decl (L src (AMatch (FunRhs (L _ name) _ _) pats _)) - | dst `isSubspanOf` src = do - L _ dec <- annotateDecl dflags $ make_decl name pats - case dec of - ValD _ (FunBind { fun_matches = MG { mg_alts = L _ alts@(first_match : _)} - }) -> do - -- For whatever reason, ExactPrint annotates newlines to the ends of - -- case matches and type signatures, but only allows us to insert - -- them at the beginning of those things. Thus, we need want to - -- insert a preceeding newline (done in 'annotateDecl') on all - -- matches, except for the first one --- since it gets its newline - -- from the line above. - when (ix == 0) $ - setPrecedingLinesT first_match 0 0 - pure alts - _ -> lift $ Left "annotateDecl didn't produce a funbind" -graftDecl _ _ _ _ x = pure $ pure x + , pluginModifyDynflags = staticPlugin + } diff --git a/src/Wingman/Tactics.hs b/src/Wingman/Tactics.hs --- a/src/Wingman/Tactics.hs +++ b/src/Wingman/Tactics.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} module Wingman.Tactics ( module Wingman.Tactics @@ -6,7 +7,7 @@ ) where import ConLike (ConLike(RealDataCon)) -import Control.Applicative (Alternative(empty)) +import Control.Applicative (Alternative(empty), (<|>)) import Control.Lens ((&), (%~), (<>~)) import Control.Monad (filterM) import Control.Monad (unless) @@ -23,6 +24,7 @@ import Data.Maybe import Data.Set (Set) import qualified Data.Set as S +import Data.Traversable (for) import DataCon import Development.IDE.GHC.Compat import GHC.Exts @@ -34,7 +36,6 @@ import Refinery.Tactic.Internal import TcType import Type hiding (Var) -import TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar) import Wingman.CodeGen import Wingman.GHC import Wingman.Judgements @@ -63,7 +64,7 @@ -- reasonable for a default value. (pure (noLoc $ var' name)) { syn_trace = tracePrim $ "assume " <> occNameString name - , syn_used_vals = S.singleton name + , syn_used_vals = S.singleton name <> getAncestry jdg name } Nothing -> cut @@ -117,21 +118,32 @@ ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros :: TacticsM () -intros = intros' Nothing +intros = intros' IntroduceAllUnnamed + +data IntroParams + = IntroduceAllUnnamed + | IntroduceOnlyNamed [OccName] + | IntroduceOnlyUnnamed Int + deriving stock (Eq, Ord, Show) + + ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros' - :: Maybe [OccName] -- ^ When 'Nothing', generate a new name for every - -- variable. Otherwise, only bind the variables named. + :: IntroParams -> TacticsM () -intros' names = rule $ \jdg -> do +intros' params = rule $ \jdg -> do let g = jGoal jdg case tacticsSplitFunTy $ unCType g of (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g (_, _, args, res) -> do ctx <- ask - let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names + let gen_names = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args + occs = case params of + IntroduceAllUnnamed -> gen_names + IntroduceOnlyNamed names -> names + IntroduceOnlyUnnamed n -> take n gen_names num_occs = length occs top_hole = isTopHole ctx jdg bindings = zip occs $ coerce args @@ -149,6 +161,24 @@ ------------------------------------------------------------------------------ +-- | Introduce a single lambda argument, and immediately destruct it. +introAndDestruct :: TacticsM () +introAndDestruct = do + hy <- fmap unHypothesis $ hyDiff $ intros' $ IntroduceOnlyUnnamed 1 + -- This case should never happen, but I'm validating instead of parsing. + -- Adding a log to be reminded if the invariant ever goes false. + -- + -- But note that this isn't a game-ending bug. In the worst case, we'll + -- accidentally bind too many variables, and incorrectly unify between them. + -- Which means some GADT cases that should be eliminated won't be --- not the + -- end of the world. + unless (length hy == 1) $ + traceMX "BUG: Introduced too many variables for introAndDestruct! Please report me if you see this! " hy + + for_ hy destruct + + +------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. destructAuto :: HyInfo CType -> TacticsM () destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do @@ -269,7 +299,7 @@ ) saturated_args pure $ ext - & #syn_used_vals %~ S.insert func + & #syn_used_vals %~ (\x -> S.insert func x <> getAncestry jdg func) & #syn_val %~ mkApply func . fmap unLoc application :: TacticsM () @@ -436,17 +466,17 @@ auto' n = do let loop = auto' (n - 1) try intros - choice - [ overFunctions $ \fname -> do - requireConcreteHole $ apply Saturated fname - loop - , overAlgebraicTerms $ \aname -> do - destructAuto aname - loop - , splitAuto >> loop - , assumption >> loop - , recursion - ] + assumption <|> + choice + [ overFunctions $ \fname -> do + requireConcreteHole $ apply Saturated fname + loop + , overAlgebraicTerms $ \aname -> do + destructAuto aname + loop + , splitAuto >> loop + , recursion + ] overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM () overFunctions = @@ -512,10 +542,10 @@ -- | Make an n-ary function call of the form -- @(_ :: forall a b. a -> a -> b) _ _@. nary :: Int -> TacticsM () -nary n = - applyByType $ - mkInvForAllTys [alphaTyVar, betaTyVar] $ - mkFunTys' (replicate n alphaTy) betaTy +nary n = do + a <- newUnivar + b <- newUnivar + applyByType $ mkFunTys' (replicate n a) b self :: TacticsM () @@ -550,6 +580,18 @@ $ Hypothesis unifiable_diff +letBind :: [OccName] -> TacticsM () +letBind occs = do + jdg <- goal + occ_tys <- for occs + $ \occ + -> fmap (occ, ) + $ fmap (<$ jdg) + $ fmap CType + $ newUnivar + rule $ nonrecLet occ_tys + + ------------------------------------------------------------------------------ -- | Deeply nest an unsaturated function onto itself nested :: OccName -> TacticsM () @@ -586,7 +628,7 @@ with_arg :: TacticsM () with_arg = rule $ \jdg -> do let g = jGoal jdg - fresh_ty <- freshTyvars $ mkInvForAllTys [alphaTyVar] alphaTy + fresh_ty <- newUnivar a <- newSubgoal $ withNewGoal (CType fresh_ty) jdg f <- newSubgoal $ withNewGoal (coerce mkFunTys' [fresh_ty] g) jdg pure $ fmap noLoc $ (@@) <$> fmap unLoc f <*> fmap unLoc a diff --git a/src/Wingman/Types.hs b/src/Wingman/Types.hs --- a/src/Wingman/Types.hs +++ b/src/Wingman/Types.hs @@ -59,6 +59,7 @@ data TacticCommand = Auto | Intros + | IntroAndDestruct | Destruct | DestructPun | Homomorphism @@ -77,6 +78,7 @@ where go Auto _ = "Attempt to fill hole" go Intros _ = "Introduce lambda" + go IntroAndDestruct _ = "Introduce and destruct term" go Destruct var = "Case split on " <> var go DestructPun var = "Split on " <> var <> " with NamedFieldPuns" go Homomorphism var = "Homomorphic case split on " <> var @@ -528,6 +530,7 @@ , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)] , rtr_jdg :: Judgement , rtr_ctx :: Context + , rtr_timed_out :: Bool } deriving Show @@ -549,7 +552,7 @@ instance Show UserFacingMessage where 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 TimedOut = "Wingman timed out while finding a solution. \nYou might get a better result if you increase the timeout duration." show NothingToDo = "Nothing to do" show (InfrastructureError t) = "Internal error: " <> T.unpack t diff --git a/test/AutoTupleSpec.hs b/test/AutoTupleSpec.hs --- a/test/AutoTupleSpec.hs +++ b/test/AutoTupleSpec.hs @@ -1,14 +1,16 @@ +{-# LANGUAGE NumDecimals #-} + {-# OPTIONS_GHC -fno-warn-orphans #-} module AutoTupleSpec where +import Control.Monad (replicateM) +import Control.Monad.State (evalState) import Data.Either (isRight) import OccName (mkVarOcc) import System.IO.Unsafe import Test.Hspec import Test.QuickCheck -import Type (mkTyVarTy) -import TysPrim (alphaTyVars) import TysWiredIn (mkBoxedTupleTy) import Wingman.Judgements (mkFirstJudgement) import Wingman.Machinery @@ -22,7 +24,8 @@ property $ do -- Pick some number of variables n <- choose (1, 7) - let vars = fmap mkTyVarTy $ take n alphaTyVars + let vars = flip evalState defaultTacticState + $ replicateM n newUnivar -- Pick a random ordering in_vars <- shuffle vars -- Randomly associate them into tuple types @@ -36,6 +39,7 @@ -- We should always be able to find a solution unsafePerformIO (runTactic + 2e6 emptyContext (mkFirstJudgement emptyContext diff --git a/test/CodeAction/AutoSpec.hs b/test/CodeAction/AutoSpec.hs --- a/test/CodeAction/AutoSpec.hs +++ b/test/CodeAction/AutoSpec.hs @@ -49,6 +49,7 @@ autoTest 2 25 "AutoInfixInfix" autoTest 19 12 "AutoTypeLevel" autoTest 11 9 "AutoForallClassMethod" + autoTest 2 8 "AutoUnusedPatternMatch" failing "flaky in CI" $ autoTest 2 11 "GoldenApplicativeThen" diff --git a/test/CodeAction/IntroDestructSpec.hs b/test/CodeAction/IntroDestructSpec.hs new file mode 100644 --- /dev/null +++ b/test/CodeAction/IntroDestructSpec.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE OverloadedStrings #-} + +module CodeAction.IntroDestructSpec where + +import Wingman.Types +import Test.Hspec +import Utils + + +spec :: Spec +spec = do + let test l c = goldenTest IntroAndDestruct "" l c + . mappend "IntroDestruct" + + describe "golden" $ do + test 4 5 "One" + test 2 5 "Many" + test 4 11 "LetBinding" + + describe "provider" $ do + mkTest + "Can intro and destruct an algebraic ty" + "IntroDestructProvider" 2 12 + [ (id, IntroAndDestruct, "") + ] + mkTest + "Won't intro and destruct a non-algebraic ty" + "IntroDestructProvider" 5 12 + [ (not, IntroAndDestruct, "") + ] + mkTest + "Can't intro, so no option" + "IntroDestructProvider" 8 17 + [ (not, IntroAndDestruct, "") + ] + diff --git a/test/CodeAction/RefineSpec.hs b/test/CodeAction/RefineSpec.hs --- a/test/CodeAction/RefineSpec.hs +++ b/test/CodeAction/RefineSpec.hs @@ -16,6 +16,7 @@ refineTest 2 8 "RefineCon" refineTest 4 10 "RefineReader" refineTest 8 10 "RefineGADT" + refineTest 2 8 "RefineIntroWhere" describe "messages" $ do mkShowMessageTest Refine "" 2 8 "MessageForallA" TacticErrors diff --git a/test/CodeAction/RunMetaprogramSpec.hs b/test/CodeAction/RunMetaprogramSpec.hs --- a/test/CodeAction/RunMetaprogramSpec.hs +++ b/test/CodeAction/RunMetaprogramSpec.hs @@ -39,5 +39,7 @@ metaTest 4 28 "MetaUseSymbol" metaTest 7 53 "MetaDeepOf" metaTest 2 34 "MetaWithArg" + metaTest 2 18 "MetaLetSimple" + metaTest 2 12 "IntrosTooMany" diff --git a/test/UnificationSpec.hs b/test/UnificationSpec.hs --- a/test/UnificationSpec.hs +++ b/test/UnificationSpec.hs @@ -4,6 +4,8 @@ module UnificationSpec where import Control.Arrow +import Control.Monad (replicateM, join) +import Control.Monad.State (evalState) import Data.Bool (bool) import Data.Functor ((<&>)) import Data.Maybe (mapMaybe) @@ -13,10 +15,9 @@ import TcType (substTy, tcGetTyVar_maybe) import Test.Hspec import Test.QuickCheck -import Type (mkTyVarTy) -import TysPrim (alphaTyVars) import TysWiredIn (mkBoxedTupleTy) import Wingman.GHC +import Wingman.Machinery (newUnivar) import Wingman.Types @@ -25,8 +26,11 @@ it "should be able to unify univars with skolems on either side of the equality" $ do property $ do -- Pick some number of unification vars and skolem - n <- choose (1, 1) - let (skolems, take n -> univars) = splitAt n $ fmap mkTyVarTy alphaTyVars + n <- choose (1, 20) + let (skolems, take n -> univars) + = splitAt n + $ flip evalState defaultTacticState + $ replicateM (n * 2) newUnivar -- Randomly pair them skolem_uni_pairs <- for (zip skolems univars) randomSwap @@ -42,13 +46,25 @@ (CType lhs) (CType rhs) of Just subst -> - -- For each pair, running the unification over the univar should - -- result in the skolem - conjoin $ zip univars skolems <&> \(uni, skolem) -> - let substd = substTy subst uni - in counterexample (show substd) $ - counterexample (show skolem) $ - CType substd === CType skolem + conjoin $ join $ + [ -- For each pair, running the unification over the univar should + -- result in the skolem + zip univars skolems <&> \(uni, skolem) -> + let substd = substTy subst uni + in counterexample (show substd) $ + counterexample (show skolem) $ + CType substd === CType skolem + + -- And also, no two univars should equal to one another + -- before or after substitution. + , zip univars (tail univars) <&> \(uni1, uni2) -> + let uni1_sub = substTy subst uni1 + uni2_sub = substTy subst uni2 + in counterexample (show uni1) $ + counterexample (show uni2) $ + CType uni1 =/= CType uni2 .&&. + CType uni1_sub =/= CType uni2_sub + ] Nothing -> True === False diff --git a/test/golden/AutoUnusedPatternMatch.expected.hs b/test/golden/AutoUnusedPatternMatch.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoUnusedPatternMatch.expected.hs @@ -0,0 +1,2 @@ +test :: Bool -> () +test _ = () diff --git a/test/golden/AutoUnusedPatternMatch.hs b/test/golden/AutoUnusedPatternMatch.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoUnusedPatternMatch.hs @@ -0,0 +1,2 @@ +test :: Bool -> () +test = _ diff --git a/test/golden/IntroDestructLetBinding.expected.hs b/test/golden/IntroDestructLetBinding.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructLetBinding.expected.hs @@ -0,0 +1,6 @@ +test :: IO () +test = do + let x :: Bool -> Int + x False = _w0 + x True = _w1 + pure () diff --git a/test/golden/IntroDestructLetBinding.hs b/test/golden/IntroDestructLetBinding.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructLetBinding.hs @@ -0,0 +1,5 @@ +test :: IO () +test = do + let x :: Bool -> Int + x = _ + pure () diff --git a/test/golden/IntroDestructMany.expected.hs b/test/golden/IntroDestructMany.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructMany.expected.hs @@ -0,0 +1,4 @@ +x :: Bool -> Maybe Int -> String -> Int +x False = _w0 +x True = _w1 + diff --git a/test/golden/IntroDestructMany.hs b/test/golden/IntroDestructMany.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructMany.hs @@ -0,0 +1,3 @@ +x :: Bool -> Maybe Int -> String -> Int +x = _ + diff --git a/test/golden/IntroDestructOne.expected.hs b/test/golden/IntroDestructOne.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructOne.expected.hs @@ -0,0 +1,6 @@ +module Test where + +x :: Bool -> Int +x False = _w0 +x True = _w1 + diff --git a/test/golden/IntroDestructOne.hs b/test/golden/IntroDestructOne.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructOne.hs @@ -0,0 +1,5 @@ +module Test where + +x :: Bool -> Int +x = _ + diff --git a/test/golden/IntroDestructProvider.hs b/test/golden/IntroDestructProvider.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntroDestructProvider.hs @@ -0,0 +1,9 @@ +hasAlgTy :: Maybe Int -> Int +hasAlgTy = _ + +hasFunTy :: (Int -> Int) -> Int +hasFunTy = _ + +isSaturated :: Bool -> Int +isSaturated b = _ + diff --git a/test/golden/MetaLetSimple.expected.hs b/test/golden/MetaLetSimple.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaLetSimple.expected.hs @@ -0,0 +1,7 @@ +test :: Int +test + = let + a = _w0 + b = _w1 + c = _w2 + in _w3 diff --git a/test/golden/MetaLetSimple.hs b/test/golden/MetaLetSimple.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaLetSimple.hs @@ -0,0 +1,2 @@ +test :: Int +test = [wingman| let a b c |] diff --git a/test/golden/RefineIntroWhere.expected.hs b/test/golden/RefineIntroWhere.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/RefineIntroWhere.expected.hs @@ -0,0 +1,6 @@ +test :: Maybe Int -> Int +test = \ m_n -> _w0 + where + -- Don't delete me! + blah = undefined + diff --git a/test/golden/RefineIntroWhere.hs b/test/golden/RefineIntroWhere.hs new file mode 100644 --- /dev/null +++ b/test/golden/RefineIntroWhere.hs @@ -0,0 +1,6 @@ +test :: Maybe Int -> Int +test = _ + where + -- Don't delete me! + blah = undefined +