hls-tactics-plugin (empty) → 0.5.1.0

raw patch · 21 files changed

+3085/−0 lines, 21 filesdep +QuickCheckdep +aesondep +base

Dependencies added: QuickCheck, aeson, base, checkers, containers, deepseq, directory, extra, filepath, fingertree, generic-lens, ghc, ghc-boot-th, ghc-exactprint, ghc-source-gen, ghcide, haskell-lsp, hie-bios, hls-plugin-api, hls-tactics-plugin, hspec, lens, mtl, refinery, retrie, shake, syb, text, transformers

Files

• LICENSE +201/−0
• hls-tactics-plugin.cabal +97/−0
• src/Ide/Plugin/Tactic.hs +368/−0
• src/Ide/Plugin/Tactic/Auto.hs +28/−0
• src/Ide/Plugin/Tactic/CodeGen.hs +262/−0
• src/Ide/Plugin/Tactic/Context.hs +96/−0
• src/Ide/Plugin/Tactic/Debug.hs +55/−0
• src/Ide/Plugin/Tactic/GHC.hs +156/−0
• src/Ide/Plugin/Tactic/Judgements.hs +380/−0
• src/Ide/Plugin/Tactic/KnownStrategies.hs +39/−0
• src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +112/−0
• src/Ide/Plugin/Tactic/Machinery.hs +254/−0
• src/Ide/Plugin/Tactic/Naming.hs +93/−0
• src/Ide/Plugin/Tactic/Range.hs +18/−0
• src/Ide/Plugin/Tactic/Tactics.hs +287/−0
• src/Ide/Plugin/Tactic/TestTypes.hs +27/−0
• src/Ide/Plugin/Tactic/Types.hs +367/−0
• src/Ide/TreeTransform.hs +122/−0
• test/AutoTupleSpec.hs +57/−0
• test/Main.hs +1/−0
• test/UnificationSpec.hs +65/−0

@@ -0,0 +1,201 @@+                                 Apache License+                           Version 2.0, January 2004+                        http://www.apache.org/licenses/++   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION++   1. Definitions.++      "License" shall mean the terms and conditions for use, reproduction,+      and distribution as defined by Sections 1 through 9 of this document.++      "Licensor" shall mean the copyright owner or entity authorized by+      the copyright owner that is granting the License.++      "Legal Entity" shall mean the union of the acting entity and all+      other entities that control, are controlled by, or are under common+      control with that entity. For the purposes of this definition,+      "control" means (i) the power, direct or indirect, to cause the+      direction or management of such entity, whether by contract or+      otherwise, or (ii) ownership of fifty percent (50%) or more of the+      outstanding shares, or (iii) beneficial ownership of such entity.++      "You" (or "Your") shall mean an individual or Legal Entity+      exercising permissions granted by this License.++      "Source" form shall mean the preferred form for making modifications,+      including but not limited to software source code, documentation+      source, and configuration files.++      "Object" form shall mean any form resulting from mechanical+      transformation or translation of a Source form, including but+      not limited to compiled object code, generated documentation,+      and conversions to other media types.++      "Work" shall mean the work of authorship, whether in Source or+      Object form, made available under the License, as indicated by a+      copyright notice that is included in or attached to the work+      (an example is provided in the Appendix below).++      "Derivative Works" shall mean any work, whether in Source or Object+      form, that is based on (or derived from) the Work and for which the+      editorial revisions, annotations, elaborations, or other modifications+      represent, as a whole, an original work of authorship. For the purposes+      of this License, Derivative Works shall not include works that remain+      separable from, or merely link (or bind by name) to the interfaces of,+      the Work and Derivative Works thereof.++      "Contribution" shall mean any work of authorship, including+      the original version of the Work and any modifications or additions+      to that Work or Derivative Works thereof, that is intentionally+      submitted to Licensor for inclusion in the Work by the copyright owner+      or by an individual or Legal Entity authorized to submit on behalf of+      the copyright owner. For the purposes of this definition, "submitted"+      means any form of electronic, verbal, or written communication sent+      to the Licensor or its representatives, including but not limited to+      communication on electronic mailing lists, source code control systems,+      and issue tracking systems that are managed by, or on behalf of, the+      Licensor for the purpose of discussing and improving the Work, but+      excluding communication that is conspicuously marked or otherwise+      designated in writing by the copyright owner as "Not a Contribution."++      "Contributor" shall mean Licensor and any individual or Legal Entity+      on behalf of whom a Contribution has been received by Licensor and+      subsequently incorporated within the Work.++   2. Grant of Copyright License. Subject to the terms and conditions of+      this License, each Contributor hereby grants to You a perpetual,+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable+      copyright license to reproduce, prepare Derivative Works of,+      publicly display, publicly perform, sublicense, and distribute the+      Work and such Derivative Works in Source or Object form.++   3. Grant of Patent License. Subject to the terms and conditions of+      this License, each Contributor hereby grants to You a perpetual,+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable+      (except as stated in this section) patent license to make, have made,+      use, offer to sell, sell, import, and otherwise transfer the Work,+      where such license applies only to those patent claims licensable+      by such Contributor that are necessarily infringed by their+      Contribution(s) alone or by combination of their Contribution(s)+      with the Work to which such Contribution(s) was submitted. If You+      institute patent litigation against any entity (including a+      cross-claim or counterclaim in a lawsuit) alleging that the Work+      or a Contribution incorporated within the Work constitutes direct+      or contributory patent infringement, then any patent licenses+      granted to You under this License for that Work shall terminate+      as of the date such litigation is filed.++   4. Redistribution. You may reproduce and distribute copies of the+      Work or Derivative Works thereof in any medium, with or without+      modifications, and in Source or Object form, provided that You+      meet the following conditions:++      (a) You must give any other recipients of the Work or+          Derivative Works a copy of this License; and++      (b) You must cause any modified files to carry prominent notices+          stating that You changed the files; and++      (c) You must retain, in the Source form of any Derivative Works+          that You distribute, all copyright, patent, trademark, and+          attribution notices from the Source form of the Work,+          excluding those notices that do not pertain to any part of+          the Derivative Works; and++      (d) If the Work includes a "NOTICE" text file as part of its+          distribution, then any Derivative Works that You distribute must+          include a readable copy of the attribution notices contained+          within such NOTICE file, excluding those notices that do not+          pertain to any part of the Derivative Works, in at least one+          of the following places: within a NOTICE text file distributed+          as part of the Derivative Works; within the Source form or+          documentation, if provided along with the Derivative Works; or,+          within a display generated by the Derivative Works, if and+          wherever such third-party notices normally appear. The contents+          of the NOTICE file are for informational purposes only and+          do not modify the License. You may add Your own attribution+          notices within Derivative Works that You distribute, alongside+          or as an addendum to the NOTICE text from the Work, provided+          that such additional attribution notices cannot be construed+          as modifying the License.++      You may add Your own copyright statement to Your modifications and+      may provide additional or different license terms and conditions+      for use, reproduction, or distribution of Your modifications, or+      for any such Derivative Works as a whole, provided Your use,+      reproduction, and distribution of the Work otherwise complies with+      the conditions stated in this License.++   5. Submission of Contributions. Unless You explicitly state otherwise,+      any Contribution intentionally submitted for inclusion in the Work+      by You to the Licensor shall be under the terms and conditions of+      this License, without any additional terms or conditions.+      Notwithstanding the above, nothing herein shall supersede or modify+      the terms of any separate license agreement you may have executed+      with Licensor regarding such Contributions.++   6. Trademarks. This License does not grant permission to use the trade+      names, trademarks, service marks, or product names of the Licensor,+      except as required for reasonable and customary use in describing the+      origin of the Work and reproducing the content of the NOTICE file.++   7. Disclaimer of Warranty. Unless required by applicable law or+      agreed to in writing, Licensor provides the Work (and each+      Contributor provides its Contributions) on an "AS IS" BASIS,+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+      implied, including, without limitation, any warranties or conditions+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A+      PARTICULAR PURPOSE. You are solely responsible for determining the+      appropriateness of using or redistributing the Work and assume any+      risks associated with Your exercise of permissions under this License.++   8. Limitation of Liability. In no event and under no legal theory,+      whether in tort (including negligence), contract, or otherwise,+      unless required by applicable law (such as deliberate and grossly+      negligent acts) or agreed to in writing, shall any Contributor be+      liable to You for damages, including any direct, indirect, special,+      incidental, or consequential damages of any character arising as a+      result of this License or out of the use or inability to use the+      Work (including but not limited to damages for loss of goodwill,+      work stoppage, computer failure or malfunction, or any and all+      other commercial damages or losses), even if such Contributor+      has been advised of the possibility of such damages.++   9. Accepting Warranty or Additional Liability. While redistributing+      the Work or Derivative Works thereof, You may choose to offer,+      and charge a fee for, acceptance of support, warranty, indemnity,+      or other liability obligations and/or rights consistent with this+      License. However, in accepting such obligations, You may act only+      on Your own behalf and on Your sole responsibility, not on behalf+      of any other Contributor, and only if You agree to indemnify,+      defend, and hold each Contributor harmless for any liability+      incurred by, or claims asserted against, such Contributor by reason+      of your accepting any such warranty or additional liability.++   END OF TERMS AND CONDITIONS++   APPENDIX: How to apply the Apache License to your work.++      To apply the Apache License to your work, attach the following+      boilerplate notice, with the fields enclosed by brackets "[]"+      replaced with your own identifying information. (Don't include+      the brackets!)  The text should be enclosed in the appropriate+      comment syntax for the file format. We also recommend that a+      file or class name and description of purpose be included on the+      same "printed page" as the copyright notice for easier+      identification within third-party archives.++   Copyright [yyyy] [name of copyright owner]++   Licensed under the Apache License, Version 2.0 (the "License");+   you may not use this file except in compliance with the License.+   You may obtain a copy of the License at++       http://www.apache.org/licenses/LICENSE-2.0++   Unless required by applicable law or agreed to in writing, software+   distributed under the License is distributed on an "AS IS" BASIS,+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+   See the License for the specific language governing permissions and+   limitations under the License.

@@ -0,0 +1,97 @@+cabal-version:      2.2+category:           Development+name:               hls-tactics-plugin+version:            0.5.1.0+synopsis:           Tactics plugin for Haskell Language Server+description:        Please see README.md+author:             Sandy Maguire, Reed Mullanix+maintainer:         sandy@sandymaguire.me+copyright:          Sandy Maguire, Reed Mullanix+license:            Apache-2.0+license-file:       LICENSE+build-type:         Simple+-- extra-source-files:+--   README.md+--   ChangeLog.md++flag pedantic+  description: Enable -Werror+  default:     False+  manual:      True++library+  hs-source-dirs:   src+  exposed-modules:+    Ide.Plugin.Tactic+    Ide.Plugin.Tactic.Auto+    Ide.Plugin.Tactic.CodeGen+    Ide.Plugin.Tactic.Context+    Ide.Plugin.Tactic.Debug+    Ide.Plugin.Tactic.GHC+    Ide.Plugin.Tactic.Judgements+    Ide.Plugin.Tactic.KnownStrategies+    Ide.Plugin.Tactic.KnownStrategies.QuickCheck+    Ide.Plugin.Tactic.Machinery+    Ide.Plugin.Tactic.Naming+    Ide.Plugin.Tactic.Range+    Ide.Plugin.Tactic.Tactics+    Ide.Plugin.Tactic.Types+    Ide.Plugin.Tactic.TestTypes+    Ide.TreeTransform++  ghc-options:+    -Wno-name-shadowing -Wredundant-constraints+  if flag(pedantic)+    ghc-options: -Werror++  build-depends:+    , aeson+    , base           >=4.12 && <5+    , containers+    , directory+    , extra+    , filepath+    , fingertree+    , generic-lens+    , ghc+    , ghc-boot-th+    , ghc-exactprint+    , ghc-source-gen+    , ghcide         >=0.1+    , haskell-lsp    ^>=0.22+    , hls-plugin-api+    , lens+    , mtl+    , refinery       ^>=0.3+    , retrie         >=0.1.1.0+    , shake          >=0.17.5+    , syb+    , text+    , transformers+    , deepseq++  default-language: Haskell2010++test-suite tests+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+    AutoTupleSpec+    UnificationSpec+  hs-source-dirs:+      test+  ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      QuickCheck+    , base+    , checkers+    , hspec+    , mtl+    , hls-tactics-plugin+    , hls-plugin-api+    , hie-bios+    , ghc+    , containers+  build-tool-depends: hspec-discover:hspec-discover+  default-language: Haskell2010+

