hls-tactics-plugin 1.0.0.0 → 1.1.0.0

raw patch · 231 files changed

+6128/−3685 lines, 231 filesdep +hls-test-utilsdep +tasty-hspecdep +unordered-containersdep −bytestringdep −checkersdep −data-defaultdep ~basedep ~ghcidedep ~hls-plugin-apinew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: hls-test-utils, tasty-hspec, unordered-containers

Dependencies removed: bytestring, checkers, data-default, hie-bios, lsp-test, megaparsec, tasty, tasty-ant-xml, tasty-expected-failure, tasty-golden, tasty-rerun

Dependency ranges changed: base, ghcide, hls-plugin-api, shake

API changes (from Hackage documentation)

Files

• README.md +72/−0
• hls-tactics-plugin.cabal +86/−73
• src/Ide/Plugin/Tactic.hs +1/−263
• src/Ide/Plugin/Tactic/Auto.hs +0/−28
• src/Ide/Plugin/Tactic/CaseSplit.hs +0/−87
• src/Ide/Plugin/Tactic/CodeGen.hs +0/−205
• src/Ide/Plugin/Tactic/CodeGen/Utils.hs +0/−72
• src/Ide/Plugin/Tactic/Context.hs +0/−95
• src/Ide/Plugin/Tactic/Debug.hs +0/−59
• src/Ide/Plugin/Tactic/FeatureSet.hs +0/−92
• src/Ide/Plugin/Tactic/GHC.hs +0/−292
• src/Ide/Plugin/Tactic/Judgements.hs +0/−407
• src/Ide/Plugin/Tactic/KnownStrategies.hs +0/−39
• src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +0/−110
• src/Ide/Plugin/Tactic/LanguageServer.hs +0/−212
• src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs +0/−192
• src/Ide/Plugin/Tactic/Machinery.hs +0/−253
• src/Ide/Plugin/Tactic/Naming.hs +0/−97
• src/Ide/Plugin/Tactic/Range.hs +0/−18
• src/Ide/Plugin/Tactic/Simplify.hs +0/−108
• src/Ide/Plugin/Tactic/Tactics.hs +0/−281
• src/Ide/Plugin/Tactic/TestTypes.hs +0/−50
• src/Ide/Plugin/Tactic/Types.hs +0/−389
• src/Wingman/Auto.hs +30/−0
• src/Wingman/CaseSplit.hs +82/−0
• src/Wingman/CodeGen.hs +215/−0
• src/Wingman/CodeGen/Utils.hs +83/−0
• src/Wingman/Context.hs +113/−0
• src/Wingman/Debug.hs +59/−0
• src/Wingman/FeatureSet.hs +94/−0
• src/Wingman/GHC.hs +346/−0
• src/Wingman/Judgements.hs +429/−0
• src/Wingman/Judgements/SYB.hs +83/−0
• src/Wingman/Judgements/Theta.hs +188/−0
• src/Wingman/KnownStrategies.hs +97/−0
• src/Wingman/KnownStrategies/QuickCheck.hs +114/−0
• src/Wingman/LanguageServer.hs +516/−0
• src/Wingman/LanguageServer/TacticProviders.hs +296/−0
• src/Wingman/Machinery.hs +300/−0
• src/Wingman/Naming.hs +96/−0
• src/Wingman/Plugin.hs +216/−0
• src/Wingman/Range.hs +23/−0
• src/Wingman/Simplify.hs +104/−0
• src/Wingman/Tactics.hs +397/−0
• src/Wingman/Types.hs +489/−0
• test/AutoTupleSpec.hs +11/−11
• test/CodeAction/AutoSpec.hs +90/−0
• test/CodeAction/DestructAllSpec.hs +42/−0
• test/CodeAction/DestructSpec.hs +37/−0
• test/CodeAction/IntrosSpec.hs +21/−0
• test/CodeAction/RefineSpec.hs +28/−0
• test/CodeAction/UseDataConSpec.hs +47/−0
• test/GoldenSpec.hs +0/−224
• test/Main.hs +8/−1
• test/ProviderSpec.hs +72/−0
• test/Server.hs +0/−19
• test/Spec.hs +1/−0
• test/UnificationSpec.hs +3/−8
• test/Utils.hs +204/−0
• test/golden/AutoEmptyString.hs +2/−0
• test/golden/AutoEmptyString.hs.expected +2/−0
• test/golden/AutoEndo.hs +10/−0
• test/golden/AutoEndo.hs.expected +11/−0
• test/golden/AutoInfixApply.hs +3/−0
• test/golden/AutoInfixApply.hs.expected +3/−0
• test/golden/AutoInfixApplyMany.hs +3/−0
• test/golden/AutoInfixApplyMany.hs.expected +3/−0
• test/golden/AutoInfixInfix.hs +2/−0
• test/golden/AutoInfixInfix.hs.expected +2/−0
• test/golden/AutoPatSynUse.hs +8/−0
• test/golden/AutoPatSynUse.hs.expected +8/−0
• test/golden/AutoSplitGADT.hs +12/−0
• test/golden/AutoSplitGADT.hs.expected +12/−0
• test/golden/AutoThetaEqCtx.hs +5/−0
• test/golden/AutoThetaEqCtx.hs.expected +5/−0
• test/golden/AutoThetaEqGADT.hs +7/−0
• test/golden/AutoThetaEqGADT.hs.expected +7/−0
• test/golden/AutoThetaEqGADTDestruct.hs +8/−0
• test/golden/AutoThetaEqGADTDestruct.hs.expected +8/−0
• test/golden/AutoThetaFix.hs +13/−0
• test/golden/AutoThetaFix.hs.expected +13/−0
• test/golden/AutoThetaGADT.hs +7/−0
• test/golden/AutoThetaGADT.hs.expected +7/−0
• test/golden/AutoThetaGADTDestruct.hs +7/−0
• test/golden/AutoThetaGADTDestruct.hs.expected +7/−0
• test/golden/AutoThetaRankN.hs +8/−0
• test/golden/AutoThetaRankN.hs.expected +8/−0
• test/golden/AutoThetaRefl.hs +7/−0
• test/golden/AutoThetaRefl.hs.expected +7/−0
• test/golden/AutoThetaReflDestruct.hs +8/−0
• test/golden/AutoThetaReflDestruct.hs.expected +8/−0
• test/golden/AutoZip.hs +3/−0
• test/golden/AutoZip.hs.expected +6/−0
• test/golden/ConProviders.hs +21/−0
• test/golden/DestructAllAnd.hs +2/−0
• test/golden/DestructAllAnd.hs.expected +5/−0
• test/golden/DestructAllFunc.hs +3/−0
• test/golden/DestructAllFunc.hs.expected +4/−0
• test/golden/DestructAllMany.hs +4/−0
• test/golden/DestructAllMany.hs.expected +27/−0
• test/golden/DestructAllNonVarTopMatch.hs +3/−0
• test/golden/DestructAllNonVarTopMatch.hs.expected +6/−0
• test/golden/DestructAllProvider.hs +12/−0
• test/golden/Fgmap.hs +2/−0
• test/golden/Fgmap.hs.expected +2/−0
• test/golden/FmapBoth.hs +3/−0
• test/golden/FmapBoth.hs.expected +3/−0
• test/golden/FmapJoin.hs +2/−0
• test/golden/FmapJoin.hs.expected +2/−0
• test/golden/FmapJoinInLet.hs +4/−0
• test/golden/FmapJoinInLet.hs.expected +4/−0
• test/golden/GoldenApplicativeThen.hs +2/−0
• test/golden/GoldenArbitrary.hs +26/−0
• test/golden/GoldenArbitrary.hs.expected +53/−0
• test/golden/GoldenBigTuple.hs +4/−0
• test/golden/GoldenBigTuple.hs.expected +4/−0
• test/golden/GoldenEitherAuto.hs +2/−0
• test/golden/GoldenEitherAuto.hs.expected +3/−0
• test/golden/GoldenEitherHomomorphic.hs +2/−0
• test/golden/GoldenEitherHomomorphic.hs.expected +3/−0
• test/golden/GoldenFish.hs +5/−0
• test/golden/GoldenFmapTree.hs +4/−0
• test/golden/GoldenFmapTree.hs.expected +5/−0
• test/golden/GoldenFoldr.hs +2/−0
• test/golden/GoldenFoldr.hs.expected +3/−0
• test/golden/GoldenFromMaybe.hs +2/−0
• test/golden/GoldenFromMaybe.hs.expected +3/−0
• test/golden/GoldenGADTAuto.hs +7/−0
• test/golden/GoldenGADTAuto.hs.expected +7/−0
• test/golden/GoldenGADTDestruct.hs +7/−0
• test/golden/GoldenGADTDestruct.hs.expected +7/−0
• test/golden/GoldenGADTDestructCoercion.hs +8/−0
• test/golden/GoldenGADTDestructCoercion.hs.expected +8/−0
• test/golden/GoldenIdTypeFam.hs +7/−0
• test/golden/GoldenIdTypeFam.hs.expected +7/−0
• test/golden/GoldenIdentityFunctor.hs +3/−0
• test/golden/GoldenIdentityFunctor.hs.expected +3/−0
• test/golden/GoldenIntros.hs +2/−0
• test/golden/GoldenIntros.hs.expected +2/−0
• test/golden/GoldenJoinCont.hs +4/−0
• test/golden/GoldenJoinCont.hs.expected +4/−0
• test/golden/GoldenListFmap.hs +2/−0
• test/golden/GoldenListFmap.hs.expected +3/−0
• test/golden/GoldenNote.hs +2/−0
• test/golden/GoldenNote.hs.expected +3/−0
• test/golden/GoldenPureList.hs +2/−0
• test/golden/GoldenPureList.hs.expected +2/−0
• test/golden/GoldenSafeHead.hs +2/−0
• test/golden/GoldenSafeHead.hs.expected +3/−0
• test/golden/GoldenShow.hs +2/−0
• test/golden/GoldenShow.hs.expected +2/−0
• test/golden/GoldenShowCompose.hs +2/−0
• test/golden/GoldenShowCompose.hs.expected +2/−0
• test/golden/GoldenShowMapChar.hs +2/−0
• test/golden/GoldenShowMapChar.hs.expected +2/−0
• test/golden/GoldenSuperclass.hs +8/−0
• test/golden/GoldenSuperclass.hs.expected +8/−0
• test/golden/GoldenSwap.hs +2/−0
• test/golden/GoldenSwap.hs.expected +2/−0
• test/golden/GoldenSwapMany.hs +2/−0
• test/golden/GoldenSwapMany.hs.expected +2/−0
• test/golden/KnownBigSemigroup.hs +7/−0
• test/golden/KnownBigSemigroup.hs.expected +9/−0
• test/golden/KnownCounterfactualSemigroup.hs +7/−0
• test/golden/KnownCounterfactualSemigroup.hs.expected +8/−0
• test/golden/KnownDestructedSemigroup.hs +5/−0
• test/golden/KnownDestructedSemigroup.hs.expected +5/−0
• test/golden/KnownMissingMonoid.hs +8/−0
• test/golden/KnownMissingMonoid.hs.expected +8/−0
• test/golden/KnownMissingSemigroup.hs +5/−0
• test/golden/KnownMissingSemigroup.hs.expected +5/−0
• test/golden/KnownModuleInstanceSemigroup.hs +11/−0
• test/golden/KnownModuleInstanceSemigroup.hs.expected +11/−0
• test/golden/KnownMonoid.hs +8/−0
• test/golden/KnownMonoid.hs.expected +8/−0
• test/golden/KnownPolyMonoid.hs +8/−0
• test/golden/KnownPolyMonoid.hs.expected +8/−0
• test/golden/KnownThetaSemigroup.hs +5/−0
• test/golden/KnownThetaSemigroup.hs.expected +5/−0
• test/golden/LayoutBind.hs +6/−0
• test/golden/LayoutBind.hs.expected +8/−0
• test/golden/LayoutDollarApp.hs +3/−0
• test/golden/LayoutDollarApp.hs.expected +5/−0
• test/golden/LayoutLam.hs +3/−0
• test/golden/LayoutLam.hs.expected +5/−0
• test/golden/LayoutOpApp.hs +2/−0
• test/golden/LayoutOpApp.hs.expected +4/−0
• test/golden/LayoutSplitClass.hs +4/−0
• test/golden/LayoutSplitClass.hs.expected +5/−0
• test/golden/LayoutSplitGuard.hs +3/−0
• test/golden/LayoutSplitGuard.hs.expected +5/−0
• test/golden/LayoutSplitIn.hs +5/−0
• test/golden/LayoutSplitIn.hs.expected +5/−0
• test/golden/LayoutSplitLet.hs +6/−0
• test/golden/LayoutSplitLet.hs.expected +7/−0
• test/golden/LayoutSplitPatSyn.hs +10/−0
• test/golden/LayoutSplitPatSyn.hs.expected +11/−0
• test/golden/LayoutSplitPattern.hs +8/−0
• test/golden/LayoutSplitPattern.hs.expected +9/−0
• test/golden/LayoutSplitViewPat.hs +5/−0
• test/golden/LayoutSplitViewPat.hs.expected +6/−0
• test/golden/LayoutSplitWhere.hs +12/−0
• test/golden/LayoutSplitWhere.hs.expected +14/−0
• test/golden/MessageForallA.hs +2/−0
• test/golden/NewtypeRecord.hs +7/−0
• test/golden/NewtypeRecord.hs.expected +7/−0
• test/golden/ProvideAlreadyDestructed.hs +9/−0
• test/golden/ProvideLocalHyOnly.hs +2/−0
• test/golden/RecordCon.hs +9/−0
• test/golden/RecordCon.hs.expected +9/−0
• test/golden/RefineCon.hs +3/−0
• test/golden/RefineCon.hs.expected +3/−0
• test/golden/RefineGADT.hs +9/−0
• test/golden/RefineGADT.hs.expected +9/−0
• test/golden/RefineIntro.hs +2/−0
• test/golden/RefineIntro.hs.expected +2/−0
• test/golden/RefineReader.hs +5/−0
• test/golden/RefineReader.hs.expected +5/−0
• test/golden/SplitPattern.hs +8/−0
• test/golden/SplitPattern.hs.expected +12/−0
• test/golden/T1.hs +3/−0
• test/golden/T2.hs +12/−0
• test/golden/T3.hs +8/−0
• test/golden/UseConLeft.hs +3/−0
• test/golden/UseConLeft.hs.expected +3/−0
• test/golden/UseConPair.hs +2/−0
• test/golden/UseConPair.hs.expected +2/−0
• test/golden/UseConRight.hs +3/−0
• test/golden/UseConRight.hs.expected +3/−0
• test/golden/hie.yaml +1/−0
• test/golden/test.cabal +17/−0

@@ -34,6 +34,78 @@ [hls]: https://github.com/haskell/haskell-language-server/releases  +## Editor Configuration++### Enabling Jump to Hole++Set the `haskell.plugin.tactics.config.hole_severity` config option to `4`, or+`hint` if your editor uses a GUI for its configuration. This has the potential+to negatively impact performance --- please holler if you notice any appreciable+slowdown by enabling this option.+++### coc.nvim++The following vimscript maps Wingman code-actions to your leader key:++```viml+" use [h and ]h to navigate between holes+nnoremap <silent> [h :<C-U>call CocActionAsync('diagnosticPrevious', 'hint')<CR>+nnoremap <silent> ]h :<C-U>call <SID>JumpToNextHole()<CR>++" <leader>d to perform a pattern match, <leader>n to fill a hole+nnoremap <silent> <leader>d  :<C-u>set operatorfunc=<SID>WingmanDestruct<CR>g@l+nnoremap <silent> <leader>n  :<C-u>set operatorfunc=<SID>WingmanFillHole<CR>g@l++" beta only+nnoremap <silent> <leader>r  :<C-u>set operatorfunc=<SID>WingmanRefine<CR>g@l+nnoremap <silent> <leader>c  :<C-u>set operatorfunc=<SID>WingmanUseCtor<CR>g@l+nnoremap <silent> <leader>a  :<C-u>set operatorfunc=<SID>WingmanDestructAll<CR>g@l+++function! s:JumpToNextHole()+  call CocActionAsync('diagnosticNext', 'hint')+endfunction++function! s:GotoNextHole()+  " wait for the hole diagnostics to reload+  sleep 500m+  " and then jump to the next hole+  normal 0+  call <SID>JumpToNextHole()+endfunction++function! s:WingmanRefine(type)+  call CocAction('codeAction', a:type, ['refactor.wingman.refine'])+  call <SID>GotoNextHole()+endfunction++function! s:WingmanDestruct(type)+  call CocAction('codeAction', a:type, ['refactor.wingman.caseSplit'])+  call <SID>GotoNextHole()+endfunction++function! s:WingmanDestructAll(type)+  call CocAction('codeAction', a:type, ['refactor.wingman.splitFuncArgs'])+  call <SID>GotoNextHole()+endfunction++function! s:WingmanFillHole(type)+  call CocAction('codeAction', a:type, ['refactor.wingman.fillHole'])+  call <SID>GotoNextHole()+endfunction++function! s:WingmanUseCtor(type)+  call CocAction('codeAction', a:type, ['refactor.wingman.useConstructor'])+  call <SID>GotoNextHole()+endfunction+```++### Other Editors++Please open a PR if you have a working configuration!++ ## Features  * [Type-directed code synthesis][auto], including pattern matching and recursion

