hls-tactics-plugin 1.3.0.0 → 1.4.0.0

raw patch · 35 files changed

+1178/−432 lines, 35 filesdep +unagi-chanPVP ok

version bump matches the API change (PVP)

Dependencies added: unagi-chan

API changes (from Hackage documentation)

Files

• hls-tactics-plugin.cabal +7/−1
• src/Ide/Plugin/Tactic.hs +1/−5
• src/Refinery/Future.hs +140/−0
• src/Wingman/AbstractLSP.hs +270/−0
• src/Wingman/AbstractLSP/TacticActions.hs +173/−0
• src/Wingman/AbstractLSP/Types.hs +171/−0
• src/Wingman/CodeGen.hs +21/−1
• src/Wingman/EmptyCase.hs +42/−48
• src/Wingman/GHC.hs +8/−3
• src/Wingman/LanguageServer.hs +20/−6
• src/Wingman/LanguageServer/TacticProviders.hs +30/−56
• src/Wingman/Machinery.hs +52/−29
• src/Wingman/Metaprogramming/Parser.hs +19/−6
• src/Wingman/Plugin.hs +16/−237
• src/Wingman/Tactics.hs +67/−25
• src/Wingman/Types.hs +4/−1
• test/AutoTupleSpec.hs +7/−3
• test/CodeAction/AutoSpec.hs +1/−0
• test/CodeAction/IntroDestructSpec.hs +36/−0
• test/CodeAction/RefineSpec.hs +1/−0
• test/CodeAction/RunMetaprogramSpec.hs +2/−0
• test/UnificationSpec.hs +27/−11
• test/golden/AutoUnusedPatternMatch.expected.hs +2/−0
• test/golden/AutoUnusedPatternMatch.hs +2/−0
• test/golden/IntroDestructLetBinding.expected.hs +6/−0
• test/golden/IntroDestructLetBinding.hs +5/−0
• test/golden/IntroDestructMany.expected.hs +4/−0
• test/golden/IntroDestructMany.hs +3/−0
• test/golden/IntroDestructOne.expected.hs +6/−0
• test/golden/IntroDestructOne.hs +5/−0
• test/golden/IntroDestructProvider.hs +9/−0
• test/golden/MetaLetSimple.expected.hs +7/−0
• test/golden/MetaLetSimple.hs +2/−0
• test/golden/RefineIntroWhere.expected.hs +6/−0
• test/golden/RefineIntroWhere.hs +6/−0

@@ -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 <https://github.com/haskell/haskell-language-server#readme>@@ -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

@@ -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 

@@ -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)+

@@ -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+        }+

@@ -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+

@@ -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+

@@ -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 

@@ -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

@@ -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]

@@ -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  

@@ -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 

@@ -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   ------------------------------------------------------------------------------

@@ -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 "<splice>" (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

@@ -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+      } 

@@ -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

@@ -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 

@@ -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

@@ -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"

@@ -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, "")+      ]+

@@ -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

@@ -39,5 +39,7 @@     metaTest  4 28 "MetaUseSymbol"     metaTest  7 53 "MetaDeepOf"     metaTest  2 34 "MetaWithArg"+    metaTest  2 18 "MetaLetSimple"+     metaTest  2 12 "IntrosTooMany" 

@@ -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  

@@ -0,0 +1,2 @@+test :: Bool -> ()+test _ = ()

@@ -0,0 +1,2 @@+test :: Bool -> ()+test = _

@@ -0,0 +1,6 @@+test :: IO ()+test = do+  let x :: Bool -> Int+      x False = _w0+      x True = _w1+  pure ()

@@ -0,0 +1,5 @@+test :: IO ()+test = do+  let x :: Bool -> Int+      x = _+  pure ()

@@ -0,0 +1,4 @@+x :: Bool -> Maybe Int -> String -> Int+x False = _w0+x True = _w1+

@@ -0,0 +1,3 @@+x :: Bool -> Maybe Int -> String -> Int+x = _+

@@ -0,0 +1,6 @@+module Test where++x :: Bool -> Int+x False = _w0+x True = _w1+

@@ -0,0 +1,5 @@+module Test where++x :: Bool -> Int+x = _+

@@ -0,0 +1,9 @@+hasAlgTy :: Maybe Int -> Int+hasAlgTy = _++hasFunTy :: (Int -> Int) -> Int+hasFunTy = _++isSaturated :: Bool -> Int+isSaturated b = _+

@@ -0,0 +1,7 @@+test :: Int+test+  = let+      a = _w0+      b = _w1+      c = _w2+    in _w3

@@ -0,0 +1,2 @@+test :: Int+test = [wingman| let a b c |]

@@ -0,0 +1,6 @@+test :: Maybe Int -> Int+test = \ m_n -> _w0+  where+    -- Don't delete me!+    blah = undefined+

@@ -0,0 +1,6 @@+test :: Maybe Int -> Int+test = _+  where+    -- Don't delete me!+    blah = undefined+