hls-tactics-plugin 1.1.0.0 → 1.2.0.0

raw patch · 265 files changed

+3704/−1126 lines, 265 filesdep +hls-graphdep +hyphenationdep +megaparsecdep −shakedep ~extradep ~ghcidenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: hls-graph, hyphenation, megaparsec, parser-combinators, prettyprinter

Dependencies removed: shake

Dependency ranges changed: extra, ghcide

API changes (from Hackage documentation)

Files

• README.md +0/−2
• hls-tactics-plugin.cabal +18/−6
• src/Wingman/Auto.hs +4/−1
• src/Wingman/CaseSplit.hs +11/−3
• src/Wingman/CodeGen.hs +149/−46
• src/Wingman/CodeGen/Utils.hs +2/−2
• src/Wingman/Context.hs +35/−20
• src/Wingman/EmptyCase.hs +160/−0
• src/Wingman/FeatureSet.hs +0/−94
• src/Wingman/GHC.hs +55/−3
• src/Wingman/Judgements.hs +42/−11
• src/Wingman/Judgements/SYB.hs +15/−6
• src/Wingman/Judgements/Theta.hs +40/−12
• src/Wingman/KnownStrategies.hs +6/−17
• src/Wingman/LanguageServer.hs +157/−51
• src/Wingman/LanguageServer/Metaprogram.hs +89/−0
• src/Wingman/LanguageServer/TacticProviders.hs +88/−47
• src/Wingman/Machinery.hs +86/−10
• src/Wingman/Metaprogramming/Lexer.hs +85/−0
• src/Wingman/Metaprogramming/Parser.hs +434/−0
• src/Wingman/Metaprogramming/Parser/Documentation.hs +228/−0
• src/Wingman/Metaprogramming/ProofState.hs +113/−0
• src/Wingman/Naming.hs +194/−36
• src/Wingman/Plugin.hs +50/−31
• src/Wingman/Simplify.hs +10/−1
• src/Wingman/StaticPlugin.hs +96/−0
• src/Wingman/Tactics.hs +141/−25
• src/Wingman/Types.hs +45/−6
• test/AutoTupleSpec.hs +1/−0
• test/CodeAction/AutoSpec.hs +60/−63
• test/CodeAction/DestructAllSpec.hs +9/−13
• test/CodeAction/DestructPunSpec.hs +20/−0
• test/CodeAction/DestructSpec.hs +21/−21
• test/CodeAction/IntrosSpec.hs +5/−7
• test/CodeAction/RefineSpec.hs +6/−12
• test/CodeAction/RunMetaprogramSpec.hs +36/−0
• test/CodeAction/UseDataConSpec.hs +7/−12
• test/CodeLens/EmptyCaseSpec.hs +20/−0
• test/ProviderSpec.hs +12/−16
• test/Utils.hs +41/−33
• test/golden/AutoEmptyString.expected.hs +2/−0
• test/golden/AutoEmptyString.hs.expected +0/−2
• test/golden/AutoEndo.expected.hs +11/−0
• test/golden/AutoEndo.hs.expected +0/−11
• test/golden/AutoInfixApply.expected.hs +3/−0
• test/golden/AutoInfixApply.hs.expected +0/−3
• test/golden/AutoInfixApplyMany.expected.hs +3/−0
• test/golden/AutoInfixApplyMany.hs.expected +0/−3
• test/golden/AutoInfixInfix.expected.hs +2/−0
• test/golden/AutoInfixInfix.hs.expected +0/−2
• test/golden/AutoPatSynUse.expected.hs +8/−0
• test/golden/AutoPatSynUse.hs.expected +0/−8
• test/golden/AutoSplitGADT.expected.hs +12/−0
• test/golden/AutoSplitGADT.hs.expected +0/−12
• test/golden/AutoThetaEqCtx.expected.hs +5/−0
• test/golden/AutoThetaEqCtx.hs.expected +0/−5
• test/golden/AutoThetaEqGADT.expected.hs +7/−0
• test/golden/AutoThetaEqGADT.hs.expected +0/−7
• test/golden/AutoThetaEqGADTDestruct.expected.hs +8/−0
• test/golden/AutoThetaEqGADTDestruct.hs.expected +0/−8
• test/golden/AutoThetaFix.expected.hs +13/−0
• test/golden/AutoThetaFix.hs.expected +0/−13
• test/golden/AutoThetaGADT.expected.hs +7/−0
• test/golden/AutoThetaGADT.hs.expected +0/−7
• test/golden/AutoThetaGADTDestruct.expected.hs +7/−0
• test/golden/AutoThetaGADTDestruct.hs.expected +0/−7
• test/golden/AutoThetaMultipleUnification.expected.hs +21/−0
• test/golden/AutoThetaMultipleUnification.hs +21/−0
• test/golden/AutoThetaRankN.expected.hs +8/−0
• test/golden/AutoThetaRankN.hs.expected +0/−8
• test/golden/AutoThetaRefl.expected.hs +7/−0
• test/golden/AutoThetaRefl.hs.expected +0/−7
• test/golden/AutoThetaReflDestruct.expected.hs +8/−0
• test/golden/AutoThetaReflDestruct.hs.expected +0/−8
• test/golden/AutoThetaSplitUnification.expected.hs +17/−0
• test/golden/AutoThetaSplitUnification.hs +17/−0
• test/golden/AutoZip.expected.hs +6/−0
• test/golden/AutoZip.hs.expected +0/−6
• test/golden/DestructAllAnd.expected.hs +5/−0
• test/golden/DestructAllAnd.hs.expected +0/−5
• test/golden/DestructAllFunc.expected.hs +4/−0
• test/golden/DestructAllFunc.hs.expected +0/−4
• test/golden/DestructAllGADTEvidence.expected.hs +21/−0
• test/golden/DestructAllGADTEvidence.hs +20/−0
• test/golden/DestructAllMany.expected.hs +27/−0
• test/golden/DestructAllMany.hs.expected +0/−27
• test/golden/DestructAllNonVarTopMatch.expected.hs +6/−0
• test/golden/DestructAllNonVarTopMatch.hs.expected +0/−6
• test/golden/DestructCthulhu.expected.hs +54/−0
• test/golden/DestructCthulhu.hs +31/−0
• test/golden/DestructDataFam.expected.hs +8/−0
• test/golden/DestructDataFam.hs +8/−0
• test/golden/DestructPun.expected.hs +8/−0
• test/golden/DestructPun.hs +7/−0
• test/golden/DestructTyFam.expected.hs +9/−0
• test/golden/DestructTyFam.hs +8/−0
• test/golden/DestructTyToDataFam.expected.hs +18/−0
• test/golden/DestructTyToDataFam.hs +18/−0
• test/golden/EmptyCaseADT.expected.hs +8/−0
• test/golden/EmptyCaseADT.hs +5/−0
• test/golden/EmptyCaseApply.expected.hs +3/−0
• test/golden/EmptyCaseApply.hs +1/−0
• test/golden/EmptyCaseGADT.expected.hs +13/−0
• test/golden/EmptyCaseGADT.hs +11/−0
• test/golden/EmptyCaseNested.expected.hs +5/−0
• test/golden/EmptyCaseNested.hs +3/−0
• test/golden/EmptyCaseParens.expected.hs +3/−0
• test/golden/EmptyCaseParens.hs +1/−0
• test/golden/EmptyCaseShadow.expected.hs +10/−0
• test/golden/EmptyCaseShadow.hs +7/−0
• test/golden/Fgmap.expected.hs +2/−0
• test/golden/Fgmap.hs.expected +0/−2
• test/golden/FmapBoth.expected.hs +3/−0
• test/golden/FmapBoth.hs.expected +0/−3
• test/golden/FmapJoin.expected.hs +2/−0
• test/golden/FmapJoin.hs.expected +0/−2
• test/golden/FmapJoinInLet.expected.hs +4/−0
• test/golden/FmapJoinInLet.hs.expected +0/−4
• test/golden/GoldenArbitrary.expected.hs +53/−0
• test/golden/GoldenArbitrary.hs.expected +0/−53
• test/golden/GoldenBigTuple.expected.hs +4/−0
• test/golden/GoldenBigTuple.hs.expected +0/−4
• test/golden/GoldenEitherAuto.expected.hs +3/−0
• test/golden/GoldenEitherAuto.hs.expected +0/−3
• test/golden/GoldenEitherHomomorphic.expected.hs +3/−0
• test/golden/GoldenEitherHomomorphic.hs.expected +0/−3
• test/golden/GoldenFmapTree.expected.hs +5/−0
• test/golden/GoldenFmapTree.hs.expected +0/−5
• test/golden/GoldenFoldr.expected.hs +3/−0
• test/golden/GoldenFoldr.hs.expected +0/−3
• test/golden/GoldenFromMaybe.expected.hs +3/−0
• test/golden/GoldenFromMaybe.hs.expected +0/−3
• test/golden/GoldenGADTAuto.expected.hs +7/−0
• test/golden/GoldenGADTAuto.hs.expected +0/−7
• test/golden/GoldenGADTDestruct.expected.hs +7/−0
• test/golden/GoldenGADTDestruct.hs.expected +0/−7
• test/golden/GoldenGADTDestructCoercion.expected.hs +8/−0
• test/golden/GoldenGADTDestructCoercion.hs.expected +0/−8
• test/golden/GoldenIdTypeFam.expected.hs +7/−0
• test/golden/GoldenIdTypeFam.hs.expected +0/−7
• test/golden/GoldenIdentityFunctor.expected.hs +3/−0
• test/golden/GoldenIdentityFunctor.hs.expected +0/−3
• test/golden/GoldenIntros.expected.hs +2/−0
• test/golden/GoldenIntros.hs.expected +0/−2
• test/golden/GoldenJoinCont.expected.hs +4/−0
• test/golden/GoldenJoinCont.hs.expected +0/−4
• test/golden/GoldenListFmap.expected.hs +3/−0
• test/golden/GoldenListFmap.hs.expected +0/−3
• test/golden/GoldenNote.expected.hs +3/−0
• test/golden/GoldenNote.hs.expected +0/−3
• test/golden/GoldenPureList.expected.hs +2/−0
• test/golden/GoldenPureList.hs.expected +0/−2
• test/golden/GoldenSafeHead.expected.hs +3/−0
• test/golden/GoldenSafeHead.hs.expected +0/−3
• test/golden/GoldenShow.expected.hs +2/−0
• test/golden/GoldenShow.hs.expected +0/−2
• test/golden/GoldenShowCompose.expected.hs +2/−0
• test/golden/GoldenShowCompose.hs.expected +0/−2
• test/golden/GoldenShowMapChar.expected.hs +2/−0
• test/golden/GoldenShowMapChar.hs.expected +0/−2
• test/golden/GoldenSuperclass.expected.hs +8/−0
• test/golden/GoldenSuperclass.hs.expected +0/−8
• test/golden/GoldenSwap.expected.hs +2/−0
• test/golden/GoldenSwap.hs.expected +0/−2
• test/golden/GoldenSwapMany.expected.hs +2/−0
• test/golden/GoldenSwapMany.hs.expected +0/−2
• test/golden/KnownBigSemigroup.expected.hs +9/−0
• test/golden/KnownBigSemigroup.hs.expected +0/−9
• test/golden/KnownCounterfactualSemigroup.expected.hs +7/−0
• test/golden/KnownCounterfactualSemigroup.hs.expected +0/−8
• test/golden/KnownDestructedSemigroup.expected.hs +5/−0
• test/golden/KnownDestructedSemigroup.hs.expected +0/−5
• test/golden/KnownMissingMonoid.expected.hs +8/−0
• test/golden/KnownMissingMonoid.hs.expected +0/−8
• test/golden/KnownMissingSemigroup.expected.hs +5/−0
• test/golden/KnownMissingSemigroup.hs.expected +0/−5
• test/golden/KnownModuleInstanceSemigroup.expected.hs +12/−0
• test/golden/KnownModuleInstanceSemigroup.hs.expected +0/−11
• test/golden/KnownMonoid.expected.hs +8/−0
• test/golden/KnownMonoid.hs.expected +0/−8
• test/golden/KnownPolyMonoid.expected.hs +8/−0
• test/golden/KnownPolyMonoid.hs.expected +0/−8
• test/golden/KnownThetaSemigroup.expected.hs +5/−0
• test/golden/KnownThetaSemigroup.hs.expected +0/−5
• test/golden/LayoutBind.expected.hs +8/−0
• test/golden/LayoutBind.hs.expected +0/−8
• test/golden/LayoutDollarApp.expected.hs +5/−0
• test/golden/LayoutDollarApp.hs.expected +0/−5
• test/golden/LayoutLam.expected.hs +5/−0
• test/golden/LayoutLam.hs.expected +0/−5
• test/golden/LayoutOpApp.expected.hs +4/−0
• test/golden/LayoutOpApp.hs.expected +0/−4
• test/golden/LayoutRec.expected.hs +5/−0
• test/golden/LayoutRec.hs +5/−0
• test/golden/LayoutSplitClass.expected.hs +5/−0
• test/golden/LayoutSplitClass.hs.expected +0/−5
• test/golden/LayoutSplitGuard.expected.hs +5/−0
• test/golden/LayoutSplitGuard.hs.expected +0/−5
• test/golden/LayoutSplitIn.expected.hs +5/−0
• test/golden/LayoutSplitIn.hs.expected +0/−5
• test/golden/LayoutSplitLet.expected.hs +7/−0
• test/golden/LayoutSplitLet.hs.expected +0/−7
• test/golden/LayoutSplitPatSyn.expected.hs +11/−0
• test/golden/LayoutSplitPatSyn.hs.expected +0/−11
• test/golden/LayoutSplitPattern.expected.hs +9/−0
• test/golden/LayoutSplitPattern.hs.expected +0/−9
• test/golden/LayoutSplitViewPat.expected.hs +6/−0
• test/golden/LayoutSplitViewPat.hs.expected +0/−6
• test/golden/LayoutSplitWhere.expected.hs +14/−0
• test/golden/LayoutSplitWhere.hs.expected +0/−14
• test/golden/MessageCantUnify.hs +8/−0
• test/golden/MetaBegin.expected.hs +1/−0
• test/golden/MetaBegin.hs +1/−0
• test/golden/MetaBindAll.expected.hs +2/−0
• test/golden/MetaBindAll.hs +2/−0
• test/golden/MetaBindOne.expected.hs +2/−0
• test/golden/MetaBindOne.hs +2/−0
• test/golden/MetaCataCollapse.expected.hs +14/−0
• test/golden/MetaCataCollapse.hs +10/−0
• test/golden/MetaCataCollapseUnary.expected.hs +8/−0
• test/golden/MetaCataCollapseUnary.hs +8/−0
• test/golden/MetaChoice.expected.hs +2/−0
• test/golden/MetaChoice.hs +2/−0
• test/golden/MetaMaybeAp.expected.hs +5/−0
• test/golden/MetaMaybeAp.hs +11/−0
• test/golden/MetaTry.expected.hs +2/−0
• test/golden/MetaTry.hs +2/−0
• test/golden/MetaUseImport.expected.hs +6/−0
• test/golden/MetaUseImport.hs +6/−0
• test/golden/MetaUseLocal.expected.hs +7/−0
• test/golden/MetaUseLocal.hs +7/−0
• test/golden/MetaUseMethod.expected.hs +12/−0
• test/golden/MetaUseMethod.hs +12/−0
• test/golden/NewtypeRecord.expected.hs +7/−0
• test/golden/NewtypeRecord.hs.expected +0/−7
• test/golden/PunGADT.expected.hs +12/−0
• test/golden/PunGADT.hs +12/−0
• test/golden/PunMany.expected.hs +8/−0
• test/golden/PunMany.hs +7/−0
• test/golden/PunManyGADT.expected.hs +19/−0
• test/golden/PunManyGADT.hs +18/−0
• test/golden/PunShadowing.expected.hs +5/−0
• test/golden/PunShadowing.hs +5/−0
• test/golden/PunSimple.expected.hs +5/−0
• test/golden/PunSimple.hs +5/−0
• test/golden/RecordCon.expected.hs +9/−0
• test/golden/RecordCon.hs.expected +0/−9
• test/golden/RefineCon.expected.hs +3/−0
• test/golden/RefineCon.hs.expected +0/−3
• test/golden/RefineGADT.expected.hs +9/−0
• test/golden/RefineGADT.hs +1/−1
• test/golden/RefineGADT.hs.expected +0/−9
• test/golden/RefineIntro.expected.hs +2/−0
• test/golden/RefineIntro.hs.expected +0/−2
• test/golden/RefineReader.expected.hs +5/−0
• test/golden/RefineReader.hs +1/−1
• test/golden/RefineReader.hs.expected +0/−5
• test/golden/SplitPattern.expected.hs +12/−0
• test/golden/SplitPattern.hs.expected +0/−12
• test/golden/UseConLeft.expected.hs +3/−0
• test/golden/UseConLeft.hs.expected +0/−3
• test/golden/UseConPair.expected.hs +2/−0
• test/golden/UseConPair.hs.expected +0/−2
• test/golden/UseConRight.expected.hs +3/−0
• test/golden/UseConRight.hs.expected +0/−3

@@ -56,8 +56,6 @@ " <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