@@ -1,7 +1,7 @@-cabal-version:      2.2+cabal-version:      2.4 category:           Development name:               hls-tactics-plugin-version:            1.0.0.0+version:            1.1.0.0 synopsis:           Wingman plugin for Haskell Language Server description:        Please see README.md author:             Sandy Maguire, Reed Mullanix@@ -14,7 +14,10 @@ build-type:         Simple extra-source-files:   README.md---   ChangeLog.md+  test/golden/*.cabal+  test/golden/*.expected+  test/golden/*.hs+  test/golden/*.yaml  flag pedantic   description: Enable -Werror@@ -22,39 +25,44 @@   manual:      True  library-  hs-source-dirs:   src+  hs-source-dirs:     src   exposed-modules:     Ide.Plugin.Tactic-    Ide.Plugin.Tactic.Auto-    Ide.Plugin.Tactic.CaseSplit-    Ide.Plugin.Tactic.CodeGen-    Ide.Plugin.Tactic.CodeGen.Utils-    Ide.Plugin.Tactic.Context-    Ide.Plugin.Tactic.Debug-    Ide.Plugin.Tactic.FeatureSet-    Ide.Plugin.Tactic.GHC-    Ide.Plugin.Tactic.Judgements-    Ide.Plugin.Tactic.KnownStrategies-    Ide.Plugin.Tactic.KnownStrategies.QuickCheck-    Ide.Plugin.Tactic.LanguageServer-    Ide.Plugin.Tactic.LanguageServer.TacticProviders-    Ide.Plugin.Tactic.Machinery-    Ide.Plugin.Tactic.Naming-    Ide.Plugin.Tactic.Range-    Ide.Plugin.Tactic.Simplify-    Ide.Plugin.Tactic.Tactics-    Ide.Plugin.Tactic.Types-    Ide.Plugin.Tactic.TestTypes+    Wingman.Auto+    Wingman.CaseSplit+    Wingman.CodeGen+    Wingman.CodeGen.Utils+    Wingman.Context+    Wingman.Debug+    Wingman.FeatureSet+    Wingman.GHC+    Wingman.Judgements+    Wingman.Judgements.SYB+    Wingman.Judgements.Theta+    Wingman.KnownStrategies+    Wingman.KnownStrategies.QuickCheck+    Wingman.LanguageServer+    Wingman.LanguageServer.TacticProviders+    Wingman.Machinery+    Wingman.Naming+    Wingman.Plugin+    Wingman.Range+    Wingman.Simplify+    Wingman.Tactics+    Wingman.Types    ghc-options:-    -Wno-name-shadowing -Wredundant-constraints -Wno-unticked-promoted-constructors+    -Wall -Wno-name-shadowing -Wredundant-constraints+    -Wno-unticked-promoted-constructors+   if flag(pedantic)     ghc-options: -Werror    build-depends:     , aeson-    , base           >=4.12 && <5+    , base                  >=4.12    && <5     , containers+    , deepseq     , directory     , extra     , filepath@@ -64,80 +72,85 @@     , ghc-boot-th     , ghc-exactprint     , ghc-source-gen-    , ghcide         ^>= 1.0.0.0-    , lsp-    , hls-plugin-api ^>= 1.0.0.0+    , ghcide                ^>=1.2+    , hls-plugin-api        ^>=1.1     , lens+    , lsp     , mtl-    , refinery       ^>=0.3-    , retrie         >=0.1.1.0-    , shake          >=0.17.5+    , refinery              ^>=0.3+    , retrie                >=0.1.1.0+    , shake     , syb     , text     , transformers-    , deepseq--  default-language: Haskell2010-  default-extensions: DataKinds, TypeOperators-+    , unordered-containers -executable test-server   default-language:   Haskell2010-  build-depends:-    , base-    , data-default-    , ghcide-    , hls-tactics-plugin-    , hls-plugin-api-    , shake-  main-is: Server.hs-  hs-source-dirs: test-  ghc-options:-    "-with-rtsopts=-I0 -A128M"-    -threaded -Wall -Wno-name-shadowing -Wredundant-constraints+  default-extensions:+    DataKinds+    DeriveAnyClass+    DeriveDataTypeable+    DeriveFoldable+    DeriveFunctor+    DeriveGeneric+    DeriveTraversable+    DerivingStrategies+    DerivingVia+    FlexibleContexts+    FlexibleInstances+    GADTs+    GeneralizedNewtypeDeriving+    LambdaCase+    MultiParamTypeClasses+    NumDecimals+    OverloadedLabels+    PatternSynonyms+    ScopedTypeVariables+    TypeApplications+    TypeOperators+    ViewPatterns  test-suite tests-  type: exitcode-stdio-1.0-  main-is: Main.hs+  type:               exitcode-stdio-1.0+  main-is:            Main.hs   other-modules:     AutoTupleSpec-    GoldenSpec+    CodeAction.AutoSpec+    CodeAction.DestructAllSpec+    CodeAction.DestructSpec+    CodeAction.IntrosSpec+    CodeAction.RefineSpec+    CodeAction.UseDataConSpec+    ProviderSpec+    Spec     UnificationSpec-  hs-source-dirs:-      test-  ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+    Utils++  hs-source-dirs:     test+  ghc-options:+    -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+   build-depends:-      QuickCheck     , aeson     , base-    , bytestring-    , checkers     , containers-    , data-default     , deepseq     , directory     , filepath     , ghc-    , ghcide                >= 0.7.5.0-    , hie-bios+    , ghcide     , hls-plugin-api     , hls-tactics-plugin+    , hls-test-utils  ^>= 1.0     , hspec     , hspec-expectations     , lens-    , lsp-test     , lsp-types-    , megaparsec     , mtl-    , tasty-    , tasty-ant-xml           >=1.1.6-    , tasty-expected-failure-    , tasty-golden+    , QuickCheck+    , tasty-hspec     , tasty-hunit-    , tasty-rerun     , text-  build-tool-depends:-      hspec-discover:hspec-discover-    , hls-tactics-plugin:test-server -any-  default-language: Haskell2010 +  build-tool-depends: hspec-discover:hspec-discover -any+  default-language:   Haskell2010

@@ -1,11 +1,3 @@-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE NumDecimals         #-}-{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}- -- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic   ( descriptor@@ -13,259 +5,5 @@   , TacticCommand (..)   ) where -import           Bag                                              (bagToList,-                                                                   listToBag)-import           Control.Exception                                (evaluate)-import           Control.Monad-import           Control.Monad.Trans-import           Control.Monad.Trans.Maybe-import           Data.Aeson-import           Data.Bifunctor                                   (Bifunctor (bimap))-import           Data.Bool                                        (bool)-import           Data.Data                                        (Data)-import           Data.Generics.Aliases                            (mkQ)-import           Data.Generics.Schemes                            (everything)-import           Data.Maybe-import           Data.Monoid-import qualified Data.Text                                        as T-import           Data.Traversable-import           Development.IDE.Core.Shake                       (IdeState (..))-import           Development.IDE.GHC.Compat-import           Development.IDE.GHC.ExactPrint-import           Development.Shake.Classes-import           Ide.Plugin.Tactic.CaseSplit-import           Ide.Plugin.Tactic.FeatureSet                     (Feature (..),-                                                                   hasFeature)-import           Ide.Plugin.Tactic.GHC-import           Ide.Plugin.Tactic.LanguageServer-import           Ide.Plugin.Tactic.LanguageServer.TacticProviders-import           Ide.Plugin.Tactic.Range-import           Ide.Plugin.Tactic.Tactics-import           Ide.Plugin.Tactic.TestTypes-import           Ide.Plugin.Tactic.Types-import           Ide.Types-import           Language.LSP.Server-import           Language.LSP.Types-import           Language.LSP.Types.Capabilities-import           OccName-import           Prelude                                          hiding (span)-import           System.Timeout---descriptor :: PluginId -> PluginDescriptor IdeState-descriptor plId = (defaultPluginDescriptor plId)-    { pluginCommands-        = fmap (\tc ->-            PluginCommand-              (tcCommandId tc)-              (tacticDesc $ tcCommandName tc)-              (tacticCmd $ commandTactic tc))-              [minBound .. maxBound]-    , pluginHandlers =-        mkPluginHandler STextDocumentCodeAction codeActionProvider-    }----codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction-codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do-      features <- getFeatureSet (shakeExtras state)-      liftIO $ fromMaybeT (Right $ List []) $ do-        (_, jdg, _, dflags) <- judgementForHole state nfp range features-        actions <- lift $-          -- This foldMap is over the function monoid.-          foldMap commandProvider [minBound .. maxBound]-            dflags-            features-            plId-            uri-            range-            jdg-        pure $ Right $ List actions-codeActionProvider _ _ _ = pure $ Right $ List []---tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams-tacticCmd tac state (TacticParams uri range var_name)-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do-      features <- getFeatureSet (shakeExtras state)-      ccs <- getClientCapabilities-      res <- liftIO $ fromMaybeT (Right Nothing) $ do-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range features-        let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'-        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp--        timingOut 2e8 $ join $-          bimap (mkErr InvalidRequest . T.pack . show)-                (mkWorkspaceEdits span dflags ccs uri pm)-            $ runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name--      case res of-        Left err -> pure $ Left err-        Right medit -> do-          forM_ medit $ \edit ->-            sendRequest-              SWorkspaceApplyEdit-              (ApplyWorkspaceEditParams Nothing edit)-              (const $ pure ())-          pure $ Right Null-tacticCmd _ _ _ =-  pure $ Left $ mkErr InvalidRequest "Bad URI"---timingOut-    :: Int                     -- ^ Time in microseconds-    -> Either ResponseError a  -- ^ Computation to run-    -> MaybeT IO (Either ResponseError a)-timingOut t m = do-  x <- lift $ timeout t $ evaluate m-  pure $ joinNote (mkErr InvalidRequest "timed out") x---mkErr :: ErrorCode -> T.Text -> ResponseError-mkErr code err = ResponseError code err Nothing---joinNote :: e -> Maybe (Either e a) -> Either e a-joinNote e Nothing  = Left e-joinNote _ (Just a) = a------------------------------------------------------------------------------------ | Turn a 'RunTacticResults' into concrete edits to make in the source--- document.-mkWorkspaceEdits-    :: RealSrcSpan-    -> DynFlags-    -> ClientCapabilities-    -> Uri-    -> Annotated ParsedSource-    -> RunTacticResults-    -> Either ResponseError (Maybe WorkspaceEdit)-mkWorkspaceEdits span dflags ccs uri pm rtr = do-  let g = graftHole (RealSrcSpan span) rtr-      response = transform dflags ccs uri g pm-   in case response of-        Right res -> Right $ Just res-        Left err  -> Left $ mkErr InternalError $ T.pack err------------------------------------------------------------------------------------ | Graft a 'RunTacticResults' into the correct place in an AST. Correctly--- deals with top-level holes, in which we might need to fiddle with the--- 'Match's that bind variables.-graftHole-    :: SrcSpan-    -> RunTacticResults-    -> Graft (Either String) ParsedSource-graftHole span rtr-  | _jIsTopHole (rtr_jdg rtr)-      = graftSmallestDeclsWithM span-      $ graftDecl span $ \pats ->-        splitToDecl (fst $ last $ ctxDefiningFuncs $ rtr_ctx rtr)-      $ iterateSplit-      $ mkFirstAgda (fmap unXPat pats)-      $ unLoc-      $ rtr_extract rtr-graftHole span rtr-  = graftWithoutParentheses span-    -- Parenthesize the extract iff we're not in a top level hole-  $ bool maybeParensAST id (_jIsTopHole $ rtr_jdg rtr)-  $ rtr_extract rtr------------------------------------------------------------------------------------ | Merge in the 'Match'es of a 'FunBind' into a 'HsDecl'. Used to perform--- agda-style case splitting in which we need to separate one 'Match' into--- many, without affecting any matches which might exist but don't need to be--- split.-mergeFunBindMatches-    :: ([Pat GhcPs] -> LHsDecl GhcPs)-    -> SrcSpan-    -> HsBind GhcPs-    -> Either String (HsBind GhcPs)-mergeFunBindMatches make_decl span-    (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =-  pure $ fb-    { fun_matches = mg-      { mg_alts = L alts_src $ do-          alt@(L alt_src match) <- alts-          case span `isSubspanOf` alt_src of-            True -> do-              let pats = fmap fromPatCompatPs $ m_pats match-                  L _ (ValD _ (FunBind {fun_matches = MG-                        {mg_alts = L _ to_add}})) = make_decl pats-              to_add-            False -> pure alt-      }-    }-mergeFunBindMatches _ _ _ =-  Left "mergeFunBindMatches: called on something that isnt a funbind"---throwError :: String -> TransformT (Either String) a-throwError = lift . Left------------------------------------------------------------------------------------ | Helper function to route 'mergeFunBindMatches' into the right place in an--- AST --- correctly dealing with inserting into instance declarations.-graftDecl-    :: SrcSpan-    -> ([Pat GhcPs] -> LHsDecl GhcPs)-    -> LHsDecl GhcPs-    -> TransformT (Either String) (Maybe [LHsDecl GhcPs])-graftDecl span-    make_decl-    (L src (ValD ext fb))-  = either throwError (pure . Just . pure . L src . ValD ext) $-      mergeFunBindMatches make_decl span fb--- TODO(sandy): add another case for default methods in class definitions-graftDecl span-    make_decl-    (L src (InstD ext-      cid@ClsInstD{cid_inst =-        cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))-  = do-      binds' <--        for (bagToList binds) $ \b@(L bsrc bind) -> do-          case bind of-            fb@FunBind{} | span `isSubspanOf` bsrc ->-              either throwError (pure . L bsrc) $-                mergeFunBindMatches make_decl span fb-            _ -> pure b--      pure $ Just $ pure $ L src $ InstD ext $ cid-        { cid_inst = cidi-          { cid_binds = listToBag binds'-          }-        }-graftDecl span _ x = do-  traceMX "biggest" $-    unsafeRender $-      locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x-  traceMX "first" $-    unsafeRender $-      locateFirst @(Match GhcPs (LHsExpr GhcPs)) x-  throwError "graftDecl: don't know about this AST form"---fromMaybeT :: Functor m => a -> MaybeT m a -> m a-fromMaybeT def = fmap (fromMaybe def) . runMaybeT---locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r-locateBiggest ss x = getFirst $ everything (<>)-  ( mkQ mempty $ \case-    L span r | ss `isSubspanOf` span -> pure r-    _                                -> mempty-  ) x---locateFirst :: (Data r, Data a) => a -> Maybe r-locateFirst x = getFirst $ everything (<>)-  ( mkQ mempty $ \case-    r -> pure r-  ) x+import Wingman.Plugin 

@@ -1,28 +0,0 @@-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-

@@ -1,87 +0,0 @@-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE ViewPatterns        #-}--module Ide.Plugin.Tactic.CaseSplit-  ( mkFirstAgda-  , iterateSplit-  , splitToDecl-  ) where--import           Data.Bool (bool)-import           Data.Data-import           Data.Generics-import           Data.Set (Set)-import qualified Data.Set as S-import           Development.IDE.GHC.Compat-import           GHC.Exts (IsString(fromString))-import           GHC.SourceGen (funBinds, match, wildP)-import           Ide.Plugin.Tactic.GHC-import           Ide.Plugin.Tactic.Types-import           OccName------------------------------------------------------------------------------------- | Construct an 'AgdaMatch' from patterns in scope (should be the LHS of the--- match) and a body.-mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch-mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body-mkFirstAgda pats body = AgdaMatch pats body------------------------------------------------------------------------------------ | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by--- splitting it into multiple matches: one for each alternative of the case.-agdaSplit :: AgdaMatch -> [AgdaMatch]-agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do-  (pat, body) <- matches-  -- TODO(sandy): use an at pattern if necessary-  pure $ AgdaMatch (rewriteVarPat var pat pats) body-agdaSplit x = [x]------------------------------------------------------------------------------------ | Replace unused bound patterns with wild patterns.-wildify :: AgdaMatch -> AgdaMatch-wildify (AgdaMatch pats body) =-  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body-   in AgdaMatch (make_wild pats) body------------------------------------------------------------------------------------ | Helper function for 'wildify'.-wildifyT :: Data a => Set OccName -> a -> a-wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case-  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP-  (x :: Pat GhcPs) -> x------------------------------------------------------------------------------------ | Replace a 'VarPat' with the given @'Pat' GhcPs@.-rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a-rewriteVarPat name rep = everywhere $ mkT $ \case-  VarPat _ (L _ var) | eqRdrName name var -> rep-  (x :: Pat GhcPs) -> x------------------------------------------------------------------------------------ | Construct an 'HsDecl' from a set of 'AgdaMatch'es.-splitToDecl-    :: OccName  -- ^ The name of the function-    -> [AgdaMatch]-    -> LHsDecl GhcPs-splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do-  AgdaMatch pats body <- ams-  pure $ match pats body------------------------------------------------------------------------------------ | Sometimes 'agdaSplit' exposes another opportunity to do 'agdaSplit'. This--- function runs it a few times, hoping it will find a fixpoint.-iterateSplit :: AgdaMatch -> [AgdaMatch]-iterateSplit am =-  let iterated = iterate (agdaSplit =<<) $ pure am-   in fmap wildify . head . drop 5 $ iterated-

@@ -1,205 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TupleSections    #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE ViewPatterns     #-}--module Ide.Plugin.Tactic.CodeGen-  ( module Ide.Plugin.Tactic.CodeGen-  , module Ide.Plugin.Tactic.CodeGen.Utils-  ) 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.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           Ide.Plugin.Tactic.CodeGen.Utils-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 $ hyByName $ 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 (hyNamesInScope 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) -> HyInfo CType -> Judgement -> Rule-destruct' f hi jdg = do-  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic-  let term = hi_name hi-  useOccName jdg term-  (tr, ms)-      <- destructMatches-           f-           (Just term)-           (hi_type hi)-           $ 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 tyapps = do-  let args = dataConInstOrigArgTys' dc tyapps-  (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-

@@ -1,72 +0,0 @@-{-# LANGUAGE ViewPatterns #-}--module Ide.Plugin.Tactic.CodeGen.Utils where--import Data.List-import DataCon-import Development.IDE.GHC.Compat-import GHC.Exts-import GHC.SourceGen (recordConE, RdrNameStr)-import GHC.SourceGen.Overloaded-import Ide.Plugin.Tactic.GHC (getRecordFields)-import Name------------------------------------------------------------------------------------ | Make a data constructor with the given arguments.-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'-  | Just fields <- getRecordFields dcon =-      noLoc $ recordConE (coerceName dcon_name) $ do-        (arg, (field, _)) <- zip args fields-        pure (coerceName field, arg)-  | 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 "$"-

@@ -1,95 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE LambdaCase       #-}--module Ide.Plugin.Tactic.Context where--import           Bag-import           Control.Arrow-import           Control.Monad.Reader-import           Data.List-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)-import Ide.Plugin.Tactic.FeatureSet (FeatureSet)---mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context-mkContext features locals tcg = Context-  { ctxDefiningFuncs = locals-  , ctxModuleFuncs = fmap splitId-                   . (getFunBindId =<<)-                   . fmap unLoc-                   . bagToList-                   $ tcg_binds tcg-  , ctxFeatureSet = features-  }------------------------------------------------------------------------------------ | Find all of the class methods that exist from the givens in the context.-contextMethodHypothesis :: Context -> Hypothesis CType-contextMethodHypothesis ctx-  = Hypothesis-  . 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 :: [HyInfo a] -> [HyInfo a]-excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)-  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

@@ -1,59 +0,0 @@-{-# LANGUAGE BangPatterns     #-}-{-# LANGUAGE CPP              #-}-{-# LANGUAGE TypeApplications #-}--module Ide.Plugin.Tactic.Debug-  ( unsafeRender-  , unsafeRender'-  , traceM-  , traceShowId-  , trace-  , traceX-  , traceIdX-  , traceMX-  , traceFX-  ) 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--traceFX :: String -> (a -> String) -> a -> a-traceFX str f a = trace (mappend ("!!!" <> str <> ": ") $ f a) a-

@@ -1,92 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE PatternSynonyms   #-}-{-# LANGUAGE ViewPatterns      #-}--module Ide.Plugin.Tactic.FeatureSet-  ( Feature (..)-  , FeatureSet-  , hasFeature-  , defaultFeatures-  , allFeatures-  , parseFeatureSet-  , prettyFeatureSet-  ) where--import           Data.List (intercalate)-import           Data.Maybe (mapMaybe, listToMaybe)-import           Data.Set (Set)-import qualified Data.Set as S-import qualified Data.Text as T------------------------------------------------------------------------------------ | All the available features. A 'FeatureSet' describes the ones currently--- available to the user.-data Feature = CantHaveAnEmptyDataType-  deriving (Eq, Ord, Show, Read, Enum, Bounded)------------------------------------------------------------------------------------ | A collection of enabled features.-type FeatureSet = Set Feature------------------------------------------------------------------------------------ | Parse a feature set.-parseFeatureSet :: T.Text -> FeatureSet-parseFeatureSet-  = mappend defaultFeatures-  . S.fromList-  . mapMaybe (readMaybe . mappend featurePrefix . rot13 . T.unpack)-  . T.split (== '/')------------------------------------------------------------------------------------ | Features that are globally enabled for all users.-defaultFeatures :: FeatureSet-defaultFeatures = S.fromList-  [-  ]------------------------------------------------------------------------------------ | All available features.-allFeatures :: FeatureSet-allFeatures = S.fromList $ enumFromTo minBound maxBound------------------------------------------------------------------------------------ | Pretty print a feature set.-prettyFeatureSet :: FeatureSet -> String-prettyFeatureSet-  = intercalate "/"-  . fmap (rot13 . drop (length featurePrefix) . show)-  . S.toList------------------------------------------------------------------------------------ | Is a given 'Feature' currently enabled?-hasFeature :: Feature -> FeatureSet -> Bool-hasFeature = S.member------------------------------------------------------------------------------------ | Like 'read', but not partial.-readMaybe :: Read a => String -> Maybe a-readMaybe = fmap fst . listToMaybe . reads---featurePrefix :: String-featurePrefix = "Feature"---rot13 :: String -> String-rot13 = fmap (toEnum . rot13int . fromEnum)---rot13int :: Integral a => a -> a-rot13int x-  | (fromIntegral x :: Word) - 97 < 26 = 97 + rem (x - 84) 26-  | (fromIntegral x :: Word) - 65 < 26 = 65 + rem (x - 52) 26-  | otherwise   = x-

@@ -1,292 +0,0 @@-{-# LANGUAGE CPP                 #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE PatternSynonyms     #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE ViewPatterns        #-}--module Ide.Plugin.Tactic.GHC where--import           Control.Monad.State-import           Data.Function (on)-import           Data.List (isPrefixOf)-import qualified Data.Map as M-import           Data.Maybe (isJust)-import           Data.Set (Set)-import qualified Data.Set as S-import           Data.Traversable-import           DataCon-import           Development.IDE.GHC.Compat-import           GHC.SourceGen (match, case', lambda)-import           Generics.SYB (mkQ, everything, listify, Data, 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------------------------------------------------------------------------------------ | Given a datacon, extract its record fields' names and types. Returns--- nothing if the datacon is not a record.-getRecordFields :: DataCon -> Maybe [(OccName, CType)]-getRecordFields dc =-  case dataConFieldLabels dc of-    [] -> Nothing-    lbls -> for lbls $ \lbl -> do-      (_, ty) <- dataConFieldType_maybe dc $ flLabel lbl-      pure (mkVarOccFS $ flLabel lbl, CType ty)------------------------------------------------------------------------------------ | 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------------------------------------------------------------------------------------ | We can't compare 'RdrName' for equality directly. Instead, compare them by--- their 'OccName's.-eqRdrName :: RdrName -> RdrName -> Bool-eqRdrName = (==) `on` occNameString . occName------------------------------------------------------------------------------------ | Does this thing contain any references to 'HsVar's with the given--- 'RdrName'?-containsHsVar :: Data a => RdrName -> a -> Bool-containsHsVar name x = not $ null $ listify (-  \case-    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | eqRdrName a name -> True-    _ -> False-  ) x------------------------------------------------------------------------------------ | Does this thing contain any holes?-containsHole :: Data a => a -> Bool-containsHole x = not $ null $ listify (-  \case-    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name-    _ -> False-  ) x------------------------------------------------------------------------------------ | Check if an 'OccName' is a hole-isHole :: OccName -> Bool--- TODO(sandy): Make this more robust-isHole = isPrefixOf "_" . occNameString------------------------------------------------------------------------------------ | Get all of the referenced occnames.-allOccNames :: Data a => a -> Set OccName-allOccNames = everything (<>) $ mkQ mempty $ \case-    a -> S.singleton a-------------------------------------------------------------------------------------- | A pattern over the otherwise (extremely) messy AST for lambdas.-pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs-pattern Lambda pats body <--  HsLam _-    (MG {mg_alts = L _ [L _-      (Match { m_pats = fmap fromPatCompatPs -> pats-             , m_grhss = UnguardedRHSs body-             })]})-  where-    -- If there are no patterns to bind, just stick in the body-    Lambda [] body   = body-    Lambda pats body = lambda pats body------------------------------------------------------------------------------------ | A GRHS that caontains no guards.-pattern UnguardedRHSs :: HsExpr GhcPs -> GRHSs GhcPs (LHsExpr GhcPs)-pattern UnguardedRHSs body <--  GRHSs {grhssGRHSs = [L _ (GRHS _ [] (L _ body))]}------------------------------------------------------------------------------------ | A match with a single pattern. Case matches are always 'SinglePatMatch'es.-pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)-pattern SinglePatMatch pat body <--  Match { m_pats = [fromPatCompatPs -> pat]-        , m_grhss = UnguardedRHSs body-        }------------------------------------------------------------------------------------ | Helper function for defining the 'Case' pattern.-unpackMatches :: [Match GhcPs (LHsExpr GhcPs)] -> Maybe [(Pat GhcPs, HsExpr GhcPs)]-unpackMatches [] = Just []-unpackMatches (SinglePatMatch pat body : matches) =-  (:) <$> pure (pat, body) <*> unpackMatches matches-unpackMatches _ = Nothing------------------------------------------------------------------------------------ | A pattern over the otherwise (extremely) messy AST for lambdas.-pattern Case :: HsExpr GhcPs -> [(Pat GhcPs, HsExpr GhcPs)] -> HsExpr GhcPs-pattern Case scrutinee matches <--  HsCase _ (L _ scrutinee)-    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})-  where-    Case scrutinee matches =-      case' scrutinee $ fmap (\(pat, body) -> match [pat] body) matches------------------------------------------------------------------------------------ | 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---- It's hard to generalize over these since weird type families are involved.-fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc-fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs-#if __GLASGOW_HASKELL__ == 808-type PatCompat pass = Pat pass-fromPatCompatTc = id-fromPatCompatPs = id-#else-type PatCompat pass = LPat pass-fromPatCompatTc = unLoc-fromPatCompatPs = 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 (fromPatCompatTc -> 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------------------------------------------------------------------------------------ | In GHC 8.8, sometimes patterns are wrapped in 'XPat'.--- The nitty gritty details are explained at--- https://blog.shaynefletcher.org/2020/03/ghc-haskell-pats-and-lpats.html------ We need to remove these in order to succesfull find patterns.-unXPat :: Pat GhcPs -> Pat GhcPs-#if __GLASGOW_HASKELL__ == 808-unXPat (XPat (L _ pat)) = unXPat pat-#endif-unXPat pat = pat-

@@ -1,407 +0,0 @@-{-# 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-  , hyNamesInScope-  , hyByName-  ) where--import           Control.Arrow-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 -> Hypothesis CType-hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span------------------------------------------------------------------------------------ | Convert a @Set Id@ into a hypothesis.-buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType-buildHypothesis-  = Hypothesis-  . mapMaybe go-  where-    go (occName -> occ, t)-      | Just ty <- t-      , isAlpha . head . occNameString $ occ = Just $ HyInfo occ 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" <>~ (Hypothesis $ zip [0..] ns <&>-    \(pos, (name, ty)) -> HyInfo name (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 $ hyByName $ 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) $ hyByName $ 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 $ hyByName $ 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 = hyByName-         . 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) (hyByName $ 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" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->-    case S.member (hi_name hi) 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 -> Hypothesis a-jHypothesis-  = Hypothesis-  . filter (not . isDisallowed . hi_provenance)-  . unHypothesis-  . jEntireHypothesis------------------------------------------------------------------------------------ | The whole hypothesis, including things disallowed.-jEntireHypothesis :: Judgement' a -> Hypothesis a-jEntireHypothesis = _jHypothesis------------------------------------------------------------------------------------ | Just the local hypothesis.-jLocalHypothesis :: Judgement' a -> Hypothesis a-jLocalHypothesis-  = Hypothesis-  . filter (isLocalHypothesis . hi_provenance)-  . unHypothesis-  . 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------------------------------------------------------------------------------------ | What names are currently in scope in the hypothesis?-hyNamesInScope :: Hypothesis a -> Set OccName-hyNamesInScope = M.keysSet . hyByName------------------------------------------------------------------------------------ | Fold a hypothesis into a single mapping from name to info. This--- unavoidably will cause duplicate names (things like methods) to shadow one--- another.-hyByName :: Hypothesis a -> Map OccName (HyInfo a)-hyByName-  = M.fromList-  . fmap (hi_name &&& id)-  . unHypothesis------------------------------------------------------------------------------------ | Only the hypothesis members which are pattern vals-jPatHypothesis :: Judgement' a -> Map OccName PatVal-jPatHypothesis-  = M.mapMaybe (getPatVal . hi_provenance)-  . hyByName-  . 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-    :: Hypothesis 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

@@ -1,39 +0,0 @@-{-# 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-    ]-

@@ -1,110 +0,0 @@-{-# LANGUAGE ViewPatterns #-}--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

@@ -1,212 +0,0 @@-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE GADTs               #-}-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE ScopedTypeVariables #-}--module Ide.Plugin.Tactic.LanguageServer where--import           Control.Arrow-import           Control.Monad-import           Control.Monad.Trans.Maybe-import           Data.Aeson                           (Value (Object), fromJSON)-import           Data.Aeson.Types                     (Result (Error, Success))-import           Data.Coerce-import           Data.Functor                         ((<&>))-import           Data.Generics.Aliases                (mkQ)-import           Data.Generics.Schemes                (everything)-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                      (ShakeExtras,-                                                       getPluginConfig)-import           Development.IDE.Core.PositionMapping-import           Development.IDE.Core.RuleTypes-import           Development.IDE.Core.Service         (runAction)-import           Development.IDE.Core.Shake           (IdeState (..),-                                                       useWithStale)-import           Development.IDE.GHC.Compat-import           Development.IDE.GHC.Error            (realSrcSpanToRange)-import           Development.IDE.Spans.LocalBindings  (Bindings,-                                                       getDefiningBindings)-import           Development.Shake                    (Action, RuleResult)-import           Development.Shake.Classes-import qualified FastString-import           Ide.Plugin.Config                    (PluginConfig (plcConfig))-import qualified Ide.Plugin.Config                    as Plugin-import           Ide.Plugin.Tactic.Context-import           Ide.Plugin.Tactic.FeatureSet-import           Ide.Plugin.Tactic.GHC-import           Ide.Plugin.Tactic.Judgements-import           Ide.Plugin.Tactic.Range-import           Ide.Plugin.Tactic.TestTypes          (TacticCommand,-                                                       cfg_feature_set)-import           Ide.Plugin.Tactic.Types-import           Language.LSP.Server                  (MonadLsp)-import           Language.LSP.Types-import           OccName-import           Prelude                              hiding (span)-import           SrcLoc                               (containsSpan)-import           TcRnTypes                            (tcg_binds)---tacticDesc :: T.Text -> T.Text-tacticDesc name = "fill the hole using the " <> name <> " tactic"------------------------------------------------------------------------------------ | The name of the command for the LS.-tcCommandName :: TacticCommand -> T.Text-tcCommandName = T.pack . show---runIde :: IdeState -> Action a -> IO a-runIde state = runAction "tactic" state---runStaleIde-    :: forall a r-     . ( r ~ RuleResult a-       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a-       , Show r, Typeable r, NFData r-       )-    => IdeState-    -> NormalizedFilePath-    -> a-    -> MaybeT IO (r, PositionMapping)-runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp------------------------------------------------------------------------------------ | Get the current feature set from the plugin config.-getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet-getFeatureSet extras = do-  pcfg <- getPluginConfig extras "tactics"-  pure $ case fromJSON $ Object $ plcConfig pcfg of-    Success cfg -> cfg_feature_set cfg-    Error _     -> defaultFeatures---getIdeDynflags-    :: IdeState-    -> NormalizedFilePath-    -> MaybeT IO DynFlags-getIdeDynflags state nfp = do-  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'-  -- which don't change very often.-  ((modsum,_), _) <- runStaleIde state nfp GetModSummaryWithoutTimestamps-  pure $ ms_hspp_opts modsum------------------------------------------------------------------------------------ | Find the last typechecked module, and find the most specific span, as well--- as the judgement at the given range.-judgementForHole-    :: IdeState-    -> NormalizedFilePath-    -> Range-    -> FeatureSet-    -> MaybeT IO (Range, Judgement, Context, DynFlags)-judgementForHole state nfp range features = do-  (asts, amapping) <- runStaleIde state nfp GetHieAst-  case asts of-    HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"-    HAR _ hf _ _ HieFresh -> do-      (binds, _) <- runStaleIde state nfp GetBindings-      (tcmod, _) <- runStaleIde state nfp TypeCheck-      (rss, g)   <- liftMaybe $ getSpanAndTypeAtHole amapping range hf-      resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss-      let (jdg, ctx) = mkJudgementAndContext features g binds rss tcmod-      dflags <- getIdeDynflags state nfp-      pure (resulting_range, jdg, ctx, dflags)---mkJudgementAndContext-    :: FeatureSet-    -> Type-    -> Bindings-    -> RealSrcSpan-    -> TcModuleResult-    -> (Judgement, Context)-mkJudgementAndContext features g binds rss tcmod = do-      let tcg  = tmrTypechecked tcmod-          tcs = tcg_binds tcg-          ctx = mkContext features-                  (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-       in ( mkFirstJudgement-              (local_hy <> cls_hy)-              (isRhsHole rss tcs)-              g-          , ctx-          )---getSpanAndTypeAtHole-    :: PositionMapping-    -> Range-    -> HieASTs b-    -> Maybe (Span, b)-getSpanAndTypeAtHole amapping range hf = do-  range' <- fromCurrentRange amapping range-  join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \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)---liftMaybe :: Monad m => Maybe a -> MaybeT m a-liftMaybe a = MaybeT $ pure a---spliceProvenance-    :: Map OccName Provenance-    -> Hypothesis a-    -> Hypothesis a-spliceProvenance provs x =-  Hypothesis $ flip fmap (unHypothesis x) $ \hi ->-    overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi------------------------------------------------------------------------------------ | 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------------------------------------------------------------------------------------ | 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-

@@ -1,192 +0,0 @@-{-# LANGUAGE DeriveAnyClass     #-}-{-# LANGUAGE DeriveGeneric      #-}-{-# LANGUAGE DerivingStrategies #-}-{-# LANGUAGE OverloadedStrings  #-}-{-# LANGUAGE ViewPatterns       #-}--module Ide.Plugin.Tactic.LanguageServer.TacticProviders-  ( commandProvider-  , commandTactic-  , tcCommandId-  , TacticParams (..)-  ) where--import           Control.Monad-import           Control.Monad.Error.Class (MonadError(throwError))-import           Data.Aeson-import           Data.Coerce-import qualified Data.Map as M-import           Data.Maybe-import           Data.Monoid-import qualified Data.Text as T-import           Data.Traversable-import           Development.IDE.GHC.Compat-import           GHC.Generics-import           GHC.LanguageExtensions.Type (Extension (LambdaCase))-import           Ide.Plugin.Tactic.Auto-import           Ide.Plugin.Tactic.FeatureSet-import           Ide.Plugin.Tactic.GHC-import           Ide.Plugin.Tactic.Judgements-import           Ide.Plugin.Tactic.Tactics-import           Ide.Plugin.Tactic.TestTypes-import           Ide.Plugin.Tactic.Types-import           Ide.PluginUtils-import           Ide.Types-import           Language.LSP.Types-import           OccName-import           Prelude hiding (span)-import           Refinery.Tactic (goal)------------------------------------------------------------------------------------ | A mapping from tactic commands to actual tactics for refinery.-commandTactic :: TacticCommand -> OccName -> TacticsM ()-commandTactic Auto         = const auto-commandTactic Intros       = const intros-commandTactic Destruct     = useNameFromHypothesis destruct-commandTactic Homomorphism = useNameFromHypothesis homo-commandTactic DestructLambdaCase     = const destructLambdaCase-commandTactic HomomorphismLambdaCase = const homoLambdaCase------------------------------------------------------------------------------------ | 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 'TacticProvider' is a way of giving context-sensitive actions to the LS--- UI.-type TacticProvider-     = DynFlags-    -> FeatureSet-    -> PluginId-    -> Uri-    -> Range-    -> Judgement-    -> IO [Command |? CodeAction]---data TacticParams = TacticParams-    { tp_file     :: Uri    -- ^ Uri of the file to fill the hole in-    , tp_range    :: Range  -- ^ The range of the hole-    , tp_var_name :: T.Text-    }-  deriving stock (Show, Eq, Generic)-  deriving anyclass (ToJSON, FromJSON)------------------------------------------------------------------------------------ | Restrict a 'TacticProvider', making sure it appears only when the given--- 'Feature' is in the feature set.-requireFeature :: Feature -> TacticProvider -> TacticProvider-requireFeature f tp dflags fs plId uri range jdg = do-  guard $ hasFeature f fs-  tp dflags fs plId uri range jdg------------------------------------------------------------------------------------ | Restrict a 'TacticProvider', making sure it appears only when the given--- predicate holds for the goal.-requireExtension :: Extension -> TacticProvider -> TacticProvider-requireExtension ext tp dflags fs plId uri range jdg =-  case xopt ext dflags of-    True  -> tp dflags fs 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 fs plId uri range jdg =-  case p $ unCType $ jGoal jdg of-    True  -> tp dflags fs 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 fs plId uri range jdg =-  let hy = jHypothesis jdg-      g  = jGoal jdg-   in fmap join $ for (unHypothesis hy) $ \hi ->-        let ty = unCType $ hi_type hi-         in case p (unCType g) ty of-              True  -> tp (hi_name hi) ty dflags fs plId uri range jdg-              False -> pure []------------------------------------------------------------------------------------- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to--- look it up in the hypothesis.-useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a-useNameFromHypothesis f name = do-  hy <- jHypothesis <$> goal-  case M.lookup name $ hyByName hy of-    Just hi -> f hi-    Nothing -> throwError $ NotInScope name------------------------------------------------------------------------------------ | 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 { tp_file = uri , tp_range = range , tp_var_name = name }-      cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])-  pure-    $ pure-    $ InR-    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing Nothing Nothing-    $ Just cmd------------------------------------------------------------------------------------ | Construct a 'CommandId'-tcCommandId :: TacticCommand -> CommandId-tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"------------------------------------------------------------------------------------- | 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-

@@ -1,253 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE DerivingVia           #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE LambdaCase            #-}-{-# LANGUAGE MonoLocalBinds        #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RecordWildCards       #-}-{-# 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.Simplify (simplify)-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-                $ hyByName-                $ jHypothesis jdg-        unused_topvals = M.keysSet-                       $ M.filter (isTopLevel . hi_provenance)-                       $ hyByName-                       $ 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-                { rtr_trace = tr-                , rtr_extract = simplify ext-                , rtr_other_solns = reverse . fmap fst $ take 5 sorted-                , rtr_jdg = jdg-                , rtr_ctx = ctx-                }-          -- guaranteed to not be empty-          _ -> Left []--assoc23 :: (a, b, c) -> (a, (b, c))-assoc23 (a, b, c) = (a, (b, c))---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 [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 ( HyInfo (occName method) (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

@@ -1,97 +0,0 @@-{-# 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.Set (Set)-import qualified Data.Set as S-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 (f a) = "fa"-mkTyName (tcSplitAppTys -> (t, args@(_:_)))-  = mkTyName t ++ 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-    :: Set 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 S.member (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)-  => Set OccName-  -> t Type-  -> m (t OccName)-mkManyGoodNames in_scope args =-  flip evalStateT in_scope $ for args $ \at -> do-    in_scope <- get-    let n = mkGoodName in_scope at-    modify $ S.insert n-    pure n------------------------------------------------------------------------------------ | Which names are in scope?-getInScope :: Map OccName a -> [OccName]-getInScope = M.keys

@@ -1,18 +0,0 @@-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))-

@@ -1,108 +0,0 @@-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE PatternSynonyms     #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE ViewPatterns        #-}--module Ide.Plugin.Tactic.Simplify-  ( simplify-  ) where--import Data.Generics (everywhere, mkT, GenericT)-import Data.List.Extra (unsnoc)-import Data.Monoid (Endo (..))-import Development.IDE.GHC.Compat-import GHC.SourceGen (var)-import GHC.SourceGen.Expr (lambda)-import Ide.Plugin.Tactic.CodeGen.Utils-import Ide.Plugin.Tactic.GHC (fromPatCompatPs, containsHsVar)------------------------------------------------------------------------------------ | A pattern over the otherwise (extremely) messy AST for lambdas.-pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs-pattern Lambda pats body <--  HsLam _-    (MG {mg_alts = L _ [L _-      (Match { m_pats = fmap fromPatCompatPs -> pats-             , m_grhss = GRHSs {grhssGRHSs = [L _ (-                 GRHS _ [] (L _ body))]}-             })]})-  where-    -- If there are no patterns to bind, just stick in the body-    Lambda [] body   = body-    Lambda pats body = lambda pats body------------------------------------------------------------------------------------ | Simlify an expression.-simplify :: LHsExpr GhcPs -> LHsExpr GhcPs-simplify-  = head-  . drop 3   -- Do three passes; this should be good enough for the limited-             -- amount of gas we give to auto-  . iterate (everywhere $ foldEndo-    [ simplifyEtaReduce-    , simplifyRemoveParens-    , simplifyCompose-    ])------------------------------------------------------------------------------------ | Like 'foldMap' but for endomorphisms.-foldEndo :: Foldable t => t (a -> a) -> a -> a-foldEndo = appEndo . foldMap Endo------------------------------------------------------------------------------------ | Perform an eta reduction. For example, transforms @\x -> (f g) x@ into--- @f g@.-simplifyEtaReduce :: GenericT-simplifyEtaReduce = mkT $ \case-  Lambda-      [VarPat _ (L _ pat)]-      (HsVar _ (L _ a)) | pat == a ->-    var "id"-  Lambda-      (unsnoc -> Just (pats, (VarPat _ (L _ pat))))-      (HsApp _ (L _ f) (L _ (HsVar _ (L _ a))))-      | pat == a-        -- We can only perform this simplifiation if @pat@ is otherwise unused.-      , not (containsHsVar pat f) ->-    Lambda pats f-  x -> x------------------------------------------------------------------------------------ | Perform an eta-reducing function composition. For example, transforms--- @\x -> f (g (h x))@ into @f . g . h@.-simplifyCompose :: GenericT-simplifyCompose = mkT $ \case-  Lambda-      (unsnoc -> Just (pats, (VarPat _ (L _ pat))))-      (unroll -> (fs@(_:_), (HsVar _ (L _ a))))-      | pat == a-        -- We can only perform this simplifiation if @pat@ is otherwise unused.-      , not (containsHsVar pat fs) ->-    Lambda pats (foldr1 (infixCall ".") fs)-  x -> x------------------------------------------------------------------------------------ | Removes unnecessary parentheses on any token that doesn't need them.-simplifyRemoveParens :: GenericT-simplifyRemoveParens = mkT $ \case-  HsPar _ (L _ x) | isAtomicHsExpr x -> x-  (x :: HsExpr GhcPs) -> x------------------------------------------------------------------------------------ | Unrolls a right-associative function application of the form--- @HsApp f (HsApp g (HsApp h x))@ into @([f, g, h], x)@.-unroll :: HsExpr GhcPs -> ([HsExpr GhcPs], HsExpr GhcPs)-unroll (HsPar _ (L _ x)) = unroll x-unroll (HsApp _ (L _ f) (L _ a)) =-  let (fs, r) = unroll a-   in (f : fs, r)-unroll x = ([], x)-

@@ -1,281 +0,0 @@-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# 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           Data.Set (Set)-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 (S.toList . 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 $ hyByName $ 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 defs) $ \(name, ty) -> do-    modify $ pushRecursionStack .  countRecursiveCall-    ensure guardStructurallySmallerRecursion popRecursionStack $ do-      (localTactic (apply $ HyInfo name RecursivePrv ty) $ 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 (hyNamesInScope $ 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 :: HyInfo CType -> TacticsM ()-destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do-  jdg <- goal-  let subtactic = rule $ destruct' (const subgoal) hi-  case isPatternMatch $ hi_provenance hi of-    True ->-      pruning subtactic $ \jdgs ->-        let getHyTypes = S.fromList . fmap hi_type . unHypothesis . jHypothesis-            new_hy = foldMap getHyTypes jdgs-            old_hy = getHyTypes jdg-        in case S.null $ new_hy S.\\ old_hy of-              True  -> Just $ UnhelpfulDestruct $ hi_name hi-              False -> Nothing-    False -> subtactic------------------------------------------------------------------------------------ | Case split, and leave holes in the matches.-destruct :: HyInfo CType -> TacticsM ()-destruct hi = requireConcreteHole $ tracing "destruct(user)" $-  rule $ destruct' (const subgoal) hi------------------------------------------------------------------------------------ | Case split, using the same data constructor in the matches.-homo :: HyInfo CType -> 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 :: HyInfo CType -> TacticsM ()-apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do-  jdg <- goal-  let hy = jHypothesis jdg-      g  = jGoal jdg-      ty = unCType $ hi_type hi-      func = hi_name hi-  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------------------------------------------------------------------------------------ | 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 :: (HyInfo CType -> TacticsM ()) -> TacticsM ()-overFunctions =-  attemptOn $ filter (isFunction . unCType . hi_type)-           . unHypothesis-           . jHypothesis--overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()-overAlgebraicTerms =-  attemptOn $ filter (isJust . algebraicTyCon . unCType . hi_type)-            . unHypothesis-            . jHypothesis---allNames :: Judgement -> Set OccName-allNames = hyNamesInScope . jHypothesis-

@@ -1,50 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--module Ide.Plugin.Tactic.TestTypes where--import qualified Data.Text as T-import Data.Aeson-import Ide.Plugin.Tactic.FeatureSet----------------------------------------------------------------------------------- | 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"------------------------------------------------------------------------------------ | Plugin configuration for tactics-newtype Config = Config-  { cfg_feature_set :: FeatureSet-  }--emptyConfig :: Config-emptyConfig = Config defaultFeatures--instance ToJSON Config where-  toJSON (Config features) = object-    [ "features" .= prettyFeatureSet features-    ]--instance FromJSON Config where-  parseJSON = withObject "Config" $ \obj -> do-    features <- parseFeatureSet <$> obj .: "features"-    pure $ Config features-

@@ -1,389 +0,0 @@-{-# LANGUAGE DeriveFunctor              #-}-{-# LANGUAGE DeriveGeneric              #-}-{-# LANGUAGE DerivingVia                #-}-{-# LANGUAGE FlexibleContexts           #-}-{-# LANGUAGE FlexibleInstances          #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE MultiParamTypeClasses      #-}-{-# LANGUAGE OverloadedStrings          #-}-{-# LANGUAGE TypeApplications           #-}-{-# 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.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 Ide.Plugin.Tactic.FeatureSet (FeatureSet)-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--instance Show (HsExpr GhcPs) where-  show  = unsafeRender--instance Show (Pat GhcPs) 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---newtype Hypothesis a = Hypothesis-  { unHypothesis :: [HyInfo a]-  }-  deriving stock (Functor, Eq, Show, Generic, Ord)-  deriving newtype (Semigroup, Monoid)------------------------------------------------------------------------------------ | The provenance and type of a hypothesis term.-data HyInfo a = HyInfo-  { hi_name       :: OccName-  , 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 name prv ty) = HyInfo name (f prv) ty------------------------------------------------------------------------------------ | The current bindings and goal for a hole to be filled by refinery.-data Judgement' a = Judgement-  { _jHypothesis :: !(Hypothesis 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-  , ctxFeatureSet :: FeatureSet-  }-  deriving stock (Eq, Ord, Show)------------------------------------------------------------------------------------ | An empty context-emptyContext :: Context-emptyContext  = Context mempty 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)]-  , rtr_jdg         :: Judgement-  , rtr_ctx         :: Context-  } deriving Show---data AgdaMatch = AgdaMatch-  { amPats :: [Pat GhcPs]-  , amBody :: HsExpr GhcPs-  }-  deriving (Show)-

@@ -0,0 +1,30 @@+module Wingman.Auto where++import           Control.Monad.State (gets)+import qualified Data.Set as S+import           Refinery.Tactic+import           Wingman.Context+import           Wingman.Judgements+import           Wingman.KnownStrategies+import           Wingman.Machinery (tracing)+import           Wingman.Tactics+import           Wingman.Types+++------------------------------------------------------------------------------+-- | 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+    . S.fromList+    $ fmap fst current+

@@ -0,0 +1,82 @@+module Wingman.CaseSplit+  ( mkFirstAgda+  , iterateSplit+  , splitToDecl+  ) where++import           Data.Bool (bool)+import           Data.Data+import           Data.Generics+import           Data.Set (Set)+import qualified Data.Set as S+import           Development.IDE.GHC.Compat+import           GHC.Exts (IsString (fromString))+import           GHC.SourceGen (funBinds, match, wildP)+import           OccName+import           Wingman.GHC+import           Wingman.Types++++------------------------------------------------------------------------------+-- | Construct an 'AgdaMatch' from patterns in scope (should be the LHS of the+-- match) and a body.+mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch+mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body+mkFirstAgda pats body                = AgdaMatch pats body+++------------------------------------------------------------------------------+-- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by+-- splitting it into multiple matches: one for each alternative of the case.+agdaSplit :: AgdaMatch -> [AgdaMatch]+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do+  (pat, body) <- matches+  -- TODO(sandy): use an at pattern if necessary+  pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body+agdaSplit x = [x]+++------------------------------------------------------------------------------+-- | Replace unused bound patterns with wild patterns.+wildify :: AgdaMatch -> AgdaMatch+wildify (AgdaMatch pats body) =+  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body+   in AgdaMatch (make_wild pats) body+++------------------------------------------------------------------------------+-- | Helper function for 'wildify'.+wildifyT :: Data a => Set OccName -> a -> a+wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case+  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP+  (x :: Pat GhcPs)                                                    -> x+++------------------------------------------------------------------------------+-- | Replace a 'VarPat' with the given @'Pat' GhcPs@.+rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a+rewriteVarPat name rep = everywhere $ mkT $ \case+  VarPat _ (L _ var) | eqRdrName name var -> rep+  (x :: Pat GhcPs)                        -> x+++------------------------------------------------------------------------------+-- | Construct an 'HsDecl' from a set of 'AgdaMatch'es.+splitToDecl+    :: OccName  -- ^ The name of the function+    -> [AgdaMatch]+    -> LHsDecl GhcPs+splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do+  AgdaMatch pats body <- ams+  pure $ match pats body+++------------------------------------------------------------------------------+-- | Sometimes 'agdaSplit' exposes another opportunity to do 'agdaSplit'. This+-- function runs it a few times, hoping it will find a fixpoint.+iterateSplit :: AgdaMatch -> [AgdaMatch]+iterateSplit am =+  let iterated = iterate (agdaSplit =<<) $ pure am+   in fmap wildify . head . drop 5 $ iterated+

@@ -0,0 +1,215 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE OverloadedLabels #-}+{-# LANGUAGE TupleSections    #-}+{-# LANGUAGE TypeApplications #-}++module Wingman.CodeGen+  ( module Wingman.CodeGen+  , module Wingman.CodeGen.Utils+  ) where+++import           ConLike+import           Control.Lens ((%~), (<>~), (&))+import           Control.Monad.Except+import           Control.Monad.State+import           Data.Bool (bool)+import           Data.Generics.Labels ()+import           Data.List+import           Data.Monoid (Endo(..))+import qualified Data.Set as S+import           Data.Traversable+import           DataCon+import           Development.IDE.GHC.Compat+import           GHC.Exts+import           GHC.SourceGen.Binds+import           GHC.SourceGen.Expr+import           GHC.SourceGen.Overloaded+import           GHC.SourceGen.Pat+import           GhcPlugins (isSymOcc)+import           PatSyn+import           Type hiding (Var)+import           Wingman.CodeGen.Utils+import           Wingman.GHC+import           Wingman.Judgements+import           Wingman.Judgements.Theta+import           Wingman.Machinery+import           Wingman.Naming+import           Wingman.Types+++destructMatches+    :: (ConLike -> Judgement -> Rule)+       -- ^ How to construct each match+    -> Maybe OccName+       -- ^ Scrutinee+    -> CType+       -- ^ Type being destructed+    -> Judgement+    -> RuleM (Synthesized [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 con = RealDataCon dc+              ev = concatMap mkEvidence $ dataConInstArgTys dc apps+              -- We explicitly do not need to add the method hypothesis to+              -- #syn_scoped+              method_hy = foldMap evidenceToHypothesis ev+              args = conLikeInstOrigArgTys' con apps+          modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev+          subst <- gets ts_unifier+          names <- mkManyGoodNames (hyNamesInScope hy) args+          let hy' = patternHypothesis scrut con jdg+                  $ zip names+                  $ coerce args+              j = fmap (CType . substTyAddInScope subst . unCType)+                $ introduce hy'+                $ introduce method_hy+                $ withNewGoal g jdg+          ext <- f con j+          pure $ ext+            & #syn_trace %~ rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}")+                          . pure+            & #syn_scoped <>~ hy'+            & #syn_val     %~ match [mkDestructPat con names] . unLoc+++------------------------------------------------------------------------------+-- | Produces a pattern for a data con and the names of its fields.+mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs+mkDestructPat con names+  | RealDataCon dcon <- con+  , isTupleDataCon dcon =+      tuple pat_args+  | otherwise =+      infixifyPatIfNecessary con $+        conP+          (coerceName $ conLikeName con)+          pat_args+  where+    pat_args = fmap bvar' names+++infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs+infixifyPatIfNecessary dcon x+  | conLikeIsInfix dcon =+      case x of+        ConPatIn op (PrefixCon [lhs, rhs]) ->+          ConPatIn op $ InfixCon lhs rhs+        y -> y+  | otherwise = x++++unzipTrace :: [Synthesized a] -> Synthesized [a]+unzipTrace = sequenceA+++-- | 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.+conLikeInstOrigArgTys'+  :: ConLike+      -- ^ '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 ConLike with returned type is instantiated with the second argument.+conLikeInstOrigArgTys' con uniTys =+  let exvars = conLikeExTys con+   in conLikeInstOrigArgTys 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.+++conLikeExTys :: ConLike -> [TyCoVar]+conLikeExTys (RealDataCon d) = dataConExTys d+conLikeExTys (PatSynCon p) = patSynExTys p++patSynExTys :: PatSyn -> [TyCoVar]+patSynExTys ps = patSynExTyVars ps+++------------------------------------------------------------------------------+-- | Combinator for performing case splitting, and running sub-rules on the+-- resulting matches.++destruct' :: (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule+destruct' f hi jdg = do+  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic+  let term = hi_name hi+  ext+      <- destructMatches+           f+           (Just term)+           (hi_type hi)+           $ disallowing AlreadyDestructed (S.singleton term) jdg+  pure $ ext+    & #syn_trace     %~ rose ("destruct " <> show term) . pure+    & #syn_used_vals %~ S.insert term+    & #syn_val       %~ noLoc . case' (var' term)+++------------------------------------------------------------------------------+-- | Combinator for performign case splitting, and running sub-rules on the+-- resulting matches.+destructLambdaCase' :: (ConLike -> 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+    :: Bool       -- Should we blacklist destruct?+    -> Judgement+    -> ConLike            -- ^ The data con to build+    -> [Type]             -- ^ Type arguments for the data con+    -> RuleM (Synthesized (LHsExpr GhcPs))+buildDataCon should_blacklist jdg dc tyapps = do+  let args = conLikeInstOrigArgTys' dc tyapps+  ext+      <- fmap unzipTrace+       $ traverse ( \(arg, n) ->+                    newSubgoal+                  . filterSameTypeFromOtherPositions dc n+                  . bool id blacklistingDestruct should_blacklist+                  . flip withNewGoal jdg+                  $ CType arg+                  ) $ zip args [0..]+  pure $ ext+    & #syn_trace %~ rose (show dc) . pure+    & #syn_val   %~ mkCon dc tyapps+++------------------------------------------------------------------------------+-- | Make a function application, correctly handling the infix case.+mkApply :: OccName -> [HsExpr GhcPs] -> LHsExpr GhcPs+mkApply occ (lhs : rhs : more)+  | isSymOcc occ+  = noLoc $ foldl' (@@) (op lhs (coerceName occ) rhs) more+mkApply occ args = noLoc $ foldl' (@@) (var' occ) args+

@@ -0,0 +1,83 @@+module Wingman.CodeGen.Utils where++import ConLike (ConLike(RealDataCon), conLikeName)+import Data.List+import DataCon+import Development.IDE.GHC.Compat+import GHC.Exts+import GHC.SourceGen (RdrNameStr, recordConE, string)+import GHC.SourceGen.Overloaded+import GhcPlugins (nilDataCon, charTy, eqType)+import Name+import Wingman.GHC (getRecordFields)+++------------------------------------------------------------------------------+-- | Make a data constructor with the given arguments.+mkCon :: ConLike -> [Type] -> [LHsExpr GhcPs] -> LHsExpr GhcPs+mkCon con apps (fmap unLoc -> args)+  | RealDataCon dcon <- con+  , dcon == nilDataCon+  , [ty] <- apps+  , ty `eqType` charTy = noLoc $ string ""++  | RealDataCon dcon <- con+  , isTupleDataCon dcon =+      noLoc $ tuple args++  | RealDataCon dcon <- con+  , dataConIsInfix dcon+  , (lhs : rhs : args') <- args =+      noLoc $ foldl' (@@) (op lhs (coerceName con_name) rhs) args'++  | Just fields <- getRecordFields con+  , length fields >= 2 =  --  record notation is unnatural on single field ctors+      noLoc $ recordConE (coerceName con_name) $ do+        (arg, (field, _)) <- zip args fields+        pure (coerceName field, arg)++  | otherwise =+      noLoc $ foldl' (@@) (bvar' $ occName con_name) args+  where+    con_name = conLikeName con+++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,113 @@+module Wingman.Context where++import           Bag+import           Control.Arrow+import           Control.Monad.Reader+import           Data.Foldable.Extra (allM)+import           Data.Maybe (fromMaybe, isJust)+import qualified Data.Set as S+import           Development.IDE.GHC.Compat+import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)+import           InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)+import           OccName+import           TcRnTypes+import           TcType (tcSplitTyConApp, tcSplitPhiTy)+import           TysPrim (alphaTys)+import           Wingman.FeatureSet (FeatureSet)+import           Wingman.Judgements.Theta+import           Wingman.Types+++mkContext+    :: FeatureSet+    -> [(OccName, CType)]+    -> TcGblEnv+    -> ExternalPackageState+    -> KnownThings+    -> [Evidence]+    -> Context+mkContext features locals tcg eps kt ev = Context+  { ctxDefiningFuncs = locals+  , ctxModuleFuncs = fmap splitId+                   . (getFunBindId =<<)+                   . fmap unLoc+                   . bagToList+                   $ tcg_binds tcg+  , ctxFeatureSet = features+  , ctxInstEnvs =+      InstEnvs+        (eps_inst_env eps)+        (tcg_inst_env tcg)+        (tcVisibleOrphanMods tcg)+  , ctxKnownThings = kt+  , ctxTheta = evidenceToThetaType ev+  }+++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+++------------------------------------------------------------------------------+-- | Extract something from 'KnownThings'.+getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a+getKnownThing f = asks $ f . ctxKnownThings+++------------------------------------------------------------------------------+-- | Like 'getInstance', but uses a class from the 'KnownThings'.+getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))+getKnownInstance f tys = do+  cls <- getKnownThing f+  getInstance cls tys+++------------------------------------------------------------------------------+-- | Determine if there is an instance that exists for the given 'Class' at the+-- specified types. Deeply checks contexts to ensure the instance is actually+-- real.+--+-- If so, this returns a 'PredType' that corresponds to the type of the+-- dictionary.+getInstance :: MonadReader Context m => Class -> [Type] -> m (Maybe (Class, PredType))+getInstance cls tys = do+  env <- asks ctxInstEnvs+  let (mres, _, _) = lookupInstEnv False env cls tys+  case mres of+    ((inst, mapps) : _) -> do+      -- Get the instantiated type of the dictionary+      let df = piResultTys (idType $ is_dfun inst) $ zipWith fromMaybe alphaTys mapps+      -- pull off its resulting arguments+      let (theta, df') = tcSplitPhiTy df+      allM hasClassInstance theta >>= \case+        True -> pure $ Just (cls, df')+        False -> pure Nothing+    _ -> pure Nothing+++------------------------------------------------------------------------------+-- | Like 'getInstance', but only returns whether or not it succeeded. Can fail+-- fast, and uses a cached Theta from the context.+hasClassInstance :: MonadReader Context m => PredType -> m Bool+hasClassInstance predty = do+  theta <- asks ctxTheta+  case S.member (CType predty) theta of+    True -> pure True+    False -> do+      let (con, apps) = tcSplitTyConApp predty+      case tyConClass_maybe con of+        Nothing -> pure False+        Just cls -> fmap isJust $ getInstance cls apps+

@@ -0,0 +1,59 @@+{-# LANGUAGE BangPatterns     #-}+{-# LANGUAGE CPP              #-}+{-# LANGUAGE TypeApplications #-}++module Wingman.Debug+  ( unsafeRender+  , unsafeRender'+  , traceM+  , traceShowId+  , trace+  , traceX+  , traceIdX+  , traceMX+  , traceFX+  ) 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++traceFX :: String -> (a -> String) -> a -> a+traceFX str f a = trace (mappend ("!!!" <> str <> ": ") $ f a) a+

@@ -0,0 +1,94 @@+{-# LANGUAGE OverloadedStrings #-}++module Wingman.FeatureSet+  ( Feature (..)+  , FeatureSet+  , hasFeature+  , defaultFeatures+  , allFeatures+  , parseFeatureSet+  , prettyFeatureSet+  ) where++import           Data.List  (intercalate)+import           Data.Maybe (listToMaybe, mapMaybe)+import           Data.Set   (Set)+import qualified Data.Set   as S+import qualified Data.Text  as T+++------------------------------------------------------------------------------+-- | All the available features. A 'FeatureSet' describes the ones currently+-- available to the user.+data Feature+  = FeatureDestructAll+  | FeatureUseDataCon+  | FeatureRefineHole+  | FeatureKnownMonoid+  deriving (Eq, Ord, Show, Read, Enum, Bounded)+++------------------------------------------------------------------------------+-- | A collection of enabled features.+type FeatureSet = Set Feature+++------------------------------------------------------------------------------+-- | Parse a feature set.+parseFeatureSet :: T.Text -> FeatureSet+parseFeatureSet+  = mappend defaultFeatures+  . S.fromList+  . mapMaybe (readMaybe . mappend featurePrefix . rot13 . T.unpack)+  . T.split (== '/')+++------------------------------------------------------------------------------+-- | Features that are globally enabled for all users.+defaultFeatures :: FeatureSet+defaultFeatures = S.fromList+  [+  ]+++------------------------------------------------------------------------------+-- | All available features.+allFeatures :: FeatureSet+allFeatures = S.fromList $ enumFromTo minBound maxBound+++------------------------------------------------------------------------------+-- | Pretty print a feature set.+prettyFeatureSet :: FeatureSet -> String+prettyFeatureSet+  = intercalate "/"+  . fmap (rot13 . drop (length featurePrefix) . show)+  . S.toList+++------------------------------------------------------------------------------+-- | Is a given 'Feature' currently enabled?+hasFeature :: Feature -> FeatureSet -> Bool+hasFeature = S.member+++------------------------------------------------------------------------------+-- | Like 'read', but not partial.+readMaybe :: Read a => String -> Maybe a+readMaybe = fmap fst . listToMaybe . reads+++featurePrefix :: String+featurePrefix = "Feature"+++rot13 :: String -> String+rot13 = fmap (toEnum . rot13int . fromEnum)+++rot13int :: Integral a => a -> a+rot13int x+  | (fromIntegral x :: Word) - 97 < 26 = 97 + rem (x - 84) 26+  | (fromIntegral x :: Word) - 65 < 26 = 65 + rem (x - 52) 26+  | otherwise   = x+

@@ -0,0 +1,346 @@+{-# LANGUAGE CPP               #-}+{-# LANGUAGE OverloadedStrings #-}++module Wingman.GHC where++import           ConLike+import           Control.Applicative (empty)+import           Control.Monad.State+import           Control.Monad.Trans.Maybe (MaybeT(..))+import           Data.Function (on)+import           Data.Functor ((<&>))+import           Data.List (isPrefixOf)+import qualified Data.Map as M+import           Data.Maybe (isJust)+import           Data.Set (Set)+import qualified Data.Set as S+import           Data.Traversable+import           DataCon+import           Development.IDE (HscEnvEq (hscEnv))+import           Development.IDE.Core.Compile (lookupName)+import           Development.IDE.GHC.Compat+import           GHC.SourceGen (lambda)+import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)+import           GhcPlugins (extractModule, GlobalRdrElt (gre_name))+import           OccName+import           TcRnMonad+import           TcType+import           TyCoRep+import           Type+import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)+import           Unique+import           Var+import           Wingman.Types+++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+++------------------------------------------------------------------------------+-- | Get the data cons of a type, if it has any.+tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])+tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =+  splitTyConApp_maybe ty <&> \(tc, apps) ->+    ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc+    , apps+    )+tacticsGetDataCons _ = Nothing++------------------------------------------------------------------------------+-- | 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+++------------------------------------------------------------------------------+-- | Given a datacon, extract its record fields' names and types. Returns+-- nothing if the datacon is not a record.+getRecordFields :: ConLike -> Maybe [(OccName, CType)]+getRecordFields dc =+  case conLikeFieldLabels dc of+    [] -> Nothing+    lbls -> for lbls $ \lbl -> do+      let ty = conLikeFieldType dc $ flLabel lbl+      pure (mkVarOccFS $ flLabel lbl, CType ty)+++------------------------------------------------------------------------------+-- | 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+++------------------------------------------------------------------------------+-- | We can't compare 'RdrName' for equality directly. Instead, sloppily+-- compare them by their 'OccName's.+eqRdrName :: RdrName -> RdrName -> Bool+eqRdrName = (==) `on` occNameString . occName+++------------------------------------------------------------------------------+-- | Compare two 'OccName's for unqualified equality.+sloppyEqOccName :: OccName -> OccName -> Bool+sloppyEqOccName = (==) `on` occNameString+++------------------------------------------------------------------------------+-- | Does this thing contain any references to 'HsVar's with the given+-- 'RdrName'?+containsHsVar :: Data a => RdrName -> a -> Bool+containsHsVar name x = not $ null $ listify (+  \case+    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | eqRdrName a name -> True+    _                                                      -> False+  ) x+++------------------------------------------------------------------------------+-- | Does this thing contain any holes?+containsHole :: Data a => a -> Bool+containsHole x = not $ null $ listify (+  \case+    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name+    _                                      -> False+  ) x+++------------------------------------------------------------------------------+-- | Check if an 'OccName' is a hole+isHole :: OccName -> Bool+-- TODO(sandy): Make this more robust+isHole = isPrefixOf "_" . occNameString+++------------------------------------------------------------------------------+-- | Get all of the referenced occnames.+allOccNames :: Data a => a -> Set OccName+allOccNames = everything (<>) $ mkQ mempty $ \case+    a -> S.singleton a+++------------------------------------------------------------------------------+-- | Unpack the relevant parts of a 'Match'+pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)+pattern AMatch ctx pats body <-+  Match { m_ctxt = ctx+        , m_pats = fmap fromPatCompat -> pats+        , m_grhss = UnguardedRHSs (unLoc -> body)+        }+++------------------------------------------------------------------------------+-- | A pattern over the otherwise (extremely) messy AST for lambdas.+pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs+pattern Lambda pats body <-+  HsLam _+    (MG {mg_alts = L _ [L _ (AMatch _ pats body) ]})+  where+    -- If there are no patterns to bind, just stick in the body+    Lambda [] body   = body+    Lambda pats body = lambda pats body+++------------------------------------------------------------------------------+-- | A GRHS that caontains no guards.+pattern UnguardedRHSs :: LHsExpr p -> GRHSs p (LHsExpr p)+pattern UnguardedRHSs body <-+  GRHSs {grhssGRHSs = [L _ (GRHS _ [] body)]}+++------------------------------------------------------------------------------+-- | A match with a single pattern. Case matches are always 'SinglePatMatch'es.+pattern SinglePatMatch :: PatCompattable p => Pat p -> LHsExpr p -> Match p (LHsExpr p)+pattern SinglePatMatch pat body <-+  Match { m_pats = [fromPatCompat -> pat]+        , m_grhss = UnguardedRHSs body+        }+++------------------------------------------------------------------------------+-- | Helper function for defining the 'Case' pattern.+unpackMatches :: PatCompattable p => [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]+unpackMatches [] = Just []+unpackMatches (SinglePatMatch pat body : matches) =+  (:) <$> pure (pat, body) <*> unpackMatches matches+unpackMatches _ = Nothing+++------------------------------------------------------------------------------+-- | A pattern over the otherwise (extremely) messy AST for lambdas.+pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p+pattern Case scrutinee matches <-+  HsCase _ (L _ scrutinee)+    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})+++------------------------------------------------------------------------------+-- | 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++class PatCompattable p where+  fromPatCompat :: PatCompat p -> Pat p+  toPatCompat :: Pat p -> PatCompat p++#if __GLASGOW_HASKELL__ == 808+instance PatCompattable GhcTc where+  fromPatCompat = id+  toPatCompat = id++instance PatCompattable GhcPs where+  fromPatCompat = id+  toPatCompat = id++type PatCompat pass = Pat pass+#else+instance PatCompattable GhcTc where+  fromPatCompat = unLoc+  toPatCompat = noLoc++instance PatCompattable GhcPs where+  fromPatCompat = unLoc+  toPatCompat = noLoc++type PatCompat pass = LPat pass+#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)] _)+++dataConExTys :: DataCon -> [TyCoVar]+#if __GLASGOW_HASKELL__ >= 808+dataConExTys = DataCon.dataConExTyCoVars+#else+dataConExTys = DataCon.dataConExTyVars+#endif+++------------------------------------------------------------------------------+-- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'.+-- The nitty gritty details are explained at+-- https://blog.shaynefletcher.org/2020/03/ghc-haskell-pats-and-lpats.html+--+-- We need to remove these in order to succesfull find patterns.+unXPat :: Pat GhcPs -> Pat GhcPs+#if __GLASGOW_HASKELL__ == 808+unXPat (XPat (L _ pat)) = unXPat pat+#endif+unXPat pat              = pat+++------------------------------------------------------------------------------+-- | Build a 'KnownThings'.+knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings+knownThings tcg hscenv= do+  let cls = knownClass tcg hscenv+  KnownThings+    <$> cls (mkClsOcc "Semigroup")+    <*> cls (mkClsOcc "Monoid")+++------------------------------------------------------------------------------+-- | Like 'knownThing' but specialized to classes.+knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class+knownClass = knownThing $ \case+  ATyCon tc -> tyConClass_maybe tc+  _         -> Nothing+++------------------------------------------------------------------------------+-- | Helper function for defining 'knownThings'.+knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a+knownThing f tcg hscenv occ = do+  let modul = extractModule tcg+      rdrenv = tcg_rdr_env tcg++  case lookupOccEnv rdrenv occ of+    Nothing -> empty+    Just elts -> do+      mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts+      case mvar of+        Just tt -> liftMaybe $ f tt+        _ -> empty++liftMaybe :: Monad m => Maybe a -> MaybeT m a+liftMaybe a = MaybeT $ pure a+

@@ -0,0 +1,429 @@+module Wingman.Judgements where++import           ConLike (ConLike)+import           Control.Arrow+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           Development.IDE.Core.UseStale (Tracked, unTrack)+import           Development.IDE.Spans.LocalBindings+import           OccName+import           SrcLoc+import           Type+import           Wingman.GHC (algebraicTyCon)+import           Wingman.Types+++------------------------------------------------------------------------------+-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.+hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType+hypothesisFromBindings (unTrack -> span) (unTrack -> bs) = buildHypothesis $ getLocalScope bs span+++------------------------------------------------------------------------------+-- | Convert a @Set Id@ into a hypothesis.+buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType+buildHypothesis+  = Hypothesis+  . mapMaybe go+  where+    go (occName -> occ, t)+      | Just ty <- t+      , isAlpha . head . occNameString $ occ = Just $ HyInfo occ 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+++introduce :: Hypothesis a -> Judgement' a -> Judgement' a+-- NOTE(sandy): It's important that we put the new hypothesis terms first,+-- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs+-- after a previously-destructed term.+introduce hy = field @"_jHypothesis" %~ mappend hy+++------------------------------------------------------------------------------+-- | Helper function for implementing functions which introduce new hypotheses.+introduceHypothesis+    :: (Int -> Int -> Provenance)+        -- ^ A function from the total number of args and position of this arg+        -- to its provenance.+    -> [(OccName, a)]+    -> Hypothesis a+introduceHypothesis f ns =+  Hypothesis $ zip [0..] ns <&> \(pos, (name, ty)) ->+    HyInfo name (f (length ns) pos) ty+++------------------------------------------------------------------------------+-- | Introduce bindings in the context of a lamba.+lambdaHypothesis+    :: Maybe OccName   -- ^ The name of the top level function. For any other+                       -- function, this should be 'Nothing'.+    -> [(OccName, a)]+    -> Hypothesis a+lambdaHypothesis func =+  introduceHypothesis $ \count pos ->+    maybe UserPrv (\x -> TopLevelArgPrv x pos count) func+++------------------------------------------------------------------------------+-- | Introduce a binding in a recursive context.+recursiveHypothesis :: [(OccName, a)] -> Hypothesis a+recursiveHypothesis = introduceHypothesis $ const $ 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.keysSet $ M.filterWithKey go $ hyByName $ 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)+              $ hyByName+              $ 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 -> ConLike -> Int -> [OccName]+findDconPositionVals jdg dcon pos = do+  (name, hi) <- M.toList $ hyByName $ 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 :: ConLike -> Int -> Judgement -> Judgement+filterSameTypeFromOtherPositions dcon pos jdg =+  let hy = hyByName+         . 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) (hyByName $ jHypothesis jdg)+          M.\\ hy+   in disallowing Shadowed (M.keysSet 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+++provAncestryOf :: Provenance -> Set OccName+provAncestryOf (TopLevelArgPrv o _ _) = S.singleton o+provAncestryOf (PatternMatchPrv (PatVal mo so _ _)) =+  maybe mempty S.singleton mo <> so+provAncestryOf (ClassMethodPrv _) = mempty+provAncestryOf UserPrv = mempty+provAncestryOf RecursivePrv = mempty+provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2+++------------------------------------------------------------------------------+-- 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+++patternHypothesis+    :: Maybe OccName+    -> ConLike+    -> Judgement' a+    -> [(OccName, a)]+    -> Hypothesis a+patternHypothesis scrutinee dc jdg+  = introduceHypothesis $ \_ pos ->+      PatternMatchPrv $+        PatVal+          scrutinee+          (maybe+              mempty+              (\scrut -> S.singleton scrut <> getAncestry jdg scrut)+              scrutinee)+          (Uniquely dc)+          pos+++------------------------------------------------------------------------------+-- | Prevent some occnames from being used in the hypothesis. This will hide+-- them from 'jHypothesis', but not from 'jEntireHypothesis'.+disallowing :: DisallowReason -> S.Set OccName -> Judgement' a -> Judgement' a+disallowing reason ns =+  field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->+    case S.member (hi_name hi) 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 -> Hypothesis a+jHypothesis+  = Hypothesis+  . filter (not . isDisallowed . hi_provenance)+  . unHypothesis+  . jEntireHypothesis+++------------------------------------------------------------------------------+-- | The whole hypothesis, including things disallowed.+jEntireHypothesis :: Judgement' a -> Hypothesis a+jEntireHypothesis = _jHypothesis+++------------------------------------------------------------------------------+-- | Just the local hypothesis.+jLocalHypothesis :: Judgement' a -> Hypothesis a+jLocalHypothesis+  = Hypothesis+  . filter (isLocalHypothesis . hi_provenance)+  . unHypothesis+  . jHypothesis+++------------------------------------------------------------------------------+-- | Given a judgment, return the hypotheses that are acceptable to destruct.+--+-- We use the ordering of the hypothesis for this purpose. Since new bindings+-- are always inserted at the beginning, we can impose a canonical ordering on+-- which order to try destructs by what order they are introduced --- stopping+-- at the first one we've already destructed.+jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType]+jAcceptableDestructTargets+  = filter (isJust . algebraicTyCon . unCType . hi_type)+  . takeWhile (not . isAlreadyDestructed . hi_provenance)+  . unHypothesis+  . jEntireHypothesis+++------------------------------------------------------------------------------+-- | 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+++------------------------------------------------------------------------------+-- | What names are currently in scope in the hypothesis?+hyNamesInScope :: Hypothesis a -> Set OccName+hyNamesInScope = M.keysSet . hyByName+++------------------------------------------------------------------------------+-- | Are there any top-level function argument bindings in this judgement?+jHasBoundArgs :: Judgement' a -> Bool+jHasBoundArgs+  = not+  . null+  . filter (isTopLevel . hi_provenance)+  . unHypothesis+  . jLocalHypothesis+++------------------------------------------------------------------------------+-- | Fold a hypothesis into a single mapping from name to info. This+-- unavoidably will cause duplicate names (things like methods) to shadow one+-- another.+hyByName :: Hypothesis a -> Map OccName (HyInfo a)+hyByName+  = M.fromList+  . fmap (hi_name &&& id)+  . unHypothesis+++------------------------------------------------------------------------------+-- | Only the hypothesis members which are pattern vals+jPatHypothesis :: Judgement' a -> Map OccName PatVal+jPatHypothesis+  = M.mapMaybe (getPatVal . hi_provenance)+  . hyByName+  . 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+    :: Hypothesis 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++------------------------------------------------------------------------------+-- | Has this term already been disallowed?+isAlreadyDestructed :: Provenance -> Bool+isAlreadyDestructed (DisallowedPrv AlreadyDestructed _) = True+isAlreadyDestructed _ = False+++------------------------------------------------------------------------------+-- | Eliminates 'DisallowedPrv' provenances.+expandDisallowed :: Provenance -> Provenance+expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv+expandDisallowed prv                   = prv

@@ -0,0 +1,83 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE RankNTypes          #-}++-- | Custom SYB traversals+module Wingman.Judgements.SYB where++import Data.Foldable (foldl')+import Data.Generics hiding (typeRep)+import Development.IDE.GHC.Compat+import GHC.Exts (Any)+import Type.Reflection+import Unsafe.Coerce (unsafeCoerce)+++------------------------------------------------------------------------------+-- | Like 'everything', but only looks inside 'Located' terms that contain the+-- given 'SrcSpan'.+everythingContaining+    :: forall r+     . Monoid r+    => SrcSpan+    -> GenericQ r+    -> GenericQ r+everythingContaining dst f = go+  where+    go :: GenericQ r+    go x =+      case genericIsSubspan dst x of+        Just False -> mempty+        _ -> foldl' (<>) (f x) (gmapQ go x)+++------------------------------------------------------------------------------+-- | Helper function for implementing 'everythingWithin'+--+-- NOTE(sandy): Subtly broken. In an ideal world, this function shuld return+-- @Just False@ for nodes of /any type/ which do not contain the span. But if+-- this functionality exists anywhere within the SYB machinery, I have yet to+-- find it.+genericIsSubspan+    :: SrcSpan+    -> GenericQ (Maybe Bool)+genericIsSubspan dst = mkQ1 (L noSrcSpan ()) Nothing $ \case+  L span _ -> Just $ dst `isSubspanOf` span+++------------------------------------------------------------------------------+-- | Like 'mkQ', but allows for polymorphic instantiation of its specific case.+-- This instantation matches whenever the dynamic value has the same+-- constructor as the proxy @f ()@ value.+mkQ1 :: forall a r f+      . (Data a, Data (f ()))+     => f ()                  -- ^ Polymorphic constructor to match on+     -> r                     -- ^ Default value+     -> (forall b. f b -> r)  -- ^ Polymorphic match+     -> a+     -> r+mkQ1 proxy r br a =+    case l_con == a_con && sameTypeModuloLastApp @a @(f ()) of+      -- We have proven that the two values share the same constructor, and+      -- that they have the same type if you ignore the final application.+      -- Therefore, it is safe to coerce @a@ to @f b@, since @br@ is universal+      -- over @b@ and can't inspect it.+      True  -> br $ unsafeCoerce @_ @(f Any) a+      False -> r+  where+    l_con = toConstr proxy+    a_con = toConstr a+++------------------------------------------------------------------------------+-- | Given @a ~ f1 a1@ and @b ~ f2 b2@, returns true if @f1 ~ f2@.+sameTypeModuloLastApp :: forall a b. (Typeable a, Typeable b) => Bool+sameTypeModuloLastApp =+  let tyrep1 = typeRep @a+      tyrep2 = typeRep @b+   in case (tyrep1 , tyrep2) of+        (App a _, App b _) ->+          case eqTypeRep a b of+            Just HRefl -> True+            Nothing    -> False+        _ -> False+

@@ -0,0 +1,188 @@+{-# LANGUAGE CPP          #-}+{-# LANGUAGE ViewPatterns #-}++module Wingman.Judgements.Theta+  ( Evidence+  , getEvidenceAtHole+  , mkEvidence+  , evidenceToSubst+  , evidenceToHypothesis+  , evidenceToThetaType+  ) where++import           Class (classTyVars)+import           Control.Applicative (empty)+import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)+import           Data.Set (Set)+import qualified Data.Set as S+import           Development.IDE.Core.UseStale+import           Development.IDE.GHC.Compat+import           Generics.SYB hiding (tyConName, empty)+import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)+#if __GLASGOW_HASKELL__ > 806+import           GhcPlugins (eqTyCon)+#else+import           GhcPlugins (nameRdrName, tyConName)+import           PrelNames (eqTyCon_RDR)+#endif+import           TcEvidence+import           TcType (substTy)+import           TcType (tcTyConAppTyCon_maybe)+import           TysPrim (eqPrimTyCon)+import           Wingman.Machinery+import           Wingman.Types+++------------------------------------------------------------------------------+-- | Something we've learned about the type environment.+data Evidence+    -- | The two types are equal, via a @a ~ b@ relationship+  = EqualityOfTypes Type Type+    -- | We have an instance in scope+  | HasInstance PredType+  deriving (Show)+++------------------------------------------------------------------------------+-- | Given a 'PredType', pull an 'Evidence' out of it.+mkEvidence :: PredType -> [Evidence]+mkEvidence (getEqualityTheta -> Just (a, b))+  = pure $ EqualityOfTypes a b+mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (tyConClass_maybe -> Just cls)) = do+  (_, apps) <- maybeToList $ splitTyConApp_maybe inst+  let tvs     = classTyVars cls+      subst   = zipTvSubst tvs apps+  sc_ev <- traverse (mkEvidence . substTy subst) $ classSCTheta cls+  HasInstance inst : sc_ev+mkEvidence _ = empty+++------------------------------------------------------------------------------+-- | Build a set of 'PredType's from the evidence.+evidenceToThetaType :: [Evidence] -> Set CType+evidenceToThetaType evs = S.fromList $ do+  HasInstance t <- evs+  pure $ CType t+++------------------------------------------------------------------------------+-- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.+getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]+getEvidenceAtHole (unTrack -> dst)+  = concatMap mkEvidence+  . (everything (<>) $+        mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)+  . unTrack+++------------------------------------------------------------------------------+-- | Update our knowledge of which types are equal.+evidenceToSubst :: Evidence -> TacticState -> TacticState+evidenceToSubst (EqualityOfTypes a b) ts =+  let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b]+      -- If we can unify our skolems, at least one is no longer a skolem.+      -- Removing them from this set ensures we can get a subtitution between+      -- the two. But it's okay to leave them in 'ts_skolems' in general, since+      -- they won't exist after running this substitution.+      skolems = ts_skolems ts S.\\ tyvars+   in+  case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of+    Just subst -> updateSubst subst ts+    Nothing -> ts+evidenceToSubst HasInstance{} ts = ts+++------------------------------------------------------------------------------+-- | Get all of the methods that are in scope from this piece of 'Evidence'.+evidenceToHypothesis :: Evidence -> Hypothesis CType+evidenceToHypothesis EqualityOfTypes{} = mempty+evidenceToHypothesis (HasInstance t) =+  Hypothesis . excludeForbiddenMethods . fromMaybe [] $ methodHypothesis t+++------------------------------------------------------------------------------+-- | Given @a ~ b@ or @a ~# b@, returns @Just (a, b)@, otherwise @Nothing@.+getEqualityTheta :: PredType -> Maybe (Type, Type)+getEqualityTheta (splitTyConApp_maybe -> Just (tc, [_k, a, b]))+#if __GLASGOW_HASKELL__ > 806+  | tc == eqTyCon+#else+  | nameRdrName (tyConName tc) == eqTyCon_RDR+#endif+  = Just (a, b)+getEqualityTheta (splitTyConApp_maybe -> Just (tc, [_k1, _k2, a, b]))+  | tc == eqPrimTyCon = Just (a, b)+getEqualityTheta _ = Nothing+++------------------------------------------------------------------------------+-- | 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 :: [HyInfo a] -> [HyInfo a]+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)+  where+    forbiddenMethods :: Set OccName+    forbiddenMethods = S.map mkVarOcc $ S.fromList+      [ -- monadfail+        "fail"+        -- show+      , "showsPrec", "showList"+        -- functor+      , "<$"+        -- applicative+      , "liftA2", "<*", "*>"+        -- monad+      , "return", ">>"+        -- alternative+      , "some", "many"+        -- foldable+      , "foldr1", "foldl1", "elem", "maximum", "minimum", "sum", "product"+        -- traversable+      , "sequenceA", "mapM", "sequence"+        -- semigroup+      , "sconcat", "stimes"+        -- monoid+      , "mconcat"+      ]+++------------------------------------------------------------------------------+-- | Extract evidence from 'AbsBinds' in scope.+absBinds ::  SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]+absBinds dst (L src (AbsBinds _ _ h _ _ _ _))+  | dst `isSubspanOf` src = fmap idType h+absBinds _ _ = []+++------------------------------------------------------------------------------+-- | Extract evidence from 'HsWrapper's in scope+wrapperBinds ::  SrcSpan -> LHsExpr GhcTc -> [PredType]+wrapperBinds dst (L src (HsWrap _ h _))+  | dst `isSubspanOf` src = wrapper h+wrapperBinds _ _ = []+++------------------------------------------------------------------------------+-- | Extract evidence from the 'ConPatOut's bound in this 'Match'.+matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]+matchBinds dst (L src (Match _ _ pats _))+  | dst `isSubspanOf` src = everything (<>) (mkQ mempty patBinds) pats+matchBinds _ _ = []+++------------------------------------------------------------------------------+-- | Extract evidence from a 'ConPatOut'.+patBinds ::  Pat GhcTc -> [PredType]+patBinds (ConPatOut { pat_dicts = dicts })+  = fmap idType dicts+patBinds _ = []+++------------------------------------------------------------------------------+-- | Extract the types of the evidence bindings in scope.+wrapper ::  HsWrapper -> [PredType]+wrapper (WpCompose h h2) = wrapper h <> wrapper h2+wrapper (WpEvLam v) = [idType v]+wrapper _ = []+

@@ -0,0 +1,97 @@+module Wingman.KnownStrategies where++import Control.Monad.Error.Class+import OccName (mkVarOcc)+import Refinery.Tactic+import Wingman.Context (getCurrentDefinitions, getKnownInstance)+import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)+import Wingman.Machinery (tracing)+import Wingman.Tactics+import Wingman.Types+import Wingman.Judgements (jGoal)+import Data.Foldable (for_)+import Wingman.FeatureSet+import Control.Applicative (empty)+import Control.Monad.Reader.Class (asks)+++knownStrategies :: TacticsM ()+knownStrategies = choice+  [ known "fmap" deriveFmap+  , known "mempty" deriveMempty+  , known "arbitrary" deriveArbitrary+  , featureGuard FeatureKnownMonoid $ known "<>" deriveMappend+  , featureGuard FeatureKnownMonoid $ known "mappend" deriveMappend+  ]+++------------------------------------------------------------------------------+-- | Guard a tactic behind a feature.+featureGuard :: Feature -> TacticsM a -> TacticsM a+featureGuard feat t = do+  fs <- asks ctxFeatureSet+  case hasFeature feat fs of+    True -> t+    False -> empty+++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+    ]+++------------------------------------------------------------------------------+-- | We derive mappend by binding the arguments, introducing the constructor,+-- and then calling mappend recursively. At each recursive call, we filter away+-- any binding that isn't in an analogous position.+--+-- The recursive call first attempts to use an instace in scope. If that fails,+-- it fals back to trying a theta method from the hypothesis with the correct+-- name.+deriveMappend :: TacticsM ()+deriveMappend = do+  try intros+  destructAll+  split+  g <- goal+  minst <- getKnownInstance kt_semigroup+         . pure+         . unCType+         $ jGoal g+  for_ minst $ \(cls, df) -> do+    restrictPositionForApplication+      (applyMethod cls df $ mkVarOcc "<>")+      assumption+  try $+    restrictPositionForApplication+      (applyByName $ mkVarOcc "<>")+      assumption+++------------------------------------------------------------------------------+-- | We derive mempty by introducing the constructor, and then trying to+-- 'mempty' everywhere. This smaller 'mempty' might come from an instance in+-- scope, or it might come from the hypothesis theta.+deriveMempty :: TacticsM ()+deriveMempty = do+  split+  g <- goal+  minst <- getKnownInstance kt_monoid [unCType $ jGoal g]+  for_ minst $ \(cls, df) -> do+    applyMethod cls df $ mkVarOcc "mempty"+  try assumption+

@@ -0,0 +1,114 @@+module Wingman.KnownStrategies.QuickCheck where++import ConLike (ConLike(RealDataCon))+import Control.Monad.Except (MonadError (throwError))+import Data.Bool (bool)+import Data.Generics (everything, mkQ)+import Data.List (partition)+import DataCon (DataCon, dataConName)+import Development.IDE.GHC.Compat (GhcPs, HsExpr, 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 OccName (HasOccName (occName), mkVarOcc, occNameString)+import Refinery.Tactic (goal, rule)+import TyCon (TyCon, tyConDataCons, tyConName)+import Type (splitTyConApp_maybe)+import Wingman.CodeGen+import Wingman.Judgements (jGoal)+import Wingman.Machinery (tracePrim)+import Wingman.Types+++------------------------------------------------------------------------------+-- | 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+          $ Synthesized (tracePrim "deriveArbitrary")+              -- TODO(sandy): This thing is not actually empty! We produced+              -- a bespoke binding "terminal", and a not-so-bespoke "n".+              -- But maybe it's fine for known rules?+              mempty+              mempty+              mempty+          $ 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 = conLikeInstOrigArgTys' (RealDataCon 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,516 @@+{-# LANGUAGE CPP               #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies      #-}++module Wingman.LanguageServer where++import           ConLike+import           Control.Arrow+import           Control.Monad+import           Control.Monad.State (State, get, put, evalState)+import           Control.Monad.Trans.Maybe+import           Data.Coerce+import           Data.Functor ((<&>))+import           Data.Generics.Aliases (mkQ)+import           Data.Generics.Schemes (everything)+import qualified Data.HashMap.Strict as Map+import           Data.IORef (readIORef)+import qualified Data.Map as M+import           Data.Maybe+import           Data.Monoid+import           Data.Set (Set)+import qualified Data.Set as S+import qualified Data.Text as T+import           Data.Traversable+import           Development.IDE (getFilesOfInterest, ShowDiagnostic (ShowDiag), srcSpanToRange)+import           Development.IDE (hscEnv)+import           Development.IDE.Core.RuleTypes+import           Development.IDE.Core.Rules (usePropertyAction)+import           Development.IDE.Core.Service (runAction)+import           Development.IDE.Core.Shake (IdeState (..), uses, define, use)+import qualified Development.IDE.Core.Shake as IDE+import           Development.IDE.Core.UseStale+import           Development.IDE.GHC.Compat+import           Development.IDE.GHC.Error (realSrcSpanToRange)+import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)+import           Development.Shake (Action, RuleResult, Rules, action)+import           Development.Shake.Classes (Typeable, Binary, Hashable, NFData)+import qualified FastString+import           GHC.Generics (Generic)+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)+import qualified Ide.Plugin.Config as Plugin+import           Ide.Plugin.Properties+import           Ide.PluginUtils (usePropertyLsp)+import           Ide.Types (PluginId)+import           Language.LSP.Server (MonadLsp, sendNotification)+import           Language.LSP.Types+import           OccName+import           Prelude hiding (span)+import           SrcLoc (containsSpan)+import           TcRnTypes (tcg_binds, TcGblEnv)+import           Wingman.Context+import           Wingman.FeatureSet+import           Wingman.GHC+import           Wingman.Judgements+import           Wingman.Judgements.SYB (everythingContaining)+import           Wingman.Judgements.Theta+import           Wingman.Range+import           Wingman.Types+++tacticDesc :: T.Text -> T.Text+tacticDesc name = "fill the hole using the " <> name <> " tactic"+++------------------------------------------------------------------------------+-- | The name of the command for the LS.+tcCommandName :: TacticCommand -> T.Text+tcCommandName = T.pack . show+++runIde :: IdeState -> Action a -> IO a+runIde state = runAction "tactic" state+++runCurrentIde+    :: forall a r+     . ( r ~ RuleResult a+       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a+       , Show r, Typeable r, NFData r+       )+    => IdeState+    -> NormalizedFilePath+    -> a+    -> MaybeT IO (Tracked 'Current r)+runCurrentIde state nfp a = MaybeT $ fmap (fmap unsafeMkCurrent) $ runIde state $ use a nfp+++runStaleIde+    :: forall a r+     . ( r ~ RuleResult a+       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a+       , Show r, Typeable r, NFData r+       )+    => IdeState+    -> NormalizedFilePath+    -> a+    -> MaybeT IO (TrackedStale r)+runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp+++unsafeRunStaleIde+    :: forall a r+     . ( r ~ RuleResult a+       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a+       , Show r, Typeable r, NFData r+       )+    => IdeState+    -> NormalizedFilePath+    -> a+    -> MaybeT IO r+unsafeRunStaleIde state nfp a = do+  (r, _) <- MaybeT $ runIde state $ IDE.useWithStale a nfp+  pure r+++------------------------------------------------------------------------------++properties :: Properties+  '[ 'PropertyKey "hole_severity" ('TEnum (Maybe DiagnosticSeverity))+   , 'PropertyKey "max_use_ctor_actions" 'TInteger+   , 'PropertyKey "features" 'TString+   , 'PropertyKey "timeout_duration" 'TInteger+   ]+properties = emptyProperties+  & defineIntegerProperty #timeout_duration+    "The timeout for Wingman actions, in seconds" 2+  & defineStringProperty #features+    "Feature set used by Wingman" ""+  & defineIntegerProperty #max_use_ctor_actions+    "Maximum number of `Use constructor <x>` code actions that can appear" 5+  & defineEnumProperty #hole_severity+    "The severity to use when showing hole diagnostics. These are noisy, but some editors don't allow jumping to all severities."+    [ (Just DsError,   "error")+    , (Just DsWarning, "warning")+    , (Just DsInfo,    "info")+    , (Just DsHint,    "hint")+    , (Nothing,        "none")+    ]+    Nothing+++-- | Get the the plugin config+getTacticConfig :: MonadLsp Plugin.Config m => PluginId -> m Config+getTacticConfig pId =+  Config+    <$> (parseFeatureSet <$> usePropertyLsp #features pId properties)+    <*> usePropertyLsp #max_use_ctor_actions pId properties+    <*> usePropertyLsp #timeout_duration pId properties++------------------------------------------------------------------------------+-- | Get the current feature set from the plugin config.+getFeatureSet :: MonadLsp Plugin.Config m => PluginId -> m FeatureSet+getFeatureSet  = fmap cfg_feature_set . getTacticConfig+++getIdeDynflags+    :: IdeState+    -> NormalizedFilePath+    -> MaybeT IO DynFlags+getIdeDynflags state nfp = do+  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'+  -- which don't change very often.+  msr <- unsafeRunStaleIde state nfp GetModSummaryWithoutTimestamps+  pure $ ms_hspp_opts $ msrModSummary msr+++------------------------------------------------------------------------------+-- | Find the last typechecked module, and find the most specific span, as well+-- as the judgement at the given range.+judgementForHole+    :: IdeState+    -> NormalizedFilePath+    -> Tracked 'Current Range+    -> FeatureSet+    -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)+judgementForHole state nfp range features = do+  TrackedStale asts amapping  <- runStaleIde state nfp GetHieAst+  case unTrack asts of+    HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"+    HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do+      range' <- liftMaybe $ mapAgeFrom amapping range+      binds <- runStaleIde state nfp GetBindings+      tcg <- fmap (fmap tmrTypechecked)+           $ runStaleIde state nfp TypeCheck+      hscenv <- runStaleIde state nfp GhcSessionDeps++      (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf+      new_rss <- liftMaybe $ mapAgeTo amapping rss++      -- KnownThings is just the instances in scope. There are no ranges+      -- involved, so it's not crucial to track ages.+      let henv = untrackedStaleValue $ hscenv+      eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv+      kt <- knownThings (untrackedStaleValue tcg) henv++      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt++      dflags <- getIdeDynflags state nfp+      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)+++mkJudgementAndContext+    :: FeatureSet+    -> Type+    -> TrackedStale Bindings+    -> Tracked 'Current RealSrcSpan+    -> TrackedStale TcGblEnv+    -> ExternalPackageState+    -> KnownThings+    -> Maybe (Judgement, Context)+mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do+  binds_rss <- mapAgeFrom bmap rss+  tcg_rss <- mapAgeFrom tcgmap rss++  let tcs = fmap tcg_binds tcg+      ctx = mkContext features+              (mapMaybe (sequenceA . (occName *** coerce))+                $ unTrack+                $ getDefiningBindings <$> binds <*> binds_rss)+              (unTrack tcg)+              eps+              kt+              evidence+      top_provs = getRhsPosVals tcg_rss tcs+      already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs+      local_hy = spliceProvenance top_provs+               $ hypothesisFromBindings binds_rss binds+      evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs+      cls_hy = foldMap evidenceToHypothesis evidence+      subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState+  pure $+    ( disallowing AlreadyDestructed already_destructed+    $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement+          (local_hy <> cls_hy)+          (isRhsHole tcg_rss tcs)+          g+    , ctx+    )+++------------------------------------------------------------------------------+-- | Determine which bindings have already been destructed by the location of+-- the hole.+getAlreadyDestructed+    :: Tracked age SrcSpan+    -> Tracked age (LHsBinds GhcTc)+    -> Set OccName+getAlreadyDestructed (unTrack -> span) (unTrack -> binds) =+  everythingContaining span+    (mkQ mempty $ \case+      Case (HsVar _ (L _ (occName -> var))) _ ->+        S.singleton var+      (_ :: HsExpr GhcTc) -> mempty+    ) binds+++getSpanAndTypeAtHole+    :: Tracked age Range+    -> Tracked age (HieASTs b)+    -> Maybe (Tracked age RealSrcSpan, b)+getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do+  join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \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+        -- Ensure we're actually looking at a hole here+        guard $ all (either (const False) $ isHole . occName)+          $ M.keysSet $ nodeIdentifiers info+        pure (unsafeCopyAge r $ nodeSpan ast', ty)++++------------------------------------------------------------------------------+-- | Combine two (possibly-overlapping) hypotheses; using the provenance from+-- the first hypothesis if the bindings overlap.+spliceProvenance+    :: Hypothesis a  -- ^ Bindings to keep+    -> Hypothesis a  -- ^ Bindings to keep if they don't overlap with the first set+    -> Hypothesis a+spliceProvenance top x =+  let bound = S.fromList $ fmap hi_name $ unHypothesis top+   in mappend top $ Hypothesis . filter (flip S.notMember bound . hi_name) $ unHypothesis x+++------------------------------------------------------------------------------+-- | Compute top-level position vals of a function+getRhsPosVals+    :: Tracked age RealSrcSpan+    -> Tracked age TypecheckedSource+    -> Hypothesis CType+getRhsPosVals (unTrack -> rss) (unTrack -> tcs)+  = 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+        -> flip evalState 0 $ buildTopLevelHypothesis name ps+      _ -> mempty+  ) tcs+++------------------------------------------------------------------------------+-- | Construct a hypothesis given the patterns from the left side of a HsMatch.+-- These correspond to things that the user put in scope before running+-- tactics.+buildTopLevelHypothesis+    :: OccName  -- ^ Function name+    -> [PatCompat GhcTc]+    -> State Int (Hypothesis CType)+buildTopLevelHypothesis name ps = do+  fmap mconcat $+    for (zip [0..] ps) $ \(ix, p) ->+      buildPatHy (TopLevelArgPrv name ix $ length ps) p+++------------------------------------------------------------------------------+-- | Construct a hypothesis for a single pattern, including building+-- sub-hypotheses for constructor pattern matches.+buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)+buildPatHy prov (fromPatCompat -> p0) =+  case p0 of+    VarPat  _ x   -> pure $ mkIdHypothesis (unLoc x) prov+    LazyPat _ p   -> buildPatHy prov p+    AsPat   _ x p -> do+      hy' <- buildPatHy prov p+      pure $ mkIdHypothesis (unLoc x) prov <> hy'+    ParPat  _ p   -> buildPatHy prov p+    BangPat _ p   -> buildPatHy prov p+    ViewPat _ _ p -> buildPatHy prov p+    -- Desugar lists into cons+    ListPat _ [] -> pure mempty+    ListPat x@(ListPatTc ty _) (p : ps) ->+      mkDerivedConHypothesis prov (RealDataCon consDataCon) [ty]+        [ (0, p)+        , (1, toPatCompat $ ListPat x ps)+        ]+    -- Desugar tuples into an explicit constructor+    TuplePat tys pats boxity ->+      mkDerivedConHypothesis+        prov+        (RealDataCon $ tupleDataCon boxity $ length pats)+        tys+          $ zip [0.. ] pats+    ConPatOut (L _ con) args _ _ _ f _ ->+      case f of+        PrefixCon l_pgt ->+          mkDerivedConHypothesis prov con args $ zip [0..] l_pgt+        InfixCon pgt pgt5 ->+          mkDerivedConHypothesis prov con args $ zip [0..] [pgt, pgt5]+        RecCon r ->+          mkDerivedRecordHypothesis prov con args r+#if __GLASGOW_HASKELL__ >= 808+    SigPat  _ p _ -> buildPatHy prov p+#endif+#if __GLASGOW_HASKELL__ == 808+    XPat   p      -> buildPatHy prov $ unLoc p+#endif+    _             -> pure mempty+++------------------------------------------------------------------------------+-- | Like 'mkDerivedConHypothesis', but for record patterns.+mkDerivedRecordHypothesis+    :: Provenance+    -> ConLike  -- ^ Destructing constructor+    -> [Type]   -- ^ Applied type variables+    -> HsRecFields GhcTc (PatCompat GhcTc)+    -> State Int (Hypothesis CType)+mkDerivedRecordHypothesis prov dc args (HsRecFields (fmap unLoc -> fs) _)+  | Just rec_fields <- getRecordFields dc+  = do+    let field_lookup = M.fromList $ zip (fmap (occNameFS . fst) rec_fields) [0..]+    mkDerivedConHypothesis prov dc args $ fs <&> \(HsRecField (L _ rec_occ) p _) ->+      ( field_lookup M.! (occNameFS $ occName $ unLoc $ rdrNameFieldOcc rec_occ)+      , p+      )+mkDerivedRecordHypothesis _ _ _ _ =+  error "impossible! using record pattern on something that isn't a record"+++------------------------------------------------------------------------------+-- | Construct a fake variable name. Used to track the provenance of top-level+-- pattern matches which otherwise wouldn't have anything to attach their+-- 'TopLevelArgPrv' to.+mkFakeVar :: State Int OccName+mkFakeVar = do+  i <- get+  put $ i + 1+  pure $ mkVarOcc $ "_" <> show i+++------------------------------------------------------------------------------+-- | Construct a fake varible to attach the current 'Provenance' to, and then+-- build a sub-hypothesis for the pattern match.+mkDerivedConHypothesis+    :: Provenance+    -> ConLike                   -- ^ Destructing constructor+    -> [Type]                    -- ^ Applied type variables+    -> [(Int, PatCompat GhcTc)]  -- ^ Patterns, and their order in the data con+    -> State Int (Hypothesis CType)+mkDerivedConHypothesis prov dc args ps = do+  var <- mkFakeVar+  hy' <- fmap mconcat $+    for ps $ \(ix, p) -> do+      let prov' = PatternMatchPrv+               $ PatVal (Just var)+                        (S.singleton var <> provAncestryOf prov)+                        (Uniquely dc)+                        ix+      buildPatHy prov' p+  pure+    $ mappend hy'+    $ Hypothesis+    $ pure+    $ HyInfo var (DisallowedPrv AlreadyDestructed prov)+    $ CType+    -- TODO(sandy): This is the completely wrong type, but we don't have a good+    -- way to get the real one. It's probably OK though, since we're generating+    -- this term with a disallowed provenance, and it doesn't actually exist+    -- anyway.+    $ conLikeResTy dc args+++------------------------------------------------------------------------------+-- | Build a 'Hypothesis' given an 'Id'.+mkIdHypothesis :: Id -> Provenance -> Hypothesis CType+mkIdHypothesis (splitId -> (name, ty)) prov =+  Hypothesis $ pure $ HyInfo name prov ty+++------------------------------------------------------------------------------+-- | Is this hole immediately to the right of an equals sign?+isRhsHole :: Tracked age RealSrcSpan -> Tracked age TypecheckedSource -> Bool+isRhsHole (unTrack -> rss) (unTrack -> tcs) =+  everything (||) (mkQ False $ \case+      TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span+      _                                        -> False+    ) tcs+++ufmSeverity :: UserFacingMessage -> MessageType+ufmSeverity TacticErrors            = MtError+ufmSeverity TimedOut                = MtInfo+ufmSeverity NothingToDo             = MtInfo+ufmSeverity (InfrastructureError _) = MtError+++mkShowMessageParams :: UserFacingMessage -> ShowMessageParams+mkShowMessageParams ufm = ShowMessageParams (ufmSeverity ufm) $ T.pack $ show ufm+++showLspMessage :: MonadLsp cfg m => ShowMessageParams -> m ()+showLspMessage = sendNotification SWindowShowMessage+++-- This rule only exists for generating file diagnostics+-- so the RuleResult is empty+data WriteDiagnostics = WriteDiagnostics+    deriving (Eq, Show, Typeable, Generic)++instance Hashable WriteDiagnostics+instance NFData   WriteDiagnostics+instance Binary   WriteDiagnostics++type instance RuleResult WriteDiagnostics = ()++wingmanRules :: PluginId -> Rules ()+wingmanRules plId = do+  define $ \WriteDiagnostics nfp ->+    usePropertyAction #hole_severity plId properties >>= \case+      Nothing -> pure (mempty, Just ())+      Just severity ->+        use GetParsedModule nfp >>= \case+          Nothing ->+            pure ([], Nothing)+          Just pm -> do+            let holes :: [Range]+                holes =+                  everything (<>)+                    (mkQ mempty $ \case+                      L span (HsVar _ (L _ name))+                        | isHole (occName name) ->+                            maybeToList $ srcSpanToRange span+                      L span (HsUnboundVar _ (TrueExprHole occ))+                        | isHole occ ->+                            maybeToList $ srcSpanToRange span+#if __GLASGOW_HASKELL__ <= 808+                      L span (EWildPat _) ->+                        maybeToList $ srcSpanToRange span+#endif+                      (_ :: LHsExpr GhcPs) -> mempty+                    ) $ pm_parsed_source pm+            pure+              ( fmap (\r -> (nfp, ShowDiag, mkDiagnostic severity r)) holes+              , Just ()+              )++  action $ do+    files <- getFilesOfInterest+    void $ uses WriteDiagnostics $ Map.keys files+++mkDiagnostic :: DiagnosticSeverity -> Range -> Diagnostic+mkDiagnostic severity r =+  Diagnostic r+    (Just severity)+    (Just $ InR "hole")+    (Just "wingman")+    "Hole"+    (Just $ List [DtUnnecessary])+    Nothing+

@@ -0,0 +1,296 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards   #-}++module Wingman.LanguageServer.TacticProviders+  ( commandProvider+  , commandTactic+  , tcCommandId+  , TacticParams (..)+  , TacticProviderData (..)+  ) where++import           Control.Monad+import           Control.Monad.Error.Class (MonadError (throwError))+import           Data.Aeson+import           Data.Bool (bool)+import           Data.Coerce+import qualified Data.Map as M+import           Data.Maybe+import           Data.Monoid+import qualified Data.Text as T+import           Data.Traversable+import           DataCon (dataConName)+import           Development.IDE.Core.UseStale (Tracked, Age(..))+import           Development.IDE.GHC.Compat+import           GHC.Generics+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))+import           Ide.PluginUtils+import           Ide.Types+import           Language.LSP.Types+import           OccName+import           Prelude hiding (span)+import           Refinery.Tactic (goal)+import           Wingman.Auto+import           Wingman.FeatureSet+import           Wingman.GHC+import           Wingman.Judgements+import           Wingman.Tactics+import           Wingman.Types+++------------------------------------------------------------------------------+-- | A mapping from tactic commands to actual tactics for refinery.+commandTactic :: TacticCommand -> OccName -> TacticsM ()+commandTactic Auto                   = const auto+commandTactic Intros                 = const intros+commandTactic Destruct               = useNameFromHypothesis destruct+commandTactic Homomorphism           = useNameFromHypothesis homo+commandTactic DestructLambdaCase     = const destructLambdaCase+commandTactic HomomorphismLambdaCase = const homoLambdaCase+commandTactic DestructAll            = const destructAll+commandTactic UseDataCon             = userSplit+commandTactic Refine                 = const refine+++------------------------------------------------------------------------------+-- | The LSP kind+tacticKind :: TacticCommand -> T.Text+tacticKind Auto                   = "fillHole"+tacticKind Intros                 = "introduceLambda"+tacticKind Destruct               = "caseSplit"+tacticKind Homomorphism           = "homomorphicCaseSplit"+tacticKind DestructLambdaCase     = "lambdaCase"+tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase"+tacticKind DestructAll            = "splitFuncArgs"+tacticKind UseDataCon             = "useConstructor"+tacticKind Refine                 = "refine"+++------------------------------------------------------------------------------+-- | Whether or not this code action is preferred -- ostensibly refers to+-- whether or not we can bind it to a key in vs code?+tacticPreferred :: TacticCommand -> Bool+tacticPreferred Auto                   = True+tacticPreferred Intros                 = True+tacticPreferred Destruct               = True+tacticPreferred Homomorphism           = False+tacticPreferred DestructLambdaCase     = False+tacticPreferred HomomorphismLambdaCase = False+tacticPreferred DestructAll            = True+tacticPreferred UseDataCon             = True+tacticPreferred Refine                 = True+++mkTacticKind :: TacticCommand -> CodeActionKind+mkTacticKind =+  CodeActionUnknown . mappend "refactor.wingman." . tacticKind+++------------------------------------------------------------------------------+-- | 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 ""+commandProvider DestructAll =+  requireFeature FeatureDestructAll $+    withJudgement $ \jdg ->+      case _jIsTopHole jdg && jHasBoundArgs jdg of+        True  -> provide DestructAll ""+        False -> mempty+commandProvider UseDataCon =+  withConfig $ \cfg ->+    requireFeature FeatureUseDataCon $+      filterTypeProjection+          ( guardLength (<= cfg_max_use_ctor_actions cfg)+          . fromMaybe []+          . fmap fst+          . tacticsGetDataCons+          ) $ \dcon ->+        provide UseDataCon+          . T.pack+          . occNameString+          . occName+          $ dataConName dcon+commandProvider Refine =+  requireFeature FeatureRefineHole $+    provide Refine ""+++------------------------------------------------------------------------------+-- | Return an empty list if the given predicate doesn't hold over the length+guardLength :: (Int -> Bool) -> [a] -> [a]+guardLength f as = bool [] as $ f $ length as+++------------------------------------------------------------------------------+-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS+-- UI.+type TacticProvider+     = TacticProviderData+    -> IO [Command |? CodeAction]++data TacticProviderData = TacticProviderData+  { tpd_dflags :: DynFlags+  , tpd_config :: Config+  , tpd_plid   :: PluginId+  , tpd_uri    :: Uri+  , tpd_range  :: Tracked 'Current Range+  , tpd_jdg    :: Judgement+  }+++data TacticParams = TacticParams+    { tp_file     :: Uri    -- ^ Uri of the file to fill the hole in+    , tp_range    :: Tracked 'Current Range  -- ^ The range of the hole+    , tp_var_name :: T.Text+    }+  deriving stock (Show, Eq, Generic)+  deriving anyclass (ToJSON, FromJSON)+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- 'Feature' is in the feature set.+requireFeature :: Feature -> TacticProvider -> TacticProvider+requireFeature f tp tpd =+  case hasFeature f $ cfg_feature_set $ tpd_config tpd of+    True  -> tp tpd+    False -> pure []+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- predicate holds for the goal.+requireExtension :: Extension -> TacticProvider -> TacticProvider+requireExtension ext tp tpd =+  case xopt ext $ tpd_dflags tpd of+    True  -> tp tpd+    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 tpd =+  case p $ unCType $ jGoal $ tpd_jdg tpd of+    True  -> tp tpd+    False -> pure []+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- predicate holds for the goal.+withJudgement :: (Judgement -> TacticProvider) -> TacticProvider+withJudgement tp tpd = tp (tpd_jdg tpd) tpd+++------------------------------------------------------------------------------+-- | 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 tpd =+  let jdg = tpd_jdg tpd+      hy  = jLocalHypothesis jdg+      g   = jGoal jdg+   in fmap join $ for (unHypothesis hy) $ \hi ->+        let ty = unCType $ hi_type hi+         in case p (unCType g) ty of+              True  -> tp (hi_name hi) ty tpd+              False -> pure []+++------------------------------------------------------------------------------+-- | Multiply a 'TacticProvider' by some feature projection out of the goal+-- type. Used e.g. to crete a code action for every data constructor.+filterTypeProjection+    :: (Type -> [a])  -- ^ Features of the goal to look into further+    -> (a -> TacticProvider)+    -> TacticProvider+filterTypeProjection p tp tpd =+  fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a ->+      tp a tpd+++------------------------------------------------------------------------------+-- | Get access to the 'Config' when building a 'TacticProvider'.+withConfig :: (Config -> TacticProvider) -> TacticProvider+withConfig tp tpd = tp (tpd_config tpd) tpd++++------------------------------------------------------------------------------+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to+-- look it up in the hypothesis.+useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a+useNameFromHypothesis f name = do+  hy <- jHypothesis <$> goal+  case M.lookup name $ hyByName hy of+    Just hi -> f hi+    Nothing -> throwError $ NotInScope name+++------------------------------------------------------------------------------+-- | Terminal constructor for providing context-sensitive tactics. Tactics+-- given by 'provide' are always available.+provide :: TacticCommand -> T.Text -> TacticProvider+provide tc name TacticProviderData{..} = do+  let title = tacticTitle tc name+      params = TacticParams { tp_file = tpd_uri , tp_range = tpd_range , tp_var_name = name }+      cmd = mkLspCommand tpd_plid (tcCommandId tc) title (Just [toJSON params])+  pure+    $ pure+    $ InR+    $ CodeAction+        { _title       = title+        , _kind        = Just $ mkTacticKind tc+        , _diagnostics = Nothing+        , _isPreferred = Just $ tacticPreferred tc+        , _disabled    = Nothing+        , _edit        = Nothing+        , _command     = Just cmd+        , _xdata       = Nothing+        }+++------------------------------------------------------------------------------+-- | Construct a 'CommandId'+tcCommandId :: TacticCommand -> CommandId+tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"+++------------------------------------------------------------------------------+-- | 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+