@@ -0,0 +1,368 @@+{-# LANGUAGE DeriveAnyClass      #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE NumDecimals         #-}+{-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections       #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE ViewPatterns        #-}++-- | A plugin that uses tactics to synthesize code+module Ide.Plugin.Tactic+  ( descriptor+  , tacticTitle+  , TacticCommand (..)+  ) where++import           Control.Arrow+import           Control.Monad+import           Control.Monad.Trans+import           Control.Monad.Trans.Maybe+import           Data.Aeson+import           Data.Coerce+import           Data.Functor ((<&>))+import           Data.Generics.Aliases (mkQ)+import           Data.Generics.Schemes (everything)+import           Data.List+import           Data.Map (Map)+import qualified Data.Map as M+import           Data.Maybe+import           Data.Monoid+import qualified Data.Set as S+import qualified Data.Text as T+import           Data.Traversable+import           Development.IDE.Core.PositionMapping+import           Development.IDE.Core.RuleTypes+import           Development.IDE.Core.Service (runAction)+import           Development.IDE.Core.Shake (useWithStale, IdeState (..))+import           Development.IDE.GHC.Compat+import           Development.IDE.GHC.Error (realSrcSpanToRange)+import           Development.IDE.Spans.LocalBindings (getDefiningBindings)+import           Development.Shake (Action)+import           DynFlags (xopt)+import qualified FastString+import           GHC.Generics (Generic)+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))+import           Ide.Plugin.Tactic.Auto+import           Ide.Plugin.Tactic.Context+import           Ide.Plugin.Tactic.GHC+import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Range+import           Ide.Plugin.Tactic.Tactics+import           Ide.Plugin.Tactic.TestTypes+import           Ide.Plugin.Tactic.Types+import           Ide.PluginUtils+import           Ide.TreeTransform (transform, graft, useAnnotatedSource)+import           Ide.Types+import           Language.Haskell.LSP.Core (clientCapabilities)+import           Language.Haskell.LSP.Types+import           OccName+import           SrcLoc (containsSpan)+import           System.Timeout+import           TcRnTypes (tcg_binds)+++descriptor :: PluginId -> PluginDescriptor IdeState+descriptor plId = (defaultPluginDescriptor plId)+    { pluginCommands+        = fmap (\tc ->+            PluginCommand+              (tcCommandId tc)+              (tacticDesc $ tcCommandName tc)+              (tacticCmd $ commandTactic tc))+              [minBound .. maxBound]+    , pluginCodeActionProvider = Just codeActionProvider+    }++tacticDesc :: T.Text -> T.Text+tacticDesc name = "fill the hole using the " <> name <> " tactic"++------------------------------------------------------------------------------+-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS+-- UI.+type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult]+++------------------------------------------------------------------------------+-- | Construct a 'CommandId'+tcCommandId :: TacticCommand -> CommandId+tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"+++------------------------------------------------------------------------------+-- | The name of the command for the LS.+tcCommandName :: TacticCommand -> T.Text+tcCommandName = T.pack . show++------------------------------------------------------------------------------+-- | Mapping from tactic commands to their contextual providers. See 'provide',+-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.+commandProvider :: TacticCommand -> TacticProvider+commandProvider Auto  = provide Auto ""+commandProvider Intros =+  filterGoalType isFunction $+    provide Intros ""+commandProvider Destruct =+  filterBindingType destructFilter $ \occ _ ->+    provide Destruct $ T.pack $ occNameString occ+commandProvider Homomorphism =+  filterBindingType homoFilter $ \occ _ ->+    provide Homomorphism $ T.pack $ occNameString occ+commandProvider DestructLambdaCase =+  requireExtension LambdaCase $+    filterGoalType (isJust . lambdaCaseable) $+      provide DestructLambdaCase ""+commandProvider HomomorphismLambdaCase =+  requireExtension LambdaCase $+    filterGoalType ((== Just True) . lambdaCaseable) $+      provide HomomorphismLambdaCase ""+++------------------------------------------------------------------------------+-- | A mapping from tactic commands to actual tactics for refinery.+commandTactic :: TacticCommand -> OccName -> TacticsM ()+commandTactic Auto         = const auto+commandTactic Intros       = const intros+commandTactic Destruct     = destruct+commandTactic Homomorphism = homo+commandTactic DestructLambdaCase     = const destructLambdaCase+commandTactic HomomorphismLambdaCase = const homoLambdaCase+++------------------------------------------------------------------------------+-- | We should show homos only when the goal type is the same as the binding+-- type, and that both are usual algebraic types.+homoFilter :: Type -> Type -> Bool+homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2+homoFilter _ _ = False+++------------------------------------------------------------------------------+-- | We should show destruct for bindings only when those bindings have usual+-- algebraic types.+destructFilter :: Type -> Type -> Bool+destructFilter _ (algebraicTyCon -> Just _) = True+destructFilter _ _ = False+++runIde :: IdeState -> Action a -> IO a+runIde state = runAction "tactic" state+++codeActionProvider :: CodeActionProvider IdeState+codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =+      fromMaybeT (Right $ List []) $ do+        (_, jdg, _, dflags) <- judgementForHole state nfp range+        actions <- lift $+          -- This foldMap is over the function monoid.+          foldMap commandProvider [minBound .. maxBound]+            dflags+            plId+            uri+            range+            jdg+        pure $ Right $ List actions+codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []+++codeActions :: [CodeAction] -> List CAResult+codeActions = List . fmap CACodeAction+++------------------------------------------------------------------------------+-- | Terminal constructor for providing context-sensitive tactics. Tactics+-- given by 'provide' are always available.+provide :: TacticCommand -> T.Text -> TacticProvider+provide tc name _ plId uri range _ = do+  let title = tacticTitle tc name+      params = TacticParams { file = uri , range = range , var_name = name }+  cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])+  pure+    $ pure+    $ CACodeAction+    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing+    $ Just cmd+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- predicate holds for the goal.+requireExtension :: Extension -> TacticProvider -> TacticProvider+requireExtension ext tp dflags plId uri range jdg =+  case xopt ext dflags of+    True  -> tp dflags plId uri range jdg+    False -> pure []+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- predicate holds for the goal.+filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider+filterGoalType p tp dflags plId uri range jdg =+  case p $ unCType $ jGoal jdg of+    True  -> tp dflags plId uri range jdg+    False -> pure []+++------------------------------------------------------------------------------+-- | Multiply a 'TacticProvider' for each binding, making sure it appears only+-- when the given predicate holds over the goal and binding types.+filterBindingType+    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.+    -> (OccName -> Type -> TacticProvider)+    -> TacticProvider+filterBindingType p tp dflags plId uri range jdg =+  let hy = jHypothesis jdg+      g  = jGoal jdg+   in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) ->+        case p (unCType g) ty of+          True  -> tp occ ty dflags plId uri range jdg+          False -> pure []+++data TacticParams = TacticParams+    { file :: Uri -- ^ Uri of the file to fill the hole in+    , range :: Range -- ^ The range of the hole+    , var_name :: T.Text+    }+  deriving (Show, Eq, Generic, ToJSON, FromJSON)+++------------------------------------------------------------------------------+-- | Find the last typechecked module, and find the most specific span, as well+-- as the judgement at the given range.+judgementForHole+    :: IdeState+    -> NormalizedFilePath+    -> Range+    -> MaybeT IO (Range, Judgement, Context, DynFlags)+judgementForHole state nfp range = do+  (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp+  range' <- liftMaybe $ fromCurrentRange amapping range++  (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp++  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'+  -- which don't change very often.+  ((modsum,_), _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp+  let dflags = ms_hspp_opts modsum++  (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast ->+      case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of+        Nothing -> Nothing+        Just ast' -> do+          let info = nodeInfo ast'+          ty <- listToMaybe $ nodeType info+          guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info+          pure (nodeSpan ast', ty)++  resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss+  (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp+  let tcg  = tmrTypechecked tcmod+      tcs = tcg_binds tcg+      ctx = mkContext+              (mapMaybe (sequenceA . (occName *** coerce))+                $ getDefiningBindings binds rss)+              tcg+      top_provs = getRhsPosVals rss tcs+      local_hy = spliceProvenance top_provs+               $ hypothesisFromBindings rss binds+      cls_hy = contextMethodHypothesis ctx+  pure ( resulting_range+       , mkFirstJudgement+           (local_hy <> cls_hy)+           (isRhsHole rss tcs)+           goal+       , ctx+       , dflags+       )+++spliceProvenance+    :: Map OccName Provenance+    -> Map OccName (HyInfo a)+    -> Map OccName (HyInfo a)+spliceProvenance provs =+  M.mapWithKey $ \name hi ->+    overProvenance (maybe id const $ M.lookup name provs) hi+++tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams+tacticCmd tac lf state (TacticParams uri range var_name)+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =+      fromMaybeT (Right Null, Nothing) $ do+        (range', jdg, ctx, dflags) <- judgementForHole state nfp range+        let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'+        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp+        x <- lift $ timeout 2e8 $+          case runTactic ctx jdg+                $ tac+                $ mkVarOcc+                $ T.unpack var_name of+            Left err ->+              pure $ (, Nothing)+                $ Left+                $ ResponseError InvalidRequest (T.pack $ show err) Nothing+            Right rtr -> do+              traceMX "solns" $ rtr_other_solns rtr+              let g = graft (RealSrcSpan span) $ rtr_extract rtr+                  response = transform dflags (clientCapabilities lf) uri g pm+              pure $ case response of+                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))+                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)+        pure $ case x of+          Just y -> y+          Nothing -> (, Nothing)+                   $ Left+                   $ ResponseError InvalidRequest "timed out" Nothing+tacticCmd _ _ _ _ =+  pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing+       , Nothing+       )+++fromMaybeT :: Functor m => a -> MaybeT m a -> m a+fromMaybeT def = fmap (fromMaybe def) . runMaybeT++liftMaybe :: Monad m => Maybe a -> MaybeT m a+liftMaybe a = MaybeT $ pure a+++------------------------------------------------------------------------------+-- | Is this hole immediately to the right of an equals sign?+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool+isRhsHole rss tcs = everything (||) (mkQ False $ \case+  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span+  _ -> False+  ) tcs+++------------------------------------------------------------------------------+-- | Compute top-level position vals of a function+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance+getRhsPosVals rss tcs+  = M.fromList+  $ join+  $ maybeToList+  $ getFirst+  $ everything (<>) (mkQ mempty $ \case+      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+        -> First $ do+            patnames <- traverse getPatName ps+            pure $ zip patnames $ [0..] <&> TopLevelArgPrv name+      _ -> mempty+  ) tcs++++-- TODO(sandy): Make this more robust+isHole :: OccName -> Bool+isHole = isPrefixOf "_" . occNameString+

@@ -0,0 +1,28 @@+module Ide.Plugin.Tactic.Auto where++import Control.Monad.State (gets)+import Ide.Plugin.Tactic.Context+import Ide.Plugin.Tactic.Judgements+import Ide.Plugin.Tactic.KnownStrategies+import Ide.Plugin.Tactic.Machinery (tracing)+import Ide.Plugin.Tactic.Tactics+import Ide.Plugin.Tactic.Types+import Refinery.Tactic+++------------------------------------------------------------------------------+-- | Automatically solve a goal.+auto :: TacticsM ()+auto = do+  jdg <- goal+  skolems <- gets ts_skolems+  current <- getCurrentDefinitions+  traceMX "goal" jdg+  traceMX "ctx" current+  traceMX "skolems" skolems+  commit knownStrategies+    . tracing "auto"+    . localTactic (auto' 4)+    . disallowing RecursiveCall+    $ fmap fst current+

@@ -0,0 +1,262 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TupleSections    #-}+{-# LANGUAGE ViewPatterns     #-}++module Ide.Plugin.Tactic.CodeGen where++import           Control.Lens ((+~), (%~), (<>~))+import           Control.Monad.Except+import           Control.Monad.State (MonadState)+import           Control.Monad.State.Class (modify)+import           Data.Generics.Product (field)+import           Data.List+import qualified Data.Map as M+import qualified Data.Set as S+import           Data.Traversable+import           DataCon+import           Development.IDE.GHC.Compat+import           GHC.Exts+import           GHC.SourceGen (RdrNameStr)+import           GHC.SourceGen.Binds+import           GHC.SourceGen.Expr+import           GHC.SourceGen.Overloaded+import           GHC.SourceGen.Pat+import           Ide.Plugin.Tactic.GHC+import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Machinery+import           Ide.Plugin.Tactic.Naming+import           Ide.Plugin.Tactic.Types+import           Name+import           Type hiding (Var)+++useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()+useOccName jdg name =+  -- Only score points if this is in the local hypothesis+  case M.lookup name $ jLocalHypothesis jdg of+    Just{}  -> modify+             $ (withUsedVals $ S.insert name)+             . (field @"ts_unused_top_vals" %~ S.delete name)+    Nothing -> pure ()+++------------------------------------------------------------------------------+-- | Doing recursion incurs a small penalty in the score.+countRecursiveCall :: TacticState -> TacticState+countRecursiveCall = field @"ts_recursion_count" +~ 1+++------------------------------------------------------------------------------+-- | Insert some values into the unused top values field. These are+-- subsequently removed via 'useOccName'.+addUnusedTopVals :: MonadState TacticState m => S.Set OccName -> m ()+addUnusedTopVals vals = modify $ field @"ts_unused_top_vals" <>~ vals+++destructMatches+    :: (DataCon -> Judgement -> Rule)+       -- ^ How to construct each match+    -> Maybe OccName+       -- ^ Scrutinee+    -> CType+       -- ^ Type being destructed+    -> Judgement+    -> RuleM (Trace, [RawMatch])+destructMatches f scrut t jdg = do+  let hy = jEntireHypothesis jdg+      g  = jGoal jdg+  case splitTyConApp_maybe $ unCType t of+    Nothing -> throwError $ GoalMismatch "destruct" g+    Just (tc, apps) -> do+      let dcs = tyConDataCons tc+      case dcs of+        [] -> throwError $ GoalMismatch "destruct" g+        _ -> fmap unzipTrace $ for dcs $ \dc -> do+          let args = dataConInstOrigArgTys' dc apps+          names <- mkManyGoodNames hy args+          let hy' = zip names $ coerce args+              j = introducingPat scrut dc hy'+                $ withNewGoal g jdg+          (tr, sg) <- f dc j+          modify $ withIntroducedVals $ mappend $ S.fromList names+          pure ( rose ("match " <> show dc <> " {" <>+                          intercalate ", " (fmap show names) <> "}")+                    $ pure tr+               , match [mkDestructPat dc names] $ unLoc sg+               )+++------------------------------------------------------------------------------+-- | Produces a pattern for a data con and the names of its fields.+mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs+mkDestructPat dcon names+  | isTupleDataCon dcon =+      tuple pat_args+  | otherwise =+      infixifyPatIfNecessary dcon $+        conP+          (coerceName $ dataConName dcon)+          pat_args+  where+    pat_args = fmap bvar' names+++infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs+infixifyPatIfNecessary dcon x+  | dataConIsInfix dcon =+      case x of+        ConPatIn op (PrefixCon [lhs, rhs]) ->+          ConPatIn op $ InfixCon lhs rhs+        y -> y+  | otherwise = x++++unzipTrace :: [(Trace, a)] -> (Trace, [a])+unzipTrace l =+  let (trs, as) = unzip l+   in (rose mempty trs, as)+++-- | Essentially same as 'dataConInstOrigArgTys' in GHC,+--  but only accepts universally quantified types as the second arguments+--  and automatically introduces existentials.+--+-- NOTE: The behaviour depends on GHC's 'dataConInstOrigArgTys'.+--       We need some tweaks if the compiler changes the implementation.+dataConInstOrigArgTys'+  :: DataCon+      -- ^ 'DataCon'structor+  -> [Type]+      -- ^ /Universally/ quantified type arguments to a result type.+      --   It /MUST NOT/ contain any dictionaries, coercion and existentials.+      --+      --   For example, for @MkMyGADT :: b -> MyGADT a c@, we+      --   must pass @[a, c]@ as this argument but not @b@, as @b@ is an existential.+  -> [Type]+      -- ^ Types of arguments to the DataCon with returned type is instantiated with the second argument.+dataConInstOrigArgTys' con uniTys =+  let exvars = dataConExTys con+   in dataConInstOrigArgTys con $+        uniTys ++ fmap mkTyVarTy exvars+      -- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys'+      -- unifies the second argument with DataCon's universals followed by existentials.+      -- If the definition of 'dataConInstOrigArgTys' changes,+      -- this place must be changed accordingly.++------------------------------------------------------------------------------+-- | Combinator for performing case splitting, and running sub-rules on the+-- resulting matches.++destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule+destruct' f term jdg = do+  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic+  let hy = jHypothesis jdg+  case M.lookup term hy of+    Nothing -> throwError $ UndefinedHypothesis term+    Just (hi_type -> t) -> do+      useOccName jdg term+      (tr, ms)+          <- destructMatches+               f+               (Just term)+               t+               $ disallowing AlreadyDestructed [term] jdg+      pure ( rose ("destruct " <> show term) $ pure tr+           , noLoc $ case' (var' term) ms+           )+++------------------------------------------------------------------------------+-- | Combinator for performign case splitting, and running sub-rules on the+-- resulting matches.+destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule+destructLambdaCase' f jdg = do+  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic+  let g  = jGoal jdg+  case splitFunTy_maybe (unCType g) of+    Just (arg, _) | isAlgType arg ->+      fmap (fmap noLoc $ lambdaCase) <$>+        destructMatches f Nothing (CType arg) jdg+    _ -> throwError $ GoalMismatch "destructLambdaCase'" g+++------------------------------------------------------------------------------+-- | Construct a data con with subgoals for each field.+buildDataCon+    :: Judgement+    -> DataCon            -- ^ The data con to build+    -> [Type]             -- ^ Type arguments for the data con+    -> RuleM (Trace, LHsExpr GhcPs)+buildDataCon jdg dc apps = do+  let args = dataConInstOrigArgTys' dc apps+  (tr, sgs)+      <- fmap unzipTrace+       $ traverse ( \(arg, n) ->+                    newSubgoal+                  . filterSameTypeFromOtherPositions dc n+                  . blacklistingDestruct+                  . flip withNewGoal jdg+                  $ CType arg+                  ) $ zip args [0..]+  pure+    . (rose (show dc) $ pure tr,)+    $ mkCon dc sgs+++mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs+mkCon dcon (fmap unLoc -> args)+  | isTupleDataCon dcon =+      noLoc $ tuple args+  | dataConIsInfix dcon+  , (lhs : rhs : args') <- args =+      noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'+  | otherwise =+      noLoc $ foldl' (@@) (bvar' $ occName $ dcon_name) args+  where+    dcon_name = dataConName dcon++++coerceName :: HasOccName a => a -> RdrNameStr+coerceName = fromString . occNameString . occName++++------------------------------------------------------------------------------+-- | Like 'var', but works over standard GHC 'OccName's.+var' :: Var a => OccName -> a+var' = var . fromString . occNameString+++------------------------------------------------------------------------------+-- | Like 'bvar', but works over standard GHC 'OccName's.+bvar' :: BVar a => OccName -> a+bvar' = bvar . fromString . occNameString+++------------------------------------------------------------------------------+-- | Get an HsExpr corresponding to a function name.+mkFunc :: String -> HsExpr GhcPs+mkFunc = var' . mkVarOcc+++------------------------------------------------------------------------------+-- | Get an HsExpr corresponding to a value name.+mkVal :: String -> HsExpr GhcPs+mkVal = var' . mkVarOcc+++------------------------------------------------------------------------------+-- | Like 'op', but easier to call.+infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs+infixCall s = flip op (fromString s)+++------------------------------------------------------------------------------+-- | Like '(@@)', but uses a dollar instead of parentheses.+appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs+appDollar = infixCall "$"+

@@ -0,0 +1,96 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase       #-}++module Ide.Plugin.Tactic.Context where++import           Bag+import           Control.Arrow+import           Control.Monad.Reader+import           Data.List+import           Data.Map (Map)+import qualified Data.Map as M+import           Data.Maybe (mapMaybe)+import           Data.Set (Set)+import qualified Data.Set as S+import           Development.IDE.GHC.Compat+import           Ide.Plugin.Tactic.GHC (tacticsThetaTy)+import           Ide.Plugin.Tactic.Machinery (methodHypothesis)+import           Ide.Plugin.Tactic.Types+import           OccName+import           TcRnTypes+import           TcType (substTy, tcSplitSigmaTy)+import           Unify (tcUnifyTy)+++mkContext :: [(OccName, CType)] -> TcGblEnv -> Context+mkContext locals tcg = Context+  { ctxDefiningFuncs = locals+  , ctxModuleFuncs = fmap splitId+                   . (getFunBindId =<<)+                   . fmap unLoc+                   . bagToList+                   $ tcg_binds tcg+  }+++------------------------------------------------------------------------------+-- | Find all of the class methods that exist from the givens in the context.+contextMethodHypothesis :: Context -> Map OccName (HyInfo CType)+contextMethodHypothesis ctx+  = M.fromList+  . excludeForbiddenMethods+  . join+  . concatMap+      ( mapMaybe methodHypothesis+      . tacticsThetaTy+      . unCType+      )+  . mapMaybe (definedThetaType ctx)+  . fmap fst+  $ ctxDefiningFuncs ctx+++------------------------------------------------------------------------------+-- | Many operations are defined in typeclasses for performance reasons, rather+-- than being a true part of the class. This function filters out those, in+-- order to keep our hypothesis space small.+excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)]+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)+  where+    forbiddenMethods :: Set OccName+    forbiddenMethods = S.map mkVarOcc $ S.fromList+      [ -- monadfail+        "fail"+      ]+++------------------------------------------------------------------------------+-- | Given the name of a function that exists in 'ctxDefiningFuncs', get its+-- theta type.+definedThetaType :: Context -> OccName -> Maybe CType+definedThetaType ctx name = do+  (_, CType mono) <- find ((== name) . fst) $ ctxDefiningFuncs ctx+  (_, CType poly) <- find ((== name) . fst) $ ctxModuleFuncs ctx+  let (_, _, poly') = tcSplitSigmaTy poly+  subst <- tcUnifyTy poly' mono+  pure $ CType $ substTy subst $ snd $ splitForAllTys poly+++splitId :: Id -> (OccName, CType)+splitId = occName &&& CType . idType+++getFunBindId :: HsBindLR GhcTc GhcTc -> [Id]+getFunBindId (AbsBinds _ _ _ abes _ _ _)+  = abes >>= \case+      ABE _ poly _ _ _ -> pure poly+      _ -> []+getFunBindId _ = []+++getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]+getCurrentDefinitions = asks $ ctxDefiningFuncs++getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]+getModuleHypothesis = asks ctxModuleFuncs+

@@ -0,0 +1,55 @@+{-# LANGUAGE BangPatterns     #-}+{-# LANGUAGE CPP              #-}+{-# LANGUAGE TypeApplications #-}++module Ide.Plugin.Tactic.Debug+  ( unsafeRender+  , unsafeRender'+  , traceM+  , traceShowId+  , trace+  , traceX+  , traceIdX+  , traceMX+  ) where++import Control.DeepSeq+import Control.Exception+import Debug.Trace+import DynFlags (unsafeGlobalDynFlags)+import Outputable hiding ((<>))+import System.IO.Unsafe (unsafePerformIO)++#if __GLASGOW_HASKELL__ >= 808+import PlainPanic (PlainGhcException)+type GHC_EXCEPTION = PlainGhcException+#else+import Panic (GhcException)+type GHC_EXCEPTION = GhcException+#endif+++------------------------------------------------------------------------------+-- | Print something+unsafeRender :: Outputable a => a -> String+unsafeRender = unsafeRender' . ppr+++unsafeRender' :: SDoc -> String+unsafeRender' sdoc = unsafePerformIO $ do+  let z = showSDoc unsafeGlobalDynFlags sdoc+  -- We might not have unsafeGlobalDynFlags (like during testing), in which+  -- case GHC panics. Instead of crashing, let's just fail to print.+  !res <- try @GHC_EXCEPTION $ evaluate $ deepseq z z+  pure $ either (const "<unsafeRender'>") id res+{-# NOINLINE unsafeRender' #-}++traceMX :: (Monad m, Show a) => String -> a -> m ()+traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a++traceX :: (Show a) => String -> a -> b -> b+traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)++traceIdX :: (Show a) => String -> a -> a+traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a+

@@ -0,0 +1,156 @@+{-# LANGUAGE CPP              #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PatternSynonyms  #-}+{-# LANGUAGE ViewPatterns     #-}++module Ide.Plugin.Tactic.GHC where++import           Control.Monad.State+import qualified Data.Map as M+import           Data.Maybe (isJust)+import           Data.Traversable+import qualified DataCon as DataCon+import           Development.IDE.GHC.Compat+import           Generics.SYB (mkT, everywhere)+import           Ide.Plugin.Tactic.Types+import           OccName+import           TcType+import           TyCoRep+import           Type+import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)+import           Unique+import           Var++tcTyVar_maybe :: Type -> Maybe Var+tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty'+tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty  -- look through casts, as+                                                -- this is only used for+                                                -- e.g., FlexibleContexts+tcTyVar_maybe (TyVarTy v)   = Just v+tcTyVar_maybe _             = Nothing+++instantiateType :: Type -> ([TyVar], Type)+instantiateType t = do+  let vs  = tyCoVarsOfTypeList t+      vs' = fmap cloneTyVar vs+      subst = foldr (\(v,t) a -> extendTCvSubst a v $ TyVarTy t) emptyTCvSubst+            $ zip vs vs'+   in (vs', substTy subst t)+++cloneTyVar :: TyVar -> TyVar+cloneTyVar t =+  let uniq = getUnique t+      some_magic_number = 49+   in setVarUnique t $ deriveUnique uniq some_magic_number+++------------------------------------------------------------------------------+-- | Is this a function type?+isFunction :: Type -> Bool+isFunction (tacticsSplitFunTy -> (_, _, [], _)) = False+isFunction _ = True+++------------------------------------------------------------------------------+-- | Split a function, also splitting out its quantified variables and theta+-- context.+tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)+tacticsSplitFunTy t+  = let (vars, theta, t') = tcSplitSigmaTy t+        (args, res) = tcSplitFunTys t'+     in (vars, theta, args, res)+++------------------------------------------------------------------------------+-- | Rip the theta context out of a regular type.+tacticsThetaTy :: Type -> ThetaType+tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta+++------------------------------------------------------------------------------+-- | Instantiate all of the quantified type variables in a type with fresh+-- skolems.+freshTyvars :: MonadState TacticState m => Type -> m Type+freshTyvars t = do+  let (tvs, _, _, _) = tacticsSplitFunTy t+  reps <- fmap M.fromList+        $ for tvs $ \tv -> do+            uniq <- freshUnique+            pure $ (tv, setTyVarUnique tv uniq)+  pure $+    everywhere+      (mkT $ \tv ->+        case M.lookup tv reps of+          Just tv' -> tv'+          Nothing -> tv+      ) t+++------------------------------------------------------------------------------+-- | Is this an algebraic type?+algebraicTyCon :: Type -> Maybe TyCon+algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))+  | tycon == intTyCon    = Nothing+  | tycon == floatTyCon  = Nothing+  | tycon == doubleTyCon = Nothing+  | tycon == charTyCon   = Nothing+  | tycon == funTyCon    = Nothing+  | otherwise = Just tycon+algebraicTyCon _ = Nothing++------------------------------------------------------------------------------+-- | Can ths type be lambda-cased?+--+-- Return: 'Nothing' if no+--         @Just False@ if it can't be homomorphic+--         @Just True@ if it can+lambdaCaseable :: Type -> Maybe Bool+lambdaCaseable (splitFunTy_maybe -> Just (arg, res))+  | isJust (algebraicTyCon arg)+  = Just $ isJust $ algebraicTyCon res+lambdaCaseable _ = Nothing++fromPatCompat :: PatCompat GhcTc -> Pat GhcTc+#if __GLASGOW_HASKELL__ == 808+type PatCompat pass = Pat pass+fromPatCompat = id+#else+type PatCompat pass = LPat pass+fromPatCompat = unLoc+#endif++------------------------------------------------------------------------------+-- | Should make sure it's a fun bind+pattern TopLevelRHS :: OccName -> [PatCompat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)+pattern TopLevelRHS name ps body <-+  Match _+    (FunRhs (L _ (occName -> name)) _ _)+    ps+    (GRHSs _+      [L _ (GRHS _ [] body)] _)++getPatName :: PatCompat GhcTc -> Maybe OccName+getPatName (fromPatCompat -> p0) =+  case p0 of+    VarPat  _ x   -> Just $ occName $ unLoc x+    LazyPat _ p   -> getPatName p+    AsPat   _ x _ -> Just $ occName $ unLoc x+    ParPat  _ p   -> getPatName p+    BangPat _ p   -> getPatName p+    ViewPat _ _ p -> getPatName p+#if __GLASGOW_HASKELL__ >= 808+    SigPat  _ p _ -> getPatName p+#endif+#if __GLASGOW_HASKELL__ == 808+    XPat   p      -> getPatName $ unLoc p+#endif+    _             -> Nothing++dataConExTys :: DataCon -> [TyCoVar]+#if __GLASGOW_HASKELL__ >= 808+dataConExTys = DataCon.dataConExTyCoVars+#else+dataConExTys = DataCon.dataConExTyVars+#endif

@@ -0,0 +1,380 @@+{-# LANGUAGE DataKinds        #-}+{-# LANGUAGE LambdaCase       #-}+{-# LANGUAGE RecordWildCards  #-}+{-# LANGUAGE TupleSections    #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns     #-}++module Ide.Plugin.Tactic.Judgements+  ( blacklistingDestruct+  , unwhitelistingSplit+  , introducingLambda+  , introducingRecursively+  , introducingPat+  , jGoal+  , jHypothesis+  , jEntireHypothesis+  , jPatHypothesis+  , substJdg+  , unsetIsTopHole+  , filterSameTypeFromOtherPositions+  , isDestructBlacklisted+  , withNewGoal+  , jLocalHypothesis+  , isSplitWhitelisted+  , isPatternMatch+  , filterPosition+  , isTopHole+  , disallowing+  , mkFirstJudgement+  , hypothesisFromBindings+  , isTopLevel+  ) where++import           Control.Lens hiding (Context)+import           Data.Bool+import           Data.Char+import           Data.Coerce+import           Data.Generics.Product (field)+import           Data.Map (Map)+import qualified Data.Map as M+import           Data.Maybe+import           Data.Set (Set)+import qualified Data.Set as S+import           DataCon (DataCon)+import           Development.IDE.Spans.LocalBindings+import           Ide.Plugin.Tactic.Types+import           OccName+import           SrcLoc+import           Type+++------------------------------------------------------------------------------+-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.+hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)+hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span+++------------------------------------------------------------------------------+-- | Convert a @Set Id@ into a hypothesis.+buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType)+buildHypothesis+  = M.fromList+  . mapMaybe go+  where+    go (occName -> occ, t)+      | Just ty <- t+      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty)+      | otherwise = Nothing+++blacklistingDestruct :: Judgement -> Judgement+blacklistingDestruct =+  field @"_jBlacklistDestruct" .~ True+++unwhitelistingSplit :: Judgement -> Judgement+unwhitelistingSplit =+  field @"_jWhitelistSplit" .~ False+++isDestructBlacklisted :: Judgement -> Bool+isDestructBlacklisted = _jBlacklistDestruct+++isSplitWhitelisted :: Judgement -> Bool+isSplitWhitelisted = _jWhitelistSplit+++withNewGoal :: a -> Judgement' a -> Judgement' a+withNewGoal t = field @"_jGoal" .~ t+++------------------------------------------------------------------------------+-- | Helper function for implementing functions which introduce new hypotheses.+introducing+    :: (Int -> Provenance)  -- ^ A function from the position of the arg to its+                            -- provenance.+    -> [(OccName, a)]+    -> Judgement' a+    -> Judgement' a+introducing f ns =+  field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>+    \(pos, (name, ty)) -> (name, HyInfo (f pos) ty))+++------------------------------------------------------------------------------+-- | Introduce bindings in the context of a lamba.+introducingLambda+    :: Maybe OccName   -- ^ The name of the top level function. For any other+                       -- function, this should be 'Nothing'.+    -> [(OccName, a)]+    -> Judgement' a+    -> Judgement' a+introducingLambda func = introducing $ \pos ->+  maybe UserPrv (\x -> TopLevelArgPrv x pos) func+++------------------------------------------------------------------------------+-- | Introduce a binding in a recursive context.+introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a+introducingRecursively = introducing $ const RecursivePrv+++------------------------------------------------------------------------------+-- | Check whether any of the given occnames are an ancestor of the term.+hasPositionalAncestry+    :: Foldable t+    => t OccName   -- ^ Desired ancestors.+    -> Judgement+    -> OccName     -- ^ Potential child+    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor+                   -- just false if it's a descendent+                   -- otherwise nothing+hasPositionalAncestry ancestors jdg name+  | not $ null ancestors+  = case any (== name) ancestors of+      True  -> Just True+      False ->+        case M.lookup name $ jAncestryMap jdg of+          Just ancestry ->+            bool Nothing (Just False) $ any (flip S.member ancestry) ancestors+          Nothing -> Nothing+  | otherwise = Nothing+++------------------------------------------------------------------------------+-- | Helper function for disallowing hypotheses that have the wrong ancestry.+filterAncestry+    :: Foldable t+    => t OccName+    -> DisallowReason+    -> Judgement+    -> Judgement+filterAncestry ancestry reason jdg =+    disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg+  where+    go name _+      = not+      . isJust+      $ hasPositionalAncestry ancestry jdg name+++------------------------------------------------------------------------------+-- | @filter defn pos@ removes any hypotheses which are bound in @defn@ to+-- a position other than @pos@. Any terms whose ancestry doesn't include @defn@+-- remain.+filterPosition :: OccName -> Int -> Judgement -> Judgement+filterPosition defn pos jdg =+  filterAncestry (findPositionVal jdg defn pos) (WrongBranch pos) jdg+++------------------------------------------------------------------------------+-- | Helper function for determining the ancestry list for 'filterPosition'.+findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName+findPositionVal jdg defn pos = listToMaybe $ do+  -- It's important to inspect the entire hypothesis here, as we need to trace+  -- ancstry through potentially disallowed terms in the hypothesis.+  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg+  case hi_provenance hi of+    TopLevelArgPrv defn' pos'+      | defn == defn'+      , pos  == pos' -> pure name+    PatternMatchPrv pv+      | pv_scrutinee pv == Just defn+      , pv_position pv  == pos -> pure name+    _ -> []+++------------------------------------------------------------------------------+-- | Helper function for determining the ancestry list for+-- 'filterSameTypeFromOtherPositions'.+findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]+findDconPositionVals jdg dcon pos = do+  (name, hi) <- M.toList $ jHypothesis jdg+  case hi_provenance hi of+    PatternMatchPrv pv+      | pv_datacon  pv == Uniquely dcon+      , pv_position pv == pos -> pure name+    _ -> []+++------------------------------------------------------------------------------+-- | Disallow any hypotheses who have the same type as anything bound by the+-- given position for the datacon. Used to ensure recursive functions like+-- 'fmap' preserve the relative ordering of their arguments by eliminating any+-- other term which might match.+filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement+filterSameTypeFromOtherPositions dcon pos jdg =+  let hy = jHypothesis+         $ filterAncestry+             (findDconPositionVals jdg dcon pos)+             (WrongBranch pos)+             jdg+      tys = S.fromList $ hi_type <$> M.elems hy+      to_remove =+        M.filter (flip S.member tys . hi_type) (jHypothesis jdg)+          M.\\ hy+   in disallowing Shadowed (M.keys to_remove) jdg+++------------------------------------------------------------------------------+-- | Return the ancestry of a 'PatVal', or 'mempty' otherwise.+getAncestry :: Judgement' a -> OccName -> Set OccName+getAncestry jdg name =+  case M.lookup name $ jPatHypothesis jdg of+    Just pv -> pv_ancestry pv+    Nothing -> mempty+++jAncestryMap :: Judgement' a -> Map OccName (Set OccName)+jAncestryMap jdg =+  flip M.map (jPatHypothesis jdg) pv_ancestry+++------------------------------------------------------------------------------+-- TODO(sandy): THIS THING IS A BIG BIG HACK+--+-- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined+-- (eg, we might be in a where block). The head of this list is not guaranteed+-- to be the one we're interested in.+extremelyStupid__definingFunction :: Context -> OccName+extremelyStupid__definingFunction =+  fst . head . ctxDefiningFuncs+++------------------------------------------------------------------------------+-- | Pattern vals are currently tracked in jHypothesis, with an extra piece of+-- data sitting around in jPatternVals.+introducingPat+    :: Maybe OccName+    -> DataCon+    -> [(OccName, a)]+    -> Judgement' a+    -> Judgement' a+introducingPat scrutinee dc ns jdg+  = introducing (\pos ->+      PatternMatchPrv $+        PatVal+          scrutinee+          (maybe mempty+                (\scrut -> S.singleton scrut <> getAncestry jdg scrut)+                scrutinee)+          (Uniquely dc)+          pos+    ) ns jdg+++------------------------------------------------------------------------------+-- | Prevent some occnames from being used in the hypothesis. This will hide+-- them from 'jHypothesis', but not from 'jEntireHypothesis'.+disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a+disallowing reason (S.fromList -> ns) =+  field @"_jHypothesis" %~ (M.mapWithKey $ \name hi ->+    case S.member name ns of+      True -> overProvenance (DisallowedPrv reason) hi+      False -> hi+                           )+++------------------------------------------------------------------------------+-- | The hypothesis, consisting of local terms and the ambient environment+-- (impors and class methods.) Hides disallowed values.+jHypothesis :: Judgement' a -> Map OccName (HyInfo a)+jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis+++------------------------------------------------------------------------------+-- | The whole hypothesis, including things disallowed.+jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)+jEntireHypothesis = _jHypothesis+++------------------------------------------------------------------------------+-- | Just the local hypothesis.+jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)+jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis+++------------------------------------------------------------------------------+-- | If we're in a top hole, the name of the defining function.+isTopHole :: Context -> Judgement' a -> Maybe OccName+isTopHole ctx =+  bool Nothing (Just $ extremelyStupid__definingFunction ctx) . _jIsTopHole+++unsetIsTopHole :: Judgement' a -> Judgement' a+unsetIsTopHole = field @"_jIsTopHole" .~ False+++------------------------------------------------------------------------------+-- | Only the hypothesis members which are pattern vals+jPatHypothesis :: Judgement' a -> Map OccName PatVal+jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis+++getPatVal :: Provenance-> Maybe PatVal+getPatVal prov =+  case prov of+    PatternMatchPrv pv -> Just pv+    _                  -> Nothing+++jGoal :: Judgement' a -> a+jGoal = _jGoal+++substJdg :: TCvSubst -> Judgement -> Judgement+substJdg subst = fmap $ coerce . substTy subst . coerce+++mkFirstJudgement+    :: M.Map OccName (HyInfo CType)+    -> Bool  -- ^ are we in the top level rhs hole?+    -> Type+    -> Judgement' CType+mkFirstJudgement hy top goal = Judgement+  { _jHypothesis        = hy+  , _jBlacklistDestruct = False+  , _jWhitelistSplit    = True+  , _jIsTopHole         = top+  , _jGoal              = CType goal+  }+++------------------------------------------------------------------------------+-- | Is this a top level function binding?+isTopLevel :: Provenance -> Bool+isTopLevel TopLevelArgPrv{} = True+isTopLevel _                = False+++------------------------------------------------------------------------------+-- | Is this a local function argument, pattern match or user val?+isLocalHypothesis :: Provenance -> Bool+isLocalHypothesis UserPrv{}         = True+isLocalHypothesis PatternMatchPrv{} = True+isLocalHypothesis TopLevelArgPrv{}  = True+isLocalHypothesis _                 = False+++------------------------------------------------------------------------------+-- | Is this a pattern match?+isPatternMatch :: Provenance -> Bool+isPatternMatch PatternMatchPrv{} = True+isPatternMatch _                 = False+++------------------------------------------------------------------------------+-- | Was this term ever disallowed?+isDisallowed :: Provenance -> Bool+isDisallowed DisallowedPrv{} = True+isDisallowed _               = False+++------------------------------------------------------------------------------+-- | Eliminates 'DisallowedPrv' provenances.+expandDisallowed :: Provenance -> Provenance+expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv+expandDisallowed prv = prv+

@@ -0,0 +1,39 @@+{-# LANGUAGE LambdaCase #-}++module Ide.Plugin.Tactic.KnownStrategies where++import Control.Monad.Error.Class+import Ide.Plugin.Tactic.Context (getCurrentDefinitions)+import Ide.Plugin.Tactic.Tactics+import Ide.Plugin.Tactic.Types+import OccName (mkVarOcc)+import Refinery.Tactic+import Ide.Plugin.Tactic.Machinery (tracing)+import Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary)+++knownStrategies :: TacticsM ()+knownStrategies = choice+  [ known "fmap" deriveFmap+  , known "arbitrary" deriveArbitrary+  ]+++known :: String -> TacticsM () -> TacticsM ()+known name t = do+  getCurrentDefinitions >>= \case+    [(def, _)] | def == mkVarOcc name ->+      tracing ("known " <> name) t+    _ -> throwError NoApplicableTactic+++deriveFmap :: TacticsM ()+deriveFmap = do+  try intros+  overAlgebraicTerms homo+  choice+    [ overFunctions apply >> auto' 2+    , assumption+    , recursion+    ]+

@@ -0,0 +1,112 @@+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE LambdaCase #-}++module Ide.Plugin.Tactic.KnownStrategies.QuickCheck where++import Control.Monad.Except (MonadError(throwError))+import Data.Bool (bool)+import Data.List (partition)+import DataCon ( DataCon, dataConName )+import Development.IDE.GHC.Compat (HsExpr, GhcPs, noLoc)+import GHC.Exts ( IsString(fromString) )+import GHC.List ( foldl' )+import GHC.SourceGen (int)+import GHC.SourceGen.Binds ( match, valBind )+import GHC.SourceGen.Expr ( case', lambda, let' )+import GHC.SourceGen.Overloaded ( App((@@)), HasList(list) )+import GHC.SourceGen.Pat ( conP )+import Ide.Plugin.Tactic.CodeGen+import Ide.Plugin.Tactic.Judgements (jGoal)+import Ide.Plugin.Tactic.Machinery (tracePrim)+import Ide.Plugin.Tactic.Types+import OccName (occNameString,  mkVarOcc, HasOccName(occName) )+import Refinery.Tactic (goal,  rule )+import TyCon (tyConName,  TyCon, tyConDataCons )+import Type ( splitTyConApp_maybe )+import Data.Generics (mkQ, everything)+++------------------------------------------------------------------------------+-- | Known tactic for deriving @arbitrary :: Gen a@. This tactic splits the+-- type's data cons into terminal and inductive cases, and generates code that+-- produces a terminal if the QuickCheck size parameter is <=1, or any data con+-- otherwise. It correctly scales recursive parameters, ensuring termination.+deriveArbitrary :: TacticsM ()+deriveArbitrary = do+  ty <- jGoal <$> goal+  case splitTyConApp_maybe $ unCType ty of+    Just (gen_tc, [splitTyConApp_maybe -> Just (tc, apps)])+        | occNameString (occName $ tyConName gen_tc) == "Gen" -> do+      rule $ \_ -> do+        let dcs = tyConDataCons tc+            (terminal, big) = partition ((== 0) . genRecursiveCount)+                        $ fmap (mkGenerator tc apps) dcs+            terminal_expr = mkVal "terminal"+            oneof_expr = mkVal "oneof"+        pure+          ( tracePrim "deriveArbitrary"+          , noLoc $+              let' [valBind (fromString "terminal") $ list $ fmap genExpr terminal] $+                appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $+                  case' (infixCall "<=" (mkVal "n") (int 1))+                    [ match [conP (fromString "True") []] $+                        oneof_expr @@ terminal_expr+                    , match [conP (fromString "False") []] $+                        appDollar oneof_expr $+                          infixCall "<>"+                            (list $ fmap genExpr big)+                            terminal_expr+                    ]+          )+    _ -> throwError $ GoalMismatch "deriveArbitrary" ty+++------------------------------------------------------------------------------+-- | Helper data type for the generator of a specific data con.+data Generator = Generator+  { genRecursiveCount :: Integer+  , genExpr :: HsExpr GhcPs+  }+++------------------------------------------------------------------------------+-- | Make a 'Generator' for a given tycon instantiated with the given @[Type]@.+mkGenerator :: TyCon -> [Type] -> DataCon -> Generator+mkGenerator tc apps dc = do+  let dc_expr   = var' $ occName $ dataConName dc+      args = dataConInstOrigArgTys' dc apps+      num_recursive_calls = sum $ fmap (bool 0 1 . doesTypeContain tc) args+      mkArbitrary = mkArbitraryCall tc num_recursive_calls+  Generator num_recursive_calls $ case args of+    []  -> mkFunc "pure" @@ dc_expr+    (a : as) ->+      foldl'+        (infixCall "<*>")+        (infixCall "<$>" dc_expr $ mkArbitrary a)+        (fmap mkArbitrary as)+++------------------------------------------------------------------------------+-- | Check if the given 'TyCon' exists anywhere in the 'Type'.+doesTypeContain :: TyCon -> Type -> Bool+doesTypeContain recursive_tc =+  everything (||) $ mkQ False (== recursive_tc)+++------------------------------------------------------------------------------+-- | Generate the correct sort of call to @arbitrary@. For recursive calls, we+-- need to scale down the size parameter, either by a constant factor of 1 if+-- it's the only recursive parameter, or by @`div` n@ where n is the number of+-- recursive parameters. For all other types, just call @arbitrary@ directly.+mkArbitraryCall :: TyCon -> Integer -> Type -> HsExpr GhcPs+mkArbitraryCall recursive_tc n ty =+  let arbitrary = mkFunc "arbitrary"+   in case doesTypeContain recursive_tc ty of+        True ->+          mkFunc "scale"+            @@ bool (mkFunc "flip" @@ mkFunc "div" @@ int n)+                    (mkFunc "subtract" @@ int 1)+                    (n == 1)+            @@ arbitrary+        False -> arbitrary+

@@ -0,0 +1,254 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE DerivingStrategies    #-}+{-# LANGUAGE DerivingVia           #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MonoLocalBinds        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards       #-}+{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE ViewPatterns          #-}+{-# OPTIONS_GHC -fno-warn-orphans  #-}++module Ide.Plugin.Tactic.Machinery+  ( module Ide.Plugin.Tactic.Machinery+  ) where++import           Class (Class(classTyVars))+import           Control.Arrow+import           Control.Monad.Error.Class+import           Control.Monad.Reader+import           Control.Monad.State (MonadState(..))+import           Control.Monad.State.Class (gets, modify)+import           Control.Monad.State.Strict (StateT (..))+import           Data.Bool (bool)+import           Data.Coerce+import           Data.Either+import           Data.Foldable+import           Data.Functor ((<&>))+import           Data.Generics (mkQ, everything, gcount)+import           Data.List (sortBy)+import qualified Data.Map as M+import           Data.Ord (comparing, Down(..))+import           Data.Set (Set)+import qualified Data.Set as S+import           Development.IDE.GHC.Compat+import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Types+import           OccName (HasOccName(occName))+import           Refinery.ProofState+import           Refinery.Tactic+import           Refinery.Tactic.Internal+import           TcType+import           Type+import           Unify+++substCTy :: TCvSubst -> CType -> CType+substCTy subst = coerce . substTy subst . coerce+++------------------------------------------------------------------------------+-- | Produce a subgoal that must be solved before we can solve the original+-- goal.+newSubgoal+    :: Judgement+    -> Rule+newSubgoal j = do+    unifier <- gets ts_unifier+    subgoal+      $ substJdg unifier+      $ unsetIsTopHole j+++------------------------------------------------------------------------------+-- | Attempt to generate a term of the right type using in-scope bindings, and+-- a given tactic.+runTactic+    :: Context+    -> Judgement+    -> TacticsM ()       -- ^ Tactic to use+    -> Either [TacticError] RunTacticResults+runTactic ctx jdg t =+    let skolems = S.fromList+                $ foldMap (tyCoVarsOfTypeWellScoped . unCType)+                $ (:) (jGoal jdg)+                $ fmap hi_type+                $ toList+                $ jHypothesis jdg+        unused_topvals = M.keysSet+                       $ M.filter (isTopLevel . hi_provenance)+                       $ jHypothesis jdg+        tacticState =+          defaultTacticState+            { ts_skolems = skolems+            , ts_unused_top_vals = unused_topvals+            }+    in case partitionEithers+          . flip runReader ctx+          . unExtractM+          $ runTacticT t jdg tacticState of+      (errs, []) -> Left $ take 50 $ errs+      (_, fmap assoc23 -> solns) -> do+        let sorted =+              flip sortBy solns $ comparing $ \((_, ext), (jdg, holes)) ->+                Down $ scoreSolution ext jdg holes+        case sorted of+          (((tr, ext), _) : _) ->+            Right+              . RunTacticResults tr ext+              . reverse+              . fmap fst+              $ take 5 sorted+          -- guaranteed to not be empty+          _ -> Left []++assoc23 :: (a, b, c) -> (a, (b, c))+assoc23 (a, b, c) = (a, (b, c))+++tracePrim :: String -> Trace+tracePrim = flip rose []+++tracing+    :: Functor m+    => String+    -> TacticT jdg (Trace, ext) err s m a+    -> TacticT jdg (Trace, ext) err s m a+tracing s (TacticT m)+  = TacticT $ StateT $ \jdg ->+      mapExtract' (first $ rose s . pure) $ runStateT m jdg+++------------------------------------------------------------------------------+-- | Recursion is allowed only when we can prove it is on a structurally+-- smaller argument. The top of the 'ts_recursion_stack' witnesses the smaller+-- pattern val.+guardStructurallySmallerRecursion+    :: TacticState+    -> Maybe TacticError+guardStructurallySmallerRecursion s =+  case head $ ts_recursion_stack s of+     Just _  -> Nothing+     Nothing -> Just NoProgress+++------------------------------------------------------------------------------+-- | Mark that the current recursive call is structurally smaller, due to+-- having been matched on a pattern value.+--+-- Implemented by setting the top of the 'ts_recursion_stack'.+markStructuralySmallerRecursion :: MonadState TacticState m => PatVal -> m ()+markStructuralySmallerRecursion pv = do+  modify $ withRecursionStack $ \case+    (_ : bs) -> Just pv : bs+    []       -> []+++------------------------------------------------------------------------------+-- | Given the results of running a tactic, score the solutions by+-- desirability.+--+-- TODO(sandy): This function is completely unprincipled and was just hacked+-- together to produce the right test results.+scoreSolution+    :: LHsExpr GhcPs+    -> TacticState+    -> [Judgement]+    -> ( Penalize Int  -- number of holes+       , Reward Bool   -- all bindings used+       , Penalize Int  -- unused top-level bindings+       , Penalize Int  -- number of introduced bindings+       , Reward Int    -- number used bindings+       , Penalize Int  -- number of recursive calls+       , Penalize Int  -- size of extract+       )+scoreSolution ext TacticState{..} holes+  = ( Penalize $ length holes+    , Reward   $ S.null $ ts_intro_vals S.\\ ts_used_vals+    , Penalize $ S.size ts_unused_top_vals+    , Penalize $ S.size ts_intro_vals+    , Reward   $ S.size ts_used_vals+    , Penalize $ ts_recursion_count+    , Penalize $ solutionSize ext+    )+++------------------------------------------------------------------------------+-- | Compute the number of 'LHsExpr' nodes; used as a rough metric for code+-- size.+solutionSize :: LHsExpr GhcPs -> Int+solutionSize = everything (+) $ gcount $ mkQ False $ \case+  (_ :: LHsExpr GhcPs) -> True+++newtype Penalize a = Penalize a+  deriving (Eq, Ord, Show) via (Down a)++newtype Reward a = Reward a+  deriving (Eq, Ord, Show) via a+++------------------------------------------------------------------------------+-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.+tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst+tryUnifyUnivarsButNotSkolems skolems goal inst =+  case tcUnifyTysFG+         (bool BindMe Skolem . flip S.member skolems)+         [unCType inst]+         [unCType goal] of+    Unifiable subst -> pure subst+    _ -> Nothing++++------------------------------------------------------------------------------+-- | Attempt to unify two types.+unify :: CType -- ^ The goal type+      -> CType -- ^ The type we are trying unify the goal type with+      -> RuleM ()+unify goal inst = do+  skolems <- gets ts_skolems+  case tryUnifyUnivarsButNotSkolems skolems goal inst of+    Just subst ->+      modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) })+    Nothing -> throwError (UnificationError inst goal)+++------------------------------------------------------------------------------+-- | Get the class methods of a 'PredType', correctly dealing with+-- instantiation of quantified class types.+methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]+methodHypothesis ty = do+  (tc, apps) <- splitTyConApp_maybe ty+  cls <- tyConClass_maybe tc+  let methods = classMethods cls+      tvs     = classTyVars cls+      subst   = zipTvSubst tvs apps+  sc_methods <- fmap join+              $ traverse (methodHypothesis . substTy subst)+              $ classSCTheta cls+  pure $ mappend sc_methods $ methods <&> \method ->+    let (_, _, ty) = tcSplitSigmaTy $ idType method+    in ( occName method+       , HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty+       )+++------------------------------------------------------------------------------+-- | Run the given tactic iff the current hole contains no univars. Skolems and+-- already decided univars are OK though.+requireConcreteHole :: TacticsM a -> TacticsM a+requireConcreteHole m = do+  jdg     <- goal+  skolems <- gets ts_skolems+  let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg+  case S.size $ vars S.\\ skolems of+    0 -> m+    _ -> throwError TooPolymorphic+

@@ -0,0 +1,93 @@+{-# LANGUAGE ViewPatterns #-}++module Ide.Plugin.Tactic.Naming where++import           Control.Monad.State.Strict+import           Data.Bool (bool)+import           Data.Char+import           Data.Map (Map)+import qualified Data.Map as M+import           Data.Traversable+import           Name+import           TcType+import           TyCon+import           Type+import           TysWiredIn (listTyCon, pairTyCon, unitTyCon)+++------------------------------------------------------------------------------+-- | Use type information to create a reasonable name.+mkTyName :: Type -> String+-- eg. mkTyName (a -> B) = "fab"+mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b))+  = "f" ++ mkTyName a ++ mkTyName b+-- eg. mkTyName (a -> b -> C) = "f_C"+mkTyName (tcSplitFunTys -> ((_:_), b))+  = "f_" ++ mkTyName b+-- eg. mkTyName (Either A B) = "eab"+mkTyName (splitTyConApp_maybe -> Just (c, args))+  = mkTyConName c ++ foldMap mkTyName args+-- eg. mkTyName a = "a"+mkTyName (getTyVar_maybe -> Just tv)+  = occNameString $ occName tv+-- eg. mkTyName (forall x. y) = "y"+mkTyName (tcSplitSigmaTy -> ((_:_), _, t))+  = mkTyName t+mkTyName _ = "x"+++------------------------------------------------------------------------------+-- | Get a good name for a type constructor.+mkTyConName :: TyCon -> String+mkTyConName tc+  | tc == listTyCon = "l_"+  | tc == pairTyCon = "p_"+  | tc == unitTyCon = "unit"+  | otherwise+      = take 1+      . fmap toLower+      . filterReplace isSymbol      's'+      . filterReplace isPunctuation 'p'+      . occNameString+      $ getOccName tc+++------------------------------------------------------------------------------+-- | Maybe replace an element in the list if the predicate matches+filterReplace :: (a -> Bool) -> a -> [a] -> [a]+filterReplace f r = fmap (\a -> bool a r $ f a)+++------------------------------------------------------------------------------+-- | Produce a unique, good name for a type.+mkGoodName+    :: [OccName]  -- ^ Bindings in scope; used to ensure we don't shadow anything+    -> Type       -- ^ The type to produce a name for+    -> OccName+mkGoodName in_scope t =+  let tn = mkTyName t+   in mkVarOcc $ case elem (mkVarOcc tn) in_scope of+        True -> tn ++ show (length in_scope)+        False -> tn+++------------------------------------------------------------------------------+-- | Like 'mkGoodName' but creates several apart names.+mkManyGoodNames+  :: (Traversable t, Monad m)+  => M.Map OccName a+  -> t Type+  -> m (t OccName)+mkManyGoodNames hy args =+  flip evalStateT (getInScope hy) $ for args $ \at -> do+    in_scope <- get+    let n = mkGoodName in_scope at+    modify (n :)+    pure n+++------------------------------------------------------------------------------+-- | Which names are in scope?+getInScope :: Map OccName a -> [OccName]+getInScope = M.keys+

@@ -0,0 +1,18 @@+module Ide.Plugin.Tactic.Range where++import qualified FastString as FS+import           Development.IDE.Types.Location+import           SrcLoc++------------------------------------------------------------------------------+-- | Convert a DAML compiler Range to a GHC SrcSpan+-- TODO(sandy): this doesn't belong here+rangeToSrcSpan :: String -> Range -> SrcSpan+rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range++rangeToRealSrcSpan :: String -> Range -> RealSrcSpan+rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) =+    mkRealSrcSpan+      (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1))+      (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1))+

@@ -0,0 +1,287 @@+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE ViewPatterns          #-}++module Ide.Plugin.Tactic.Tactics+  ( module Ide.Plugin.Tactic.Tactics+  , runTactic+  ) where++import           Control.Monad (when)+import           Control.Monad.Except (throwError)+import           Control.Monad.Reader.Class (MonadReader(ask))+import           Control.Monad.State.Class+import           Control.Monad.State.Strict (StateT(..), runStateT)+import           Data.Bool (bool)+import           Data.Foldable+import           Data.List+import qualified Data.Map as M+import           Data.Maybe+import qualified Data.Set as S+import           DataCon+import           Development.IDE.GHC.Compat+import           GHC.Exts+import           GHC.SourceGen.Expr+import           GHC.SourceGen.Overloaded+import           Ide.Plugin.Tactic.CodeGen+import           Ide.Plugin.Tactic.Context+import           Ide.Plugin.Tactic.GHC+import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Machinery+import           Ide.Plugin.Tactic.Naming+import           Ide.Plugin.Tactic.Types+import           Name (occNameString)+import           Refinery.Tactic+import           Refinery.Tactic.Internal+import           TcType+import           Type hiding (Var)+++------------------------------------------------------------------------------+-- | Use something in the hypothesis to fill the hole.+assumption :: TacticsM ()+assumption = attemptOn allNames assume+++------------------------------------------------------------------------------+-- | Use something named in the hypothesis to fill the hole.+assume :: OccName -> TacticsM ()+assume name = rule $ \jdg -> do+  let g  = jGoal jdg+  case M.lookup name $ jHypothesis jdg of+    Just (hi_type -> ty) -> do+      unify ty $ jGoal jdg+      for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion+      useOccName jdg name+      pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name+    Nothing -> throwError $ UndefinedHypothesis name+++recursion :: TacticsM ()+recursion = requireConcreteHole $ tracing "recursion" $ do+  defs <- getCurrentDefinitions+  attemptOn (const $ fmap fst defs) $ \name -> do+    modify $ pushRecursionStack .  countRecursiveCall+    ensure guardStructurallySmallerRecursion popRecursionStack $ do+      (localTactic (apply name) $ introducingRecursively defs)+        <@> fmap (localTactic assumption . filterPosition name) [0..]+++------------------------------------------------------------------------------+-- | Introduce a lambda binding every variable.+intros :: TacticsM ()+intros = rule $ \jdg -> do+  let hy = jHypothesis jdg+      g  = jGoal jdg+  ctx <- ask+  case tcSplitFunTys $ unCType g of+    ([], _) -> throwError $ GoalMismatch "intros" g+    (as, b) -> do+      vs <- mkManyGoodNames (jEntireHypothesis jdg) as+      let top_hole = isTopHole ctx jdg+          jdg' = introducingLambda top_hole (zip vs $ coerce as)+               $ withNewGoal (CType b) jdg+      modify $ withIntroducedVals $ mappend $ S.fromList vs+      when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs+      (tr, sg) <- newSubgoal jdg'+      pure+        . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, )+        . noLoc+        . lambda (fmap bvar' vs)+        $ unLoc sg+++------------------------------------------------------------------------------+-- | Case split, and leave holes in the matches.+destructAuto :: OccName -> TacticsM ()+destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do+  jdg <- goal+  case M.lookup name $ jHypothesis jdg of+    Nothing -> throwError $ NotInScope name+    Just hi ->+      let subtactic = rule $ destruct' (const subgoal) name+      in case isPatternMatch $ hi_provenance hi of+            True ->+              pruning subtactic $ \jdgs ->+                let getHyTypes = S.fromList . fmap hi_type . M.elems . jHypothesis+                    new_hy = foldMap getHyTypes jdgs+                    old_hy = getHyTypes jdg+                in case S.null $ new_hy S.\\ old_hy of+                      True  -> Just $ UnhelpfulDestruct name+                      False -> Nothing+            False -> subtactic+++------------------------------------------------------------------------------+-- | Case split, and leave holes in the matches.+destruct :: OccName -> TacticsM ()+destruct name = requireConcreteHole $ tracing "destruct(user)" $+  rule $ destruct' (const subgoal) name+++------------------------------------------------------------------------------+-- | Case split, using the same data constructor in the matches.+homo :: OccName -> TacticsM ()+homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg ->+  buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)+++------------------------------------------------------------------------------+-- | LambdaCase split, and leave holes in the matches.+destructLambdaCase :: TacticsM ()+destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal)+++------------------------------------------------------------------------------+-- | LambdaCase split, using the same data constructor in the matches.+homoLambdaCase :: TacticsM ()+homoLambdaCase =+  tracing "homoLambdaCase" $+    rule $ destructLambdaCase' $ \dc jdg ->+      buildDataCon jdg dc+        . snd+        . splitAppTys+        . unCType+        $ jGoal jdg+++apply :: OccName -> TacticsM ()+apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do+  jdg <- goal+  let hy = jHypothesis jdg+      g  = jGoal jdg+  case M.lookup func hy of+    Just (hi_type -> CType ty) -> do+      ty' <- freshTyvars ty+      let (_, _, args, ret) = tacticsSplitFunTy ty'+      requireNewHoles $ rule $ \jdg -> do+        unify g (CType ret)+        useOccName jdg func+        (tr, sgs)+            <- fmap unzipTrace+            $ traverse ( newSubgoal+                        . blacklistingDestruct+                        . flip withNewGoal jdg+                        . CType+                        ) args+        pure+          . (tr, )+          . noLoc+          . foldl' (@@) (var' func)+          $ fmap unLoc sgs+    Nothing -> do+      throwError $ GoalMismatch "apply" g+++------------------------------------------------------------------------------+-- | Choose between each of the goal's data constructors.+split :: TacticsM ()+split = tracing "split(user)" $ do+  jdg <- goal+  let g = jGoal jdg+  case splitTyConApp_maybe $ unCType g of+    Nothing -> throwError $ GoalMismatch "split" g+    Just (tc, _) -> do+      let dcs = tyConDataCons tc+      choice $ fmap splitDataCon dcs+++------------------------------------------------------------------------------+-- | Choose between each of the goal's data constructors. Different than+-- 'split' because it won't split a data con if it doesn't result in any new+-- goals.+splitAuto :: TacticsM ()+splitAuto = requireConcreteHole $ tracing "split(auto)" $ do+  jdg <- goal+  let g = jGoal jdg+  case splitTyConApp_maybe $ unCType g of+    Nothing -> throwError $ GoalMismatch "split" g+    Just (tc, _) -> do+      let dcs = tyConDataCons tc+      case isSplitWhitelisted jdg of+        True -> choice $ fmap splitDataCon dcs+        False -> do+          choice $ flip fmap dcs $ \dc -> requireNewHoles $+            splitDataCon dc+++------------------------------------------------------------------------------+-- | Allow the given tactic to proceed if and only if it introduces holes that+-- have a different goal than current goal.+requireNewHoles :: TacticsM () -> TacticsM ()+requireNewHoles m = do+  jdg <- goal+  pruning m $ \jdgs ->+    case null jdgs || any (/= jGoal jdg) (fmap jGoal jdgs) of+      True  -> Nothing+      False -> Just NoProgress+++------------------------------------------------------------------------------+-- | Attempt to instantiate the given data constructor to solve the goal.+splitDataCon :: DataCon -> TacticsM ()+splitDataCon dc =+  requireConcreteHole $ tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do+    let g = jGoal jdg+    case splitTyConApp_maybe $ unCType g of+      Just (tc, apps) -> do+        case elem dc $ tyConDataCons tc of+          True -> buildDataCon (unwhitelistingSplit jdg) dc apps+          False -> throwError $ IncorrectDataCon dc+      Nothing -> throwError $ GoalMismatch "splitDataCon" g+++------------------------------------------------------------------------------+-- | @matching f@ takes a function from a judgement to a @Tactic@, and+-- then applies the resulting @Tactic@.+matching :: (Judgement -> TacticsM ()) -> TacticsM ()+matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f s) s+++attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()+attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames)+++localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a+localTactic t f = do+  TacticT $ StateT $ \jdg ->+    runStateT (unTacticT t) $ f jdg+++auto' :: Int -> TacticsM ()+auto' 0 = throwError NoProgress+auto' n = do+  let loop = auto' (n - 1)+  try intros+  choice+    [ overFunctions $ \fname -> do+        apply fname+        loop+    , overAlgebraicTerms $ \aname -> do+        destructAuto aname+        loop+    , splitAuto >> loop+    , assumption >> loop+    , recursion+    ]++overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()+overFunctions =+  attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . jHypothesis++overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()+overAlgebraicTerms =+  attemptOn $+    M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . jHypothesis+++allNames :: Judgement -> [OccName]+allNames = M.keys . jHypothesis+

@@ -0,0 +1,27 @@+{-# LANGUAGE OverloadedStrings #-}++module Ide.Plugin.Tactic.TestTypes where++import qualified Data.Text as T++------------------------------------------------------------------------------+-- | The list of tactics exposed to the outside world. These are attached to+-- actual tactics via 'commandTactic' and are contextually provided to the+-- editor via 'commandProvider'.+data TacticCommand+  = Auto+  | Intros+  | Destruct+  | Homomorphism+  | DestructLambdaCase+  | HomomorphismLambdaCase+  deriving (Eq, Ord, Show, Enum, Bounded)++-- | Generate a title for the command.+tacticTitle :: TacticCommand -> T.Text -> T.Text+tacticTitle Auto _ = "Attempt to fill hole"+tacticTitle Intros _ = "Introduce lambda"+tacticTitle Destruct var = "Case split on " <> var+tacticTitle Homomorphism var = "Homomorphic case split on " <> var+tacticTitle DestructLambdaCase _ = "Lambda case split"+tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"

@@ -0,0 +1,367 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DerivingStrategies         #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses      #-}+{-# LANGUAGE TypeSynonymInstances       #-}+{-# OPTIONS_GHC -fno-warn-orphans       #-}++module Ide.Plugin.Tactic.Types+  ( module Ide.Plugin.Tactic.Types+  , module Ide.Plugin.Tactic.Debug+  , OccName+  , Name+  , Type+  , TyVar+  , Span+  , Range+  ) where++import Control.Lens hiding (Context)+import Control.Monad.Reader+import Control.Monad.State+import Data.Coerce+import Data.Function+import Data.Generics.Product (field)+import Data.Map (Map)+import Data.Set (Set)+import Data.Tree+import Development.IDE.GHC.Compat hiding (Node)+import Development.IDE.GHC.Orphans ()+import Development.IDE.Types.Location+import GHC.Generics+import Ide.Plugin.Tactic.Debug+import OccName+import Refinery.Tactic+import System.IO.Unsafe (unsafePerformIO)+import Type+import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)+import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)+++------------------------------------------------------------------------------+-- | A wrapper around 'Type' which supports equality and ordering.+newtype CType = CType { unCType :: Type }++instance Eq CType where+  (==) = eqType `on` unCType++instance Ord CType where+  compare = nonDetCmpType `on` unCType++instance Show CType where+  show  = unsafeRender . unCType++instance Show OccName where+  show  = unsafeRender++instance Show Var where+  show  = unsafeRender++instance Show TCvSubst where+  show  = unsafeRender++instance Show DataCon where+  show  = unsafeRender++instance Show Class where+  show  = unsafeRender+++------------------------------------------------------------------------------+data TacticState = TacticState+    { ts_skolems   :: !(Set TyVar)+      -- ^ The known skolems.+    , ts_unifier   :: !(TCvSubst)+      -- ^ The current substitution of univars.+    , ts_used_vals :: !(Set OccName)+      -- ^ Set of values used by tactics.+    , ts_intro_vals :: !(Set OccName)+      -- ^ Set of values introduced by tactics.+    , ts_unused_top_vals :: !(Set OccName)+      -- ^ Set of currently unused arguments to the function being defined.+    , ts_recursion_stack :: ![Maybe PatVal]+      -- ^ Stack for tracking whether or not the current recursive call has+      -- used at least one smaller pat val. Recursive calls for which this+      -- value is 'False' are guaranteed to loop, and must be pruned.+    , ts_recursion_count :: !Int+      -- ^ Number of calls to recursion. We penalize each.+    , ts_unique_gen :: !UniqSupply+    } deriving stock (Show, Generic)++instance Show UniqSupply where+  show _ = "<uniqsupply>"+++------------------------------------------------------------------------------+-- | A 'UniqSupply' to use in 'defaultTacticState'+unsafeDefaultUniqueSupply :: UniqSupply+unsafeDefaultUniqueSupply =+  unsafePerformIO $ mkSplitUniqSupply '🚒'+{-# NOINLINE unsafeDefaultUniqueSupply #-}+++defaultTacticState :: TacticState+defaultTacticState =+  TacticState+    { ts_skolems         = mempty+    , ts_unifier         = emptyTCvSubst+    , ts_used_vals       = mempty+    , ts_intro_vals      = mempty+    , ts_unused_top_vals = mempty+    , ts_recursion_stack = mempty+    , ts_recursion_count = 0+    , ts_unique_gen      = unsafeDefaultUniqueSupply+    }+++------------------------------------------------------------------------------+-- | Generate a new 'Unique'+freshUnique :: MonadState TacticState m => m Unique+freshUnique = do+  (uniq, supply) <- gets $ takeUniqFromSupply . ts_unique_gen+  modify' $! field @"ts_unique_gen" .~ supply+  pure uniq+++withRecursionStack+  :: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState+withRecursionStack f =+  field @"ts_recursion_stack" %~ f++pushRecursionStack :: TacticState -> TacticState+pushRecursionStack = withRecursionStack (Nothing :)++popRecursionStack :: TacticState -> TacticState+popRecursionStack = withRecursionStack tail+++withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState+withUsedVals f =+  field @"ts_used_vals" %~ f+++withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState+withIntroducedVals f =+  field @"ts_intro_vals" %~ f+++------------------------------------------------------------------------------+-- | Describes where hypotheses came from. Used extensively to prune stupid+-- solutions from the search space.+data Provenance+  = -- | An argument given to the topmost function that contains the current+    -- hole. Recursive calls are restricted to values whose provenance lines up+    -- with the same argument.+    TopLevelArgPrv+      OccName   -- ^ Binding function+      Int       -- ^ Argument Position+    -- | A binding created in a pattern match.+  | PatternMatchPrv PatVal+    -- | A class method from the given context.+  | ClassMethodPrv+      (Uniquely Class)     -- ^ Class+    -- | A binding explicitly written by the user.+  | UserPrv+    -- | The recursive hypothesis. Present only in the context of the recursion+    -- tactic.+  | RecursivePrv+    -- | A hypothesis which has been disallowed for some reason. It's important+    -- to keep these in the hypothesis set, rather than filtering it, in order+    -- to continue tracking downstream provenance.+  | DisallowedPrv DisallowReason Provenance+  deriving stock (Eq, Show, Generic, Ord)+++------------------------------------------------------------------------------+-- | Why was a hypothesis disallowed?+data DisallowReason+  = WrongBranch Int+  | Shadowed+  | RecursiveCall+  | AlreadyDestructed+  deriving stock (Eq, Show, Generic, Ord)+++------------------------------------------------------------------------------+-- | Provenance of a pattern value.+data PatVal = PatVal+  { pv_scrutinee :: Maybe OccName+    -- ^ Original scrutinee which created this PatVal. Nothing, for lambda+    -- case.+  , pv_ancestry  :: Set OccName+    -- ^ The set of values which had to be destructed to discover this term.+    -- Always contains the scrutinee.+  , pv_datacon   :: Uniquely DataCon+    -- ^ The datacon which introduced this term.+  , pv_position  :: Int+    -- ^ The position of this binding in the datacon's arguments.+  } deriving stock (Eq, Show, Generic, Ord)+++------------------------------------------------------------------------------+-- | A wrapper which uses a 'Uniquable' constraint for providing 'Eq' and 'Ord'+-- instances.+newtype Uniquely a = Uniquely { getViaUnique :: a }+  deriving Show via a++instance Uniquable a => Eq (Uniquely a) where+  (==) = (==) `on` getUnique . getViaUnique++instance Uniquable a => Ord (Uniquely a) where+  compare = nonDetCmpUnique `on` getUnique . getViaUnique+++------------------------------------------------------------------------------+-- | The provenance and type of a hypothesis term.+data HyInfo a = HyInfo+  { hi_provenance :: Provenance+  , hi_type       :: a+  }+  deriving stock (Functor, Eq, Show, Generic, Ord)+++------------------------------------------------------------------------------+-- | Map a function over the provenance.+overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a+overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty+++------------------------------------------------------------------------------+-- | The current bindings and goal for a hole to be filled by refinery.+data Judgement' a = Judgement+  { _jHypothesis :: !(Map OccName (HyInfo a))+  , _jBlacklistDestruct :: !(Bool)+  , _jWhitelistSplit :: !(Bool)+  , _jIsTopHole    :: !Bool+  , _jGoal         :: !(a)+  }+  deriving stock (Eq, Generic, Functor, Show)++type Judgement = Judgement' CType+++newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }+    deriving (Functor, Applicative, Monad, MonadReader Context)++------------------------------------------------------------------------------+-- | Orphan instance for producing holes when attempting to solve tactics.+instance MonadExtract (Trace, LHsExpr GhcPs) ExtractM where+  hole = pure (mempty, noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_")+++------------------------------------------------------------------------------+-- | Reasons a tactic might fail.+data TacticError+  = UndefinedHypothesis OccName+  | GoalMismatch String CType+  | UnsolvedSubgoals [Judgement]+  | UnificationError CType CType+  | NoProgress+  | NoApplicableTactic+  | IncorrectDataCon DataCon+  | RecursionOnWrongParam OccName Int OccName+  | UnhelpfulDestruct OccName+  | UnhelpfulSplit OccName+  | TooPolymorphic+  | NotInScope OccName+  deriving stock (Eq)++instance Show TacticError where+    show (UndefinedHypothesis name) =+      occNameString name <> " is not available in the hypothesis."+    show (GoalMismatch tac (CType typ)) =+      mconcat+        [ "The tactic "+        , tac+        , " doesn't apply to goal type "+        , unsafeRender typ+        ]+    show (UnsolvedSubgoals _) =+      "There were unsolved subgoals"+    show (UnificationError (CType t1) (CType t2)) =+        mconcat+          [ "Could not unify "+          , unsafeRender t1+          , " and "+          , unsafeRender t2+          ]+    show NoProgress =+      "Unable to make progress"+    show NoApplicableTactic =+      "No tactic could be applied"+    show (IncorrectDataCon dcon) =+      "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"+    show (RecursionOnWrongParam call p arg) =+      "Recursion on wrong param (" <> show call <> ") on arg"+        <> show p <> ": " <> show arg+    show (UnhelpfulDestruct n) =+      "Destructing patval " <> show n <> " leads to no new types"+    show (UnhelpfulSplit n) =+      "Splitting constructor " <> show n <> " leads to no new goals"+    show TooPolymorphic =+      "The tactic isn't applicable because the goal is too polymorphic"+    show (NotInScope name) =+      "Tried to do something with the out of scope name " <> show name+++------------------------------------------------------------------------------+type TacticsM  = TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM+type RuleM     = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM+type Rule      = RuleM (Trace, LHsExpr GhcPs)++type Trace = Rose String+++------------------------------------------------------------------------------+-- | The Reader context of tactics and rules+data Context = Context+  { ctxDefiningFuncs :: [(OccName, CType)]+    -- ^ The functions currently being defined+  , ctxModuleFuncs :: [(OccName, CType)]+    -- ^ Everything defined in the current module+  }+  deriving stock (Eq, Ord)+++------------------------------------------------------------------------------+-- | An empty context+emptyContext :: Context+emptyContext  = Context mempty mempty+++newtype Rose a = Rose (Tree a)+  deriving stock (Eq, Functor, Generic)++instance Show (Rose String) where+  show = unlines . dropEveryOther . lines . drawTree . coerce++dropEveryOther :: [a] -> [a]+dropEveryOther []           = []+dropEveryOther [a]          = [a]+dropEveryOther (a : _ : as) = a : dropEveryOther as++instance Semigroup a => Semigroup (Rose a) where+  Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs)++instance Monoid a => Monoid (Rose a) where+  mempty = Rose $ Node mempty mempty++rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a+rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs+rose a rs = Rose $ Node a $ coerce rs+++------------------------------------------------------------------------------+-- | The results of 'Ide.Plugin.Tactic.Machinery.runTactic'+data RunTacticResults = RunTacticResults+  { rtr_trace       :: Trace+  , rtr_extract     :: LHsExpr GhcPs+  , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]+  } deriving Show+

@@ -0,0 +1,122 @@+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE NamedFieldPuns      #-}+{-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE RecordWildCards     #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Ide.TreeTransform+  ( Graft, graft, transform, useAnnotatedSource+  ) where++import           BasicTypes (appPrec)+import           Control.Monad+import           Control.Monad.Trans.Class+import qualified Data.Text as T+import           Development.IDE.Core.RuleTypes+import           Development.IDE.Core.Rules+import           Development.IDE.Core.Shake+import           Development.IDE.GHC.Compat  hiding (parseExpr)+import           Development.IDE.Types.Location+import           Generics.SYB+import           Ide.PluginUtils+import           Language.Haskell.GHC.ExactPrint+import           Language.Haskell.GHC.ExactPrint.Parsers+import           Language.Haskell.LSP.Types+import           Language.Haskell.LSP.Types.Capabilities (ClientCapabilities)+import           Outputable+import           Retrie.ExactPrint hiding (parseExpr)+++------------------------------------------------------------------------------+-- | Get the latest version of the annotated parse source.+useAnnotatedSource+    :: String+    -> IdeState+    -> NormalizedFilePath+    -> IO (Maybe (Annotated ParsedSource))+useAnnotatedSource herald state nfp = do+  pm <- runAction herald state $ use GetParsedModule nfp+  pure $ fmap fixAnns pm+++------------------------------------------------------------------------------+-- | A transformation for grafting source trees together. Use the semigroup+-- instance to combine 'Graft's, and run them via 'transform'.+newtype Graft a = Graft+  { runGraft :: DynFlags -> a -> TransformT (Either String) a+  }++instance Semigroup (Graft a) where+  Graft a <> Graft b = Graft $ \dflags -> a dflags >=> b dflags++instance Monoid (Graft a) where+  mempty = Graft $ const pure+++------------------------------------------------------------------------------+-- | Convert a 'Graft' into a 'WorkspaceEdit'.+transform+    :: DynFlags+    -> ClientCapabilities+    -> Uri+    -> Graft ParsedSource+    -> Annotated ParsedSource+    -> Either String WorkspaceEdit+transform dflags ccs uri f a = do+  let src = printA a+  a' <- transformA a $ runGraft f dflags+  let res = printA a'+  pure $ diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions+++------------------------------------------------------------------------------+-- | Construct a 'Graft', replacing the node at the given 'SrcSpan' with the+-- given 'LHSExpr'. The node at that position must already be a 'LHsExpr', or+-- this is a no-op.+graft+    :: forall a+     . Data a+    => SrcSpan+    -> LHsExpr GhcPs+    -> Graft a+graft dst val = Graft $ \dflags a -> do+  (anns, val') <- annotate dflags $ parenthesize val+  modifyAnnsT $ mappend anns+  pure $ everywhere'+    ( mkT $+        \case+          (L src _ :: LHsExpr GhcPs) | src == dst -> val'+          l -> l+    ) a+++------------------------------------------------------------------------------+-- | Dark magic I stole from retrie. No idea what it does.+fixAnns :: ParsedModule -> Annotated ParsedSource+fixAnns ParsedModule {..} =+  let ranns = relativiseApiAnns pm_parsed_source pm_annotations+   in unsafeMkA pm_parsed_source ranns 0+++------------------------------------------------------------------------------+-- | Given an 'LHSExpr', compute its exactprint annotations.+annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs)+annotate dflags expr = do+  uniq <- show <$> uniqueSrcSpanT+  let rendered = render dflags expr+  (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered+  let anns' = setPrecedingLines expr' 0 1 anns+  pure (anns', expr')+++------------------------------------------------------------------------------+-- | Print out something 'Outputable'.+render :: Outputable a => DynFlags -> a -> String+render dflags = showSDoc dflags . ppr+++------------------------------------------------------------------------------+-- | Put parentheses around an expression if required.+parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs+parenthesize = parenthesizeHsExpr appPrec+

@@ -0,0 +1,57 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}++module AutoTupleSpec where++import           Data.Either (isRight)+import qualified Data.Map as M+import           Ide.Plugin.Tactic.Debug+import           Ide.Plugin.Tactic.Judgements (mkFirstJudgement)+import           Ide.Plugin.Tactic.Machinery+import           Ide.Plugin.Tactic.Tactics (auto')+import           Ide.Plugin.Tactic.Types+import           OccName (mkVarOcc)+import           Test.Hspec+import           Test.QuickCheck+import           Type (mkTyVarTy)+import           TysPrim (alphaTyVars)+import           TysWiredIn (mkBoxedTupleTy)+++instance Show Type where+  show = unsafeRender+++spec :: Spec+spec = describe "auto for tuple" $ do+  it "should always be able to discover an auto solution" $ do+    property $ do+      -- Pick some number of variables+      n <- choose (1, 7)+      let vars = fmap mkTyVarTy $ take n alphaTyVars+      -- Pick a random ordering+      in_vars  <- shuffle vars+      -- Randomly associate them into tuple types+      in_type  <- mkBoxedTupleTy+                . fmap mkBoxedTupleTy+              <$> randomGroups in_vars+      out_type <- mkBoxedTupleTy+                . fmap mkBoxedTupleTy+              <$> randomGroups vars+      pure $+          -- We should always be able to find a solution+          runTactic+            emptyContext+            (mkFirstJudgement+              (M.singleton (mkVarOcc "x") $ HyInfo UserPrv $ CType in_type)+              True+              out_type)+            (auto' $ n * 2) `shouldSatisfy` isRight+++randomGroups :: [a] -> Gen [[a]]+randomGroups [] = pure []+randomGroups as = do+  n <- choose (1, length as)+  (:) <$> pure (take n as)+      <*> randomGroups (drop n as)+

@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover -optF --module-name=Main #-}

@@ -0,0 +1,65 @@+{-# LANGUAGE ViewPatterns #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module UnificationSpec where++import           Control.Arrow+import           Data.Bool (bool)+import           Data.Functor ((<&>))+import           Data.Maybe (mapMaybe)+import qualified Data.Set as S+import           Data.Traversable+import           Data.Tuple (swap)+import           Ide.Plugin.Tactic.Debug+import           Ide.Plugin.Tactic.Machinery+import           Ide.Plugin.Tactic.Types+import           TcType (tcGetTyVar_maybe, substTy)+import           Test.Hspec+import           Test.QuickCheck+import           Type (mkTyVarTy)+import           TysPrim (alphaTyVars)+import           TysWiredIn (mkBoxedTupleTy)+++instance Show Type where+  show = unsafeRender+++spec :: Spec+spec = describe "unification" $ do+  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+      -- Randomly pair them+      skolem_uni_pairs <-+        for (zip skolems univars) randomSwap+      let (lhs, rhs)+            = mkBoxedTupleTy *** mkBoxedTupleTy+            $ unzip skolem_uni_pairs+      pure $+        counterexample (show skolems) $+        counterexample (show lhs) $+        counterexample (show rhs) $+          case tryUnifyUnivarsButNotSkolems+                 (S.fromList $ mapMaybe tcGetTyVar_maybe skolems)+                 (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+            Nothing -> True === False+++randomSwap :: (a, a) -> Gen (a, a)+randomSwap ab = do+  which <- arbitrary+  pure $ bool swap id which ab++