@@ -1,7 +1,7 @@ cabal-version:      2.4 category:           Development name:               hls-tactics-plugin-version:            1.1.0.0+version:            1.2.0.0 synopsis:           Wingman plugin for Haskell Language Server description:        Please see README.md author:             Sandy Maguire, Reed Mullanix@@ -15,7 +15,6 @@ extra-source-files:   README.md   test/golden/*.cabal-  test/golden/*.expected   test/golden/*.hs   test/golden/*.yaml @@ -34,7 +33,7 @@     Wingman.CodeGen.Utils     Wingman.Context     Wingman.Debug-    Wingman.FeatureSet+    Wingman.EmptyCase     Wingman.GHC     Wingman.Judgements     Wingman.Judgements.SYB@@ -42,12 +41,18 @@     Wingman.KnownStrategies     Wingman.KnownStrategies.QuickCheck     Wingman.LanguageServer+    Wingman.LanguageServer.Metaprogram     Wingman.LanguageServer.TacticProviders     Wingman.Machinery+    Wingman.Metaprogramming.Lexer+    Wingman.Metaprogramming.Parser+    Wingman.Metaprogramming.Parser.Documentation+    Wingman.Metaprogramming.ProofState     Wingman.Naming     Wingman.Plugin     Wingman.Range     Wingman.Simplify+    Wingman.StaticPlugin     Wingman.Tactics     Wingman.Types @@ -72,14 +77,18 @@     , ghc-boot-th     , ghc-exactprint     , ghc-source-gen-    , ghcide                ^>=1.2+    , ghcide                ^>=1.4+    , hls-graph     , hls-plugin-api        ^>=1.1+    , hyphenation     , lens     , lsp+    , megaparsec            ^>=9     , mtl+    , parser-combinators+    , prettyprinter     , refinery              ^>=0.3     , retrie                >=0.1.1.0-    , shake     , syb     , text     , transformers@@ -117,10 +126,13 @@     AutoTupleSpec     CodeAction.AutoSpec     CodeAction.DestructAllSpec+    CodeAction.DestructPunSpec     CodeAction.DestructSpec     CodeAction.IntrosSpec     CodeAction.RefineSpec+    CodeAction.RunMetaprogramSpec     CodeAction.UseDataConSpec+    CodeLens.EmptyCaseSpec     ProviderSpec     Spec     UnificationSpec@@ -141,7 +153,7 @@     , ghcide     , hls-plugin-api     , hls-tactics-plugin-    , hls-test-utils  ^>= 1.0+    , hls-test-utils      ^>=1.0     , hspec     , hspec-expectations     , lens

@@ -1,5 +1,7 @@+ module Wingman.Auto where +import           Control.Monad.Reader.Class (asks) import           Control.Monad.State (gets) import qualified Data.Set as S import           Refinery.Tactic@@ -17,13 +19,14 @@ auto = do   jdg <- goal   skolems <- gets ts_skolems+  gas <- asks $ cfg_auto_gas . ctxConfig   current <- getCurrentDefinitions   traceMX "goal" jdg   traceMX "ctx" current   traceMX "skolems" skolems   commit knownStrategies     . tracing "auto"-    . localTactic (auto' 4)+    . localTactic (auto' gas)     . disallowing RecursiveCall     . S.fromList     $ fmap fst current

@@ -56,9 +56,17 @@ ------------------------------------------------------------------------------ -- | 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+rewriteVarPat name rep = everywhere $+  mkT (\case+    VarPat _ (L _ var) | eqRdrName name var -> rep+    (x :: Pat GhcPs)                        -> x+      )+  `extT` \case+    HsRecField lbl _ True+      | eqRdrName name $ unLoc $ rdrNameFieldOcc $ unLoc lbl+          -> HsRecField lbl (toPatCompat rep) False+    (x :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> x+   ------------------------------------------------------------------------------

@@ -1,7 +1,8 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE OverloadedLabels #-}-{-# LANGUAGE TupleSections    #-}-{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE FlexibleContexts  #-}+{-# LANGUAGE OverloadedLabels  #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TupleSections     #-}+{-# LANGUAGE TypeApplications  #-}  module Wingman.CodeGen   ( module Wingman.CodeGen@@ -12,21 +13,24 @@ import           ConLike import           Control.Lens ((%~), (<>~), (&)) import           Control.Monad.Except+import           Control.Monad.Reader (ask) import           Control.Monad.State import           Data.Bool (bool)+import           Data.Functor ((<&>)) 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 (occNameToStr) import           GHC.SourceGen.Binds import           GHC.SourceGen.Expr import           GHC.SourceGen.Overloaded import           GHC.SourceGen.Pat-import           GhcPlugins (isSymOcc)+import           GhcPlugins (isSymOcc, mkVarOccFS)+import           OccName (occName) import           PatSyn import           Type hiding (Var) import           Wingman.CodeGen.Utils@@ -39,7 +43,8 @@   destructMatches-    :: (ConLike -> Judgement -> Rule)+    :: Bool+    -> (ConLike -> Judgement -> Rule)        -- ^ How to construct each match     -> Maybe OccName        -- ^ Scrutinee@@ -47,49 +52,106 @@        -- ^ Type being destructed     -> Judgement     -> RuleM (Synthesized [RawMatch])-destructMatches f scrut t jdg = do+-- TODO(sandy): In an ideal world, this would be the same codepath as+-- 'destructionFor'. Make sure to change that if you ever change this.+destructMatches use_field_puns f scrut t jdg = do   let hy = jEntireHypothesis jdg       g  = jGoal jdg-  case splitTyConApp_maybe $ unCType t of+  case tacticsGetDataCons $ 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+    Just (dcs, apps) ->+      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 $ evidenceToSubst ev+        subst <- gets ts_unifier+        ctx <- ask +        let names_in_scope = hyNamesInScope hy+            names = mkManyGoodNames (hyNamesInScope hy) args+            (names', destructed) =+              mkDestructPat (bool Nothing (Just names_in_scope) use_field_puns) con names +        let hy' = patternHypothesis scrut con jdg+                $ zip names'+                $ coerce args+            j = fmap (CType . substTyAddInScope subst . unCType)+              $ introduce ctx hy'+              $ introduce ctx 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 [destructed] . unLoc++ ------------------------------------------------------------------------------+-- | Generate just the 'Match'es for a case split on a specific type.+destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]+-- TODO(sandy): In an ideal world, this would be the same codepath as+-- 'destructMatches'. Make sure to change that if you ever change this.+destructionFor hy t = do+  case tacticsGetDataCons t of+    Nothing -> Nothing+    Just ([], _) -> Nothing+    Just (dcs, apps) -> do+      for dcs $ \dc -> do+        let con   = RealDataCon dc+            args  = conLikeInstOrigArgTys' con apps+            names = mkManyGoodNames (hyNamesInScope hy) args+        pure+          . noLoc+          . Match+              noExtField+              CaseAlt+              [toPatCompat $ snd $ mkDestructPat Nothing con names]+          . GRHSs noExtField (pure $ noLoc $ GRHS noExtField [] $ noLoc $ var "_")+          . noLoc+          $ EmptyLocalBinds noExtField++++------------------------------------------------------------------------------ -- | Produces a pattern for a data con and the names of its fields.-mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs-mkDestructPat con names+mkDestructPat :: Maybe (S.Set OccName) -> ConLike -> [OccName] -> ([OccName], Pat GhcPs)+mkDestructPat already_in_scope con names   | RealDataCon dcon <- con   , isTupleDataCon dcon =-      tuple pat_args+      (names, tuple pat_args)+  | fields@(_:_) <- zip (conLikeFieldLabels con) names+  , Just in_scope <- already_in_scope =+      let (names', rec_fields) =+            unzip $ fields <&> \(label, name) -> do+              let label_occ = mkVarOccFS $ flLabel label+              case S.member label_occ in_scope of+                -- We have a shadow, so use the generated name instead+                True ->+                  (name,) $ noLoc $+                    HsRecField+                      (noLoc $ mkFieldOcc $ noLoc $ Unqual label_occ)+                      (noLoc $ bvar' name)+                      False+                -- No shadow, safe to use a pun+                False ->+                  (label_occ,) $ noLoc $+                    HsRecField+                      (noLoc $ mkFieldOcc $ noLoc $ Unqual label_occ)+                      (noLoc $ bvar' label_occ)+                      True++        in (names', )+         $ ConPatIn (noLoc $ Unqual $ occName $ conLikeName con)+         $ RecCon+         $ HsRecFields rec_fields+         $ Nothing   | otherwise =-      infixifyPatIfNecessary con $+      (names, ) $ infixifyPatIfNecessary con $         conP           (coerceName $ conLikeName con)           pat_args@@ -151,12 +213,13 @@ -- | 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+destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule+destruct' use_field_puns f hi jdg = do   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic   let term = hi_name hi   ext       <- destructMatches+           use_field_puns            f            (Just term)            (hi_type hi)@@ -170,14 +233,14 @@ ------------------------------------------------------------------------------ -- | Combinator for performign case splitting, and running sub-rules on the -- resulting matches.-destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule-destructLambdaCase' f jdg = do+destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule+destructLambdaCase' use_field_puns 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+        destructMatches use_field_puns f Nothing (CType arg) jdg     _ -> throwError $ GoalMismatch "destructLambdaCase'" g  @@ -190,7 +253,22 @@     -> [Type]             -- ^ Type arguments for the data con     -> RuleM (Synthesized (LHsExpr GhcPs)) buildDataCon should_blacklist jdg dc tyapps = do-  let args = conLikeInstOrigArgTys' dc tyapps+  args <- case dc of+    RealDataCon dc' -> do+      let (skolems', theta, args) = dataConInstSig dc' tyapps+      modify $ \ts ->+        evidenceToSubst (foldMap mkEvidence theta) ts+          & #ts_skolems <>~ S.fromList skolems'+      pure args+    _ ->+      -- If we have a 'PatSyn', we can't continue, since there is no+      -- 'dataConInstSig' equivalent for 'PatSyn's. I don't think this is+      -- a fundamental problem, but I don't know enough about the GHC internals+      -- to implement it myself.+      --+      -- Fortunately, this isn't an issue in practice, since 'PatSyn's are+      -- never in the hypothesis.+      throwError $ TacticPanic "Can't build Pattern constructors yet"   ext       <- fmap unzipTrace        $ traverse ( \(arg, n) ->@@ -212,4 +290,29 @@   | isSymOcc occ   = noLoc $ foldl' (@@) (op lhs (coerceName occ) rhs) more mkApply occ args = noLoc $ foldl' (@@) (var' occ) args+++------------------------------------------------------------------------------+-- | Run a tactic over each term in the given 'Hypothesis', binding the results+-- of each in a let expression.+letForEach+    :: (OccName -> OccName)           -- ^ How to name bound variables+    -> (HyInfo CType -> TacticsM ())  -- ^ The tactic to run+    -> Hypothesis CType               -- ^ Terms to generate bindings for+    -> Judgement                      -- ^ The goal of original hole+    -> RuleM (Synthesized (LHsExpr GhcPs))+letForEach rename solve (unHypothesis -> hy) jdg = do+  case hy of+    [] -> newSubgoal jdg+    _ -> do+      ctx <- ask+      let g = jGoal jdg+      terms <- fmap sequenceA $ for hy $ \hi -> do+        let name = rename $ hi_name hi+        res <- tacticToRule jdg $ solve hi+        pure $ fmap ((name,) . unLoc) res+      let hy' = fmap (g <$) $ syn_val terms+          matches = fmap (fmap (\(occ, expr) -> valBind (occNameToStr occ) expr)) terms+      g <- fmap (fmap unLoc) $ newSubgoal $ introduce ctx (userHypothesis hy') jdg+      pure $ fmap noLoc $ let' <$> matches <*> g 

@@ -5,7 +5,7 @@ import DataCon import Development.IDE.GHC.Compat import GHC.Exts-import GHC.SourceGen (RdrNameStr, recordConE, string)+import GHC.SourceGen (RdrNameStr (UnqualStr), recordConE, string) import GHC.SourceGen.Overloaded import GhcPlugins (nilDataCon, charTy, eqType) import Name@@ -43,7 +43,7 @@   coerceName :: HasOccName a => a -> RdrNameStr-coerceName = fromString . occNameString . occName+coerceName = UnqualStr . fromString . occNameString . occName   ------------------------------------------------------------------------------

@@ -3,45 +3,60 @@ import           Bag import           Control.Arrow import           Control.Monad.Reader+import           Data.Coerce (coerce) import           Data.Foldable.Extra (allM)-import           Data.Maybe (fromMaybe, isJust)+import           Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import           Development.IDE.GHC.Compat-import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)+import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env) import           InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import           OccName import           TcRnTypes import           TcType (tcSplitTyConApp, tcSplitPhiTy) import           TysPrim (alphaTys)-import           Wingman.FeatureSet (FeatureSet)+import           Wingman.GHC (normalizeType) import           Wingman.Judgements.Theta import           Wingman.Types   mkContext-    :: FeatureSet+    :: Config     -> [(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-  }+mkContext cfg locals tcg eps kt ev = fix $ \ctx ->+  Context+    { ctxDefiningFuncs+        = fmap (second $ coerce $ normalizeType ctx) locals+    , ctxModuleFuncs+        = fmap (second (coerce $ normalizeType ctx) . splitId)+        . mappend (locallyDefinedMethods tcg)+        . (getFunBindId =<<)+        . fmap unLoc+        . bagToList+        $ tcg_binds tcg+    , ctxConfig = cfg+    , ctxFamInstEnvs =+        (eps_fam_inst_env eps, tcg_fam_inst_env tcg)+    , ctxInstEnvs =+        InstEnvs+          (eps_inst_env eps)+          (tcg_inst_env tcg)+          (tcVisibleOrphanMods tcg)+    , ctxKnownThings = kt+    , ctxTheta = evidenceToThetaType ev+    }+++locallyDefinedMethods :: TcGblEnv -> [Id]+locallyDefinedMethods+  = foldMap classMethods+  . mapMaybe tyConClass_maybe+  . tcg_tcs+   splitId :: Id -> (OccName, CType)

@@ -0,0 +1,160 @@+{-# LANGUAGE OverloadedStrings #-}++{-# LANGUAGE NoMonoLocalBinds  #-}++module Wingman.EmptyCase where++import           Control.Applicative (empty)+import           Control.Monad+import           Control.Monad.Except (runExcept)+import           Control.Monad.Trans+import           Control.Monad.Trans.Maybe+import           Data.Aeson+import           Data.Generics.Aliases (mkQ, GenericQ)+import           Data.Generics.Schemes (everything)+import           Data.Maybe+import           Data.Monoid+import qualified Data.Text as T+import           Data.Traversable+import           Development.IDE (hscEnv)+import           Development.IDE (realSrcSpanToRange)+import           Development.IDE.Core.RuleTypes+import           Development.IDE.Core.Shake (IdeState (..))+import           Development.IDE.Core.UseStale+import           Development.IDE.GHC.Compat+import           Development.IDE.GHC.ExactPrint+import           Development.IDE.Spans.LocalBindings (getLocalScope)+import           Ide.Types+import           Language.LSP.Server+import           Language.LSP.Types+import           OccName+import           Prelude hiding (span)+import           Prelude hiding (span)+import           TcRnTypes (tcg_binds)+import           Wingman.CodeGen (destructionFor)+import           Wingman.GHC+import           Wingman.Judgements+import           Wingman.LanguageServer+import           Wingman.Types+++------------------------------------------------------------------------------+-- | The 'CommandId' for the empty case completion.+emptyCaseLensCommandId :: CommandId+emptyCaseLensCommandId = CommandId "wingman.emptyCase"+++------------------------------------------------------------------------------+-- | A command function that just applies a 'WorkspaceEdit'.+workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit+workspaceEditHandler _ideState wedit = do+  _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ())+  return $ Right Null+++------------------------------------------------------------------------------+-- | Provide the "empty case completion" code lens+codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens+codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do+      let stale a = runStaleIde "codeLensProvider" state nfp a++      cfg <- getTacticConfig plId+      ccs <- getClientCapabilities+      liftIO $ fromMaybeT (Right $ List []) $ do+        dflags <- getIdeDynflags state nfp+        TrackedStale pm _ <- stale GetAnnotatedParsedSource+        TrackedStale binds bind_map <- stale GetBindings+        holes <- emptyCaseScrutinees state nfp++        fmap (Right . List) $ for holes $ \(ss, ty) -> do+          binds_ss <- liftMaybe $ mapAgeFrom bind_map ss+          let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss+              range = realSrcSpanToRange $ unTrack ss+          matches <-+            liftMaybe $+              destructionFor+                (foldMap (hySingleton . occName . fst) bindings)+                ty+          edits <- liftMaybe $ hush $+                mkWorkspaceEdits dflags ccs uri (unTrack pm) $+                  graftMatchGroup (RealSrcSpan $ unTrack ss) $+                    noLoc matches++          pure $+            CodeLens range+              (Just+                $ mkLspCommand+                    plId+                    emptyCaseLensCommandId+                    (mkEmptyCaseLensDesc ty)+                $ Just $ pure $ toJSON $ edits+              )+              Nothing+codeLensProvider _ _ _ = pure $ Right $ List []+++------------------------------------------------------------------------------+-- | The description for the empty case lens.+mkEmptyCaseLensDesc :: Type -> T.Text+mkEmptyCaseLensDesc ty =+  "Wingman: Complete case constructors (" <> T.pack (unsafeRender ty) <> ")"+++------------------------------------------------------------------------------+-- | Silence an error.+hush :: Either e a -> Maybe a+hush (Left _) = Nothing+hush (Right a) = Just a+++------------------------------------------------------------------------------+-- | 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.+graftMatchGroup+    :: SrcSpan+    -> Located [LMatch GhcPs (LHsExpr GhcPs)]+    -> Graft (Either String) ParsedSource+graftMatchGroup ss l =+  hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case+    L span (HsCase ext scrut mg@_) -> do+      pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }+    (_ :: LHsExpr GhcPs) -> pure Nothing+++fromMaybeT :: Functor m => a -> MaybeT m a -> m a+fromMaybeT def = fmap (fromMaybe def) . runMaybeT+++------------------------------------------------------------------------------+-- | Find the last typechecked module, and find the most specific span, as well+-- as the judgement at the given range.+emptyCaseScrutinees+    :: IdeState+    -> NormalizedFilePath+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, Type)]+emptyCaseScrutinees state nfp = do+    let stale a = runStaleIde "emptyCaseScrutinees" state nfp a++    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck+    let tcg' = unTrack tcg+    hscenv <- stale GhcSessionDeps++    let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg+    for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do+      ty <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg' scrutinee+      case ss of+        RealSrcSpan r   -> do+          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r+          pure (rss', ty)+        UnhelpfulSpan _ -> empty+++------------------------------------------------------------------------------+-- | Get the 'SrcSpan' and scrutinee of every empty case.+emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]+emptyCaseQ = everything (<>) $ mkQ mempty $ \case+  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)+  (_ :: LHsExpr GhcTc) -> mempty+

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

@@ -3,10 +3,12 @@  module Wingman.GHC where +import           Bag (bagToList) import           ConLike import           Control.Applicative (empty) import           Control.Monad.State import           Control.Monad.Trans.Maybe (MaybeT(..))+import           CoreUtils (exprType) import           Data.Function (on) import           Data.Functor ((<&>)) import           Data.List (isPrefixOf)@@ -18,10 +20,14 @@ import           DataCon import           Development.IDE (HscEnvEq (hscEnv)) import           Development.IDE.Core.Compile (lookupName)-import           Development.IDE.GHC.Compat+import           Development.IDE.GHC.Compat hiding (exprType)+import           DsExpr (dsExpr)+import           DsMonad (initDs)+import           FamInst (tcLookupDataFamInst_maybe)+import           FamInstEnv (normaliseType) import           GHC.SourceGen (lambda) import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)-import           GhcPlugins (extractModule, GlobalRdrElt (gre_name))+import           GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal)) import           OccName import           TcRnMonad import           TcType@@ -70,7 +76,7 @@ -- context. tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type) tacticsSplitFunTy t-  = let (vars, theta, t') = tcSplitSigmaTy t+  = let (vars, theta, t') = tcSplitNestedSigmaTys t         (args, res) = tcSplitFunTys t'      in (vars, theta, args, res) @@ -193,6 +199,15 @@         }  +pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs+pattern SingleLet bind pats val expr <-+  HsLet _+    (L _ (HsValBinds _+      (ValBinds _ (bagToList ->+        [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _)))+    (L _ expr)++ ------------------------------------------------------------------------------ -- | A pattern over the otherwise (extremely) messy AST for lambdas. pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs@@ -341,6 +356,43 @@         Just tt -> liftMaybe $ f tt         _ -> empty + liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a+++------------------------------------------------------------------------------+-- | Get the type of an @HsExpr GhcTc@. This is slow and you should prefer to+-- not use it, but sometimes it can't be helped.+typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)+typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr+++mkFunTys' :: [Type] -> Type -> Type+mkFunTys' =+#if __GLASGOW_HASKELL__ <= 808+  mkFunTys+#else+  mkVisFunTys+#endif+++------------------------------------------------------------------------------+-- | Expand type and data families+normalizeType :: Context -> Type -> Type+normalizeType ctx ty =+  let ty' = expandTyFam ctx ty+   in case tcSplitTyConApp_maybe ty' of+        Just (tc, tys) ->+          -- try to expand any data families+          case tcLookupDataFamInst_maybe (ctxFamInstEnvs ctx) tc tys of+            Just (dtc, dtys, _) -> mkAppTys (mkTyConTy dtc) dtys+            Nothing -> ty'+        Nothing -> ty'++------------------------------------------------------------------------------+-- | Expand type families+expandTyFam :: Context -> Type -> Type+expandTyFam ctx = snd . normaliseType  (ctxFamInstEnvs ctx) Nominal+ 

@@ -17,7 +17,7 @@ import           OccName import           SrcLoc import           Type-import           Wingman.GHC (algebraicTyCon)+import           Wingman.GHC (algebraicTyCon, normalizeType) import           Wingman.Types  @@ -40,6 +40,13 @@       | otherwise = Nothing  +------------------------------------------------------------------------------+-- | Build a trivial hypothesis containing only a single name. The corresponding+-- HyInfo has no provenance or type.+hySingleton :: OccName -> Hypothesis ()+hySingleton n = Hypothesis . pure $ HyInfo n UserPrv ()++ blacklistingDestruct :: Judgement -> Judgement blacklistingDestruct =   field @"_jBlacklistDestruct" .~ True@@ -62,11 +69,19 @@ withNewGoal t = field @"_jGoal" .~ t  -introduce :: Hypothesis a -> Judgement' a -> Judgement' a+normalizeHypothesis :: Functor f => Context -> f CType -> f CType+normalizeHypothesis = fmap . coerce . normalizeType++normalizeJudgement :: Functor f => Context -> f CType -> f CType+normalizeJudgement = normalizeHypothesis+++introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType -- 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+introduce ctx hy =+  field @"_jHypothesis" %~ mappend (normalizeHypothesis ctx hy)   ------------------------------------------------------------------------------@@ -101,6 +116,12 @@   ------------------------------------------------------------------------------+-- | Introduce a binding in a recursive context.+userHypothesis :: [(OccName, a)] -> Hypothesis a+userHypothesis = introduceHypothesis $ const $ const UserPrv+++------------------------------------------------------------------------------ -- | Check whether any of the given occnames are an ancestor of the term. hasPositionalAncestry     :: Foldable t@@ -222,6 +243,7 @@ provAncestryOf (ClassMethodPrv _) = mempty provAncestryOf UserPrv = mempty provAncestryOf RecursivePrv = mempty+provAncestryOf ImportPrv = mempty provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2  @@ -295,6 +317,12 @@   ------------------------------------------------------------------------------+-- | Filter elements from the hypothesis+hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a+hyFilter f  = Hypothesis . filter f . unHypothesis+++------------------------------------------------------------------------------ -- | Given a judgment, return the hypotheses that are acceptable to destruct. -- -- We use the ordering of the hypothesis for this purpose. Since new bindings@@ -373,17 +401,20 @@   mkFirstJudgement-    :: Hypothesis CType+    :: Context+    -> 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-  }+mkFirstJudgement ctx hy top goal =+  normalizeJudgement ctx $+    Judgement+      { _jHypothesis        = hy+      , _jBlacklistDestruct = False+      , _jWhitelistSplit    = True+      , _jIsTopHole         = top+      , _jGoal              = CType goal+      }   ------------------------------------------------------------------------------

@@ -4,12 +4,15 @@ -- | 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)+import           Data.Foldable (foldl')+import           Data.Generics hiding (typeRep)+import qualified Data.Text as T+import           Development.IDE.GHC.Compat+import           GHC.Exts (Any)+import           GhcPlugins (unpackFS)+import           Type.Reflection+import           Unsafe.Coerce (unsafeCoerce)+import           Wingman.StaticPlugin (pattern WingmanMetaprogram)   ------------------------------------------------------------------------------@@ -80,4 +83,10 @@             Just HRefl -> True             Nothing    -> False         _ -> False+++metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]+metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case+  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)+  (_ :: LHsExpr GhcTc) -> mempty 

@@ -12,13 +12,16 @@  import           Class (classTyVars) import           Control.Applicative (empty)+import           Control.Lens (preview) import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)+import           Data.Generics.Sum (_Ctor) 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)+import           Generics.SYB hiding (tyConName, empty, Generic)+import           GHC.Generics+import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst) #if __GLASGOW_HASKELL__ > 806 import           GhcPlugins (eqTyCon) #else@@ -40,7 +43,7 @@   = EqualityOfTypes Type Type     -- | We have an instance in scope   | HasInstance PredType-  deriving (Show)+  deriving (Show, Generic)   ------------------------------------------------------------------------------@@ -75,21 +78,46 @@   . unTrack  ---------------------------------------------------------------------------------- | Update our knowledge of which types are equal.-evidenceToSubst :: Evidence -> TacticState -> TacticState-evidenceToSubst (EqualityOfTypes a b) ts =+mkSubst :: Set TyVar -> Type -> Type -> TCvSubst+mkSubst skolems a b =   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+      skolems' = skolems S.\\ tyvars    in-  case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of-    Just subst -> updateSubst subst ts-    Nothing -> ts-evidenceToSubst HasInstance{} ts = ts+  case tryUnifyUnivarsButNotSkolems skolems' (CType a) (CType b) of+    Just subst -> subst+    Nothing -> emptyTCvSubst+++substPair :: TCvSubst -> (Type, Type) -> (Type, Type)+substPair subst (ty, ty') = (substTy subst ty, substTy subst ty')+++------------------------------------------------------------------------------+-- | Construct a substitution given a list of types that are equal to one+-- another. This is more subtle than it seems, since there might be several+-- equalities for the same type. We must be careful to push the accumulating+-- substitution through each pair of types before adding their equalities.+allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst+allEvidenceToSubst _ [] = emptyTCvSubst+allEvidenceToSubst skolems ((a, b) : evs) =+  let subst = mkSubst skolems a b+   in unionTCvSubst subst+    $ allEvidenceToSubst skolems+    $ fmap (substPair subst) evs++------------------------------------------------------------------------------+-- | Update our knowledge of which types are equal.+evidenceToSubst :: [Evidence] -> TacticState -> TacticState+evidenceToSubst evs ts =+  updateSubst+    (allEvidenceToSubst (ts_skolems ts)+      $ mapMaybe (preview $ _Ctor @"EqualityOfTypes")+      $ evs)+    ts   ------------------------------------------------------------------------------

@@ -1,18 +1,17 @@ module Wingman.KnownStrategies where +import Control.Applicative (empty) import Control.Monad.Error.Class+import Control.Monad.Reader.Class (asks)+import Data.Foldable (for_) import OccName (mkVarOcc) import Refinery.Tactic import Wingman.Context (getCurrentDefinitions, getKnownInstance)+import Wingman.Judgements (jGoal) 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 ()@@ -20,19 +19,9 @@   [ known "fmap" deriveFmap   , known "mempty" deriveMempty   , known "arbitrary" deriveArbitrary-  , featureGuard FeatureKnownMonoid $ known "<>" deriveMappend-  , featureGuard FeatureKnownMonoid $ known "mappend" deriveMappend+  , known "<>" deriveMappend+  , 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 ()

@@ -1,28 +1,33 @@ {-# LANGUAGE CPP               #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes        #-}+{-# LANGUAGE TupleSections     #-} {-# LANGUAGE TypeFamilies      #-} +{-# LANGUAGE NoMonoLocalBinds  #-}+ module Wingman.LanguageServer where  import           ConLike-import           Control.Arrow+import           Control.Arrow ((***)) import           Control.Monad-import           Control.Monad.State (State, get, put, evalState)+import           Control.Monad.IO.Class+import           Control.Monad.RWS+import           Control.Monad.State (State, evalState) import           Control.Monad.Trans.Maybe+import           Data.Bifunctor (first) import           Data.Coerce import           Data.Functor ((<&>))-import           Data.Generics.Aliases (mkQ)-import           Data.Generics.Schemes (everything)+import           Data.Functor.Identity (runIdentity) 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 (getFilesOfInterestUntracked, ShowDiagnostic (ShowDiag), srcSpanToRange) import           Development.IDE (hscEnv) import           Development.IDE.Core.RuleTypes import           Development.IDE.Core.Rules (usePropertyAction)@@ -30,31 +35,39 @@ 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.Compat hiding (parseExpr) import           Development.IDE.GHC.Error (realSrcSpanToRange)+import           Development.IDE.GHC.ExactPrint+import           Development.IDE.Graph (Action, RuleResult, Rules, action)+import           Development.IDE.Graph.Classes (Binary, Hashable, NFData) 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           Generics.SYB hiding (Generic)+import           GhcPlugins (extractModule)+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS) import qualified Ide.Plugin.Config as Plugin import           Ide.Plugin.Properties import           Ide.PluginUtils (usePropertyLsp) import           Ide.Types (PluginId)+import           Language.Haskell.GHC.ExactPrint (Transform)+import           Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty) import           Language.LSP.Server (MonadLsp, sendNotification) import           Language.LSP.Types+import           Language.LSP.Types.Capabilities import           OccName import           Prelude hiding (span)+import           Retrie (transformA) import           SrcLoc (containsSpan)-import           TcRnTypes (tcg_binds, TcGblEnv)+import           TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env)) import           Wingman.Context-import           Wingman.FeatureSet import           Wingman.GHC import           Wingman.Judgements-import           Wingman.Judgements.SYB (everythingContaining)+import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ) import           Wingman.Judgements.Theta+import           Wingman.Metaprogramming.Lexer (ParserContext(..)) import           Wingman.Range+import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax) import           Wingman.Types  @@ -68,8 +81,8 @@ tcCommandName = T.pack . show  -runIde :: IdeState -> Action a -> IO a-runIde state = runAction "tactic" state+runIde :: String -> String -> IdeState -> Action a -> IO a+runIde herald action state = runAction ("Wingman." <> herald <> "." <> action) state   runCurrentIde@@ -78,11 +91,13 @@        , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a        , Show r, Typeable r, NFData r        )-    => IdeState+    => String+    -> IdeState     -> NormalizedFilePath     -> a     -> MaybeT IO (Tracked 'Current r)-runCurrentIde state nfp a = MaybeT $ fmap (fmap unsafeMkCurrent) $ runIde state $ use a nfp+runCurrentIde herald state nfp a =+  MaybeT $ fmap (fmap unsafeMkCurrent) $ runIde herald (show a) state $ use a nfp   runStaleIde@@ -91,11 +106,13 @@        , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a        , Show r, Typeable r, NFData r        )-    => IdeState+    => String+    -> IdeState     -> NormalizedFilePath     -> a     -> MaybeT IO (TrackedStale r)-runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp+runStaleIde herald state nfp a =+  MaybeT $ runIde herald (show a) state $ useWithStale a nfp   unsafeRunStaleIde@@ -104,12 +121,13 @@        , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a        , Show r, Typeable r, NFData r        )-    => IdeState+    => String+    -> IdeState     -> NormalizedFilePath     -> a     -> MaybeT IO r-unsafeRunStaleIde state nfp a = do-  (r, _) <- MaybeT $ runIde state $ IDE.useWithStale a nfp+unsafeRunStaleIde herald state nfp a = do+  (r, _) <- MaybeT $ runIde herald (show a) state $ IDE.useWithStale a nfp   pure r  @@ -118,14 +136,14 @@ properties :: Properties   '[ 'PropertyKey "hole_severity" ('TEnum (Maybe DiagnosticSeverity))    , 'PropertyKey "max_use_ctor_actions" 'TInteger-   , 'PropertyKey "features" 'TString    , 'PropertyKey "timeout_duration" 'TInteger+   , 'PropertyKey "auto_gas" 'TInteger    ] properties = emptyProperties+  & defineIntegerProperty #auto_gas+    "The depth of the search tree when performing \"Attempt to fill hole\". Bigger values will be able to derive more solutions, but will take exponentially more time." 4   & 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@@ -143,14 +161,9 @@ getTacticConfig :: MonadLsp Plugin.Config m => PluginId -> m Config getTacticConfig pId =   Config-    <$> (parseFeatureSet <$> usePropertyLsp #features pId properties)-    <*> usePropertyLsp #max_use_ctor_actions 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+    <*> usePropertyLsp #auto_gas pId properties   getIdeDynflags@@ -160,10 +173,15 @@ 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+  msr <- unsafeRunStaleIde "getIdeDynflags" state nfp GetModSummaryWithoutTimestamps   pure $ ms_hspp_opts $ msrModSummary msr +getAllMetaprograms :: Data a => a -> [String]+getAllMetaprograms = everything (<>) $ mkQ mempty $ \case+  WingmanMetaprogram fs -> [ unpackFS fs ]+  (_ :: HsExpr GhcTc)  -> mempty + ------------------------------------------------------------------------------ -- | Find the last typechecked module, and find the most specific span, as well -- as the judgement at the given range.@@ -171,21 +189,27 @@     :: 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+    -> Config+    -> MaybeT IO HoleJudgment+judgementForHole state nfp range cfg = do+  let stale a = runStaleIde "judgementForHole" state nfp a++  TrackedStale asts amapping  <- stale 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+      binds <- stale GetBindings+      tcg@(TrackedStale tcg_t tcg_map)+          <- fmap (fmap tmrTypechecked)+           $ stale TypeCheck +      hscenv <- stale GhcSessionDeps+       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf+       new_rss <- liftMaybe $ mapAgeTo amapping rss+      tcg_rss <- liftMaybe $ mapAgeFrom tcg_map new_rss        -- KnownThings is just the instances in scope. There are no ranges       -- involved, so it's not crucial to track ages.@@ -193,14 +217,25 @@       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv       kt <- knownThings (untrackedStaleValue tcg) henv -      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt+      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt+      let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t        dflags <- getIdeDynflags state nfp-      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)+      pure $ HoleJudgment+        { hj_range = fmap realSrcSpanToRange new_rss+        , hj_jdg = jdg+        , hj_ctx = ctx+        , hj_dflags = dflags+        , hj_hole_sort = holeSortFor mp+        }  +holeSortFor :: Maybe T.Text -> HoleSort+holeSortFor = maybe Hole Metaprogram++ mkJudgementAndContext-    :: FeatureSet+    :: Config     -> Type     -> TrackedStale Bindings     -> Tracked 'Current RealSrcSpan@@ -208,12 +243,12 @@     -> ExternalPackageState     -> KnownThings     -> Maybe (Judgement, Context)-mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do+mkJudgementAndContext cfg 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+      ctx = mkContext cfg               (mapMaybe (sequenceA . (occName *** coerce))                 $ unTrack                 $ getDefiningBindings <$> binds <*> binds_rss)@@ -227,10 +262,12 @@                $ 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+      subst = ts_unifier $ evidenceToSubst evidence defaultTacticState   pure $     ( disallowing AlreadyDestructed already_destructed-    $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement+    $ fmap (CType . substTyAddInScope subst . unCType) $+        mkFirstJudgement+          ctx           (local_hy <> cls_hy)           (isRhsHole tcg_rss tcs)           g@@ -267,8 +304,12 @@         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+        occ <- (either (const Nothing) (Just . occName) =<<)+             . listToMaybe+             . S.toList+             . M.keysSet+             $ nodeIdentifiers info+        guard $ isHole occ         pure (unsafeCopyAge r $ nodeSpan ast', ty)  @@ -500,7 +541,7 @@               )    action $ do-    files <- getFilesOfInterest+    files <- getFilesOfInterestUntracked     void $ uses WriteDiagnostics $ Map.keys files  @@ -513,4 +554,69 @@     "Hole"     (Just $ List [DtUnnecessary])     Nothing+++------------------------------------------------------------------------------+-- | Transform a 'Graft' over the AST into a 'WorkspaceEdit'.+mkWorkspaceEdits+    :: DynFlags+    -> ClientCapabilities+    -> Uri+    -> Annotated ParsedSource+    -> Graft (Either String) ParsedSource+    -> Either UserFacingMessage WorkspaceEdit+mkWorkspaceEdits dflags ccs uri pm g = do+  let pm' = runIdentity $ transformA pm annotateMetaprograms+  let response = transform dflags ccs uri g pm'+   in first (InfrastructureError . T.pack) response+++------------------------------------------------------------------------------+-- | Add ExactPrint annotations to every metaprogram in the source tree.+-- Usually the ExactPrint module can do this for us, but we've enabled+-- QuasiQuotes, so the round-trip print/parse journey will crash.+annotateMetaprograms :: Data a => a -> Transform a+annotateMetaprograms = everywhereM $ mkM $ \case+  L ss (WingmanMetaprogram mp) -> do+    let x = L ss $ MetaprogramSyntax mp+    let anns = addAnnotationsForPretty [] x mempty+    modifyAnnsT $ mappend anns+    pure x+  (x :: LHsExpr GhcPs) -> pure x+++------------------------------------------------------------------------------+-- | Find the source of a tactic metaprogram at the given span.+getMetaprogramAtSpan+    :: Tracked age SrcSpan+    -> Tracked age TcGblEnv+    -> Maybe T.Text+getMetaprogramAtSpan (unTrack -> ss)+  = fmap snd+  . listToMaybe+  . metaprogramQ ss+  . tcg_binds+  . unTrack+++------------------------------------------------------------------------------+-- | The metaprogram parser needs the ability to lookup terms from the module+-- and imports. The 'ParserContext' contains everything we need to find that+-- stuff.+getParserState+    :: IdeState+    -> NormalizedFilePath+    -> Context+    -> MaybeT IO ParserContext+getParserState state nfp ctx = do+  let stale a = runStaleIde "getParserState" state nfp a++  TrackedStale (unTrack -> tcmod) _  <- stale TypeCheck+  TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps++  let tcgblenv = tmrTypechecked tcmod+      modul = extractModule tcgblenv+      rdrenv = tcg_rdr_env tcgblenv++  pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx 

@@ -0,0 +1,89 @@+{-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE OverloadedStrings     #-}++{-# LANGUAGE NoMonoLocalBinds  #-}+{-# LANGUAGE RankNTypes #-}++module Wingman.LanguageServer.Metaprogram+  ( hoverProvider+  ) where++import           Control.Applicative (empty)+import           Control.Monad+import           Control.Monad.Reader (runReaderT)+import           Control.Monad.Trans+import           Control.Monad.Trans.Maybe+import           Data.List (find)+import           Data.Maybe+import qualified Data.Text as T+import           Data.Traversable+import           Development.IDE (positionToRealSrcLoc)+import           Development.IDE (realSrcSpanToRange)+import           Development.IDE.Core.RuleTypes+import           Development.IDE.Core.Shake (IdeState (..))+import           Development.IDE.Core.UseStale+import           Development.IDE.GHC.Compat+import           GhcPlugins (containsSpan, realSrcLocSpan)+import           Ide.Types+import           Language.LSP.Types+import           Prelude hiding (span)+import           Prelude hiding (span)+import           TcRnTypes (tcg_binds)+import           Wingman.GHC+import           Wingman.Judgements.SYB (metaprogramQ)+import           Wingman.LanguageServer+import           Wingman.Metaprogramming.Parser (attempt_it)+import           Wingman.Types+++------------------------------------------------------------------------------+-- | Provide the "empty case completion" code lens+hoverProvider :: PluginMethodHandler IdeState TextDocumentHover+hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurrent -> pos) _)+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do+      let loc = fmap (realSrcLocSpan . positionToRealSrcLoc nfp) pos++      cfg <- getTacticConfig plId+      liftIO $ fromMaybeT (Right Nothing) $ do+        holes <- getMetaprogramsAtSpan state nfp $ RealSrcSpan $ unTrack loc++        fmap (Right . Just) $+          case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of+            Just (trss, program) -> do+              let tr_range = fmap realSrcSpanToRange trss+              HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg+              ps <- getParserState state nfp ctx+              z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program+              pure $ Hover+                { _contents = HoverContents+                            $ MarkupContent MkMarkdown+                            $ either T.pack T.pack z+                , _range = Just $ unTrack tr_range+                }+            Nothing -> empty+hoverProvider _ _ _ = pure $ Right Nothing+++fromMaybeT :: Functor m => a -> MaybeT m a -> m a+fromMaybeT def = fmap (fromMaybe def) . runMaybeT+++getMetaprogramsAtSpan+    :: IdeState+    -> NormalizedFilePath+    -> SrcSpan+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]+getMetaprogramsAtSpan state nfp ss = do+    let stale a = runStaleIde "getMetaprogramsAtSpan" state nfp a++    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck++    let scrutinees = traverse (metaprogramQ ss . tcg_binds) tcg+    for scrutinees $ \aged@(unTrack -> (ss, program)) -> do+      case ss of+        RealSrcSpan r   -> do+          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r+          pure (rss', program)+        UnhelpfulSpan _ -> empty++

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP               #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards   #-} @@ -7,14 +8,14 @@   , tcCommandId   , TacticParams (..)   , TacticProviderData (..)+  , useNameFromHypothesis   ) where  import           Control.Monad-import           Control.Monad.Error.Class (MonadError (throwError))+import           Control.Monad.Reader (runReaderT) 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@@ -29,27 +30,31 @@ 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.Machinery (useNameFromHypothesis)+import           Wingman.Metaprogramming.Lexer (ParserContext)+import           Wingman.Metaprogramming.Parser (parseMetaprogram) 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+commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ())+commandTactic _ Auto                   = pure . const auto+commandTactic _ Intros                 = pure . const intros+commandTactic _ Destruct               = pure . useNameFromHypothesis destruct . mkVarOcc . T.unpack+commandTactic _ DestructPun            = pure . useNameFromHypothesis destructPun . mkVarOcc . T.unpack+commandTactic _ Homomorphism           = pure . useNameFromHypothesis homo . mkVarOcc . T.unpack+commandTactic _ DestructLambdaCase     = pure . const destructLambdaCase+commandTactic _ HomomorphismLambdaCase = pure . const homoLambdaCase+commandTactic _ DestructAll            = pure . const destructAll+commandTactic _ UseDataCon             = pure . userSplit . mkVarOcc . T.unpack+commandTactic _ Refine                 = pure . const refine+commandTactic _ BeginMetaprogram       = pure . const metaprogram+commandTactic c RunMetaprogram         = flip runReaderT c . parseMetaprogram   ------------------------------------------------------------------------------@@ -58,12 +63,15 @@ tacticKind Auto                   = "fillHole" tacticKind Intros                 = "introduceLambda" tacticKind Destruct               = "caseSplit"+tacticKind DestructPun            = "caseSplitPun" tacticKind Homomorphism           = "homomorphicCaseSplit" tacticKind DestructLambdaCase     = "lambdaCase" tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase" tacticKind DestructAll            = "splitFuncArgs" tacticKind UseDataCon             = "useConstructor" tacticKind Refine                 = "refine"+tacticKind BeginMetaprogram       = "beginMetaprogram"+tacticKind RunMetaprogram         = "runMetaprogram"   ------------------------------------------------------------------------------@@ -73,12 +81,15 @@ tacticPreferred Auto                   = True tacticPreferred Intros                 = True tacticPreferred Destruct               = True+tacticPreferred DestructPun            = False tacticPreferred Homomorphism           = False tacticPreferred DestructLambdaCase     = False tacticPreferred HomomorphismLambdaCase = False tacticPreferred DestructAll            = True tacticPreferred UseDataCon             = True tacticPreferred Refine                 = True+tacticPreferred BeginMetaprogram       = False+tacticPreferred RunMetaprogram         = True   mkTacticKind :: TacticCommand -> CodeActionKind@@ -90,49 +101,77 @@ -- | 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 Auto  =+  requireHoleSort (== Hole) $+  provide Auto "" commandProvider Intros =+  requireHoleSort (== Hole) $   filterGoalType isFunction $     provide Intros "" commandProvider Destruct =+  requireHoleSort (== Hole) $   filterBindingType destructFilter $ \occ _ ->     provide Destruct $ T.pack $ occNameString occ+commandProvider DestructPun =+  requireHoleSort (== Hole) $+    filterBindingType destructPunFilter $ \occ _ ->+      provide DestructPun $ T.pack $ occNameString occ commandProvider Homomorphism =+  requireHoleSort (== Hole) $   filterBindingType homoFilter $ \occ _ ->     provide Homomorphism $ T.pack $ occNameString occ commandProvider DestructLambdaCase =+  requireHoleSort (== Hole) $   requireExtension LambdaCase $     filterGoalType (isJust . lambdaCaseable) $       provide DestructLambdaCase "" commandProvider HomomorphismLambdaCase =+  requireHoleSort (== Hole) $   requireExtension LambdaCase $     filterGoalType ((== Just True) . lambdaCaseable) $       provide HomomorphismLambdaCase "" commandProvider DestructAll =-  requireFeature FeatureDestructAll $+  requireHoleSort (== Hole) $     withJudgement $ \jdg ->       case _jIsTopHole jdg && jHasBoundArgs jdg of         True  -> provide DestructAll ""         False -> mempty commandProvider UseDataCon =+  requireHoleSort (== Hole) $   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+    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 $+  requireHoleSort (== Hole) $     provide Refine ""+commandProvider BeginMetaprogram =+  requireGHC88OrHigher $+  requireHoleSort (== Hole) $+    provide BeginMetaprogram ""+commandProvider RunMetaprogram =+  requireGHC88OrHigher $+  withMetaprogram $ \mp ->+    provide RunMetaprogram mp  +requireGHC88OrHigher :: TacticProvider -> TacticProvider+requireGHC88OrHigher tp tpd =+#if __GLASGOW_HASKELL__ >= 808+  tp tpd+#else+  mempty+#endif++ ------------------------------------------------------------------------------ -- | Return an empty list if the given predicate doesn't hold over the length guardLength :: (Int -> Bool) -> [a] -> [a]@@ -146,6 +185,7 @@      = TacticProviderData     -> IO [Command |? CodeAction] + data TacticProviderData = TacticProviderData   { tpd_dflags :: DynFlags   , tpd_config :: Config@@ -153,6 +193,7 @@   , tpd_uri    :: Uri   , tpd_range  :: Tracked 'Current Range   , tpd_jdg    :: Judgement+  , tpd_hole_sort :: HoleSort   }  @@ -165,16 +206,19 @@   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+requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider+requireHoleSort p tp tpd =+  case p $ tpd_hole_sort tpd of     True  -> tp tpd     False -> pure [] +withMetaprogram :: (T.Text -> TacticProvider) -> TacticProvider+withMetaprogram tp tpd =+  case tpd_hole_sort tpd of+    Metaprogram mp -> tp mp tpd+    _ -> pure [] + ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal.@@ -238,19 +282,7 @@ 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@@ -293,4 +325,13 @@ destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _                          = False+++------------------------------------------------------------------------------+-- | We should show destruct punning for bindings only when those bindings have+-- usual algebraic types, and when any of their data constructors are records.+destructPunFilter :: Type -> Type -> Bool+destructPunFilter _ (algebraicTyCon -> Just tc) =+  any (not . null . dataConFieldLabels) $ tyConDataCons tc+destructPunFilter _ _                          = False 

@@ -3,11 +3,12 @@ module Wingman.Machinery where  import           Class (Class (classTyVars))+import           Control.Applicative (empty) import           Control.Lens ((<>~)) import           Control.Monad.Error.Class import           Control.Monad.Reader import           Control.Monad.State.Class (gets, modify)-import           Control.Monad.State.Strict (StateT (..))+import           Control.Monad.State.Strict (StateT (..), execStateT) import           Data.Bool (bool) import           Data.Coerce import           Data.Either@@ -22,13 +23,15 @@ import           Data.Ord (Down (..), comparing) import           Data.Set (Set) import qualified Data.Set as S+import           Development.IDE.Core.Compile (lookupName) import           Development.IDE.GHC.Compat-import           OccName (HasOccName (occName))+import           GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType)+import           OccName (HasOccName (occName), OccEnv) import           Refinery.ProofState import           Refinery.Tactic import           Refinery.Tactic.Internal import           TcType-import           Type+import           Type (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe) import           Unify import           Wingman.Judgements import           Wingman.Simplify (simplify)@@ -46,12 +49,19 @@     :: Judgement     -> Rule newSubgoal j = do-    unifier <- gets ts_unifier-    subgoal-      $ substJdg unifier-      $ unsetIsTopHole j+  ctx <- ask+  unifier <- gets ts_unifier+  subgoal+    $ normalizeJudgement ctx+    $ substJdg unifier+    $ unsetIsTopHole+    $ normalizeJudgement ctx j  +tacticToRule :: Judgement -> TacticsM () -> Rule+tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom++ ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic.@@ -82,11 +92,12 @@               flip sortBy solns $ comparing $ \(ext, (_, holes)) ->                 Down $ scoreSolution ext jdg holes         case sorted of-          ((syn, _) : _) ->+          ((syn, (_, subgoals)) : _) ->             Right $               RunTacticResults-                { rtr_trace = syn_trace syn-                , rtr_extract = simplify $ syn_val syn+                { rtr_trace    = syn_trace syn+                , rtr_extract  = simplify $ syn_val syn+                , rtr_subgoals = subgoals                 , rtr_other_solns = reverse . fmap fst $ sorted                 , rtr_jdg = jdg                 , rtr_ctx = ctx@@ -297,4 +308,69 @@     => TacticT jdg ext err s m ()     -> TacticT jdg ext err s m () try' t = commit t $ pure ()+++------------------------------------------------------------------------------+-- | Sorry leaves a hole in its extract+exact :: HsExpr GhcPs -> TacticsM ()+exact = rule . const . pure . pure . noLoc++------------------------------------------------------------------------------+-- | 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++------------------------------------------------------------------------------+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to+-- look it up in the hypothesis.+useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a+useNameFromContext f name = do+  lookupNameInContext name >>= \case+    Just ty -> f $ createImportedHyInfo name ty+    Nothing -> throwError $ NotInScope name+++------------------------------------------------------------------------------+-- | Find the type of an 'OccName' that is defined in the current module.+lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType)+lookupNameInContext name = do+  ctx <- asks ctxModuleFuncs+  pure $ case find ((== name) . fst) ctx of+    Just (_, ty) -> pure ty+    Nothing      -> empty+++------------------------------------------------------------------------------+-- | Build a 'HyInfo' for an imported term.+createImportedHyInfo :: OccName -> CType -> HyInfo CType+createImportedHyInfo on ty = HyInfo+  { hi_name = on+  , hi_provenance = ImportPrv+  , hi_type = ty+  }+++------------------------------------------------------------------------------+-- | Lookup the type of any 'OccName' that was imported. Necessarily done in+-- IO, so we only expose this functionality to the parser. Internal Haskell+-- code that wants to lookup terms should do it via 'KnownThings'.+getOccNameType+    :: HscEnv+    -> OccEnv [GlobalRdrElt]+    -> Module+    -> OccName+    -> IO (Maybe Type)+getOccNameType hscenv rdrenv modul occ =+  case lookupOccEnv rdrenv occ of+    Just (elt : _) -> do+      mvar <- lookupName hscenv modul $ gre_name elt+      pure $ case mvar of+        Just (AnId v) -> pure $ varType v+        _ -> Nothing+    _ -> pure Nothing 

@@ -0,0 +1,85 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications  #-}++module Wingman.Metaprogramming.Lexer where++import           Control.Applicative+import           Control.Monad+import           Control.Monad.Reader (ReaderT)+import           Data.Text (Text)+import qualified Data.Text as T+import           Data.Void+import           Development.IDE.GHC.Compat (HscEnv, Module)+import           GhcPlugins (GlobalRdrElt)+import           Name+import qualified Text.Megaparsec as P+import qualified Text.Megaparsec.Char as P+import qualified Text.Megaparsec.Char.Lexer as L+import Wingman.Types (Context)+++------------------------------------------------------------------------------+-- | Everything we need in order to call 'Wingman.Machinery.getOccNameType'.+data ParserContext = ParserContext+  { ps_hscEnv :: HscEnv+  , ps_occEnv :: OccEnv [GlobalRdrElt]+  , ps_module :: Module+  , ps_context :: Context+  }++type Parser = P.ParsecT Void Text (ReaderT ParserContext IO)++++lineComment :: Parser ()+lineComment = L.skipLineComment "--"++blockComment :: Parser ()+blockComment = L.skipBlockComment "{-" "-}"++sc :: Parser ()+sc = L.space P.space1 lineComment blockComment++ichar :: Parser Char+ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\''++lexeme :: Parser a -> Parser a+lexeme = L.lexeme sc++symbol :: Text -> Parser Text+symbol = L.symbol sc++symbol_ :: Text -> Parser ()+symbol_ = void . symbol++brackets :: Parser a -> Parser a+brackets = P.between (symbol "[") (symbol "]")++braces :: Parser a -> Parser a+braces = P.between (symbol "{") (symbol "}")++parens :: Parser a -> Parser a+parens = P.between (symbol "(") (symbol ")")++identifier :: Text -> Parser ()+identifier i = lexeme (P.string i *> P.notFollowedBy ichar)++-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list+variable :: Parser OccName+variable = lexeme $ do+    c <- P.alphaNumChar+    cs <- P.many ichar+    pure $ mkVarOcc (c:cs)++-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list+name :: Parser Text+name = lexeme $ do+    c <- P.alphaNumChar+    cs <- P.many (ichar <|> P.char '-')+    pure $ T.pack (c:cs)++keyword :: Text -> Parser ()+keyword = identifier+

@@ -0,0 +1,434 @@+{-# LANGUAGE DataKinds         #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications  #-}++module Wingman.Metaprogramming.Parser where++import qualified Control.Monad.Combinators.Expr as P+import qualified Control.Monad.Error.Class as E+import           Control.Monad.Reader (ReaderT, ask, MonadIO (liftIO), asks)+import           Data.Functor+import           Data.Maybe (listToMaybe)+import qualified Data.Text as T+import           GhcPlugins (occNameString)+import qualified Refinery.Tactic as R+import qualified Text.Megaparsec as P+import           Wingman.Auto+import           Wingman.Context (getCurrentDefinitions)+import           Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext)+import           Wingman.Metaprogramming.Lexer+import           Wingman.Metaprogramming.Parser.Documentation+import           Wingman.Metaprogramming.ProofState (proofState, layout)+import           Wingman.Tactics+import           Wingman.Types+++nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())+nullary name tac = identifier name $> tac+++unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())+unary_occ name tac = tac <$> (identifier name *> variable)+++------------------------------------------------------------------------------+-- | Like 'unary_occ', but runs directly in the 'Parser' monad.+unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())+unary_occM name tac = tac =<< (identifier name *> variable)+++variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())+variadic_occ name tac = tac <$> (identifier name *> P.many variable)+++commands :: [SomeMetaprogramCommand]+commands =+  [ command "assumption" Nondeterministic Nullary+      "Use any term in the hypothesis that can unify with the current goal."+      (pure assumption)+      [ Example+          Nothing+          []+          [EHI "some_a_val" "a"]+          (Just "a")+          "some_a_val"+      ]++  , command "assume" Deterministic (Ref One)+      "Use the given term from the hypothesis, unifying it with the current goal"+      (pure . assume)+      [ Example+          Nothing+          ["some_a_val"]+          [EHI "some_a_val" "a"]+          (Just "a")+          "some_a_val"+      ]++  , command "intros" Deterministic (Bind Many)+      ( mconcat+          [ "Construct a lambda expression, using the specific names if given, "+          , "generating unique names otherwise. When no arguments are given, "+          , "all of the function arguments will be bound; otherwise, this "+          , "tactic will bind only enough to saturate the given names. Extra "+          , "names are ignored."+          ])+      (pure . \case+        []    -> intros+        names -> intros' $ Just names+      )+      [ Example+          Nothing+          []+          []+          (Just "a -> b -> c -> d")+          "\\a b c -> (_ :: d)"+      , Example+          Nothing+          ["aye"]+          []+          (Just "a -> b -> c -> d")+          "\\aye -> (_ :: b -> c -> d)"+      , Example+          Nothing+          ["x", "y", "z", "w"]+          []+          (Just "a -> b -> c -> d")+          "\\x y z -> (_ :: d)"+      ]++  , command "intro" Deterministic (Bind One)+      "Construct a lambda expression, binding an argument with the given name."+      (pure . intros' . Just . pure)+      [ Example+          Nothing+          ["aye"]+          []+          (Just "a -> b -> c -> d")+          "\\aye -> (_ :: b -> c -> d)"+      ]++  , command "destruct_all" Deterministic Nullary+      "Pattern match on every function paramater, in original binding order."+      (pure destructAll)+      [ Example+          (Just "Assume `a` and `b` were bound via `f a b = _`.")+          []+          [EHI "a" "Bool", EHI "b" "Maybe Int"]+          Nothing $+          T.pack $ init $ unlines+            [ "case a of"+            , "  False -> case b of"+            , "    Nothing -> _"+            , "    Just i -> _"+            , "  True -> case b of"+            , "    Nothing -> _"+            , "    Just i -> _"+            ]+      ]++  , command "destruct" Deterministic (Ref One)+      "Pattern match on the argument."+      (pure . useNameFromHypothesis destruct)+      [ Example+          Nothing+          ["a"]+          [EHI "a" "Bool"]+          Nothing $+          T.pack $ init $ unlines+            [ "case a of"+            , "  False -> _"+            , "  True -> _"+            ]+      ]++  , command "homo" Deterministic (Ref One)+      ( mconcat+        [ "Pattern match on the argument, and fill the resulting hole in with "+        , "the same data constructor."+        ])+      (pure . useNameFromHypothesis homo)+      [ Example+          (Just $ mconcat+            [ "Only applicable when the type constructor of the argument is "+            , "the same as that of the hole."+            ])+          ["e"]+          [EHI "e" "Either a b"]+          (Just "Either x y") $+          T.pack $ init $ unlines+            [ "case e of"+            , "  Left a -> Left (_ :: x)"+            , "  Right b -> Right (_ :: y)"+            ]+      ]++  , command "application" Nondeterministic Nullary+      "Apply any function in the hypothesis that returns the correct type."+      (pure application)+      [ Example+          Nothing+          []+          [EHI "f" "a -> b"]+          (Just "b")+          "f (_ :: a)"+      ]++  , command "apply" Deterministic (Ref One)+      "Apply the given function from *local* scope."+      (pure . useNameFromHypothesis apply)+      [ Example+          Nothing+          ["f"]+          [EHI "f" "a -> b"]+          (Just "b")+          "f (_ :: a)"+      ]++  , command "split" Nondeterministic Nullary+      "Produce a data constructor for the current goal."+      (pure split)+      [ Example+          Nothing+          []+          []+          (Just "Either a b")+          "Right (_ :: b)"+      ]++  , command "ctor" Deterministic (Ref One)+      "Use the given data cosntructor."+      (pure . userSplit)+      [ Example+          Nothing+          ["Just"]+          []+          (Just "Maybe a")+          "Just (_ :: a)"+      ]++  , command "obvious" Nondeterministic Nullary+      "Produce a nullary data constructor for the current goal."+      (pure obvious)+      [ Example+          Nothing+          []+          []+          (Just "[a]")+          "[]"+      ]++  , command "auto" Nondeterministic Nullary+      ( mconcat+          [ "Repeatedly attempt to split, destruct, apply functions, and "+          , "recurse in an attempt to fill the hole."+          ])+      (pure auto)+      [ Example+          Nothing+          []+          [EHI "f" "a -> b", EHI "g" "b -> c"]+          (Just "a -> c")+          "g . f"+      ]++  , command "sorry" Deterministic Nullary+      "\"Solve\" the goal by leaving a hole."+      (pure sorry)+      [ Example+          Nothing+          []+          []+          (Just "b")+          "_ :: b"+      ]++  , command "unary" Deterministic Nullary+      ( mconcat+        [ "Produce a hole for a single-parameter function, as well as a hole for "+        , "its argument. The argument holes are completely unconstrained, and "+        , "will be solved before the function."+        ])+      (pure $ nary 1)+      [ Example+          (Just $ mconcat+            [ "In the example below, the variable `a` is free, and will unify "+            , "to the resulting extract from any subsequent tactic."+            ])+          []+          []+          (Just "Int")+          "(_2 :: a -> Int) (_1 :: a)"+      ]++  , command "binary" Deterministic Nullary+      ( mconcat+        [ "Produce a hole for a two-parameter function, as well as holes for "+        , "its arguments. The argument holes have the same type but are "+        , "otherwise unconstrained, and will be solved before the function."+        ])+      (pure $ nary 2)+      [ Example+          (Just $ mconcat+            [ "In the example below, the variable `a` is free, and will unify "+            , "to the resulting extract from any subsequent tactic."+            ])+          []+          []+          (Just "Int")+          "(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)"+      ]++  , command "recursion" Deterministic Nullary+      "Fill the current hole with a call to the defining function."+      ( pure $+          fmap listToMaybe getCurrentDefinitions >>= \case+            Just (self, _) -> useNameFromContext apply self+            Nothing -> E.throwError $ TacticPanic "no defining function"+      )+      [ Example+          (Just "In the context of `foo (a :: Int) (b :: b) = _`:")+          []+          []+          Nothing+          "foo (_ :: Int) (_ :: b)"+      ]++  , command "use" Deterministic (Ref One)+      "Apply the given function from *module* scope."+      ( \occ -> do+          ctx <- asks ps_context+          ty <- case lookupNameInContext occ ctx of+            Just ty -> pure ty+            Nothing -> CType <$> getOccTy occ+          pure $ apply $ createImportedHyInfo occ ty+      )+      [ Example+          (Just "`import Data.Char (isSpace)`")+          ["isSpace"]+          []+          (Just "Bool")+          "isSpace (_ :: Char)"+      ]++  , command "cata" Deterministic (Ref One)+      "Destruct the given term, recursing on every resulting binding."+      (pure . useNameFromHypothesis cata)+      [ Example+          (Just "Assume we're called in the context of a function `f.`")+          ["x"]+          [EHI "x" "(a, a)"]+          Nothing $+          T.pack $ init $ unlines+            [ "case x of"+            , "  (a1, a2) ->"+            , "    let a1_c = f a1"+            , "        a2_c = f a2"+            , "     in _"+            ]+      ]++  , command "collapse" Deterministic Nullary+      "Collapse every term in scope with the same type as the goal."+      (pure collapse)+      [ Example+          Nothing+          []+          [ EHI "a1" "a"+          , EHI "a2" "a"+          , EHI "a3" "a"+          ]+          (Just "a")+          "(_ :: a -> a -> a -> a) a1 a2 a3"+      ]++  ]++++oneTactic :: Parser (TacticsM ())+oneTactic =+  P.choice+    [ parens tactic+    , makeParser commands+    ]+++tactic :: Parser (TacticsM ())+tactic = flip P.makeExprParser operators oneTactic++bindOne :: TacticsM a -> TacticsM a -> TacticsM a+bindOne t t1 = t R.<@> [t1]++operators :: [[P.Operator Parser (TacticsM ())]]+operators =+    [ [ P.Prefix (symbol "*"   $> R.many_) ]+    , [ P.Prefix (symbol "try" $> R.try) ]+    , [ P.InfixR (symbol "|"   $> (R.<%>) )]+    , [ P.InfixL (symbol ";"   $> (>>))+      , P.InfixL (symbol ","   $> bindOne)+      ]+    ]+++tacticProgram :: Parser (TacticsM ())+tacticProgram = do+  sc+  r <- tactic P.<|> pure (pure ())+  P.eof+  pure r+++wrapError :: String -> String+wrapError err = "```\n" <> err <> "\n```\n"+++------------------------------------------------------------------------------+-- | Attempt to run a metaprogram tactic, returning the proof state, or the+-- errors.+attempt_it+    :: Context+    -> Judgement+    -> String+    -> ReaderT ParserContext IO (Either String String)+attempt_it ctx jdg program =+  P.runParserT tacticProgram "<splice>" (T.pack program) <&> \case+      Left peb -> Left $ wrapError $ P.errorBundlePretty peb+      Right tt -> do+        case runTactic+              ctx+              jdg+              tt+          of+            Left tes -> Left $ wrapError $ show tes+            Right rtr -> Right $ layout $ proofState rtr+++parseMetaprogram :: T.Text -> ReaderT ParserContext IO (TacticsM ())+parseMetaprogram+    = fmap (either (const $ pure ()) id)+    . P.runParserT tacticProgram "<splice>"+++------------------------------------------------------------------------------+-- | Like 'getOccNameType', but runs in the 'Parser' monad.+getOccTy :: OccName -> Parser Type+getOccTy occ = do+  ParserContext hscenv rdrenv modul _ <- ask+  mty <- liftIO $ getOccNameType hscenv rdrenv modul occ+  maybe (fail $ occNameString occ <> " is not in scope") pure mty+++------------------------------------------------------------------------------+-- | Automatically generate the metaprogram command reference.+writeDocumentation :: IO ()+writeDocumentation =+  writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $+    unlines+      [ "# Wingman Metaprogram Command Reference"+      , ""+      , prettyReadme commands+      ]+

@@ -0,0 +1,228 @@+{-# LANGUAGE OverloadedStrings #-}++module Wingman.Metaprogramming.Parser.Documentation where++import           Data.Functor ((<&>))+import           Data.List (sortOn)+import           Data.String (IsString)+import           Data.Text (Text)+import           Data.Text.Prettyprint.Doc+import           Data.Text.Prettyprint.Doc.Render.String (renderString)+import           GhcPlugins (OccName)+import qualified Text.Megaparsec as P+import           Wingman.Metaprogramming.Lexer (Parser, identifier, variable)+import           Wingman.Types (TacticsM)+++------------------------------------------------------------------------------+-- | Is a tactic deterministic or not?+data Determinism+  = Deterministic+  | Nondeterministic++prettyDeterminism :: Determinism -> Doc b+prettyDeterminism Deterministic = "deterministic"+prettyDeterminism Nondeterministic = "non-deterministic"+++------------------------------------------------------------------------------+-- | How many arguments does the tactic take?+data Count a where+  One  :: Count OccName+  Many :: Count [OccName]++prettyCount :: Count a -> Doc b+prettyCount One  = "single"+prettyCount Many = "varadic"+++------------------------------------------------------------------------------+-- | What sorts of arguments does the tactic take? Currently there is no+-- distincion between 'Ref' and 'Bind', other than documentation.+--+-- The type index here is used for the shape of the function the parser should+-- take.+data Syntax a where+  Nullary :: Syntax (Parser (TacticsM ()))+  Ref     :: Count a -> Syntax (a -> Parser (TacticsM ()))+  Bind    :: Count a -> Syntax (a -> Parser (TacticsM ()))++prettySyntax :: Syntax a -> Doc b+prettySyntax Nullary   = "none"+prettySyntax (Ref co)  = prettyCount co <+> "reference"+prettySyntax (Bind co) = prettyCount co <+> "binding"+++------------------------------------------------------------------------------+-- | An example for the documentation.+data Example = Example+  { ex_ctx    :: Maybe Text         -- ^ Specific context information about when the tactic is applicable+  , ex_args   :: [Var]              -- ^ Arguments the tactic was called with+  , ex_hyp    :: [ExampleHyInfo]    -- ^ The hypothesis+  , ex_goal   :: Maybe ExampleType  -- ^ Current goal. Nothing indicates it's uninteresting.+  , ex_result :: Text               -- ^ Resulting extract.+  }+++------------------------------------------------------------------------------+-- | An example 'HyInfo'.+data ExampleHyInfo = EHI+  { ehi_name :: Var          -- ^ Name of the variable+  , ehi_type :: ExampleType  -- ^ Type of the variable+  }+++------------------------------------------------------------------------------+-- | A variable+newtype Var = Var+  { getVar :: Text+  }+  deriving newtype (IsString, Pretty)+++------------------------------------------------------------------------------+-- | A type+newtype ExampleType = ExampleType+  { getExampleType :: Text+  }+  deriving newtype (IsString, Pretty)+++------------------------------------------------------------------------------+-- | A command to expose to the parser+data MetaprogramCommand a = MC+  { mpc_name        :: Text         -- ^ Name of the command. This is the token necessary to run the command.+  , mpc_syntax      :: Syntax a     -- ^ The command's arguments+  , mpc_det         :: Determinism  -- ^ Determinism of the command+  , mpc_description :: Text         -- ^ User-facing description+  , mpc_tactic      :: a            -- ^ Tactic to run+  , mpc_examples    :: [Example]    -- ^ Collection of documentation examples+  }++------------------------------------------------------------------------------+-- | Existentialize the pain away+data SomeMetaprogramCommand where+  SMC :: MetaprogramCommand a -> SomeMetaprogramCommand+++------------------------------------------------------------------------------+-- | Run the 'Parser' of a 'MetaprogramCommand'+makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())+makeMPParser (MC name Nullary _ _ tactic _) = do+  identifier name+  tactic+makeMPParser (MC name (Ref One) _ _ tactic _) = do+  identifier name+  variable >>= tactic+makeMPParser (MC name (Ref Many) _ _ tactic _) = do+  identifier name+  P.many variable >>= tactic+makeMPParser (MC name (Bind One) _ _ tactic _) = do+  identifier name+  variable >>= tactic+makeMPParser (MC name (Bind Many) _ _ tactic _) = do+  identifier name+  P.many variable >>= tactic+++------------------------------------------------------------------------------+-- | Compile a collection of metaprogram commands into a parser.+makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ())+makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp+++------------------------------------------------------------------------------+-- | Pretty print a command.+prettyCommand :: MetaprogramCommand a -> Doc b+prettyCommand (MC name syn det desc _ exs) = vsep+  [ "##" <+> pretty name+  , mempty+  , "arguments:" <+> prettySyntax syn <> ".  "+  , prettyDeterminism det <> "."+  , mempty+  , ">" <+> align (pretty desc)+  , mempty+  , vsep $ fmap (prettyExample name) exs+  ]+++------------------------------------------------------------------------------+-- | Pretty print a hypothesis.+prettyHyInfo :: ExampleHyInfo -> Doc a+prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi)+++------------------------------------------------------------------------------+-- | Append the given term only if the first argument has elements.+mappendIfNotNull :: [a] -> a -> [a]+mappendIfNotNull [] _ = []+mappendIfNotNull as a = as <> [a]+++------------------------------------------------------------------------------+-- | Pretty print an example.+prettyExample :: Text -> Example -> Doc a+prettyExample name (Example m_txt args hys goal res) =+  align $ vsep+    [ mempty+    , "### Example"+    , maybe mempty ((line <>) . (<> line) . (">" <+>) . align . pretty) m_txt+    , "Given:"+    , mempty+    , codeFence $ vsep+        $ mappendIfNotNull (fmap prettyHyInfo hys) mempty+           <> [ "_" <+> maybe mempty (("::" <+>). pretty) goal+              ]+    , mempty+    , hsep+        [ "running "+        , enclose "`" "`" $ pretty name <> hsep (mempty : fmap pretty args)+        , "will produce:"+        ]+    , mempty+    , codeFence $ align $ pretty res+    ]+++------------------------------------------------------------------------------+-- | Make a haskell code fence.+codeFence :: Doc a -> Doc a+codeFence d = align $ vsep+  [ "```haskell"+  , d+  , "```"+  ]+++------------------------------------------------------------------------------+-- | Render all of the commands.+prettyReadme :: [SomeMetaprogramCommand] -> String+prettyReadme+  = renderString+  . layoutPretty defaultLayoutOptions+  . vsep+  . fmap (\case SMC c -> prettyCommand c)+  . sortOn (\case SMC c -> mpc_name c)++++------------------------------------------------------------------------------+-- | Helper function to build a 'SomeMetaprogramCommand'.+command+    :: Text+    -> Determinism+    -> Syntax a+    -> Text+    -> a+    -> [Example]+    -> SomeMetaprogramCommand+command txt det syn txt' a exs = SMC $+  MC+    { mpc_name        = txt+    , mpc_det         = det+    , mpc_syntax      = syn+    , mpc_description = txt'+    , mpc_tactic      = a+    , mpc_examples    = exs+    }+

@@ -0,0 +1,113 @@+{-# LANGUAGE NamedFieldPuns    #-}+{-# LANGUAGE OverloadedStrings #-}++module Wingman.Metaprogramming.ProofState where++import           Data.Bool (bool)+import           Data.Functor ((<&>))+import qualified Data.Text as T+import           Data.Text.Prettyprint.Doc+import           Data.Text.Prettyprint.Doc.Render.Util.Panic+import           Language.LSP.Types (sectionSeparator)+import           Wingman.Judgements (jHypothesis)+import           Wingman.Types++renderSimplyDecorated+    :: Monoid out+    => (T.Text -> out) -- ^ Render plain 'Text'+    -> (ann -> out)  -- ^ How to render an annotation+    -> (ann -> out)  -- ^ How to render the removed annotation+    -> SimpleDocStream ann+    -> out+renderSimplyDecorated text push pop = go []+  where+    go _        SFail               = panicUncaughtFail+    go []       SEmpty              = mempty+    go (_:_)    SEmpty              = panicInputNotFullyConsumed+    go st       (SChar c rest)      = text (T.singleton c) <> go st rest+    go st       (SText _l t rest)   = text t <> go st rest+    go st       (SLine i rest)      =+      text (T.singleton '\n') <> text (textSpaces i) <> go st rest+    go st       (SAnnPush ann rest) = push ann <> go (ann : st) rest+    go (ann:st) (SAnnPop rest)      = pop ann <> go st rest+    go []       SAnnPop{}           = panicUnpairedPop+{-# INLINE renderSimplyDecorated #-}+++data Ann+  = Goal+  | Hypoth+  | Status+  deriving (Eq, Ord, Show, Enum, Bounded)++forceMarkdownNewlines :: String -> String+forceMarkdownNewlines = unlines . fmap (<> "  ") . lines++layout :: Doc Ann -> String+layout+  = forceMarkdownNewlines+  . T.unpack+  . renderSimplyDecorated id+    renderAnn+    renderUnann+  . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6)++renderAnn :: Ann -> T.Text+renderAnn Goal = "<span style='color:#ef4026;'>"+renderAnn Hypoth = "```haskell\n"+renderAnn Status = "<span style='color:#6495ED;'>"++renderUnann :: Ann -> T.Text+renderUnann Goal = "</span>"+renderUnann Hypoth = "\n```\n"+renderUnann Status = "</span>"++proofState :: RunTacticResults -> Doc Ann+proofState RunTacticResults{rtr_subgoals} =+  vsep+    $ ( annotate Status+      . countFinished "goals accomplished 🎉" "goal"+      $ length rtr_subgoals+      )+    : pretty sectionSeparator+    : fmap prettySubgoal rtr_subgoals+++prettySubgoal :: Judgement -> Doc Ann+prettySubgoal jdg =+  vsep $+    [ mempty | has_hy] <>+    [ annotate Hypoth $ prettyHypothesis hy | has_hy] <>+    [ "⊢" <+> annotate Goal (prettyType (_jGoal jdg))+    , pretty sectionSeparator+    ]+  where+    hy = jHypothesis jdg+    has_hy = not $ null $ unHypothesis hy+++prettyHypothesis :: Hypothesis CType -> Doc Ann+prettyHypothesis hy =+  vsep $ unHypothesis hy <&> \hi ->+    prettyHyInfo hi++prettyHyInfo :: HyInfo CType -> Doc Ann+prettyHyInfo hi = viaShow (hi_name hi) <+> "::" <+> prettyType (hi_type hi)+++prettyType :: CType -> Doc Ann+prettyType (CType ty) = viaShow ty+++countFinished :: Doc Ann -> Doc Ann -> Int -> Doc Ann+countFinished finished _ 0 = finished+countFinished _ thing n    = count thing n++count :: Doc Ann -> Int -> Doc Ann+count thing n =+  pretty n <+> thing <> bool "" "s" (n /= 1)++textSpaces :: Int -> T.Text+textSpaces n = T.replicate n $ T.singleton ' '++

@@ -1,61 +1,207 @@ module Wingman.Naming where +import           Control.Arrow import           Control.Monad.State.Strict+import           Data.Aeson (camelTo2) import           Data.Bool (bool) import           Data.Char+import           Data.List (isPrefixOf)+import           Data.List.Extra (split) import           Data.Map (Map) import qualified Data.Map as M+import           Data.Maybe (listToMaybe, fromMaybe)+import           Data.Monoid import           Data.Set (Set) import qualified Data.Set as S import           Data.Traversable+import           GhcPlugins (charTy, maybeTyCon) import           Name import           TcType+import           Text.Hyphenation (hyphenate, english_US) import           TyCon import           Type-import           TysWiredIn (listTyCon, pairTyCon, unitTyCon)+import           TysWiredIn (listTyCon, unitTyCon)+import           Wingman.GHC (tcTyVar_maybe)   --------------------------------------------------------------------------------- | 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"+-- | A classification of a variable, for which we have specific naming rules.+-- A variable can have multiple purposes simultaneously.+data Purpose+  = Function [Type] Type+  | Predicate+  | Continuation+  | Integral+  | Number+  | String+  | List Type+  | Maybe Type+  | TyConned TyCon [Type]+    -- ^ Something of the form @TC a b c@+  | TyVarred TyVar [Type]+    -- ^ Something of the form @m a b c@ +pattern IsPredicate :: Type+pattern IsPredicate <-+  (tcSplitFunTys -> ([isFunTy -> False], isBoolTy -> True)) +pattern IsFunction :: [Type] -> Type -> Type+pattern IsFunction args res <-+  (tcSplitFunTys -> (args@(_:_), res))++pattern IsString :: Type+pattern IsString <-+  (splitTyConApp_maybe -> Just ((== listTyCon) -> True, [eqType charTy -> True]))++pattern IsMaybe :: Type -> Type+pattern IsMaybe a <-+  (splitTyConApp_maybe -> Just ((== maybeTyCon) -> True, [a]))++pattern IsList :: Type -> Type+pattern IsList a <-+  (splitTyConApp_maybe -> Just ((== listTyCon) -> True, [a]))++pattern IsTyConned :: TyCon -> [Type] -> Type+pattern IsTyConned tc args <-+  (splitTyConApp_maybe -> Just (id &&& isSymOcc . getOccName -> (tc, False), args))++pattern IsTyVarred :: TyVar -> [Type] -> Type+pattern IsTyVarred v args <-+  (tcSplitAppTys -> (tcTyVar_maybe -> Just v, args))++ ------------------------------------------------------------------------------+-- | Get the 'Purpose's of a type. A type can have multiple purposes+-- simultaneously, so the order of purposes in this function corresponds to the+-- precedence of that naming rule. Which means, eg, that if a type is both+-- a 'Predicate' and a 'Function', we should prefer to use the predicate naming+-- rules, since they come first.+getPurposes :: Type -> [Purpose]+getPurposes ty = mconcat+  [ [ Predicate         | IsPredicate         <- [ty] ]+  , [ Function args res | IsFunction args res <- [ty] ]+  , with (isIntegerTy ty) [ Integral, Number          ]+  , with (isIntTy ty)     [ Integral, Number          ]+  , [ Number            | isFloatingTy ty             ]+  , [ String            | isStringTy ty               ]+  , [ Maybe a           | IsMaybe a           <- [ty] ]+  , [ List a            | IsList a            <- [ty] ]+  , [ TyVarred v args   | IsTyVarred v args   <- [ty] ]+  , [ TyConned tc args  | IsTyConned tc args  <- [ty]+                        , not (isTupleTyCon tc)+                        , tc /= listTyCon             ]+  ]+++------------------------------------------------------------------------------+-- | Return 'mempty' if the give bool is false.+with :: Monoid a => Bool -> a -> a+with False _ = mempty+with True a = a+++------------------------------------------------------------------------------+-- | Names we can give functions+functionNames :: [String]+functionNames = ["f", "g", "h"]+++------------------------------------------------------------------------------+-- | Get a ranked ordering of names for a given purpose.+purposeToName :: Purpose -> [String]+purposeToName (Function args res)+  | Just tv_args <- traverse tcTyVar_maybe $ args <> pure res+  = fmap (<> foldMap (occNameString . occName) tv_args) functionNames+purposeToName (Function _ _) = functionNames+purposeToName Predicate = pure "p"+purposeToName Continuation = pure "k"+purposeToName Integral = ["n", "i", "j"]+purposeToName Number = ["x", "y", "z", "w"]+purposeToName String = ["s", "str"]+purposeToName (List t) = fmap (<> "s") $ purposeToName =<< getPurposes t+purposeToName (Maybe t) = fmap ("m_" <>) $ purposeToName =<< getPurposes t+purposeToName (TyVarred tv args)+  | Just tv_args <- traverse tcTyVar_maybe args+  = pure $ foldMap (occNameString . occName) $ tv : tv_args+purposeToName (TyVarred tv _) = pure $ occNameString $ occName tv+purposeToName (TyConned tc args@(_:_))+  | Just tv_args <- traverse tcTyVar_maybe args+  = [ mkTyConName tc+      -- We insert primes to everything later, but it gets the lowest+      -- precedence. Here we'd like to prefer it over the more specific type+      -- name.+    , mkTyConName tc <> "'"+    , mconcat+      [ mkTyConName tc+      , bool mempty "_" $ length (mkTyConName tc) > 1+      , foldMap (occNameString . occName) tv_args+      ]+    ]+purposeToName (TyConned tc _)+  = pure+  $ mkTyConName tc+++mkTyName :: Type -> [String]+mkTyName = purposeToName <=< getPurposes+++------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String mkTyConName tc-  | tc == listTyCon = "l_"-  | tc == pairTyCon = "p_"-  | tc == unitTyCon = "unit"-  | otherwise+  | tc == unitTyCon = "u"+  | isSymOcc occ       = take 1       . fmap toLower       . filterReplace isSymbol      's'       . filterReplace isPunctuation 'p'-      . occNameString-      $ getOccName tc+      $ name+  | camels@(_:_:_) <- camelTerms name+      = foldMap (fmap toLower . take 1) camels+  | otherwise+      = getStem+      $ fmap toLower+      $ name+  where+    occ = getOccName tc+    name = occNameString occ   ------------------------------------------------------------------------------+-- | Split a string into its camel case components.+camelTerms :: String -> [String]+camelTerms = split (== '@') . camelTo2 '@'+++------------------------------------------------------------------------------+-- | A stem of a string is either a special-case shortened form, or a shortened+-- first syllable. If the string is one syllable, we take the full word if it's+-- short, or just the first two characters if it's long. Otherwise, just take+-- the first syllable.+--+-- NOTE: There's no rhyme or reason here, I just experimented until I got+-- results that were reasonably consistent with the names I would give things.+getStem :: String -> String+getStem str =+  let s = stem str+   in case (s == str, length str) of+        (False, _)             -> s+        (True, (<= 3) -> True) -> str+        _                      -> take 2 str++------------------------------------------------------------------------------+-- | Get a special-case stem, or, failing that, give back the first syllable.+stem :: String -> String+stem "char" = "c"+stem "function" = "func"+stem "bool" = "b"+stem "either" = "e"+stem "text" = "txt"+stem s = join $ take 1 $ hyphenate english_US s+++------------------------------------------------------------------------------ -- | 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)@@ -67,22 +213,34 @@     :: 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+mkGoodName in_scope (mkTyName -> tn)+  = mkVarOcc+  . fromMaybe (mkNumericSuffix in_scope $ fromMaybe "x" $ listToMaybe tn)+  . getFirst+  . foldMap (\n -> bool (pure n) mempty $ check n)+  $ tn <> fmap (<> "'") tn+  where+    check n = S.member (mkVarOcc n) in_scope   ------------------------------------------------------------------------------+-- | Given a desired name, compute a new name for it based on how many names in+-- scope conflict with it. Eg, if we want to name something @x@, but already+-- have @x@, @x'@ and @x2@ in scope, we will give back @x3@.+mkNumericSuffix :: Set OccName -> String -> String+mkNumericSuffix s nm =+  mappend nm . show . length . filter (isPrefixOf nm . occNameString) $ S.toList s+++------------------------------------------------------------------------------ -- | Like 'mkGoodName' but creates several apart names. mkManyGoodNames-  :: (Traversable t, Monad m)+  :: (Traversable t)   => Set OccName   -> t Type-  -> m (t OccName)+  -> t OccName mkManyGoodNames in_scope args =-  flip evalStateT in_scope $ for args $ \at -> do+  flip evalState in_scope $ for args $ \at -> do     in_scope <- get     let n = mkGoodName in_scope at     modify $ S.insert n

@@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}  -- | A plugin that uses tactics to synthesize code module Wingman.Plugin@@ -12,7 +13,6 @@ import           Control.Monad.Trans import           Control.Monad.Trans.Maybe import           Data.Aeson-import           Data.Bifunctor (first) import           Data.Data import           Data.Foldable (for_) import           Data.Maybe@@ -21,6 +21,7 @@ import           Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent) import           Development.IDE.GHC.Compat import           Development.IDE.GHC.ExactPrint+import           Generics.SYB.GHC import           Ide.Types import           Language.LSP.Server import           Language.LSP.Types@@ -29,29 +30,44 @@ import           Prelude hiding (span) import           System.Timeout import           Wingman.CaseSplit+import           Wingman.EmptyCase import           Wingman.GHC import           Wingman.LanguageServer+import           Wingman.LanguageServer.Metaprogram (hoverProvider) import           Wingman.LanguageServer.TacticProviders import           Wingman.Machinery (scoreSolution) import           Wingman.Range+import           Wingman.StaticPlugin import           Wingman.Tactics import           Wingman.Types+import Wingman.Metaprogramming.Lexer (ParserContext)   descriptor :: PluginId -> PluginDescriptor IdeState descriptor plId = (defaultPluginDescriptor plId)   { pluginCommands-      = fmap (\tc ->-          PluginCommand-            (tcCommandId tc)-            (tacticDesc $ tcCommandName tc)-            (tacticCmd (commandTactic tc) plId))-            [minBound .. maxBound]-  , pluginHandlers =-      mkPluginHandler STextDocumentCodeAction codeActionProvider+      = mconcat+          [ fmap (\tc ->+              PluginCommand+                (tcCommandId tc)+                (tacticDesc $ tcCommandName tc)+                (tacticCmd (flip commandTactic tc) plId))+                [minBound .. maxBound]+          , pure $+              PluginCommand+              emptyCaseLensCommandId+              "Complete the empty case"+              workspaceEditHandler+          ]+  , pluginHandlers = mconcat+      [ mkPluginHandler STextDocumentCodeAction codeActionProvider+      , mkPluginHandler STextDocumentCodeLens codeLensProvider+      , mkPluginHandler STextDocumentHover hoverProvider+      ]   , pluginRules = wingmanRules plId-  , pluginCustomConfig =-      mkCustomConfig properties+  , pluginConfigDescriptor =+      defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties}+  , pluginModifyDynflags = staticPlugin   }  @@ -60,16 +76,17 @@   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do       cfg <- getTacticConfig plId       liftIO $ fromMaybeT (Right $ List []) $ do-        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg+        HoleJudgment{..} <- judgementForHole state nfp range cfg         actions <- lift $           -- This foldMap is over the function monoid.           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData-            { tpd_dflags = dflags+            { tpd_dflags = hj_dflags             , tpd_config = cfg             , tpd_plid   = plId             , tpd_uri    = uri             , tpd_range  = range-            , tpd_jdg    = jdg+            , tpd_jdg    = hj_jdg+            , tpd_hole_sort = hj_hole_sort             }         pure $ Right $ List actions codeActionProvider _ _ _ = pure $ Right $ List []@@ -84,26 +101,34 @@   pure $ Left $ mkErr InternalError $ T.pack $ show ufm  -tacticCmd :: (OccName -> TacticsM ()) -> PluginId -> CommandFunction IdeState TacticParams+tacticCmd+    :: (ParserContext -> T.Text -> IO (TacticsM ()))+    -> PluginId+    -> CommandFunction IdeState TacticParams tacticCmd tac pId state (TacticParams uri range var_name)   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do-      features <- getFeatureSet pId+      let stale a = runStaleIde "tacticCmd" state nfp a+       ccs <- getClientCapabilities       cfg <- getTacticConfig pId       res <- liftIO $ runMaybeT $ do-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range features-        let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) range'-        TrackedStale pm pmmap <- runStaleIde state nfp GetAnnotatedParsedSource+        HoleJudgment{..} <- judgementForHole state nfp range cfg+        let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range+        TrackedStale pm pmmap <- stale GetAnnotatedParsedSource         pm_span <- liftMaybe $ mapAgeFrom pmmap span+        pc <- getParserState state nfp hj_ctx+        t <- liftIO $ tac pc var_name          timingOut (cfg_timeout_seconds cfg * seconds) $ join $-          case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of-            Left _ -> Left TacticErrors+          case runTactic hj_ctx hj_jdg t of+            Left errs ->  do+              traceMX "errs" errs+              Left TacticErrors             Right rtr ->               case rtr_extract rtr of                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->                   Left NothingToDo-                _ -> pure $ mkWorkspaceEdits pm_span dflags ccs uri pm rtr+                _ -> pure $ mkTacticResultEdits pm_span hj_dflags ccs uri pm rtr        case res of         Nothing -> do@@ -140,7 +165,7 @@ ------------------------------------------------------------------------------ -- | Turn a 'RunTacticResults' into concrete edits to make in the source -- document.-mkWorkspaceEdits+mkTacticResultEdits     :: Tracked age RealSrcSpan     -> DynFlags     -> ClientCapabilities@@ -148,14 +173,12 @@     -> Tracked age (Annotated ParsedSource)     -> RunTacticResults     -> Either UserFacingMessage WorkspaceEdit-mkWorkspaceEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do+mkTacticResultEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do   for_ (rtr_other_solns rtr) $ \soln -> do     traceMX "other solution" $ syn_val soln     traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) []   traceMX "solution" $ rtr_extract rtr-  let g = graftHole (RealSrcSpan span) rtr-      response = transform dflags ccs uri g pm-   in first (InfrastructureError . T.pack) response+  mkWorkspaceEdits dflags ccs uri pm $ graftHole (RealSrcSpan span) rtr   ------------------------------------------------------------------------------@@ -209,8 +232,4 @@           pure alts         _ -> lift $ Left "annotateDecl didn't produce a funbind" graftDecl _ _ _ _ x = pure $ pure x---fromMaybeT :: Functor m => a -> MaybeT m a -> m a-fromMaybeT def = fmap (fromMaybe def) . runMaybeT 

@@ -11,7 +11,7 @@ import GHC.SourceGen (var) import GHC.SourceGen.Expr (lambda) import Wingman.CodeGen.Utils-import Wingman.GHC (containsHsVar, fromPatCompat)+import Wingman.GHC (containsHsVar, fromPatCompat, pattern SingleLet)   ------------------------------------------------------------------------------@@ -30,6 +30,7 @@     Lambda pats body = lambda pats body  + ------------------------------------------------------------------------------ -- | Simlify an expression. simplify :: LHsExpr GhcPs -> LHsExpr GhcPs@@ -41,6 +42,7 @@     [ simplifyEtaReduce     , simplifyRemoveParens     , simplifyCompose+    , simplifySingleLet     ])  @@ -66,6 +68,13 @@         -- We can only perform this simplifiation if @pat@ is otherwise unused.       , not (containsHsVar pat f) ->     Lambda pats f+  x -> x++------------------------------------------------------------------------------+-- | Eliminates the unnecessary binding in @let a = b in a@+simplifySingleLet :: GenericT+simplifySingleLet = mkT $ \case+  SingleLet bind [] val (HsVar _ (L _ a)) | a == bind -> val   x -> x  

@@ -0,0 +1,96 @@+{-# LANGUAGE CPP #-}++module Wingman.StaticPlugin+  ( staticPlugin+  , metaprogramHoleName+  , pattern WingmanMetaprogram+  , pattern MetaprogramSyntax+  ) where++import Data.Data+import Development.IDE.GHC.Compat+import GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes))+import Generics.SYB+import GhcPlugins hiding ((<>))+import Ide.Types+++staticPlugin :: DynFlagsModifications+staticPlugin = mempty+  { dynFlagsModifyGlobal =+      \df -> allowEmptyCaseButWithWarning+           $ df+#if __GLASGOW_HASKELL__ >= 808+             { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }+  , dynFlagsModifyParser = enableQuasiQuotes+#endif+  }+++pattern MetaprogramSourceText :: SourceText+pattern MetaprogramSourceText = SourceText "wingman-meta-program"++++pattern WingmanMetaprogram :: FastString -> HsExpr p+pattern WingmanMetaprogram mp+  <- HsSCC _ MetaprogramSourceText (StringLiteral NoSourceText mp)+      (L _ ( HsVar _ _))+++enableQuasiQuotes :: DynFlags -> DynFlags+enableQuasiQuotes = flip xopt_set QuasiQuotes+++-- | Wingman wants to support destructing of empty cases, but these are a parse+-- error by default. So we want to enable 'EmptyCase', but then that leads to+-- silent errors without 'Opt_WarnIncompletePatterns'.+allowEmptyCaseButWithWarning :: DynFlags -> DynFlags+allowEmptyCaseButWithWarning =+  flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns+++#if __GLASGOW_HASKELL__ >= 808+metaprogrammingPlugin :: StaticPlugin+metaprogrammingPlugin =+    StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker })  []+  where+    worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule+    worker _ _ pm = pure $ pm { hpm_module = addMetaprogrammingSyntax $ hpm_module pm }+#endif++metaprogramHoleName :: OccName+metaprogramHoleName = mkVarOcc "_$metaprogram"+++mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs+mkMetaprogram ss mp =+  HsSCC noExtField MetaprogramSourceText (StringLiteral NoSourceText mp)+    $ L ss+    $ HsVar noExtField+    $ L ss+    $ mkRdrUnqual+    $ metaprogramHoleName+++addMetaprogrammingSyntax :: Data a => a -> a+addMetaprogrammingSyntax =+  everywhere $ mkT $ \case+    L ss (MetaprogramSyntax mp) ->+      L ss $ mkMetaprogram ss mp+    (x :: LHsExpr GhcPs) -> x+++pattern MetaprogramSyntax :: FastString -> HsExpr GhcPs+pattern MetaprogramSyntax mp <-+    HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp)+  where+    MetaprogramSyntax mp =+      HsSpliceE noExtField $+        HsQuasiQuote+          noExtField+          (mkRdrUnqual $ mkVarOcc "splice")+          (mkRdrUnqual $ mkVarOcc "wingman")+          noSrcSpan+          mp+

@@ -1,3 +1,5 @@+{-# LANGUAGE OverloadedStrings #-}+ module Wingman.Tactics   ( module Wingman.Tactics   , runTactic@@ -9,7 +11,8 @@ import           Control.Monad (unless) import           Control.Monad.Except (throwError) import           Control.Monad.Reader.Class (MonadReader (ask))-import           Control.Monad.State.Strict (StateT(..), runStateT)+import           Control.Monad.State.Strict (StateT(..), runStateT, gets)+import           Data.Bool (bool) import           Data.Foldable import           Data.Functor ((<&>)) import           Data.Generics.Labels ()@@ -21,18 +24,22 @@ import           DataCon import           Development.IDE.GHC.Compat import           GHC.Exts+import           GHC.SourceGen ((@@)) import           GHC.SourceGen.Expr import           Name (occNameString, occName)+import           OccName (mkVarOcc) import           Refinery.Tactic import           Refinery.Tactic.Internal import           TcType import           Type hiding (Var)+import           TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar) import           Wingman.CodeGen import           Wingman.Context import           Wingman.GHC import           Wingman.Judgements import           Wingman.Machinery import           Wingman.Naming+import           Wingman.StaticPlugin (pattern MetaprogramSyntax) import           Wingman.Types  @@ -76,7 +83,8 @@       unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty      let hy' = recursiveHypothesis defs-    localTactic (apply $ HyInfo name RecursivePrv ty) (introduce hy')+    ctx <- ask+    localTactic (apply $ HyInfo name RecursivePrv ty) (introduce ctx hy')       <@> fmap (localTactic assumption . filterPosition name) [0..]  @@ -93,17 +101,26 @@ ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros :: TacticsM ()-intros = rule $ \jdg -> do+intros = intros' Nothing++------------------------------------------------------------------------------+-- | Introduce a lambda binding every variable.+intros'+    :: Maybe [OccName]  -- ^ When 'Nothing', generate a new name for every+                        -- variable. Otherwise, only bind the variables named.+    -> TacticsM ()+intros' names = rule $ \jdg -> do   let 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+  case tacticsSplitFunTy $ unCType g of+    (_, _, [], _) -> throwError $ GoalMismatch "intros" g+    (_, _, as, b) -> do+      ctx <- ask+      let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names+          num_args = length vs+          top_hole = isTopHole ctx jdg           hy' = lambdaHypothesis top_hole $ zip vs $ coerce as-          jdg' = introduce hy'-               $ withNewGoal (CType b) jdg+          jdg' = introduce ctx hy'+               $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg       ext <- newSubgoal jdg'       pure $         ext@@ -142,9 +159,9 @@       ty = unCType $ hi_type hi    attemptWhen-      (rule $ destruct' (\dc jdg ->+      (rule $ destruct' False (\dc jdg ->         buildDataCon False jdg dc $ snd $ splitAppTys g) hi)-      (rule $ destruct' (const subgoal) hi)+      (rule $ destruct' False (const newSubgoal) hi)     $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of         (Just (gtc, _), Just (tytc, _)) -> gtc == tytc         _ -> False@@ -154,20 +171,28 @@ -- | Case split, and leave holes in the matches. destruct :: HyInfo CType -> TacticsM () destruct hi = requireConcreteHole $ tracing "destruct(user)" $-  rule $ destruct' (const subgoal) hi+  rule $ destruct' False (const newSubgoal) hi   ------------------------------------------------------------------------------+-- | Case split, and leave holes in the matches. Performs record punning.+destructPun :: HyInfo CType -> TacticsM ()+destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $+  rule $ destruct' True (const newSubgoal) hi+++------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: HyInfo CType -> TacticsM ()-homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg ->+homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->   buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)   ------------------------------------------------------------------------------ -- | LambdaCase split, and leave holes in the matches. destructLambdaCase :: TacticsM ()-destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal)+destructLambdaCase =+  tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const newSubgoal)   ------------------------------------------------------------------------------@@ -175,7 +200,7 @@ homoLambdaCase :: TacticsM () homoLambdaCase =   tracing "homoLambdaCase" $-    rule $ destructLambdaCase' $ \dc jdg ->+    rule $ destructLambdaCase' False $ \dc jdg ->       buildDataCon False jdg dc         . snd         . splitAppTys@@ -184,7 +209,7 @@   apply :: HyInfo CType -> TacticsM ()-apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do+apply hi = tracing ("apply' " <> show (hi_name hi)) $ do   jdg <- goal   let g  = jGoal jdg       ty = unCType $ hi_type hi@@ -205,7 +230,10 @@         & #syn_used_vals %~ S.insert func         & #syn_val       %~ mkApply func . fmap unLoc +application :: TacticsM ()+application = overFunctions apply + ------------------------------------------------------------------------------ -- | Choose between each of the goal's data constructors. split :: TacticsM ()@@ -247,8 +275,26 @@       splitDataCon dc     _ -> throwError $ GoalMismatch "splitSingle" g +------------------------------------------------------------------------------+-- | Like 'split', but prunes any data constructors which have holes.+obvious :: TacticsM ()+obvious = tracing "obvious" $ do+  pruning split $ bool (Just NoProgress) Nothing . null + ------------------------------------------------------------------------------+-- | Sorry leaves a hole in its extract+sorry :: TacticsM ()+sorry = exact $ var' $ mkVarOcc "_"+++------------------------------------------------------------------------------+-- | Sorry leaves a hole in its extract+metaprogram :: TacticsM ()+metaprogram = exact $ MetaprogramSyntax ""+++------------------------------------------------------------------------------ -- | Allow the given tactic to proceed if and only if it introduces holes that -- have a different goal than current goal. requireNewHoles :: TacticsM () -> TacticsM ()@@ -290,7 +336,7 @@ destructAll = do   jdg <- goal   let args = fmap fst-           $ sortOn (Down . snd)+           $ sortOn snd            $ mapMaybe (\(hi, prov) ->               case prov of                 TopLevelArgPrv _ idx _ -> pure (hi, idx)@@ -300,7 +346,9 @@            $ filter (isAlgType . unCType . hi_type)            $ unHypothesis            $ jHypothesis jdg-  for_ args destruct+  for_ args $ \arg -> do+    subst <- gets ts_unifier+    destruct $ fmap (coerce substTy subst) arg  -------------------------------------------------------------------------------- -- | User-facing tactic to implement "Use constructor <x>"@@ -338,10 +386,7 @@   refine :: TacticsM ()-refine = do-  try' intros-  try' splitSingle-  try' intros+refine = intros <%> splitSingle   auto' :: Int -> TacticsM ()@@ -351,7 +396,7 @@   try intros   choice     [ overFunctions $ \fname -> do-        apply fname+        requireConcreteHole $ apply fname         loop     , overAlgebraicTerms $ \aname -> do         destructAuto aname@@ -394,4 +439,75 @@       True  -> apply hi       False -> empty ++------------------------------------------------------------------------------+-- | Make a function application where the function being applied itself is+-- a hole.+applyByType :: Type -> TacticsM ()+applyByType ty = tracing ("applyByType " <> show ty) $ do+  jdg <- goal+  let g  = jGoal jdg+  ty' <- freshTyvars ty+  let (_, _, args, ret) = tacticsSplitFunTy ty'+  rule $ \jdg -> do+    unify g (CType ret)+    ext+        <- fmap unzipTrace+        $ traverse ( newSubgoal+                    . blacklistingDestruct+                    . flip withNewGoal jdg+                    . CType+                    ) args+    app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg+    pure $+      fmap noLoc $+        foldl' (@@)+          <$> fmap unLoc app+          <*> fmap (fmap unLoc) ext+++------------------------------------------------------------------------------+-- | Make an n-ary function call of the form+-- @(_ :: forall a b. a -> a -> b) _ _@.+nary :: Int -> TacticsM ()+nary n =+  applyByType $+    mkInvForAllTys [alphaTyVar, betaTyVar] $+      mkFunTys' (replicate n alphaTy) betaTy++self :: TacticsM ()+self =+  fmap listToMaybe getCurrentDefinitions >>= \case+    Just (self, _) -> useNameFromContext apply self+    Nothing -> throwError $ TacticPanic "no defining function"+++cata :: HyInfo CType -> TacticsM ()+cata hi = do+  diff <- hyDiff $ destruct hi+  rule $+    letForEach+      (mkVarOcc . flip mappend "_c" . occNameString)+      (\hi -> self >> commit (apply hi) assumption)+      diff++collapse :: TacticsM ()+collapse = do+  g <- goal+  let terms = unHypothesis $ hyFilter ((jGoal g ==) . hi_type) $ jLocalHypothesis g+  case terms of+    [hi] -> assume $ hi_name hi+    _    -> nary (length terms) <@> fmap (assume . hi_name) terms+++------------------------------------------------------------------------------+-- | Determine the difference in hypothesis due to running a tactic. Also, it+-- runs the tactic.+hyDiff :: TacticsM () -> TacticsM (Hypothesis CType)+hyDiff m = do+  g <- unHypothesis . jEntireHypothesis <$> goal+  let g_len = length g+  m+  g' <- unHypothesis . jEntireHypothesis <$> goal+  pure $ Hypothesis $ take (length g' - g_len) g' 

@@ -26,8 +26,11 @@ import           Data.Text (Text) import qualified Data.Text as T import           Data.Tree+import           Development.IDE (Range)+import           Development.IDE.Core.UseStale import           Development.IDE.GHC.Compat hiding (Node) import           Development.IDE.GHC.Orphans ()+import           FamInstEnv (FamInstEnvs) import           GHC.Generics import           GHC.SourceGen (var) import           InstEnv (InstEnvs(..))@@ -38,7 +41,6 @@ import           UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) import           Wingman.Debug-import           Wingman.FeatureSet   ------------------------------------------------------------------------------@@ -49,12 +51,15 @@   = Auto   | Intros   | Destruct+  | DestructPun   | Homomorphism   | DestructLambdaCase   | HomomorphismLambdaCase   | DestructAll   | UseDataCon   | Refine+  | BeginMetaprogram+  | RunMetaprogram   deriving (Eq, Ord, Show, Enum, Bounded)  -- | Generate a title for the command.@@ -64,22 +69,33 @@     go Auto _                   = "Attempt to fill hole"     go Intros _                 = "Introduce lambda"     go Destruct var             = "Case split on " <> var+    go DestructPun var          = "Split on " <> var <> " with NamedFieldPuns"     go Homomorphism var         = "Homomorphic case split on " <> var     go DestructLambdaCase _     = "Lambda case split"     go HomomorphismLambdaCase _ = "Homomorphic lambda case split"     go DestructAll _            = "Split all function arguments"     go UseDataCon dcon          = "Use constructor " <> dcon     go Refine _                 = "Refine hole"+    go BeginMetaprogram _       = "Use custom tactic block"+    go RunMetaprogram _         = "Run custom tactic"   ------------------------------------------------------------------------------ -- | Plugin configuration for tactics data Config = Config-  { cfg_feature_set          :: FeatureSet-  , cfg_max_use_ctor_actions :: Int+  { cfg_max_use_ctor_actions :: Int   , cfg_timeout_seconds      :: Int+  , cfg_auto_gas             :: Int   }+  deriving (Eq, Ord, Show) +emptyConfig :: Config+emptyConfig = Config+  { cfg_max_use_ctor_actions = 5+  , cfg_timeout_seconds = 2+  , cfg_auto_gas = 4+  }+ ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type }@@ -117,6 +133,9 @@ instance Show (HsExpr GhcPs) where   show  = unsafeRender +instance Show (HsExpr GhcTc) where+  show  = unsafeRender+ instance Show (HsDecl GhcPs) where   show  = unsafeRender @@ -191,6 +210,8 @@       (Uniquely Class)     -- ^ Class     -- | A binding explicitly written by the user.   | UserPrv+    -- | A binding explicitly imported by the user.+  | ImportPrv     -- | The recursive hypothesis. Present only in the context of the recursion     -- tactic.   | RecursivePrv@@ -305,6 +326,7 @@   | UnhelpfulSplit OccName   | TooPolymorphic   | NotInScope OccName+  | TacticPanic String   deriving stock (Eq)  instance Show TacticError where@@ -343,6 +365,8 @@       "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+    show (TacticPanic err) =+      "PANIC: " <> err   ------------------------------------------------------------------------------@@ -393,9 +417,10 @@     -- ^ The functions currently being defined   , ctxModuleFuncs   :: [(OccName, CType)]     -- ^ Everything defined in the current module-  , ctxFeatureSet    :: FeatureSet+  , ctxConfig        :: Config   , ctxKnownThings   :: KnownThings   , ctxInstEnvs      :: InstEnvs+  , ctxFamInstEnvs   :: FamInstEnvs   , ctxTheta         :: Set CType   } @@ -404,7 +429,7 @@     [ "Context "     , showsPrec 10 ctxDefiningFuncs ""     , showsPrec 10 ctxModuleFuncs ""-    , showsPrec 10 ctxFeatureSet ""+    , showsPrec 10 ctxConfig ""     , showsPrec 10 ctxTheta ""     ] @@ -424,8 +449,9 @@   = Context       { ctxDefiningFuncs = mempty       , ctxModuleFuncs = mempty-      , ctxFeatureSet = mempty+      , ctxConfig = emptyConfig       , ctxKnownThings = error "empty known things from emptyContext"+      , ctxFamInstEnvs = mempty       , ctxInstEnvs = InstEnvs mempty mempty mempty       , ctxTheta = mempty       }@@ -461,6 +487,7 @@ data RunTacticResults = RunTacticResults   { rtr_trace       :: Trace   , rtr_extract     :: LHsExpr GhcPs+  , rtr_subgoals    :: [Judgement]   , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]   , rtr_jdg         :: Judgement   , rtr_ctx         :: Context@@ -486,4 +513,16 @@   show TimedOut                = "Wingman timed out while trying to find a solution"   show NothingToDo             = "Nothing to do"   show (InfrastructureError t) = "Internal error: " <> T.unpack t+++data HoleSort = Hole | Metaprogram T.Text+  deriving (Eq, Ord, Show)++data HoleJudgment = HoleJudgment+  { hj_range     :: Tracked 'Current Range+  , hj_jdg       :: Judgement+  , hj_ctx       :: Context+  , hj_dflags    :: DynFlags+  , hj_hole_sort :: HoleSort+  } 

@@ -36,6 +36,7 @@           runTactic             emptyContext             (mkFirstJudgement+              emptyContext               (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type)               True               out_type)

@@ -1,16 +1,10 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module CodeAction.AutoSpec where  import Wingman.Types import Test.Hspec import Utils-import Wingman.FeatureSet (allFeatures)   spec :: Spec@@ -19,72 +13,75 @@       autoTestNoWhitespace = goldenTestNoWhitespace Auto ""    describe "golden" $ do-    autoTest 11  8 "AutoSplitGADT.hs"-    autoTest  2 11 "GoldenEitherAuto.hs"-    autoTest  4 12 "GoldenJoinCont.hs"-    autoTest  3 11 "GoldenIdentityFunctor.hs"-    autoTest  7 11 "GoldenIdTypeFam.hs"-    autoTest  2 15 "GoldenEitherHomomorphic.hs"-    autoTest  2  8 "GoldenNote.hs"-    autoTest  2 12 "GoldenPureList.hs"-    autoTest  2 12 "GoldenListFmap.hs"-    autoTest  2 13 "GoldenFromMaybe.hs"-    autoTest  2 10 "GoldenFoldr.hs"-    autoTest  2  8 "GoldenSwap.hs"-    autoTest  4 11 "GoldenFmapTree.hs"-    autoTest  7 13 "GoldenGADTAuto.hs"-    autoTest  2 12 "GoldenSwapMany.hs"-    autoTest  4 12 "GoldenBigTuple.hs"-    autoTest  2 10 "GoldenShow.hs"-    autoTest  2 15 "GoldenShowCompose.hs"-    autoTest  2  8 "GoldenShowMapChar.hs"-    autoTest  7  8 "GoldenSuperclass.hs"-    autoTest  2 12 "GoldenSafeHead.hs"-    autoTest  2 12 "FmapBoth.hs"-    autoTest  7  8 "RecordCon.hs"-    autoTest  6  8 "NewtypeRecord.hs"-    autoTest  2 14 "FmapJoin.hs"-    autoTest  2  9 "Fgmap.hs"-    autoTest  4 19 "FmapJoinInLet.hs"-    autoTest  9 12 "AutoEndo.hs"-    autoTest  2 16 "AutoEmptyString.hs"-    autoTest  7 35 "AutoPatSynUse.hs"-    autoTest  2 28 "AutoZip.hs"-    autoTest  2 17 "AutoInfixApply.hs"-    autoTest  2 19 "AutoInfixApplyMany.hs"-    autoTest  2 25 "AutoInfixInfix.hs"+    autoTest 11  8 "AutoSplitGADT"+    autoTest  2 11 "GoldenEitherAuto"+    autoTest  4 12 "GoldenJoinCont"+    autoTest  3 11 "GoldenIdentityFunctor"+    autoTest  7 11 "GoldenIdTypeFam"+    autoTest  2 15 "GoldenEitherHomomorphic"+    autoTest  2  8 "GoldenNote"+    autoTest  2 12 "GoldenPureList"+    autoTest  2 12 "GoldenListFmap"+    autoTest  2 13 "GoldenFromMaybe"+    autoTest  2 10 "GoldenFoldr"+    autoTest  2  8 "GoldenSwap"+    autoTest  4 11 "GoldenFmapTree"+    autoTest  7 13 "GoldenGADTAuto"+    autoTest  2 12 "GoldenSwapMany"+    autoTest  4 12 "GoldenBigTuple"+    autoTest  2 10 "GoldenShow"+    autoTest  2 15 "GoldenShowCompose"+    autoTest  2  8 "GoldenShowMapChar"+    autoTest  7  8 "GoldenSuperclass"+    autoTest  2 12 "GoldenSafeHead"+    autoTest  2 12 "FmapBoth"+    autoTest  7  8 "RecordCon"+    autoTest  6  8 "NewtypeRecord"+    autoTest  2 14 "FmapJoin"+    autoTest  2  9 "Fgmap"+    autoTest  4 19 "FmapJoinInLet"+    autoTest  9 12 "AutoEndo"+    autoTest  2 16 "AutoEmptyString"+    autoTest  7 35 "AutoPatSynUse"+    autoTest  2 28 "AutoZip"+    autoTest  2 17 "AutoInfixApply"+    autoTest  2 19 "AutoInfixApplyMany"+    autoTest  2 25 "AutoInfixInfix"      failing "flaky in CI" $-      autoTest 2 11 "GoldenApplicativeThen.hs"+      autoTest 2 11 "GoldenApplicativeThen"      failing "not enough auto gas" $-      autoTest 5 18 "GoldenFish.hs"+      autoTest 5 18 "GoldenFish"    describe "theta" $ do-    autoTest 12 10 "AutoThetaFix.hs"-    autoTest  7 20 "AutoThetaRankN.hs"-    autoTest  6 10 "AutoThetaGADT.hs"-    autoTest  6  8 "AutoThetaGADTDestruct.hs"-    autoTest  4  8 "AutoThetaEqCtx.hs"-    autoTest  6 10 "AutoThetaEqGADT.hs"-    autoTest  6  8 "AutoThetaEqGADTDestruct.hs"-    autoTest  6 10 "AutoThetaRefl.hs"-    autoTest  6  8 "AutoThetaReflDestruct.hs"+    autoTest 12 10 "AutoThetaFix"+    autoTest  7 20 "AutoThetaRankN"+    autoTest  6 10 "AutoThetaGADT"+    autoTest  6  8 "AutoThetaGADTDestruct"+    autoTest  4  8 "AutoThetaEqCtx"+    autoTest  6 10 "AutoThetaEqGADT"+    autoTest  6  8 "AutoThetaEqGADTDestruct"+    autoTest  6 10 "AutoThetaRefl"+    autoTest  6  8 "AutoThetaReflDestruct"+    autoTest 19 30 "AutoThetaMultipleUnification"+    autoTest 16  9 "AutoThetaSplitUnification"    describe "known" $ do-    autoTest 25 13 "GoldenArbitrary.hs"+    autoTest 25 13 "GoldenArbitrary"     autoTestNoWhitespace-              6 10 "KnownBigSemigroup.hs"-    autoTest  4 10 "KnownThetaSemigroup.hs"-    autoTest  6 10 "KnownCounterfactualSemigroup.hs"-    autoTest 10 10 "KnownModuleInstanceSemigroup.hs"-    autoTest  4 22 "KnownDestructedSemigroup.hs"-    autoTest  4 10 "KnownMissingSemigroup.hs"-    autoTest  7 12 "KnownMonoid.hs"-    autoTest  7 12 "KnownPolyMonoid.hs"-    autoTest  7 12 "KnownMissingMonoid.hs"+              6 10 "KnownBigSemigroup"+    autoTest  4 10 "KnownThetaSemigroup"+    autoTest  6 10 "KnownCounterfactualSemigroup"+    autoTest 10 10 "KnownModuleInstanceSemigroup"+    autoTest  4 22 "KnownDestructedSemigroup"+    autoTest  4 10 "KnownMissingSemigroup"+    autoTest  7 12 "KnownMonoid"+    autoTest  7 12 "KnownPolyMonoid"+    autoTest  7 12 "KnownMissingMonoid"     describe "messages" $ do-    mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA.hs" TacticErrors+    mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors+    mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors 

@@ -1,9 +1,4 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module CodeAction.DestructAllSpec where @@ -18,25 +13,26 @@   describe "provider" $ do     mkTest       "Requires args on lhs of ="-      "DestructAllProvider.hs" 3 21+      "DestructAllProvider" 3 21       [ (not, DestructAll, "")       ]     mkTest       "Can't be a non-top-hole"-      "DestructAllProvider.hs" 8 19+      "DestructAllProvider" 8 19       [ (not, DestructAll, "")       , (id, Destruct, "a")       , (id, Destruct, "b")       ]     mkTest       "Provides a destruct all otherwise"-      "DestructAllProvider.hs" 12 22+      "DestructAllProvider" 12 22       [ (id, DestructAll, "")       ]    describe "golden" $ do-    destructAllTest 2 11 "DestructAllAnd.hs"-    destructAllTest 4 23 "DestructAllMany.hs"-    destructAllTest 2 18 "DestructAllNonVarTopMatch.hs"-    destructAllTest 2 18 "DestructAllFunc.hs"+    destructAllTest 2 11 "DestructAllAnd"+    destructAllTest 4 23 "DestructAllMany"+    destructAllTest 2 18 "DestructAllNonVarTopMatch"+    destructAllTest 2 18 "DestructAllFunc"+    destructAllTest 19 18 "DestructAllGADTEvidence" 

@@ -0,0 +1,20 @@+{-# LANGUAGE OverloadedStrings #-}++module CodeAction.DestructPunSpec where++import Wingman.Types+import Test.Hspec+import Utils+++spec :: Spec+spec = do+  let destructTest = goldenTest DestructPun++  describe "golden" $ do+    destructTest "x"  4  9 "PunSimple"+    destructTest "x"  6 10 "PunMany"+    destructTest "x" 11 11 "PunGADT"+    destructTest "x" 17 11 "PunManyGADT"+    destructTest "x"  4 12 "PunShadowing"+

@@ -1,9 +1,4 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module CodeAction.DestructSpec where @@ -17,21 +12,26 @@   let destructTest = goldenTest Destruct    describe "golden" $ do-    destructTest "gadt" 7 17 "GoldenGADTDestruct.hs"-    destructTest "gadt" 8 17 "GoldenGADTDestructCoercion.hs"-    destructTest "a"    7 25 "SplitPattern.hs"+    destructTest "gadt"  7 17 "GoldenGADTDestruct"+    destructTest "gadt"  8 17 "GoldenGADTDestructCoercion"+    destructTest "a"     7 25 "SplitPattern"+    destructTest "a"     6 18 "DestructPun"+    destructTest "fp"   31 14 "DestructCthulhu"+    destructTest "b"     7 10 "DestructTyFam"+    destructTest "b"     7 10 "DestructDataFam"+    destructTest "b"    17 10 "DestructTyToDataFam"    describe "layout" $ do-    destructTest "b"  4  3 "LayoutBind.hs"-    destructTest "b"  2 15 "LayoutDollarApp.hs"-    destructTest "b"  2 18 "LayoutOpApp.hs"-    destructTest "b"  2 14 "LayoutLam.hs"-    destructTest "x" 11 15 "LayoutSplitWhere.hs"-    destructTest "x"  3 12 "LayoutSplitClass.hs"-    destructTest "b"  3  9 "LayoutSplitGuard.hs"-    destructTest "b"  4 13 "LayoutSplitLet.hs"-    destructTest "a"  4  7 "LayoutSplitIn.hs"-    destructTest "a"  4 31 "LayoutSplitViewPat.hs"-    destructTest "a"  7 17 "LayoutSplitPattern.hs"-    destructTest "a"  8 26 "LayoutSplitPatSyn.hs"+    destructTest "b"  4  3 "LayoutBind"+    destructTest "b"  2 15 "LayoutDollarApp"+    destructTest "b"  2 18 "LayoutOpApp"+    destructTest "b"  2 14 "LayoutLam"+    destructTest "x" 11 15 "LayoutSplitWhere"+    destructTest "x"  3 12 "LayoutSplitClass"+    destructTest "b"  3  9 "LayoutSplitGuard"+    destructTest "b"  4 13 "LayoutSplitLet"+    destructTest "a"  4  7 "LayoutSplitIn"+    destructTest "a"  4 31 "LayoutSplitViewPat"+    destructTest "a"  7 17 "LayoutSplitPattern"+    destructTest "a"  8 26 "LayoutSplitPatSyn" 

@@ -1,9 +1,4 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module CodeAction.IntrosSpec where @@ -17,5 +12,8 @@   let introsTest = goldenTest Intros ""    describe "golden" $ do-    introsTest 2 8 "GoldenIntros.hs"+    introsTest 2 8 "GoldenIntros"++  describe "layout" $ do+    introsTest 4 24 "LayoutRec" 

@@ -1,16 +1,10 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module CodeAction.RefineSpec where  import Wingman.Types import Test.Hspec import Utils-import Wingman.FeatureSet (allFeatures)   spec :: Spec@@ -18,11 +12,11 @@   let refineTest = goldenTest Refine ""    describe "golden" $ do-    refineTest 2 8 "RefineIntro.hs"-    refineTest 2 8 "RefineCon.hs"-    refineTest 4 8 "RefineReader.hs"-    refineTest 8 8 "RefineGADT.hs"+    refineTest  2  8 "RefineIntro"+    refineTest  2  8 "RefineCon"+    refineTest  4 10 "RefineReader"+    refineTest  8 10 "RefineGADT"    describe "messages" $ do-    mkShowMessageTest allFeatures Refine "" 2 8 "MessageForallA.hs" NothingToDo+    mkShowMessageTest Refine "" 2 8 "MessageForallA" TacticErrors 

@@ -0,0 +1,36 @@+{-# LANGUAGE CPP               #-}+{-# LANGUAGE OverloadedStrings #-}++module CodeAction.RunMetaprogramSpec where++import  Utils+import  Test.Hspec+import  Wingman.Types+++spec :: Spec+spec = do+  let metaTest l c f =+#if __GLASGOW_HASKELL__ >= 808+        goldenTest RunMetaprogram "" l c f+#else+        pure ()+#endif++#if __GLASGOW_HASKELL__ >= 808+  describe "beginMetaprogram" $ do+    goldenTest BeginMetaprogram ""  1  7 "MetaBegin"+#endif++  describe "golden" $ do+    metaTest  6 11 "MetaMaybeAp"+    metaTest  2 32 "MetaBindOne"+    metaTest  2 32 "MetaBindAll"+    metaTest  2 13 "MetaTry"+    metaTest  2 74 "MetaChoice"+    metaTest  5 40 "MetaUseImport"+    metaTest  6 31 "MetaUseLocal"+    metaTest 11 11 "MetaUseMethod"+    metaTest  9 38 "MetaCataCollapse"+    metaTest  7 16 "MetaCataCollapseUnary"+

@@ -1,9 +1,4 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module CodeAction.UseDataConSpec where @@ -20,7 +15,7 @@   describe "provider" $ do     mkTest       "Suggests all data cons for Either"-      "ConProviders.hs" 5 6+      "ConProviders" 5 6       [ (id, UseDataCon, "Left")       , (id, UseDataCon, "Right")       , (not, UseDataCon, ":")@@ -29,19 +24,19 @@       ]     mkTest       "Suggests no data cons for big types"-      "ConProviders.hs" 11 17 $ do+      "ConProviders" 11 17 $ do         c <- [1 :: Int .. 10]         pure $ (not, UseDataCon, T.pack $ show c)     mkTest       "Suggests only matching data cons for GADT"-      "ConProviders.hs" 20 12+      "ConProviders" 20 12       [ (id, UseDataCon, "IntGADT")       , (id, UseDataCon, "VarGADT")       , (not, UseDataCon, "BoolGADT")       ]    describe "golden" $ do-    useTest "(,)"   2 8 "UseConPair.hs"-    useTest "Left"  2 8 "UseConLeft.hs"-    useTest "Right" 2 8 "UseConRight.hs"+    useTest "(,)"   2 8 "UseConPair"+    useTest "Left"  2 8 "UseConLeft"+    useTest "Right" 2 8 "UseConRight" 

@@ -0,0 +1,20 @@+{-# LANGUAGE OverloadedStrings #-}++module CodeLens.EmptyCaseSpec where++import Test.Hspec+import Utils+++spec :: Spec+spec = do+  let test = mkCodeLensTest++  describe "golden" $ do+    test "EmptyCaseADT"+    test "EmptyCaseShadow"+    test "EmptyCaseParens"+    test "EmptyCaseNested"+    test "EmptyCaseApply"+    test "EmptyCaseGADT"+

@@ -1,9 +1,4 @@-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DuplicateRecordFields #-}-{-# LANGUAGE OverloadedStrings     #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE OverloadedStrings #-}  module ProviderSpec where @@ -16,57 +11,58 @@ spec = do   mkTest     "Produces intros code action"-    "T1.hs" 2 14+    "T1" 2 14     [ (id, Intros, "")     ]   mkTest     "Produces destruct and homomorphism code actions"-    "T2.hs" 2 21+    "T2" 2 21     [ (id, Destruct, "eab")     , (id, Homomorphism, "eab")+    , (not, DestructPun, "eab")     ]   mkTest     "Won't suggest homomorphism on the wrong type"-    "T2.hs" 8 8+    "T2" 8 8     [ (not, Homomorphism, "global")     ]   mkTest     "Won't suggest intros on the wrong type"-    "T2.hs" 8 8+    "T2" 8 8     [ (not, Intros, "")     ]   mkTest     "Produces (homomorphic) lambdacase code actions"-    "T3.hs" 4 24+    "T3" 4 24     [ (id, HomomorphismLambdaCase, "")     , (id, DestructLambdaCase, "")     ]   mkTest     "Produces lambdacase code actions"-    "T3.hs" 7 13+    "T3" 7 13     [ (id, DestructLambdaCase, "")     ]   mkTest     "Doesn't suggest lambdacase without -XLambdaCase"-    "T2.hs" 11 25+    "T2" 11 25     [ (not, DestructLambdaCase, "")     ]    mkTest     "Doesn't suggest destruct if already destructed"-    "ProvideAlreadyDestructed.hs" 6 18+    "ProvideAlreadyDestructed" 6 18     [ (not, Destruct, "x")     ]    mkTest     "...but does suggest destruct if destructed in a different branch"-    "ProvideAlreadyDestructed.hs" 9 7+    "ProvideAlreadyDestructed" 9 7     [ (id, Destruct, "x")     ]    mkTest     "Doesn't suggest destruct on class methods"-    "ProvideLocalHyOnly.hs" 2 12+    "ProvideLocalHyOnly" 2 12     [ (not, Destruct, "mempty")     ] 

@@ -9,7 +9,7 @@  import           Control.DeepSeq (deepseq) import qualified Control.Exception as E-import           Control.Lens hiding (failing, (<.>), (.=))+import           Control.Lens hiding (List, failing, (<.>), (.=)) import           Control.Monad (unless) import           Control.Monad.IO.Class import           Data.Aeson@@ -29,11 +29,10 @@ import           Test.Hls import           Test.Hspec import           Test.Hspec.Formatters (FailureReason(ExpectedButGot))-import           Test.Tasty.HUnit (Assertion, HUnitFailure(..))-import           Wingman.FeatureSet (FeatureSet, allFeatures, prettyFeatureSet) import           Wingman.LanguageServer (mkShowMessageParams) import           Wingman.Types + plugin :: PluginDescriptor IdeState plugin = Tactic.descriptor "tactics" @@ -61,7 +60,7 @@ mkTest     :: Foldable t     => String  -- ^ The test name-    -> FilePath  -- ^ The file to load+    -> FilePath  -- ^ The file name stem (without extension) to load     -> Int  -- ^ Cursor line     -> Int  -- ^ Cursor columnn     -> t ( Bool -> Bool   -- Use 'not' for actions that shouldnt be present@@ -71,8 +70,7 @@     -> SpecWith (Arg Bool) mkTest name fp line col ts = it name $ do   runSessionWithServer plugin tacticPath $ do-    setFeatureSet allFeatures-    doc <- openDoc fp "haskell"+    doc <- openDoc (fp <.> "hs") "haskell"     _ <- waitForDiagnostics     actions <- getCodeActions doc $ pointRange line col     let titles = mapMaybe codeActionTitle actions@@ -82,36 +80,19 @@         (title `elem` titles) `shouldSatisfy` f  -setFeatureSet :: FeatureSet -> Session ()-setFeatureSet features = do-  let unObject (Object obj) = obj-      unObject _            = undefined-      def_config = def :: Plugin.Config-      config =-        def_config-          { Plugin.plugins = M.fromList [("tactics",-              def { Plugin.plcConfig = unObject $ object ["features" .= prettyFeatureSet features] }-          )] <> Plugin.plugins def_config } -  sendNotification SWorkspaceDidChangeConfiguration $-    DidChangeConfigurationParams $-      toJSON config-- mkGoldenTest     :: (Text -> Text -> Assertion)-    -> FeatureSet     -> TacticCommand     -> Text     -> Int     -> Int     -> FilePath     -> SpecWith ()-mkGoldenTest eq features tc occ line col input =+mkGoldenTest eq tc occ line col input =   it (input <> " (golden)") $ do     runSessionWithServer plugin tacticPath $ do-      setFeatureSet features-      doc <- openDoc input "haskell"+      doc <- openDoc (input <.> "hs") "haskell"       _ <- waitForDiagnostics       actions <- getCodeActions doc $ pointRange line col       Just (InR CodeAction {_command = Just c})@@ -119,27 +100,54 @@       executeCommand c       _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit)       edited <- documentContents doc-      let expected_name = input <.> "expected"+      let expected_name = input <.> "expected" <.> "hs"       -- Write golden tests if they don't already exist       liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do         T.writeFile expected_name edited       expected <- liftIO $ T.readFile expected_name       liftIO $ edited `eq` expected ++mkCodeLensTest+    :: FilePath+    -> SpecWith ()+mkCodeLensTest input =+  it (input <> " (golden)") $ do+    runSessionWithServer plugin tacticPath $ do+      doc <- openDoc (input <.> "hs") "haskell"+      _ <- waitForDiagnostics+      lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc+      for_ lenses $ \(CodeLens _ (Just cmd) _) ->+        executeCommand cmd+      _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit)+      edited <- documentContents doc+      let expected_name = input <.> "expected" <.> "hs"+      -- Write golden tests if they don't already exist+      liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do+        T.writeFile expected_name edited+      expected <- liftIO $ T.readFile expected_name+      liftIO $ edited `shouldBe` expected++++isWingmanLens :: CodeLens -> Bool+isWingmanLens (CodeLens _ (Just (Command _ cmd _)) _)+    = T.isInfixOf ":tactics:" cmd+isWingmanLens _ = False++ mkShowMessageTest-    :: FeatureSet-    -> TacticCommand+    :: TacticCommand     -> Text     -> Int     -> Int     -> FilePath     -> UserFacingMessage     -> SpecWith ()-mkShowMessageTest features tc occ line col input ufm =+mkShowMessageTest tc occ line col input ufm =   it (input <> " (golden)") $ do     runSessionWithServer plugin tacticPath $ do-      setFeatureSet features-      doc <- openDoc input "haskell"+      doc <- openDoc (input <.> "hs") "haskell"       _ <- waitForDiagnostics       actions <- getCodeActions doc $ pointRange line col       Just (InR CodeAction {_command = Just c})@@ -150,10 +158,10 @@   goldenTest :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()-goldenTest = mkGoldenTest shouldBe allFeatures+goldenTest = mkGoldenTest shouldBe  goldenTestNoWhitespace :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()-goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces allFeatures+goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces   shouldBeIgnoringSpaces :: Text -> Text -> Assertion

@@ -0,0 +1,2 @@+empty_string :: String+empty_string = ""

@@ -1,2 +0,0 @@-empty_string :: String-empty_string = ""

@@ -0,0 +1,11 @@+data Synthesized b a = Synthesized+  { syn_trace :: b+  , syn_val   :: a+  }+  deriving (Eq, Show)+++mapTrace :: (b -> b) -> Synthesized b a -> Synthesized b a+mapTrace fbb (Synthesized b a)+  = Synthesized {syn_trace = fbb b, syn_val = a}+

@@ -1,11 +0,0 @@-data Synthesized b a = Synthesized-  { syn_trace :: b-  , syn_val   :: a-  }-  deriving (Eq, Show)---mapTrace :: (b -> b) -> Synthesized b a -> Synthesized b a-mapTrace fbb (Synthesized b a)-  = Synthesized {syn_trace = fbb b, syn_val = a}-

@@ -0,0 +1,3 @@+test :: (a -> b -> c) -> a -> (a -> b) -> c+test (/:) a f = a /: f a+

@@ -1,3 +0,0 @@-test :: (a -> b -> c) -> a -> (a -> b) -> c-test (/:) a f = a /: f a-

@@ -0,0 +1,3 @@+test :: (a -> b -> x -> c) -> a -> (a -> b) -> x -> c+test (/:) a f x = (a /: f a) x+

@@ -1,3 +0,0 @@-test :: (a -> b -> x -> c) -> a -> (a -> b) -> x -> c-test (/:) a f x = (a /: f a) x-

@@ -0,0 +1,2 @@+test :: (a -> b -> c) -> (c -> d -> e) -> a -> (a -> b) -> d -> e+test (/:) (-->) a f x = (a /: f a) --> x

@@ -1,2 +0,0 @@-test :: (a -> b -> c) -> (c -> d -> e) -> a -> (a -> b) -> d -> e-test (/:) (-->) a f x = (a /: f a) --> x

@@ -0,0 +1,8 @@+{-# LANGUAGE PatternSynonyms #-}++pattern JustSingleton :: a -> Maybe [a]+pattern JustSingleton a <- Just [a]++amIASingleton :: Maybe [a] -> Maybe a+amIASingleton (JustSingleton a) = Just a+

@@ -1,8 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}--pattern JustSingleton :: a -> Maybe [a]-pattern JustSingleton a <- Just [a]--amIASingleton :: Maybe [a] -> Maybe a-amIASingleton (JustSingleton a) = Just a-

@@ -0,0 +1,12 @@+{-# LANGUAGE GADTs #-}++data GADT b a where+  GBool :: b -> GADT b Bool+  GInt :: GADT b Int++-- wingman would prefer to use GBool since then it can use its argument. But+-- that won't unify with GADT Int, so it is forced to pick GInt and ignore the+-- argument.+test :: b -> GADT b Int+test _ = GInt+

@@ -1,12 +0,0 @@-{-# LANGUAGE GADTs #-}--data GADT b a where-  GBool :: b -> GADT b Bool-  GInt :: GADT b Int---- wingman would prefer to use GBool since then it can use its argument. But--- that won't unify with GADT Int, so it is forced to pick GInt and ignore the--- argument.-test :: b -> GADT b Int-test _ = GInt-

@@ -0,0 +1,5 @@+{-# LANGUAGE GADTs #-}++fun2 :: (a ~ b) => a -> b+fun2 = id -- id+

@@ -1,5 +0,0 @@-{-# LANGUAGE GADTs #-}--fun2 :: (a ~ b) => a -> b-fun2 = id -- id-

@@ -0,0 +1,7 @@+{-# LANGUAGE GADTs #-}++data Y a b = a ~ b => Y++fun3 :: Y a b -> a -> b+fun3 Y = id+

@@ -1,7 +0,0 @@-{-# LANGUAGE GADTs #-}--data Y a b = a ~ b => Y--fun3 :: Y a b -> a -> b-fun3 Y = id-

@@ -0,0 +1,8 @@+{-# LANGUAGE GADTs #-}++data Y a b = a ~ b => Y++fun3 :: Y a b -> a -> b+fun3 Y a = a++

@@ -1,8 +0,0 @@-{-# LANGUAGE GADTs #-}--data Y a b = a ~ b => Y--fun3 :: Y a b -> a -> b-fun3 Y a = a--

@@ -0,0 +1,13 @@+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE UndecidableInstances #-}++data Fix f a = Fix (f (Fix f a))++instance ( Functor f+           -- FIXME(sandy): Unfortunately, the recursion tactic fails to fire+           -- on this case. By explicitly adding the @Functor (Fix f)@+           -- dictionary, we can get Wingman to generate the right definition.+         , Functor (Fix f)+         ) => Functor (Fix f) where+  fmap fab (Fix f) = Fix (fmap (fmap fab) f)+

@@ -1,13 +0,0 @@-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE UndecidableInstances #-}--data Fix f a = Fix (f (Fix f a))--instance ( Functor f-           -- FIXME(sandy): Unfortunately, the recursion tactic fails to fire-           -- on this case. By explicitly adding the @Functor (Fix f)@-           -- dictionary, we can get Wingman to generate the right definition.-         , Functor (Fix f)-         ) => Functor (Fix f) where-  fmap fab (Fix fffa) = Fix (fmap (fmap fab) fffa)-

@@ -0,0 +1,7 @@+{-# LANGUAGE GADTs #-}++data X f = Monad f => X++fun1 :: X f -> a -> f a+fun1 X = pure+

@@ -1,7 +0,0 @@-{-# LANGUAGE GADTs #-}--data X f = Monad f => X--fun1 :: X f -> a -> f a-fun1 X = pure-

@@ -0,0 +1,7 @@+{-# LANGUAGE GADTs #-}++data X f = Monad f => X++fun1 :: X f -> a -> f a+fun1 X a = pure a+

@@ -1,7 +0,0 @@-{-# LANGUAGE GADTs #-}--data X f = Monad f => X--fun1 :: X f -> a -> f a-fun1 X a = pure a-

@@ -0,0 +1,21 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE GADTs          #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators  #-}++import Data.Kind++data Nat = Z | S Nat++data HList (ls :: [Type]) where+  HNil :: HList '[]+  HCons :: t -> HList ts -> HList (t ': ts)++data ElemAt (n :: Nat) t (ts :: [Type]) where+  AtZ :: ElemAt 'Z t (t ': ts)+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)++lookMeUp :: ElemAt i ty tys -> HList tys -> ty+lookMeUp AtZ (HCons t _) = t+lookMeUp (AtS ea') (HCons t hl') = _+

@@ -0,0 +1,21 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE GADTs          #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators  #-}++import Data.Kind++data Nat = Z | S Nat++data HList (ls :: [Type]) where+  HNil :: HList '[]+  HCons :: t -> HList ts -> HList (t ': ts)++data ElemAt (n :: Nat) t (ts :: [Type]) where+  AtZ :: ElemAt 'Z t (t ': ts)+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)++lookMeUp :: ElemAt i ty tys -> HList tys -> ty+lookMeUp AtZ (HCons t hl') = _+lookMeUp (AtS ea') (HCons t hl') = _+

@@ -0,0 +1,8 @@+{-# LANGUAGE RankNTypes #-}++showMe :: (forall x. Show x => x -> String) -> Int -> String+showMe f = f++showedYou :: Int -> String+showedYou = showMe show+

@@ -1,8 +0,0 @@-{-# LANGUAGE RankNTypes #-}--showMe :: (forall x. Show x => x -> String) -> Int -> String-showMe f = f--showedYou :: Int -> String-showedYou = showMe show-

@@ -0,0 +1,7 @@+{-# LANGUAGE GADTs #-}++data Z a b where Z :: Z a a++fun4 :: Z a b -> a -> b+fun4 Z = id -- id+

@@ -1,7 +0,0 @@-{-# LANGUAGE GADTs #-}--data Z a b where Z :: Z a a--fun4 :: Z a b -> a -> b-fun4 Z = id -- id-

@@ -0,0 +1,8 @@+{-# LANGUAGE GADTs #-}++data Z a b where Z :: Z a a++fun4 :: Z a b -> a -> b+fun4 Z a = a -- id++

@@ -1,8 +0,0 @@-{-# LANGUAGE GADTs #-}--data Z a b where Z :: Z a a--fun4 :: Z a b -> a -> b-fun4 Z a = a -- id--

@@ -0,0 +1,17 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE GADTs          #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators  #-}++data A = A+data B = B+data X = X+data Y = Y+++data Pairrow ax by  where+  Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y)++test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y)+test2 = Pairrow+

@@ -0,0 +1,17 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE GADTs          #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators  #-}++data A = A+data B = B+data X = X+data Y = Y+++data Pairrow ax by  where+  Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y)++test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y)+test2 = _+

@@ -0,0 +1,6 @@+zip_it_up_and_zip_it_out :: [a] -> [b] -> [(a, b)]+zip_it_up_and_zip_it_out _ [] = []+zip_it_up_and_zip_it_out [] (_ : _) = []+zip_it_up_and_zip_it_out (a : as') (b : bs')+  = (a, b) : zip_it_up_and_zip_it_out as' bs'+

@@ -1,6 +0,0 @@-zip_it_up_and_zip_it_out :: [a] -> [b] -> [(a, b)]-zip_it_up_and_zip_it_out _ [] = []-zip_it_up_and_zip_it_out [] (_ : _) = []-zip_it_up_and_zip_it_out (a : l_a5) (b : l_b3)-  = (a, b) : zip_it_up_and_zip_it_out l_a5 l_b3-

@@ -0,0 +1,5 @@+and :: Bool -> Bool -> Bool+and False False = _+and False True = _+and True False = _+and True True = _

@@ -1,5 +0,0 @@-and :: Bool -> Bool -> Bool-and False False = _-and True False = _-and False True = _-and True True = _

@@ -0,0 +1,4 @@+has_a_func :: Bool -> (a -> b) -> Bool+has_a_func False y = _+has_a_func True y = _+

@@ -1,4 +0,0 @@-has_a_func :: Bool -> (a -> b) -> Bool-has_a_func False y = _-has_a_func True y = _-

@@ -0,0 +1,21 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE GADTs          #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators  #-}++import Data.Kind++data Nat = Z | S Nat++data HList (ls :: [Type]) where+  HNil :: HList '[]+  HCons :: t -> HList ts -> HList (t ': ts)++data ElemAt (n :: Nat) t (ts :: [Type]) where+  AtZ :: ElemAt 'Z t (t ': ts)+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)++lookMeUp :: ElemAt i ty tys -> HList tys -> ty+lookMeUp AtZ (HCons t hl') = _+lookMeUp (AtS ea') (HCons t hl') = _+

@@ -0,0 +1,20 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE GADTs          #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators  #-}++import Data.Kind++data Nat = Z | S Nat++data HList (ls :: [Type]) where+  HNil :: HList '[]+  HCons :: t -> HList ts -> HList (t ': ts)++data ElemAt (n :: Nat) t (ts :: [Type]) where+  AtZ :: ElemAt 'Z t (t ': ts)+  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)++lookMeUp :: ElemAt i ty tys -> HList tys -> ty+lookMeUp ea hl = _+

@@ -0,0 +1,27 @@+data ABC = A | B | C++many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()+many () (Left a) False Nothing A = _+many () (Left a) False Nothing B = _+many () (Left a) False Nothing C = _+many () (Left a) False (Just abc') A = _+many () (Left a) False (Just abc') B = _+many () (Left a) False (Just abc') C = _+many () (Left a) True Nothing A = _+many () (Left a) True Nothing B = _+many () (Left a) True Nothing C = _+many () (Left a) True (Just abc') A = _+many () (Left a) True (Just abc') B = _+many () (Left a) True (Just abc') C = _+many () (Right b') False Nothing A = _+many () (Right b') False Nothing B = _+many () (Right b') False Nothing C = _+many () (Right b') False (Just abc') A = _+many () (Right b') False (Just abc') B = _+many () (Right b') False (Just abc') C = _+many () (Right b') True Nothing A = _+many () (Right b') True Nothing B = _+many () (Right b') True Nothing C = _+many () (Right b') True (Just abc') A = _+many () (Right b') True (Just abc') B = _+many () (Right b') True (Just abc') C = _

@@ -1,27 +0,0 @@-data ABC = A | B | C--many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> ()-many () (Left a) False Nothing A = _-many () (Right b5) False Nothing A = _-many () (Left a) True Nothing A = _-many () (Right b5) True Nothing A = _-many () (Left a6) False (Just a) A = _-many () (Right b6) False (Just a) A = _-many () (Left a6) True (Just a) A = _-many () (Right b6) True (Just a) A = _-many () (Left a) False Nothing B = _-many () (Right b5) False Nothing B = _-many () (Left a) True Nothing B = _-many () (Right b5) True Nothing B = _-many () (Left a6) False (Just a) B = _-many () (Right b6) False (Just a) B = _-many () (Left a6) True (Just a) B = _-many () (Right b6) True (Just a) B = _-many () (Left a) False Nothing C = _-many () (Right b5) False Nothing C = _-many () (Left a) True Nothing C = _-many () (Right b5) True Nothing C = _-many () (Left a6) False (Just a) C = _-many () (Right b6) False (Just a) C = _-many () (Left a6) True (Just a) C = _-many () (Right b6) True (Just a) C = _

@@ -0,0 +1,6 @@+and :: (a, b) -> Bool -> Bool -> Bool+and (a, b) False False = _+and (a, b) False True = _+and (a, b) True False = _+and (a, b) True True = _+

@@ -1,6 +0,0 @@-and :: (a, b) -> Bool -> Bool -> Bool-and (a, b) False False = _-and (a, b) True False = _-and (a, b) False True = _-and (a, b) True True = _-

@@ -0,0 +1,54 @@+{-# LANGUAGE GADTs #-}++data FreePro r c a b where+  ID        :: FreePro r c x x+  Comp      :: FreePro r c x y -> FreePro r c y z -> FreePro r c x z+  Copy      :: FreePro r c x (x, x)+  Consume   :: FreePro r c x ()+  Swap      :: FreePro r c (a, b) (b, a)+  SwapE     :: FreePro r c (Either a b) (Either b a)+  Fst       :: FreePro r c (a, b) a+  Snd       :: FreePro r c (a, b) b+  InjectL   :: FreePro r c a (Either a b)+  InjectR   :: FreePro r c b (Either a b)+  Unify     :: FreePro r c (Either a a) a+  First     :: FreePro r c a b -> FreePro r c (a, m) (b, m)+  Second    :: FreePro r c a b -> FreePro r c (m, a) (m, b)+  Alongside :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (a, a') (b, b')+  Fanout    :: FreePro r c a b -> FreePro r c a b' -> FreePro r c a (b, b')+  Left'     :: FreePro r c a b -> FreePro r c (Either a x) (Either b x)+  Right'    :: FreePro r c a b -> FreePro r c (Either x a) (Either x b)+  EitherOf  :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (Either a a') (Either b b')+  Fanin     :: FreePro r c a b -> FreePro r c a' b -> FreePro r c (Either a a') b+  LiftC     :: c a b -> FreePro r c a b+  Zero      :: FreePro r c x y+  Plus      :: FreePro r c x y -> FreePro r c x y -> FreePro r c x y+  Unleft    :: FreePro r c (Either a d) (Either b d) -> FreePro r c a b+  Unright   :: FreePro r c (Either d a) (Either d b) -> FreePro r c a b+++cthulhu :: FreePro r c a b -> FreePro r c a b+cthulhu ID = _+cthulhu (Comp fp' fp_rcyb) = _+cthulhu Copy = _+cthulhu Consume = _+cthulhu Swap = _+cthulhu SwapE = _+cthulhu Fst = _+cthulhu Snd = _+cthulhu InjectL = _+cthulhu InjectR = _+cthulhu Unify = _+cthulhu (First fp') = _+cthulhu (Second fp') = _+cthulhu (Alongside fp' fp_rca'b') = _+cthulhu (Fanout fp' fp_rcab') = _+cthulhu (Left' fp') = _+cthulhu (Right' fp') = _+cthulhu (EitherOf fp' fp_rca'b') = _+cthulhu (Fanin fp' fp_rca'b) = _+cthulhu (LiftC cab) = _+cthulhu Zero = _+cthulhu (Plus fp' fp_rcab) = _+cthulhu (Unleft fp') = _+cthulhu (Unright fp') = _

@@ -0,0 +1,31 @@+{-# LANGUAGE GADTs #-}++data FreePro r c a b where+  ID        :: FreePro r c x x+  Comp      :: FreePro r c x y -> FreePro r c y z -> FreePro r c x z+  Copy      :: FreePro r c x (x, x)+  Consume   :: FreePro r c x ()+  Swap      :: FreePro r c (a, b) (b, a)+  SwapE     :: FreePro r c (Either a b) (Either b a)+  Fst       :: FreePro r c (a, b) a+  Snd       :: FreePro r c (a, b) b+  InjectL   :: FreePro r c a (Either a b)+  InjectR   :: FreePro r c b (Either a b)+  Unify     :: FreePro r c (Either a a) a+  First     :: FreePro r c a b -> FreePro r c (a, m) (b, m)+  Second    :: FreePro r c a b -> FreePro r c (m, a) (m, b)+  Alongside :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (a, a') (b, b')+  Fanout    :: FreePro r c a b -> FreePro r c a b' -> FreePro r c a (b, b')+  Left'     :: FreePro r c a b -> FreePro r c (Either a x) (Either b x)+  Right'    :: FreePro r c a b -> FreePro r c (Either x a) (Either x b)+  EitherOf  :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (Either a a') (Either b b')+  Fanin     :: FreePro r c a b -> FreePro r c a' b -> FreePro r c (Either a a') b+  LiftC     :: c a b -> FreePro r c a b+  Zero      :: FreePro r c x y+  Plus      :: FreePro r c x y -> FreePro r c x y -> FreePro r c x y+  Unleft    :: FreePro r c (Either a d) (Either b d) -> FreePro r c a b+  Unright   :: FreePro r c (Either d a) (Either d b) -> FreePro r c a b+++cthulhu :: FreePro r c a b -> FreePro r c a b+cthulhu fp = _

@@ -0,0 +1,8 @@+{-# LANGUAGE TypeFamilies #-}++data family Yo+data instance Yo = Heya Int++test :: Yo -> Int+test (Heya n) = _+

@@ -0,0 +1,8 @@+{-# LANGUAGE TypeFamilies #-}++data family Yo+data instance Yo = Heya Int++test :: Yo -> Int+test b = _+

@@ -0,0 +1,8 @@+{-# LANGUAGE NamedFieldPuns #-}+++data Foo = Foo { a :: Bool, b :: Bool }++foo Foo {a = False, b} = _+foo Foo {a = True, b} = _+

@@ -0,0 +1,7 @@+{-# LANGUAGE NamedFieldPuns #-}+++data Foo = Foo { a :: Bool, b :: Bool }++foo Foo {a, b} = _+

@@ -0,0 +1,9 @@+{-# LANGUAGE TypeFamilies #-}++type family Yo where+  Yo = Bool++test :: Yo -> Int+test False = _+test True = _+

@@ -0,0 +1,8 @@+{-# LANGUAGE TypeFamilies #-}++type family Yo where+  Yo = Bool++test :: Yo -> Int+test b = _+

@@ -0,0 +1,18 @@+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE UndecidableInstances #-}++type family T1 a where+  T1 a = T2 Int++type family T2 a+type instance T2 Int = T3++type family T3 where+  T3 = Yo++data family Yo+data instance Yo = Heya Int++test :: T1 Bool -> Int+test (Heya n) = _+

@@ -0,0 +1,18 @@+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE UndecidableInstances #-}++type family T1 a where+  T1 a = T2 Int++type family T2 a+type instance T2 Int = T3++type family T3 where+  T3 = Yo++data family Yo+data instance Yo = Heya Int++test :: T1 Bool -> Int+test b = _+

@@ -0,0 +1,8 @@+data Foo = A Int | B Bool | C++foo :: Foo -> ()+foo x = case x of+  A n -> _+  B b -> _+  C -> _+

@@ -0,0 +1,5 @@+data Foo = A Int | B Bool | C++foo :: Foo -> ()+foo x = case x of+

@@ -0,0 +1,3 @@+blah = case show 5 of+  [] -> _+  c : s -> _

@@ -0,0 +1,1 @@+blah = case show 5 of

@@ -0,0 +1,13 @@+{-# LANGUAGE GADTs #-}++data GADT a where+  MyInt :: GADT Int+  MyBool :: GADT Bool+  MyVar :: GADT a+++test :: GADT Int -> GADT Bool+test x = case x of+  MyInt -> _+  MyVar -> _+

@@ -0,0 +1,11 @@+{-# LANGUAGE GADTs #-}++data GADT a where+  MyInt :: GADT Int+  MyBool :: GADT Bool+  MyVar :: GADT a+++test :: GADT Int -> GADT Bool+test x = case x of+

@@ -0,0 +1,5 @@+test =+  case (case (Just "") of+  Nothing -> _+  Just s -> _) of+    True -> _

@@ -0,0 +1,3 @@+test =+  case (case (Just "") of) of+    True -> _

@@ -0,0 +1,3 @@+test = True && (case True of+   False -> _+   True -> _)

@@ -0,0 +1,1 @@+test = True && case True of

@@ -0,0 +1,10 @@+data Foo = A Int | B Bool | C++-- Make sure we don't shadow the i and b bindings when we empty case+-- split+foo :: Int -> Bool -> Foo -> ()+foo i b x = case x of+  A n -> _+  B b' -> _+  C -> _+

@@ -0,0 +1,7 @@+data Foo = A Int | B Bool | C++-- Make sure we don't shadow the i and b bindings when we empty case+-- split+foo :: Int -> Bool -> Foo -> ()+foo i b x = case x of+

@@ -0,0 +1,2 @@+fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b))+fgmap = fmap . fmap

@@ -1,2 +0,0 @@-fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b))-fgmap = fmap . fmap

@@ -0,0 +1,3 @@+fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)+fmapBoth fab (fa, ga) = (fmap fab fa, fmap fab ga)+

@@ -1,3 +0,0 @@-fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)-fmapBoth fab (fa, ga) = (fmap fab fa, fmap fab ga)-

@@ -0,0 +1,2 @@+fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a)+fJoin = fmap (\ m -> m >>= id)

@@ -1,2 +0,0 @@-fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a)-fJoin = fmap (\ mma -> mma >>= id)

@@ -0,0 +1,4 @@+{-# LANGUAGE ScopedTypeVariables #-}++fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a)+fJoin =  let f = ( (\ m -> m >>= id) :: m (m a) -> m a) in fmap f

@@ -1,4 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}--fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a)-fJoin =  let f = ( (\ mma -> mma >>= id) :: m (m a) -> m a) in fmap f

@@ -0,0 +1,53 @@+-- Emulate a quickcheck import; deriveArbitrary works on any type with the+-- right name and kind+data Gen a++data Obj+  = Square Int Int+  | Circle Int+  | Polygon [(Int, Int)]+  | Rotate2 Double Obj+  | Empty+  | Full+  | Complement Obj+  | UnionR Double [Obj]+  | DifferenceR Double Obj [Obj]+  | IntersectR Double [Obj]+  | Translate Double Double Obj+  | Scale Double Double Obj+  | Mirror Double Double Obj+  | Outset Double Obj+  | Shell Double Obj+  | WithRounding Double Obj+++arbitrary :: Gen Obj+arbitrary+  = let+      terminal+        = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary,+           Polygon <$> arbitrary, pure Empty, pure Full]+    in+      sized+        $ (\ n+             -> case n <= 1 of+                  True -> oneof terminal+                  False+                    -> oneof+                         $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary,+                             Complement <$> scale (subtract 1) arbitrary,+                             (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary,+                             ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary)+                               <*> scale (flip div 2) arbitrary,+                             (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary,+                             ((Translate <$> arbitrary) <*> arbitrary)+                               <*> scale (subtract 1) arbitrary,+                             ((Scale <$> arbitrary) <*> arbitrary)+                               <*> scale (subtract 1) arbitrary,+                             ((Mirror <$> arbitrary) <*> arbitrary)+                               <*> scale (subtract 1) arbitrary,+                             (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary,+                             (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary,+                             (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary]+                              <> terminal))+

@@ -1,53 +0,0 @@--- Emulate a quickcheck import; deriveArbitrary works on any type with the--- right name and kind-data Gen a--data Obj-  = Square Int Int-  | Circle Int-  | Polygon [(Int, Int)]-  | Rotate2 Double Obj-  | Empty-  | Full-  | Complement Obj-  | UnionR Double [Obj]-  | DifferenceR Double Obj [Obj]-  | IntersectR Double [Obj]-  | Translate Double Double Obj-  | Scale Double Double Obj-  | Mirror Double Double Obj-  | Outset Double Obj-  | Shell Double Obj-  | WithRounding Double Obj---arbitrary :: Gen Obj-arbitrary-  = let-      terminal-        = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary,-           Polygon <$> arbitrary, pure Empty, pure Full]-    in-      sized-        $ (\ n-             -> case n <= 1 of-                  True -> oneof terminal-                  False-                    -> oneof-                         $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary,-                             Complement <$> scale (subtract 1) arbitrary,-                             (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary,-                             ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary)-                               <*> scale (flip div 2) arbitrary,-                             (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary,-                             ((Translate <$> arbitrary) <*> arbitrary)-                               <*> scale (subtract 1) arbitrary,-                             ((Scale <$> arbitrary) <*> arbitrary)-                               <*> scale (subtract 1) arbitrary,-                             ((Mirror <$> arbitrary) <*> arbitrary)-                               <*> scale (subtract 1) arbitrary,-                             (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary,-                             (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary,-                             (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary]-                              <> terminal))-

@@ -0,0 +1,4 @@+-- There used to be a bug where we were unable to perform a nested split. The+-- more serious regression test of this is 'AutoTupleSpec'.+bigTuple :: (a, b, c, d) -> (a, b, (c, d))+bigTuple (a, b, c, d) = (a, b, (c, d))

@@ -1,4 +0,0 @@--- There used to be a bug where we were unable to perform a nested split. The--- more serious regression test of this is 'AutoTupleSpec'.-bigTuple :: (a, b, c, d) -> (a, b, (c, d))-bigTuple (a, b, c, d) = (a, b, (c, d))

@@ -0,0 +1,3 @@+either' :: (a -> c) -> (b -> c) -> Either a b -> c+either' fac _ (Left a) = fac a+either' _ fbc (Right b) = fbc b

@@ -1,3 +0,0 @@-either' :: (a -> c) -> (b -> c) -> Either a b -> c-either' fac _ (Left a) = fac a-either' _ fbc (Right b) = fbc b

@@ -0,0 +1,3 @@+eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c+eitherSplit a (Left fab) = Left (fab a)+eitherSplit a (Right fac) = Right (fac a)

@@ -1,3 +0,0 @@-eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c-eitherSplit a (Left fab) = Left (fab a)-eitherSplit a (Right fac) = Right (fac a)

@@ -0,0 +1,5 @@+data Tree a = Leaf a | Branch (Tree a) (Tree a)++instance Functor Tree where+   fmap fab (Leaf a) = Leaf (fab a)+   fmap fab (Branch tr' tr_a) = Branch (fmap fab tr') (fmap fab tr_a)

@@ -1,5 +0,0 @@-data Tree a = Leaf a | Branch (Tree a) (Tree a)--instance Functor Tree where-   fmap fab (Leaf a) = Leaf (fab a)-   fmap fab (Branch ta2 ta3) = Branch (fmap fab ta2) (fmap fab ta3)

@@ -0,0 +1,3 @@+foldr2 :: (a -> b -> b) -> b -> [a] -> b+foldr2 _ b [] = b+foldr2 fabb b (a : as') = fabb a (foldr2 fabb b as')

@@ -1,3 +0,0 @@-foldr2 :: (a -> b -> b) -> b -> [a] -> b-foldr2 _ b [] = b-foldr2 f_b b (a : l_a4) = f_b a (foldr2 f_b b l_a4)

@@ -0,0 +1,3 @@+fromMaybe :: a -> Maybe a -> a+fromMaybe a Nothing = a+fromMaybe _ (Just a') = a'

@@ -1,3 +0,0 @@-fromMaybe :: a -> Maybe a -> a-fromMaybe a Nothing = a-fromMaybe _ (Just a2) = a2

@@ -0,0 +1,7 @@+{-# LANGUAGE GADTs #-}+module GoldenGADTAuto where+data CtxGADT a where+  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a++ctxGADT :: CtxGADT ()+ctxGADT = MkCtxGADT ()

@@ -1,7 +0,0 @@-{-# LANGUAGE GADTs #-}-module GoldenGADTAuto where-data CtxGADT a where-  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a--ctxGADT :: CtxGADT ()-ctxGADT = MkCtxGADT ()

@@ -0,0 +1,7 @@+{-# LANGUAGE GADTs #-}+module GoldenGADTDestruct where+data CtxGADT where+  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT++ctxGADT :: CtxGADT -> String+ctxGADT (MkCtxGADT a) = _

@@ -1,7 +0,0 @@-{-# LANGUAGE GADTs #-}-module GoldenGADTDestruct where-data CtxGADT where-  MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT--ctxGADT :: CtxGADT -> String-ctxGADT (MkCtxGADT a) = _

@@ -0,0 +1,8 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs #-}+module GoldenGADTDestruct where+data E a b where+  E :: forall a b. (b ~ a, Ord a) => b -> E a [a]++ctxGADT :: E a b -> String+ctxGADT (E b) = _

@@ -1,8 +0,0 @@-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE GADTs #-}-module GoldenGADTDestruct where-data E a b where-  E :: forall a b. (b ~ a, Ord a) => b -> E a [a]--ctxGADT :: E a b -> String-ctxGADT (E b) = _

@@ -0,0 +1,7 @@+{-# LANGUAGE TypeFamilies #-}++type family TyFam+type instance TyFam = Int++tyblah' :: TyFam -> Int+tyblah' = id

@@ -1,7 +0,0 @@-{-# LANGUAGE TypeFamilies #-}--type family TyFam-type instance TyFam = Int--tyblah' :: TyFam -> Int-tyblah' = id

@@ -0,0 +1,3 @@+data Ident a = Ident a+instance Functor Ident where+   fmap fab (Ident a) = Ident (fab a)

@@ -1,3 +0,0 @@-data Ident a = Ident a-instance Functor Ident where-   fmap fab (Ident a) = Ident (fab a)

@@ -0,0 +1,2 @@+blah :: Int -> Bool -> (a -> b) -> String -> Int+blah n b fab s = _

@@ -1,2 +0,0 @@-blah :: Int -> Bool -> (a -> b) -> String -> Int-blah i b fab l_c = _

@@ -0,0 +1,4 @@+type Cont r a = ((a -> r) -> r)++joinCont :: Cont r (Cont r a) -> Cont r a+joinCont f far = f (\ g -> g far)

@@ -1,4 +0,0 @@-type Cont r a = ((a -> r) -> r)--joinCont :: Cont r (Cont r a) -> Cont r a-joinCont f_r far = f_r (\ f_r2 -> f_r2 far)

@@ -0,0 +1,3 @@+fmapList :: (a -> b) -> [a] -> [b]+fmapList _ [] = []+fmapList fab (a : as') = fab a : fmapList fab as'

@@ -1,3 +0,0 @@-fmapList :: (a -> b) -> [a] -> [b]-fmapList _ [] = []-fmapList fab (a : l_a3) = fab a : fmapList fab l_a3

@@ -0,0 +1,3 @@+note :: e -> Maybe a -> Either e a+note e Nothing = Left e+note _ (Just a) = Right a

@@ -1,3 +0,0 @@-note :: e -> Maybe a -> Either e a-note e Nothing = Left e-note _ (Just a) = Right a

@@ -0,0 +1,2 @@+pureList :: a -> [a]+pureList a = a : []

@@ -1,2 +0,0 @@-pureList :: a -> [a]-pureList a = a : []

@@ -0,0 +1,3 @@+safeHead :: [x] -> Maybe x+safeHead [] = Nothing+safeHead (x : _) = Just x

@@ -1,3 +0,0 @@-safeHead :: [x] -> Maybe x-safeHead [] = Nothing-safeHead (x : _) = Just x

@@ -0,0 +1,2 @@+showMe :: Show a => a -> String+showMe = show

@@ -1,2 +0,0 @@-showMe :: Show a => a -> String-showMe = show

@@ -0,0 +1,2 @@+showCompose :: Show a => (b -> a) -> b -> String+showCompose fba = show . fba

@@ -1,2 +0,0 @@-showCompose :: Show a => (b -> a) -> b -> String-showCompose fba = show . fba

@@ -0,0 +1,2 @@+test :: Show a => a -> (String -> b) -> b+test a f = f (show a)

@@ -1,2 +0,0 @@-test :: Show a => a -> (String -> b) -> b-test a fl_cb = fl_cb (show a)

@@ -0,0 +1,8 @@+class Super a where+    super :: a++class Super a => Sub a++blah :: Sub a => a+blah = super+

@@ -1,8 +0,0 @@-class Super a where-    super :: a--class Super a => Sub a--blah :: Sub a => a-blah = super-

@@ -0,0 +1,2 @@+swap :: (a, b) -> (b, a)+swap (a, b) = (b, a)

@@ -1,2 +0,0 @@-swap :: (a, b) -> (b, a)-swap (a, b) = (b, a)

@@ -0,0 +1,2 @@+swapMany :: (a, b, c, d, e) -> (e, d, c, b, a)+swapMany (a, b, c, d, e) = (e, d, c, b, a)

@@ -1,2 +0,0 @@-swapMany :: (a, b, c, d, e) -> (e, d, c, b, a)-swapMany (a, b, c, d, e) = (e, d, c, b, a)

@@ -0,0 +1,9 @@+import Data.Monoid++data Big a = Big [Bool] (Sum Int) String (Endo a) Any++instance Semigroup (Big a) where+  (<>) (Big bs sum s en any) (Big bs' sum' str en' any')+    = Big+        (bs <> bs') (sum <> sum') (s <> str) (en <> en') (any <> any')+

@@ -1,9 +0,0 @@-import Data.Monoid--data Big a = Big [Bool] (Sum Int) String (Endo a) Any--instance Semigroup (Big a) where-  (<>) (Big l_b7 si8 l_c9 ea10 a11) (Big l_b si l_c ea a)-    = Big-        (l_b7 <> l_b) (si8 <> si) (l_c9 <> l_c) (ea10 <> ea) (a11 <> a)-

@@ -0,0 +1,7 @@+{-# LANGUAGE UndecidableInstances #-}++data Semi = Semi [String] Int++instance Semigroup Int => Semigroup Semi where+  (<>) (Semi ss n) (Semi strs i) = Semi (ss <> strs) (n <> i)+

@@ -1,8 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--data Semi = Semi [String] Int--instance Semigroup Int => Semigroup Semi where-  (<>) (Semi l_l_c5 i6) (Semi l_l_c i)-    = Semi (l_l_c5 <> l_l_c) (i6 <> i)-

@@ -0,0 +1,5 @@+data Test a = Test [a]++instance Semigroup (Test a) where+  (<>) (Test a) (Test c) = Test (a <> c)+

@@ -1,5 +0,0 @@-data Test a = Test [a]--instance Semigroup (Test a) where-  (<>) (Test a) (Test c) = Test (a <> c)-

@@ -0,0 +1,8 @@+data Mono a = Monoid [String] a++instance Semigroup (Mono a) where+  (<>) = undefined++instance Monoid (Mono a) where+  mempty = Monoid mempty _+

@@ -1,8 +0,0 @@-data Mono a = Monoid [String] a--instance Semigroup (Mono a) where-  (<>) = undefined--instance Monoid (Mono a) where-  mempty = Monoid mempty _-

@@ -0,0 +1,5 @@+data Semi = Semi [String] Int++instance Semigroup Semi where+  (<>) (Semi ss n) (Semi strs i) = Semi (ss <> strs) _+

@@ -1,5 +0,0 @@-data Semi = Semi [String] Int--instance Semigroup Semi where-  (<>) (Semi l_l_c4 i5) (Semi l_l_c i) = Semi (l_l_c4 <> l_l_c) _-

@@ -0,0 +1,12 @@+data Foo = Foo++instance Semigroup Foo where+  (<>) _ _ = Foo+++data Bar = Bar Foo Foo++instance Semigroup Bar where+  (<>) (Bar foo foo') (Bar foo2 foo3)+    = Bar (foo <> foo2) (foo' <> foo3)+

@@ -1,11 +0,0 @@-data Foo = Foo--instance Semigroup Foo where-  (<>) _ _ = Foo---data Bar = Bar Foo Foo--instance Semigroup Bar where-  (<>) (Bar f4 f5) (Bar f f3) = Bar (f4 <> f) (f5 <> f3)-

@@ -0,0 +1,8 @@+data Mono = Monoid [String]++instance Semigroup Mono where+  (<>) = undefined++instance Monoid Mono where+  mempty = Monoid mempty+

@@ -1,8 +0,0 @@-data Mono = Monoid [String]--instance Semigroup Mono where-  (<>) = undefined--instance Monoid Mono where-  mempty = Monoid mempty-

@@ -0,0 +1,8 @@+data Mono a = Monoid [String] a++instance Semigroup (Mono a) where+  (<>) = undefined++instance Monoid a => Monoid (Mono a) where+  mempty = Monoid mempty mempty+

@@ -1,8 +0,0 @@-data Mono a = Monoid [String] a--instance Semigroup (Mono a) where-  (<>) = undefined--instance Monoid a => Monoid (Mono a) where-  mempty = Monoid mempty mempty-

@@ -0,0 +1,5 @@+data Semi a = Semi a++instance Semigroup a => Semigroup (Semi a) where+  (<>) (Semi a) (Semi a') = Semi (a <> a')+

@@ -1,5 +0,0 @@-data Semi a = Semi a--instance Semigroup a => Semigroup (Semi a) where-  (<>) (Semi a4) (Semi a) = Semi (a4 <> a)-

@@ -0,0 +1,8 @@+test :: Bool -> IO ()+test b = do+  putStrLn "hello"+  case b of+    False -> _+    True -> _+  pure ()+

@@ -1,8 +0,0 @@-test :: Bool -> IO ()-test b = do-  putStrLn "hello"-  case b of-    False -> _-    True -> _-  pure ()-

@@ -0,0 +1,5 @@+test :: Bool -> Bool+test b = id $ (case b of+   False -> _+   True -> _)+

@@ -1,5 +0,0 @@-test :: Bool -> Bool-test b = id $ (case b of-   False -> _-   True -> _)-

@@ -0,0 +1,5 @@+test :: Bool -> Bool+test = \b -> case b of+  False -> _+  True -> _+

@@ -1,5 +0,0 @@-test :: Bool -> Bool-test = \b -> case b of-  False -> _-  True -> _-

@@ -0,0 +1,4 @@+test :: Bool -> Bool+test b = True && (case b of+   False -> _+   True -> _)

@@ -1,4 +0,0 @@-test :: Bool -> Bool-test b = True && (case b of-   False -> _-   True -> _)

@@ -0,0 +1,5 @@+data Pair a b = Pair {pa :: a, pb :: b}++p :: Pair (a -> a) (a -> b -> c -> b)+p = Pair {pa = _, pb = \ a b c -> _}+

@@ -0,0 +1,5 @@+data Pair a b = Pair {pa :: a, pb :: b}++p :: Pair (a -> a) (a -> b -> c -> b)+p = Pair {pa = _, pb = _}+

@@ -0,0 +1,5 @@+class Test a where+  test :: Bool -> a+  test False = _+  test True = _+

@@ -1,5 +0,0 @@-class Test a where-  test :: Bool -> a-  test False = _-  test True = _-

@@ -0,0 +1,5 @@+test :: Bool -> Bool -> Bool+test a b+  | a = case b of+  False -> _+  True -> _

@@ -1,5 +0,0 @@-test :: Bool -> Bool -> Bool-test a b-  | a = (case b of-   False -> _-   True -> _)

@@ -0,0 +1,5 @@+test :: a+test =+  let a = (1,"bbb")+   in case a of { (n, s) -> _ }+

@@ -1,5 +0,0 @@-test :: a-test =-  let a = (1,"bbb")-   in case a of { (i, l_c) -> _ }-

@@ -0,0 +1,7 @@+test :: a+test =+  let t :: Bool -> a+      t False = _+      t True = _+   in _+

@@ -1,7 +0,0 @@-test :: a-test =-  let t :: Bool -> a-      t False = _-      t True = _-   in _-

@@ -0,0 +1,11 @@+{-# LANGUAGE PatternSynonyms #-}++pattern JustSingleton :: a -> Maybe [a]+pattern JustSingleton a <- Just [a]+++test :: Maybe [Bool] -> Maybe Bool+test (JustSingleton False) = _+test (JustSingleton True) = _++

@@ -1,11 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}--pattern JustSingleton :: a -> Maybe [a]-pattern JustSingleton a <- Just [a]---test :: Maybe [Bool] -> Maybe Bool-test (JustSingleton False) = _-test (JustSingleton True) = _--

@@ -0,0 +1,9 @@+{-# LANGUAGE PatternSynonyms #-}++pattern Blah :: a -> Maybe a+pattern Blah a = Just a++test :: Maybe Bool -> a+test (Blah False) = _+test (Blah True) = _+

@@ -1,9 +0,0 @@-{-# LANGUAGE PatternSynonyms #-}--pattern Blah :: a -> Maybe a-pattern Blah a = Just a--test :: Maybe Bool -> a-test (Blah False) = _-test (Blah True) = _-

@@ -0,0 +1,6 @@+{-# LANGUAGE ViewPatterns #-}++splitLookup :: [(Int, String)] -> String+splitLookup (lookup 5 -> Nothing) = _+splitLookup (lookup 5 -> (Just s)) = _+

@@ -1,6 +0,0 @@-{-# LANGUAGE ViewPatterns #-}--splitLookup :: [(Int, String)] -> String-splitLookup (lookup 5 -> Nothing) = _-splitLookup (lookup 5 -> (Just l_c)) = _-

@@ -0,0 +1,14 @@+data A = A | B | C++some :: A -> IO ()+some a = do+    foo+    bar a+  where+      foo = putStrLn "Hi"++      bar :: A -> IO ()+      bar A = _+      bar B = _+      bar C = _+

@@ -1,14 +0,0 @@-data A = A | B | C--some :: A -> IO ()-some a = do-    foo-    bar a-  where-      foo = putStrLn "Hi"--      bar :: A -> IO ()-      bar A = _-      bar B = _-      bar C = _-

@@ -0,0 +1,8 @@+{-# LANGUAGE DataKinds, GADTs #-}++data Z ab where+  Z :: (a -> b) -> Z '(a, b)++test :: Z ab+test = _+

@@ -0,0 +1,1 @@+foo = [wingman||]

@@ -0,0 +1,1 @@+foo = _

@@ -0,0 +1,2 @@+foo :: a -> (a, a)+foo a = (a, a)

@@ -0,0 +1,2 @@+foo :: a -> (a, a)+foo a = [wingman| split; assumption |]

@@ -0,0 +1,2 @@+foo :: a -> (a, a)+foo a = (a, _)

@@ -0,0 +1,2 @@+foo :: a -> (a, a)+foo a = [wingman| split, assumption |]

@@ -0,0 +1,14 @@+{-# LANGUAGE TypeOperators #-}++import GHC.Generics++class Yo f where+    yo :: f x -> Int++instance (Yo f, Yo g) => Yo (f :*: g) where+  yo (fx :*: gx)+    = let+        fx_c = yo fx+        gx_c = yo gx+      in _ fx_c gx_c+

@@ -0,0 +1,10 @@+{-# LANGUAGE TypeOperators #-}++import GHC.Generics++class Yo f where+    yo :: f x -> Int++instance (Yo f, Yo g) => Yo (f :*: g) where+  yo = [wingman| intros x, cata x, collapse |]+

@@ -0,0 +1,8 @@+import GHC.Generics++class Yo f where+    yo :: f x -> Int++instance (Yo f) => Yo (M1 _1 _2 f) where+  yo (M1 fx) = yo fx+

@@ -0,0 +1,8 @@+import GHC.Generics++class Yo f where+    yo :: f x -> Int++instance (Yo f) => Yo (M1 _1 _2 f) where+  yo = [wingman| intros x, cata x, collapse |]+

@@ -0,0 +1,2 @@+reassoc :: (a, (b, c)) -> ((a, b), c)+reassoc (a, (b, c)) = ((a, b), c)

@@ -0,0 +1,2 @@+reassoc :: (a, (b, c)) -> ((a, b), c)+reassoc (a, (b, c)) = [wingman| split; split | assume c; assume a | assume b |]

@@ -0,0 +1,5 @@+maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b+maybeAp Nothing Nothing = Nothing+maybeAp Nothing (Just _) = Nothing+maybeAp (Just _) Nothing = Nothing+maybeAp (Just fab) (Just a) = Just (fab a)

@@ -0,0 +1,11 @@+maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b+maybeAp = [wingman|+  intros,+  destruct_all,+  obvious,+  obvious,+  obvious,+  ctor Just,+  application,+  assumption+  |]

@@ -0,0 +1,2 @@+foo :: a -> (b, a)+foo a = (_, a)

@@ -0,0 +1,2 @@+foo :: a -> (b, a)+foo a = [wingman| split; try assumption |]

@@ -0,0 +1,6 @@+import Data.Char+++result :: Char -> Bool+result = isAlpha+

@@ -0,0 +1,6 @@+import Data.Char+++result :: Char -> Bool+result = [wingman| intro c, use isAlpha, assume c |]+

@@ -0,0 +1,7 @@+test :: Int+test = 0+++resolve :: Int+resolve = test+

@@ -0,0 +1,7 @@+test :: Int+test = 0+++resolve :: Int+resolve = [wingman| use test |]+

@@ -0,0 +1,12 @@+{-# LANGUAGE MultiParamTypeClasses #-}++class Test where+  test :: Int++instance Test where+  test = 10+++resolve :: Int+resolve = test+

@@ -0,0 +1,12 @@+{-# LANGUAGE MultiParamTypeClasses #-}++class Test where+  test :: Int++instance Test where+  test = 10+++resolve :: Int+resolve = [wingman| use test |]+