hls-tactics-plugin 1.2.0.0 → 1.3.0.0

raw patch · 110 files changed

+1343/−688 lines, 110 filesdep ~ghc-source-gendep ~ghcidedep ~hls-plugin-apinew-uploaderPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc-source-gen, ghcide, hls-plugin-api, hls-test-utils, refinery

API changes (from Hackage documentation)

Files

• README.md +38/−0
• hls-tactics-plugin.cabal +10/−9
• src/Wingman/Auto.hs +1/−2
• src/Wingman/CaseSplit.hs +30/−10
• src/Wingman/CodeGen.hs +9/−9
• src/Wingman/Context.hs +6/−22
• src/Wingman/EmptyCase.hs +29/−10
• src/Wingman/GHC.hs +57/−44
• src/Wingman/Judgements.hs +15/−0
• src/Wingman/Judgements/Theta.hs +10/−4
• src/Wingman/KnownStrategies.hs +6/−10
• src/Wingman/KnownStrategies/QuickCheck.hs +2/−3
• src/Wingman/LanguageServer.hs +14/−31
• src/Wingman/LanguageServer/Metaprogram.hs +3/−4
• src/Wingman/LanguageServer/TacticProviders.hs +34/−20
• src/Wingman/Machinery.hs +123/−93
• src/Wingman/Metaprogramming/Lexer.hs +36/−20
• src/Wingman/Metaprogramming/Parser.hs +90/−47
• src/Wingman/Metaprogramming/Parser.hs-boot +7/−0
• src/Wingman/Metaprogramming/Parser/Documentation.hs +20/−12
• src/Wingman/Metaprogramming/ProofState.hs +14/−12
• src/Wingman/Plugin.hs +41/−20
• src/Wingman/StaticPlugin.hs +9/−1
• src/Wingman/Tactics.hs +140/−48
• src/Wingman/Types.hs +98/−59
• test/AutoTupleSpec.hs +20/−18
• test/CodeAction/AutoSpec.hs +5/−2
• test/CodeAction/DestructSpec.hs +82/−0
• test/CodeAction/RunMetaprogramSpec.hs +7/−0
• test/CodeLens/EmptyCaseSpec.hs +5/−0
• test/ProviderSpec.hs +1/−47
• test/UnificationSpec.hs +1/−1
• test/Utils.hs +37/−6
• test/golden/AutoForallClassMethod.expected.hs +12/−0
• test/golden/AutoForallClassMethod.hs +12/−0
• test/golden/AutoTypeLevel.expected.hs +21/−0
• test/golden/AutoTypeLevel.hs +20/−0
• test/golden/DestructAllAnd.expected.hs +4/−4
• test/golden/DestructAllFunc.expected.hs +2/−2
• test/golden/DestructAllGADTEvidence.expected.hs +2/−2
• test/golden/DestructAllMany.expected.hs +24/−24
• test/golden/DestructAllNonVarTopMatch.expected.hs +4/−4
• test/golden/DestructCthulhu.expected.hs +24/−24
• test/golden/DestructDataFam.expected.hs +1/−1
• test/golden/DestructPun.expected.hs +2/−2
• test/golden/DestructTyFam.expected.hs +2/−2
• test/golden/DestructTyToDataFam.expected.hs +1/−1
• test/golden/EmptyCaseLamCase.expected.hs +6/−0
• test/golden/EmptyCaseLamCase.hs +4/−0
• test/golden/EmptyCaseSpuriousGADT.hs +8/−0
• test/golden/GoldenGADTDestruct.expected.hs +1/−1
• test/golden/GoldenGADTDestructCoercion.expected.hs +1/−1
• test/golden/GoldenIntros.expected.hs +1/−1
• test/golden/IntrosTooMany.expected.hs +2/−0
• test/golden/IntrosTooMany.hs +2/−0
• test/golden/KnownBigSemigroup.expected.hs +1/−1
• test/golden/KnownCounterfactualSemigroup.expected.hs +1/−1
• test/golden/KnownDestructedSemigroup.expected.hs +1/−1
• test/golden/KnownMissingMonoid.expected.hs +1/−1
• test/golden/KnownMissingSemigroup.expected.hs +1/−1
• test/golden/KnownModuleInstanceSemigroup.expected.hs +1/−1
• test/golden/KnownThetaSemigroup.expected.hs +1/−1
• test/golden/LayoutBind.expected.hs +2/−2
• test/golden/LayoutDollarApp.expected.hs +2/−2
• test/golden/LayoutInfixKeep.expected.hs +5/−0
• test/golden/LayoutInfixKeep.hs +4/−0
• test/golden/LayoutLam.expected.hs +2/−2
• test/golden/LayoutOpApp.expected.hs +2/−2
• test/golden/LayoutPrefixKeep.expected.hs +4/−0
• test/golden/LayoutPrefixKeep.hs +3/−0
• test/golden/LayoutRec.expected.hs +1/−1
• test/golden/LayoutSplitClass.expected.hs +2/−2
• test/golden/LayoutSplitGuard.expected.hs +2/−2
• test/golden/LayoutSplitIn.expected.hs +1/−1
• test/golden/LayoutSplitLet.expected.hs +2/−2
• test/golden/LayoutSplitPatSyn.expected.hs +2/−2
• test/golden/LayoutSplitPattern.expected.hs +2/−2
• test/golden/LayoutSplitViewPat.expected.hs +2/−2
• test/golden/LayoutSplitWhere.expected.hs +3/−3
• test/golden/MessageNotEnoughGas.hs +13/−0
• test/golden/MetaBeginNoWildify.expected.hs +2/−0
• test/golden/MetaBeginNoWildify.hs +2/−0
• test/golden/MetaBindOne.expected.hs +1/−1
• test/golden/MetaCataAST.expected.hs +23/−0
• test/golden/MetaCataAST.hs +11/−0
• test/golden/MetaCataCollapse.expected.hs +1/−1
• test/golden/MetaDeepOf.expected.hs +8/−0
• test/golden/MetaDeepOf.hs +8/−0
• test/golden/MetaPointwise.expected.hs +8/−0
• test/golden/MetaPointwise.hs +7/−0
• test/golden/MetaTry.expected.hs +1/−1
• test/golden/MetaTry.hs +1/−1
• test/golden/MetaUseSymbol.expected.hs +4/−0
• test/golden/MetaUseSymbol.hs +4/−0
• test/golden/MetaWithArg.expected.hs +2/−0
• test/golden/MetaWithArg.hs +2/−0
• test/golden/ProviderHomomorphism.hs +22/−0
• test/golden/PunGADT.expected.hs +1/−1
• test/golden/PunMany.expected.hs +2/−2
• test/golden/PunManyGADT.expected.hs +2/−2
• test/golden/PunShadowing.expected.hs +1/−1
• test/golden/PunSimple.expected.hs +1/−1
• test/golden/RefineCon.expected.hs +1/−1
• test/golden/RefineGADT.expected.hs +1/−1
• test/golden/RefineIntro.expected.hs +1/−1
• test/golden/RefineReader.expected.hs +1/−1
• test/golden/SplitPattern.expected.hs +5/−5
• test/golden/UseConLeft.expected.hs +1/−1
• test/golden/UseConPair.expected.hs +1/−1
• test/golden/UseConRight.expected.hs +1/−1

@@ -34,6 +34,17 @@ [hls]: https://github.com/haskell/haskell-language-server/releases  +## Usage++When enabled, Wingman for Haskell will remove HLS support for hole-fit code+actions. These code actions are provided by GHC and make typechecking extremely+slow in the presence of typed holes. Because Wingman relies so heavily on typed+holes, these features are in great tension.++The solution: we just remove the hole-fit actions. If you'd prefer to use these+actions, you can get them back by compiling HLS without the Wingman plugin.++ ## Editor Configuration  ### Enabling Jump to Hole@@ -97,6 +108,33 @@   call CocAction('codeAction', a:type, ['refactor.wingman.useConstructor'])   call <SID>GotoNextHole() endfunction+```++### Emacs++When using Emacs, wingman actions should be available out-of-the-box and+show up e.g. when using `M-x helm-lsp-code-actions RET` provided by +[helm-lsp](https://github.com/emacs-lsp/helm-lsp) or as popups via+[lsp-ui-sideline](https://emacs-lsp.github.io/lsp-ui/#lsp-ui-sideline).++Additionally, if you want to bind wingman actions directly to specific+keybindings or use them from Emacs Lisp, you can do so like this:++``` emacs-lisp+;; will define elisp functions for the given lsp code actions, prefixing the+;; given function names with "lsp"+(lsp-make-interactive-code-action wingman-fill-hole "refactor.wingman.fillHole")+(lsp-make-interactive-code-action wingman-case-split "refactor.wingman.caseSplit")+(lsp-make-interactive-code-action wingman-refine "refactor.wingman.refine")+(lsp-make-interactive-code-action wingman-split-func-args "refactor.wingman.spltFuncArgs")+(lsp-make-interactive-code-action wingman-use-constructor "refactor.wingman.useConstructor")++;; example key bindings+(define-key haskell-mode-map (kbd "C-c d") #'lsp-wingman-case-split)+(define-key haskell-mode-map (kbd "C-c n") #'lsp-wingman-fill-hole)+(define-key haskell-mode-map (kbd "C-c r") #'lsp-wingman-refine)+(define-key haskell-mode-map (kbd "C-c c") #'lsp-wingman-use-constructor)+(define-key haskell-mode-map (kbd "C-c a") #'lsp-wingman-split-func-args) ```  ### Other Editors

@@ -1,9 +1,10 @@ cabal-version:      2.4 category:           Development name:               hls-tactics-plugin-version:            1.2.0.0+version:            1.3.0.0 synopsis:           Wingman plugin for Haskell Language Server-description:        Please see README.md+description:+  Please see the README on GitHub at <https://github.com/haskell/haskell-language-server#readme> author:             Sandy Maguire, Reed Mullanix maintainer:         sandy@sandymaguire.me copyright:          Sandy Maguire, Reed Mullanix@@ -69,25 +70,25 @@     , containers     , deepseq     , directory-    , extra+    , extra                 >=1.7.8     , filepath     , fingertree     , generic-lens     , ghc     , ghc-boot-th     , ghc-exactprint-    , ghc-source-gen-    , ghcide                ^>=1.4+    , ghc-source-gen        ^>=0.4.1+    , ghcide                ^>=1.4.1     , hls-graph-    , hls-plugin-api        ^>=1.1+    , hls-plugin-api        >=1.1     && <1.3     , hyphenation     , lens     , lsp-    , megaparsec            ^>=9+    , megaparsec            >=8       && <10     , mtl     , parser-combinators     , prettyprinter-    , refinery              ^>=0.3+    , refinery              ^>=0.4     , retrie                >=0.1.1.0     , syb     , text@@ -153,7 +154,7 @@     , ghcide     , hls-plugin-api     , hls-tactics-plugin-    , hls-test-utils      ^>=1.0+    , hls-test-utils      >=1.0 && <1.2     , hspec     , hspec-expectations     , lens

@@ -5,10 +5,9 @@ import           Control.Monad.State (gets) import qualified Data.Set as S import           Refinery.Tactic-import           Wingman.Context import           Wingman.Judgements import           Wingman.KnownStrategies-import           Wingman.Machinery (tracing)+import           Wingman.Machinery (tracing, getCurrentDefinitions) import           Wingman.Tactics import           Wingman.Types 

@@ -11,7 +11,7 @@ import qualified Data.Set as S import           Development.IDE.GHC.Compat import           GHC.Exts (IsString (fromString))-import           GHC.SourceGen (funBinds, match, wildP)+import           GHC.SourceGen (funBindsWithFixity, match, wildP) import           OccName import           Wingman.GHC import           Wingman.Types@@ -30,10 +30,14 @@ -- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by -- splitting it into multiple matches: one for each alternative of the case. agdaSplit :: AgdaMatch -> [AgdaMatch]-agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do-  (pat, body) <- matches-  -- TODO(sandy): use an at pattern if necessary-  pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches))+  -- Ensure the thing we're destructing is actually a pattern that's been+  -- bound.+  | containsVar var pats+  = do+    (pat, body) <- matches+    -- TODO(sandy): use an at pattern if necessary+    pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body agdaSplit x = [x]  @@ -54,6 +58,19 @@   ------------------------------------------------------------------------------+-- | Determine whether the given 'RdrName' exists as a 'VarPat' inside of @a@.+containsVar :: Data a => RdrName -> a -> Bool+containsVar name = everything (||) $+  mkQ False (\case+    VarPat _ (L _ var) -> eqRdrName name var+    (_ :: Pat GhcPs)   -> False+      )+  `extQ` \case+    HsRecField lbl _ True ->  eqRdrName name $ unLoc $ rdrNameFieldOcc $ unLoc lbl+    (_ :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> False+++------------------------------------------------------------------------------ -- | Replace a 'VarPat' with the given @'Pat' GhcPs@. rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a rewriteVarPat name rep = everywhere $@@ -68,16 +85,19 @@     (x :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> x  - ------------------------------------------------------------------------------ -- | Construct an 'HsDecl' from a set of 'AgdaMatch'es. splitToDecl-    :: OccName  -- ^ The name of the function+    :: Maybe LexicalFixity+    -> OccName  -- ^ The name of the function     -> [AgdaMatch]     -> LHsDecl GhcPs-splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do-  AgdaMatch pats body <- ams-  pure $ match pats body+splitToDecl fixity name ams = do+  traceX "fixity" fixity $+    noLoc $+      funBindsWithFixity fixity (fromString . occNameString . occName $ name) $ do+        AgdaMatch pats body <- ams+        pure $ match pats body   ------------------------------------------------------------------------------

@@ -33,6 +33,7 @@ import           OccName (occName) import           PatSyn import           Type hiding (Var)+import           TysPrim (alphaTy) import           Wingman.CodeGen.Utils import           Wingman.GHC import           Wingman.Judgements@@ -58,7 +59,7 @@   let hy = jEntireHypothesis jdg       g  = jGoal jdg   case tacticsGetDataCons $ unCType t of-    Nothing -> throwError $ GoalMismatch "destruct" g+    Nothing -> cut -- throwError $ GoalMismatch "destruct" g     Just (dcs, apps) ->       fmap unzipTrace $ for dcs $ \dc -> do         let con = RealDataCon dc@@ -67,8 +68,6 @@             -- #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@@ -79,7 +78,7 @@         let hy' = patternHypothesis scrut con jdg                 $ zip names'                 $ coerce args-            j = fmap (CType . substTyAddInScope subst . unCType)+            j = withNewCoercions (evidenceToCoercions ev)               $ introduce ctx hy'               $ introduce ctx method_hy               $ withNewGoal g jdg@@ -215,7 +214,7 @@  destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule destruct' use_field_puns f hi jdg = do-  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic+  when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic   let term = hi_name hi   ext       <- destructMatches@@ -235,13 +234,13 @@ -- resulting matches. destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule destructLambdaCase' use_field_puns f jdg = do-  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic+  when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic   let g  = jGoal jdg   case splitFunTy_maybe (unCType g) of     Just (arg, _) | isAlgType arg ->       fmap (fmap noLoc lambdaCase) <$>         destructMatches use_field_puns f Nothing (CType arg) jdg-    _ -> throwError $ GoalMismatch "destructLambdaCase'" g+    _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g   ------------------------------------------------------------------------------@@ -268,7 +267,7 @@       --       -- Fortunately, this isn't an issue in practice, since 'PatSyn's are       -- never in the hypothesis.-      throwError $ TacticPanic "Can't build Pattern constructors yet"+      cut -- throwError $ TacticPanic "Can't build Pattern constructors yet"   ext       <- fmap unzipTrace        $ traverse ( \(arg, n) ->@@ -309,7 +308,8 @@       let g = jGoal jdg       terms <- fmap sequenceA $ for hy $ \hi -> do         let name = rename $ hi_name hi-        res <- tacticToRule jdg $ solve hi+        let generalized_let_ty = CType alphaTy+        res <- tacticToRule (withNewGoal generalized_let_ty 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

@@ -8,7 +8,7 @@ import           Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import           Development.IDE.GHC.Compat-import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env)+import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env, extractModule) import           InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import           OccName import           TcRnTypes@@ -23,11 +23,11 @@     :: Config     -> [(OccName, CType)]     -> TcGblEnv+    -> HscEnv     -> ExternalPackageState-    -> KnownThings     -> [Evidence]     -> Context-mkContext cfg locals tcg eps kt ev = fix $ \ctx ->+mkContext cfg locals tcg hscenv eps ev = fix $ \ctx ->   Context     { ctxDefiningFuncs         = fmap (second $ coerce $ normalizeType ctx) locals@@ -46,8 +46,10 @@           (eps_inst_env eps)           (tcg_inst_env tcg)           (tcVisibleOrphanMods tcg)-    , ctxKnownThings = kt     , ctxTheta = evidenceToThetaType ev+    , ctx_hscEnv = hscenv+    , ctx_occEnv = tcg_rdr_env tcg+    , ctx_module = extractModule tcg     }  @@ -69,24 +71,6 @@       ABE _ poly _ _ _ -> pure poly       _                -> [] getFunBindId _ = []---getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]-getCurrentDefinitions = asks ctxDefiningFuncs------------------------------------------------------------------------------------ | Extract something from 'KnownThings'.-getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a-getKnownThing f = asks $ f . ctxKnownThings------------------------------------------------------------------------------------ | Like 'getInstance', but uses a class from the 'KnownThings'.-getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))-getKnownInstance f tys = do-  cls <- getKnownThing f-  getInstance cls tys   ------------------------------------------------------------------------------

@@ -59,7 +59,6 @@   | 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@@ -94,6 +93,13 @@ codeLensProvider _ _ _ = pure $ Right $ List []  +scrutinzedType :: EmptyCaseSort Type -> Maybe Type+scrutinzedType (EmptyCase ty) = pure  ty+scrutinzedType (EmptyLamCase ty) =+  case tacticsSplitFunTy ty of+    (_, _, tys, _) -> listToMaybe  tys++ ------------------------------------------------------------------------------ -- | The description for the empty case lens. mkEmptyCaseLensDesc :: Type -> T.Text@@ -120,6 +126,8 @@   hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case     L span (HsCase ext scrut mg@_) -> do       pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }+    L span (HsLamCase ext mg@_) -> do+      pure $ Just $ L span $ HsLamCase ext $ mg { mg_alts = l }     (_ :: LHsExpr GhcPs) -> pure Nothing  @@ -142,19 +150,30 @@     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+    fmap catMaybes $ for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do+      ty <- MaybeT+          . fmap (scrutinzedType <=< sequence)+          . traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg')+          $ scrutinee+      case null $ tacticsGetDataCons ty of+        True -> pure empty+        False ->+          case ss of+            RealSrcSpan r   -> do+              rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r+              pure $ Just (rss', ty)+            UnhelpfulSpan _ -> empty +data EmptyCaseSort a+  = EmptyCase a+  | EmptyLamCase a+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)  ------------------------------------------------------------------------------ -- | Get the 'SrcSpan' and scrutinee of every empty case.-emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)]+emptyCaseQ :: GenericQ [(SrcSpan, EmptyCaseSort (HsExpr GhcTc))] emptyCaseQ = everything (<>) $ mkQ mempty $ \case-  L new_span (Case scrutinee []) -> pure (new_span, scrutinee)+  L new_span (Case scrutinee []) -> pure (new_span, EmptyCase scrutinee)+  L new_span (expr@(LamCase [])) -> pure (new_span, EmptyLamCase expr)   (_ :: LHsExpr GhcTc) -> mempty 

@@ -4,11 +4,12 @@ module Wingman.GHC where  import           Bag (bagToList)+import           Class (classTyVars) import           ConLike-import           Control.Applicative (empty) import           Control.Monad.State import           Control.Monad.Trans.Maybe (MaybeT(..)) import           CoreUtils (exprType)+import           Data.Bool (bool) import           Data.Function (on) import           Data.Functor ((<&>)) import           Data.List (isPrefixOf)@@ -18,8 +19,6 @@ import qualified Data.Set as S import           Data.Traversable import           DataCon-import           Development.IDE (HscEnvEq (hscEnv))-import           Development.IDE.Core.Compile (lookupName) import           Development.IDE.GHC.Compat hiding (exprType) import           DsExpr (dsExpr) import           DsMonad (initDs)@@ -27,15 +26,17 @@ import           FamInstEnv (normaliseType) import           GHC.SourceGen (lambda) import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)-import           GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal))+import           GhcPlugins (Role (Nominal)) import           OccName import           TcRnMonad import           TcType import           TyCoRep import           Type import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)+import           Unify import           Unique import           Var+import           Wingman.StaticPlugin (pattern MetaprogramSyntax) import           Wingman.Types  @@ -90,11 +91,15 @@ ------------------------------------------------------------------------------ -- | Get the data cons of a type, if it has any. tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])-tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =-  splitTyConApp_maybe ty <&> \(tc, apps) ->-    ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc-    , apps-    )+tacticsGetDataCons ty+  | Just (_, ty') <- tcSplitForAllTy_maybe ty+  = tacticsGetDataCons ty'+tacticsGetDataCons ty+  | Just _ <- algebraicTyCon ty+  = splitTyConApp_maybe ty <&> \(tc, apps) ->+      ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc+      , apps+      ) tacticsGetDataCons _ = Nothing  ------------------------------------------------------------------------------@@ -113,7 +118,7 @@         case M.lookup tv reps of           Just tv' -> tv'           Nothing  -> tv-      ) t+      ) $ snd $ tcSplitForAllTys t   ------------------------------------------------------------------------------@@ -131,6 +136,9 @@ ------------------------------------------------------------------------------ -- | Is this an algebraic type? algebraicTyCon :: Type -> Maybe TyCon+algebraicTyCon ty+  | Just (_, ty') <- tcSplitForAllTy_maybe ty+  = algebraicTyCon ty' algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))   | tycon == intTyCon    = Nothing   | tycon == floatTyCon  = Nothing@@ -171,6 +179,7 @@ containsHole x = not $ null $ listify (   \case     ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name+    MetaprogramSyntax _                    -> True     _                                      -> False   ) x @@ -252,7 +261,14 @@   HsCase _ (L _ scrutinee)     (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)}) +------------------------------------------------------------------------------+-- | Like 'Case', but for lambda cases.+pattern LamCase :: PatCompattable p => [(Pat p, LHsExpr p)] -> HsExpr p+pattern LamCase matches <-+  HsLamCase _+    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)}) + ------------------------------------------------------------------------------ -- | Can ths type be lambda-cased? --@@ -323,40 +339,6 @@ unXPat pat              = pat  ---------------------------------------------------------------------------------- | Build a 'KnownThings'.-knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings-knownThings tcg hscenv= do-  let cls = knownClass tcg hscenv-  KnownThings-    <$> cls (mkClsOcc "Semigroup")-    <*> cls (mkClsOcc "Monoid")------------------------------------------------------------------------------------ | Like 'knownThing' but specialized to classes.-knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class-knownClass = knownThing $ \case-  ATyCon tc -> tyConClass_maybe tc-  _         -> Nothing------------------------------------------------------------------------------------ | Helper function for defining 'knownThings'.-knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a-knownThing f tcg hscenv occ = do-  let modul = extractModule tcg-      rdrenv = tcg_rdr_env tcg--  case lookupOccEnv rdrenv occ of-    Nothing -> empty-    Just elts -> do-      mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts-      case mvar of-        Just tt -> liftMaybe $ f tt-        _ -> empty-- liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a @@ -395,4 +377,35 @@ expandTyFam :: Context -> Type -> Type expandTyFam ctx = snd . normaliseType  (ctxFamInstEnvs ctx) Nominal ++------------------------------------------------------------------------------+-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.+tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst+tryUnifyUnivarsButNotSkolems skolems goal inst =+  case tcUnifyTysFG+         (bool BindMe Skolem . flip S.member skolems)+         [unCType inst]+         [unCType goal] of+    Unifiable subst -> pure subst+    _               -> Nothing+++updateSubst :: TCvSubst -> TacticState -> TacticState+updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) }+++------------------------------------------------------------------------------+-- | Get the class methods of a 'PredType', correctly dealing with+-- instantiation of quantified class types.+methodHypothesis :: PredType -> Maybe [HyInfo CType]+methodHypothesis ty = do+  (tc, apps) <- splitTyConApp_maybe ty+  cls <- tyConClass_maybe tc+  let methods = classMethods cls+      tvs     = classTyVars cls+      subst   = zipTvSubst tvs apps+  pure $ methods <&> \method ->+    let (_, _, ty) = tcSplitSigmaTy $ idType method+    in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty+       ) 

@@ -18,6 +18,7 @@ import           SrcLoc import           Type import           Wingman.GHC (algebraicTyCon, normalizeType)+import           Wingman.Judgements.Theta import           Wingman.Types  @@ -69,6 +70,15 @@ withNewGoal t = field @"_jGoal" .~ t  +------------------------------------------------------------------------------+-- | Add some new type equalities to the local judgement.+withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement+withNewCoercions ev j =+  let subst = allEvidenceToSubst mempty $ coerce ev+   in fmap (CType . substTyAddInScope subst . unCType) j+      & field @"j_coercion" %~ unionTCvSubst subst++ normalizeHypothesis :: Functor f => Context -> f CType -> f CType normalizeHypothesis = fmap . coerce . normalizeType @@ -365,6 +375,10 @@   . jLocalHypothesis  +jNeedsToBindArgs :: Judgement' CType -> Bool+jNeedsToBindArgs = isFunTy . unCType . jGoal++ ------------------------------------------------------------------------------ -- | Fold a hypothesis into a single mapping from name to info. This -- unavoidably will cause duplicate names (things like methods) to shadow one@@ -414,6 +428,7 @@       , _jWhitelistSplit    = True       , _jIsTopHole         = top       , _jGoal              = CType goal+      , j_coercion          = emptyTCvSubst       }  

@@ -5,14 +5,17 @@   ( Evidence   , getEvidenceAtHole   , mkEvidence+  , evidenceToCoercions   , evidenceToSubst   , evidenceToHypothesis   , evidenceToThetaType+  , allEvidenceToSubst   ) where  import           Class (classTyVars) import           Control.Applicative (empty) import           Control.Lens (preview)+import           Data.Coerce (coerce) import           Data.Maybe (fromMaybe, mapMaybe, maybeToList) import           Data.Generics.Sum (_Ctor) import           Data.Set (Set)@@ -32,7 +35,7 @@ import           TcType (substTy) import           TcType (tcTyConAppTyCon_maybe) import           TysPrim (eqPrimTyCon)-import           Wingman.Machinery+import           Wingman.GHC import           Wingman.Types  @@ -110,13 +113,16 @@     $ fmap (substPair subst) evs  ------------------------------------------------------------------------------+-- | Given some 'Evidence', get a list of which types are now equal.+evidenceToCoercions :: [Evidence] -> [(CType, CType)]+evidenceToCoercions = coerce . mapMaybe (preview $ _Ctor @"EqualityOfTypes")++------------------------------------------------------------------------------ -- | 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)+    (allEvidenceToSubst (ts_skolems ts) . coerce $ evidenceToCoercions evs)     ts  

@@ -1,15 +1,11 @@ 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 OccName (mkVarOcc, mkClsOcc) import Refinery.Tactic-import Wingman.Context (getCurrentDefinitions, getKnownInstance) import Wingman.Judgements (jGoal) import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)-import Wingman.Machinery (tracing)+import Wingman.Machinery (tracing, getKnownInstance, getCurrentDefinitions) import Wingman.Tactics import Wingman.Types @@ -29,7 +25,7 @@   getCurrentDefinitions >>= \case     [(def, _)] | def == mkVarOcc name ->       tracing ("known " <> name) t-    _ -> throwError NoApplicableTactic+    _ -> failure NoApplicableTactic   deriveFmap :: TacticsM ()@@ -37,7 +33,7 @@   try intros   overAlgebraicTerms homo   choice-    [ overFunctions apply >> auto' 2+    [ overFunctions (apply Saturated) >> auto' 2     , assumption     , recursion     ]@@ -57,7 +53,7 @@   destructAll   split   g <- goal-  minst <- getKnownInstance kt_semigroup+  minst <- getKnownInstance (mkClsOcc "Semigroup")          . pure          . unCType          $ jGoal g@@ -79,7 +75,7 @@ deriveMempty = do   split   g <- goal-  minst <- getKnownInstance kt_monoid [unCType $ jGoal g]+  minst <- getKnownInstance (mkClsOcc "Monoid") [unCType $ jGoal g]   for_ minst $ \(cls, df) -> do     applyMethod cls df $ mkVarOcc "mempty"   try assumption

@@ -1,7 +1,6 @@ module Wingman.KnownStrategies.QuickCheck where  import ConLike (ConLike(RealDataCon))-import Control.Monad.Except (MonadError (throwError)) import Data.Bool (bool) import Data.Generics (everything, mkQ) import Data.List (partition)@@ -15,7 +14,7 @@ import GHC.SourceGen.Overloaded (App ((@@)), HasList (list)) import GHC.SourceGen.Pat (conP) import OccName (HasOccName (occName), mkVarOcc, occNameString)-import Refinery.Tactic (goal, rule)+import Refinery.Tactic (goal, rule, failure) import TyCon (TyCon, tyConDataCons, tyConName) import Type (splitTyConApp_maybe) import Wingman.CodeGen@@ -61,7 +60,7 @@                             (list $ fmap genExpr big)                             terminal_expr                     ]-    _ -> throwError $ GoalMismatch "deriveArbitrary" ty+    _ -> failure $ GoalMismatch "deriveArbitrary" ty   ------------------------------------------------------------------------------

@@ -44,7 +44,6 @@ import qualified FastString import           GHC.Generics (Generic) 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@@ -53,19 +52,21 @@ 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              hiding+                                                 (SemanticTokenAbsolute (length, line),+                                                  SemanticTokenRelative (length),+                                                  SemanticTokensEdit (_start)) import           Language.LSP.Types.Capabilities import           OccName import           Prelude hiding (span) import           Retrie (transformA) import           SrcLoc (containsSpan)-import           TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env))+import           TcRnTypes (tcg_binds, TcGblEnv) import           Wingman.Context import           Wingman.GHC import           Wingman.Judgements 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@@ -138,8 +139,11 @@    , 'PropertyKey "max_use_ctor_actions" 'TInteger    , 'PropertyKey "timeout_duration" 'TInteger    , 'PropertyKey "auto_gas" 'TInteger+   , 'PropertyKey "proofstate_styling" 'TBoolean    ] properties = emptyProperties+  & defineBooleanProperty #proofstate_styling+    "Should Wingman emit styling markup when showing metaprogram proof states?" True   & 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@@ -164,6 +168,7 @@     <$> usePropertyLsp #max_use_ctor_actions pId properties     <*> usePropertyLsp #timeout_duration pId properties     <*> usePropertyLsp #auto_gas pId properties+    <*> usePropertyLsp #proofstate_styling pId properties   getIdeDynflags@@ -215,9 +220,8 @@       -- involved, so it's not crucial to track ages.       let henv = untrackedStaleValue $ hscenv       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv-      kt <- knownThings (untrackedStaleValue tcg) henv -      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt+      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps       let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t        dflags <- getIdeDynflags state nfp@@ -240,10 +244,10 @@     -> TrackedStale Bindings     -> Tracked 'Current RealSrcSpan     -> TrackedStale TcGblEnv+    -> HscEnv     -> ExternalPackageState-    -> KnownThings     -> Maybe (Judgement, Context)-mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do+mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps = do   binds_rss <- mapAgeFrom bmap rss   tcg_rss <- mapAgeFrom tcgmap rss @@ -253,8 +257,8 @@                 $ unTrack                 $ getDefiningBindings <$> binds <*> binds_rss)               (unTrack tcg)+              hscenv               eps-              kt               evidence       top_provs = getRhsPosVals tcg_rss tcs       already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs@@ -484,6 +488,7 @@   ufmSeverity :: UserFacingMessage -> MessageType+ufmSeverity NotEnoughGas            = MtInfo ufmSeverity TacticErrors            = MtError ufmSeverity TimedOut                = MtInfo ufmSeverity NothingToDo             = MtInfo@@ -597,26 +602,4 @@   . 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 

@@ -10,7 +10,6 @@  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)@@ -23,7 +22,7 @@ import           Development.IDE.Core.Shake (IdeState (..)) import           Development.IDE.Core.UseStale import           Development.IDE.GHC.Compat-import           GhcPlugins (containsSpan, realSrcLocSpan)+import           GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart) import           Ide.Types import           Language.LSP.Types import           Prelude hiding (span)@@ -51,9 +50,9 @@           case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of             Just (trss, program) -> do               let tr_range = fmap realSrcSpanToRange trss+                  rsl = realSrcSpanStart $ unTrack 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+              z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program               pure $ Hover                 { _contents = HoverContents                             $ MarkupContent MkMarkdown

@@ -12,12 +12,12 @@   ) where  import           Control.Monad-import           Control.Monad.Reader (runReaderT) import           Data.Aeson import           Data.Bool (bool) import           Data.Coerce import           Data.Maybe import           Data.Monoid+import qualified Data.Set as S import qualified Data.Text as T import           Data.Traversable import           DataCon (dataConName)@@ -27,14 +27,16 @@ import           GHC.LanguageExtensions.Type (Extension (LambdaCase)) import           Ide.PluginUtils import           Ide.Types-import           Language.LSP.Types+import           Language.LSP.Types              hiding+                                                 (SemanticTokenAbsolute (length, line),+                                                  SemanticTokenRelative (length),+                                                  SemanticTokensEdit (_start)) import           OccName import           Prelude hiding (span) import           Wingman.Auto import           Wingman.GHC import           Wingman.Judgements-import           Wingman.Machinery (useNameFromHypothesis)-import           Wingman.Metaprogramming.Lexer (ParserContext)+import           Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons) import           Wingman.Metaprogramming.Parser (parseMetaprogram) import           Wingman.Tactics import           Wingman.Types@@ -42,19 +44,19 @@  ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery.-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+commandTactic :: TacticCommand -> T.Text -> TacticsM ()+commandTactic Auto                   = const auto+commandTactic Intros                 = const intros+commandTactic Destruct               = useNameFromHypothesis destruct . mkVarOcc . T.unpack+commandTactic DestructPun            = useNameFromHypothesis destructPun . mkVarOcc . T.unpack+commandTactic Homomorphism           = useNameFromHypothesis homo . mkVarOcc . T.unpack+commandTactic DestructLambdaCase     = const destructLambdaCase+commandTactic HomomorphismLambdaCase = const homoLambdaCase+commandTactic DestructAll            = const destructAll+commandTactic UseDataCon             = userSplit . mkVarOcc . T.unpack+commandTactic Refine                 = const refine+commandTactic BeginMetaprogram       = const metaprogram+commandTactic RunMetaprogram         = parseMetaprogram   ------------------------------------------------------------------------------@@ -128,7 +130,7 @@ commandProvider HomomorphismLambdaCase =   requireHoleSort (== Hole) $   requireExtension LambdaCase $-    filterGoalType ((== Just True) . lambdaCaseable) $+    filterGoalType (liftLambdaCase False homoFilter) $       provide HomomorphismLambdaCase "" commandProvider DestructAll =   requireHoleSort (== Hole) $@@ -315,8 +317,20 @@ -- | We should show homos only when the goal type is the same as the binding -- type, and that both are usual algebraic types. homoFilter :: Type -> Type -> Bool-homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2-homoFilter _ _                                                     = False+homoFilter codomain domain =+  case uncoveredDataCons domain codomain of+    Just s -> S.null s+    _ -> False+++------------------------------------------------------------------------------+-- | Lift a function of (codomain, domain) over a lambda case.+liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r+liftLambdaCase nil f t =+  case tacticsSplitFunTy t of+    (_, _, arg : _, res) -> f res arg+    _ -> nil+   ------------------------------------------------------------------------------

@@ -1,17 +1,15 @@-{-# LANGUAGE RecordWildCards       #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TupleSections   #-}  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.Class (gets, modify, MonadState) import           Control.Monad.State.Strict (StateT (..), execStateT)-import           Data.Bool (bool)+import           Control.Monad.Trans.Maybe import           Data.Coerce-import           Data.Either import           Data.Foldable import           Data.Functor ((<&>)) import           Data.Generics (everything, gcount, mkQ)@@ -21,18 +19,18 @@ import           Data.Maybe (mapMaybe) import           Data.Monoid (getSum) import           Data.Ord (Down (..), comparing)-import           Data.Set (Set) import qualified Data.Set as S+import           Data.Traversable (for) import           Development.IDE.Core.Compile (lookupName) import           Development.IDE.GHC.Compat 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 (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe)-import           Unify+import           Type (tyCoVarsOfTypeWellScoped)+import           Wingman.Context (getInstance)+import           Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons) import           Wingman.Judgements import           Wingman.Simplify (simplify) import           Wingman.Types@@ -42,6 +40,17 @@ substCTy subst = coerce . substTy subst . coerce  +getSubstForJudgement+    :: MonadState TacticState m+    => Judgement+    -> m TCvSubst+getSubstForJudgement j = do+  -- NOTE(sandy): It's OK to use mempty here, because coercions _can_ give us+  -- substitutions for skolems.+  let coercions = j_coercion j+  unifier <- gets ts_unifier+  pure $ unionTCvSubst unifier coercions+ ------------------------------------------------------------------------------ -- | Produce a subgoal that must be solved before we can solve the original -- goal.@@ -50,7 +59,7 @@     -> Rule newSubgoal j = do   ctx <- ask-  unifier <- gets ts_unifier+  unifier <- getSubstForJudgement j   subgoal     $ normalizeJudgement ctx     $ substJdg unifier@@ -69,8 +78,8 @@     :: Context     -> Judgement     -> TacticsM ()       -- ^ Tactic to use-    -> Either [TacticError] RunTacticResults-runTactic ctx jdg t =+    -> IO (Either [TacticError] RunTacticResults)+runTactic ctx jdg t = do     let skolems = S.fromList                 $ foldMap (tyCoVarsOfTypeWellScoped . unCType)                 $ (:) (jGoal jdg)@@ -82,23 +91,23 @@           defaultTacticState             { ts_skolems = skolems             }-    in case partitionEithers-          . flip runReader ctx-          . unExtractM-          $ runTacticT t jdg tacticState of-      (errs, []) -> Left $ take 50 errs-      (_, fmap assoc23 -> solns) -> do+    res <- flip runReaderT ctx+         . unExtractM+         $ runTacticT t jdg tacticState+    pure $ case res of+      (Left errs) -> Left $ take 50 errs+      (Right solns) -> do         let sorted =-              flip sortBy solns $ comparing $ \(ext, (_, holes)) ->-                Down $ scoreSolution ext jdg holes+              flip sortBy solns $ comparing $ \(Proof ext _ holes) ->+                Down $ scoreSolution ext jdg $ fmap snd holes         case sorted of-          ((syn, (_, subgoals)) : _) ->+          ((Proof syn _ subgoals) : _) ->             Right $               RunTacticResults                 { rtr_trace    = syn_trace syn                 , rtr_extract  = simplify $ syn_val syn-                , rtr_subgoals = subgoals-                , rtr_other_solns = reverse . fmap fst $ sorted+                , rtr_subgoals = fmap snd subgoals+                , rtr_other_solns = reverse . fmap pf_extract $ sorted                 , rtr_jdg = jdg                 , rtr_ctx = ctx                 }@@ -143,7 +152,7 @@     -> TacticT jdg ext err s m a mappingExtract f (TacticT m)   = TacticT $ StateT $ \jdg ->-      mapExtract' f $ runStateT m jdg+      mapExtract id f $ runStateT m jdg   ------------------------------------------------------------------------------@@ -204,23 +213,8 @@   deriving (Eq, Ord, Show) via a  ---------------------------------------------------------------------------------- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.-tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst-tryUnifyUnivarsButNotSkolems skolems goal inst =-  case tcUnifyTysFG-         (bool BindMe Skolem . flip S.member skolems)-         [unCType inst]-         [unCType goal] of-    Unifiable subst -> pure subst-    _               -> Nothing  -updateSubst :: TCvSubst -> TacticState -> TacticState-updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) }--- ------------------------------------------------------------------------------ -- | Attempt to unify two types. unify :: CType -- ^ The goal type@@ -231,10 +225,27 @@   case tryUnifyUnivarsButNotSkolems skolems goal inst of     Just subst ->       modify $ updateSubst subst-    Nothing -> throwError (UnificationError inst goal)+    Nothing -> cut +cut :: RuleT jdg ext err s m a+cut = RuleT Empty + ------------------------------------------------------------------------------+-- | Attempt to unify two types.+canUnify+    :: MonadState TacticState m+    => CType -- ^ The goal type+    -> CType -- ^ The type we are trying unify the goal type with+    -> m Bool+canUnify goal inst = do+  skolems <- gets ts_skolems+  case tryUnifyUnivarsButNotSkolems skolems goal inst of+    Just _ -> pure True+    Nothing -> pure False+++------------------------------------------------------------------------------ -- | Prefer the first tactic to the second, if the bool is true. Otherwise, just run the second tactic. -- -- This is useful when you have a clever pruning solution that isn't always@@ -245,42 +256,6 @@   --------------------------------------------------------------------------------- | Get the class methods of a 'PredType', correctly dealing with--- instantiation of quantified class types.-methodHypothesis :: PredType -> Maybe [HyInfo CType]-methodHypothesis ty = do-  (tc, apps) <- splitTyConApp_maybe ty-  cls <- tyConClass_maybe tc-  let methods = classMethods cls-      tvs     = classTyVars cls-      subst   = zipTvSubst tvs apps-  pure $ methods <&> \method ->-    let (_, _, ty) = tcSplitSigmaTy $ idType method-    in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty-       )------------------------------------------------------------------------------------ | Mystical time-traveling combinator for inspecting the extracts produced by--- a tactic. We can use it to guard that extracts match certain predicates, for--- example.------ Note, that this thing is WEIRD. To illustrate:------ @@--- peek f--- blah--- @@------ Here, @f@ can inspect the extract _produced by @blah@,_  which means the--- causality appears to go backwards.------ 'peek' should be exposed directly by @refinery@ in the next release.-peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()-peek k = tactic $ \j -> Subgoal ((), j) $ \e -> proofState (k e) j--------------------------------------------------------------------------------- -- | Run the given tactic iff the current hole contains no univars. Skolems and -- already decided univars are OK though. requireConcreteHole :: TacticsM a -> TacticsM a@@ -290,7 +265,7 @@   let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg   case S.size $ vars S.\\ skolems of     0 -> m-    _ -> throwError TooPolymorphic+    _ -> failure TooPolymorphic   ------------------------------------------------------------------------------@@ -323,7 +298,7 @@   hy <- jHypothesis <$> goal   case M.lookup name $ hyByName hy of     Just hi -> f hi-    Nothing -> throwError $ NotInScope name+    Nothing -> failure $ NotInScope name  ------------------------------------------------------------------------------ -- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to@@ -332,7 +307,7 @@ useNameFromContext f name = do   lookupNameInContext name >>= \case     Just ty -> f $ createImportedHyInfo name ty-    Nothing -> throwError $ NotInScope name+    Nothing -> failure $ NotInScope name   ------------------------------------------------------------------------------@@ -345,6 +320,16 @@     Nothing      -> empty  +getDefiningType+    :: TacticsM CType+getDefiningType = do+  calling_fun_name <- fst . head <$> asks ctxDefiningFuncs+  maybe+    (failure $ NotInScope calling_fun_name)+    pure+      =<< lookupNameInContext calling_fun_name++ ------------------------------------------------------------------------------ -- | Build a 'HyInfo' for an imported term. createImportedHyInfo :: OccName -> CType -> HyInfo CType@@ -355,22 +340,67 @@   }  +getTyThing+    :: OccName+    -> TacticsM (Maybe TyThing)+getTyThing occ = do+  ctx <- ask+  case lookupOccEnv (ctx_occEnv ctx) occ of+    Just (elt : _) -> do+      mvar <- lift+            $ ExtractM+            $ lift+            $ lookupName (ctx_hscEnv ctx) (ctx_module ctx)+            $ gre_name elt+      pure mvar+    _ -> pure Nothing++ ------------------------------------------------------------------------------+-- | Like 'getTyThing' but specialized to classes.+knownClass :: OccName -> TacticsM (Maybe Class)+knownClass occ =+  getTyThing occ <&> \case+    Just (ATyCon tc) -> tyConClass_maybe tc+    _                -> Nothing+++------------------------------------------------------------------------------+-- | Like 'getInstance', but uses a class that it just looked up.+getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType))+getKnownInstance f tys = runMaybeT $ do+  cls <- MaybeT $ knownClass f+  MaybeT $ getInstance cls tys+++------------------------------------------------------------------------------ -- | 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+    :: OccName+    -> TacticsM Type+getOccNameType occ = do+  getTyThing occ >>= \case+    Just (AnId v) -> pure $ varType v+    _ -> failure $ NotInScope occ+++getCurrentDefinitions :: TacticsM [(OccName, CType)]+getCurrentDefinitions = do+  ctx_funcs <- asks ctxDefiningFuncs+  for ctx_funcs $ \res@(occ, _) ->+    pure . maybe res (occ,) =<< lookupNameInContext occ+++------------------------------------------------------------------------------+-- | Given two types, see if we can construct a homomorphism by mapping every+-- data constructor in the domain to the same in the codomain. This function+-- returns 'Just' when all the lookups succeeded, and a non-empty value if the+-- homomorphism *is not* possible.+uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon))+uncoveredDataCons domain codomain = do+  (g_dcs, _) <- tacticsGetDataCons codomain+  (hi_dcs, _) <- tacticsGetDataCons domain+  pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) 

@@ -7,29 +7,16 @@  import           Control.Applicative import           Control.Monad-import           Control.Monad.Reader (ReaderT)+import           Data.Foldable (asum) 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)+type Parser = P.Parsec Void Text   @@ -45,6 +32,31 @@ ichar :: Parser Char ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\'' +symchar :: Parser Char+symchar = asum+  [ P.symbolChar+  , P.char '!'+  , P.char '#'+  , P.char '$'+  , P.char '%'+  , P.char '^'+  , P.char '&'+  , P.char '*'+  , P.char '-'+  , P.char '='+  , P.char '+'+  , P.char ':'+  , P.char '<'+  , P.char '>'+  , P.char ','+  , P.char '.'+  , P.char '/'+  , P.char '?'+  , P.char '~'+  , P.char '|'+  , P.char '\\'+  ]+ lexeme :: Parser a -> Parser a lexeme = L.lexeme sc @@ -66,14 +78,18 @@ 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)+    c <- P.alphaNumChar <|> P.char '('+    fmap mkVarOcc $ case c of+      '(' -> do+        cs <- P.many symchar+        void $ P.char ')'+        pure cs+      _ -> do+        cs <- P.many ichar+        pure $ 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

@@ -7,17 +7,16 @@ 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           Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)+import           FastString (unpackFS)+import           Refinery.Tactic (failure) 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.Machinery (useNameFromHypothesis, useNameFromContext, getCurrentDefinitions) import           Wingman.Metaprogramming.Lexer import           Wingman.Metaprogramming.Parser.Documentation import           Wingman.Metaprogramming.ProofState (proofState, layout)@@ -176,9 +175,20 @@           "f (_ :: a)"       ] +  , command "pointwise" Deterministic Tactic+      "Restrict the hypothesis in the holes of the given tactic to align up with the top-level bindings. This will ensure, eg, that the first hole can see only terms that came from the first position in any terms destructed from the top-level bindings."+      (pure . flip restrictPositionForApplication (pure ()))+      [ Example+          (Just "In the context of `f (a1, b1) (a2, b2) = _`. The resulting first hole can see only 'a1' and 'a2', and the second, only 'b1' and 'b2'.")+          ["(use mappend)"]+          []+          Nothing+          "mappend _ _"+      ]+   , command "apply" Deterministic (Ref One)       "Apply the given function from *local* scope."-      (pure . useNameFromHypothesis apply)+      (pure . useNameFromHypothesis (apply Saturated))       [ Example           Nothing           ["f"]@@ -285,8 +295,8 @@       "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"+            Just (self, _) -> useNameFromContext (apply Saturated) self+            Nothing -> failure $ TacticPanic "no defining function"       )       [ Example           (Just "In the context of `foo (a :: Int) (b :: b) = _`:")@@ -298,13 +308,7 @@    , 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-      )+      (pure . use Saturated)       [ Example           (Just "`import Data.Char (isSpace)`")           ["isSpace"]@@ -344,6 +348,44 @@           "(_ :: a -> a -> a -> a) a1 a2 a3"       ] +  , command "try" Nondeterministic Tactic+      "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states."+      (pure . R.try)+      [ Example+          Nothing+          ["(apply f)"]+          [ EHI "f" "a -> b"+          ]+          (Just "b")+          $ T.pack $ unlines+            [ "-- BOTH of:\n"+            , "f (_ :: a)"+            , "\n-- and\n"+            , "_ :: b"+            ]+      ]++  , command "nested" Nondeterministic (Ref One)+      "Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context."+      (pure . nested)+      [ Example+          Nothing+          ["fmap"]+          []+          (Just "[(Int, Either Bool a)] -> [(Int, Either Bool b)]")+          "fmap (fmap (fmap _))"+      ]++  , command "with_arg" Deterministic Nullary+      "Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context."+      (pure with_arg)+      [ Example+          (Just "Where `a` is a new unifiable type variable.")+          []+          []+          (Just "r")+          "(_2 :: a -> r) (_1 :: a)"+      ]   ]  @@ -359,14 +401,9 @@ 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.InfixR (symbol "|"   $> (R.<%>) )]     , [ P.InfixL (symbol ";"   $> (>>))       , P.InfixL (symbol ","   $> bindOne)       ]@@ -385,47 +422,53 @@ wrapError err = "```\n" <> err <> "\n```\n"  +fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b+fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s))+  = P.ParseErrorBundle ne+  $ P.PosState a n+      (P.SourcePos+        (unpackFS $ srcLocFile rsl)+        ((<>) line $ P.mkPos $ srcLocLine rsl - 1)+        ((<>) col  $ P.mkPos $ srcLocCol  rsl - 1 + length @[] "[wingman|")+      )+      pos+      s+ ------------------------------------------------------------------------------ -- | Attempt to run a metaprogram tactic, returning the proof state, or the -- errors. attempt_it-    :: Context+    :: RealSrcLoc+    -> 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+    -> IO (Either String String)+attempt_it rsl ctx jdg program =+  case P.runParser tacticProgram "<splice>" (T.pack program) of+    Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb+    Right tt -> do+      res <- runTactic+            ctx+            jdg+            tt+      pure $ case res of+          Left tes -> Left $ wrapError $ show tes+          Right rtr -> Right+                     $ layout (cfg_proofstate_styling $ ctxConfig ctx)+                     $ proofState rtr  -parseMetaprogram :: T.Text -> ReaderT ParserContext IO (TacticsM ())+parseMetaprogram :: T.Text -> 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+    = either (const $ pure ()) id+    . P.runParser tacticProgram "<splice>"   ------------------------------------------------------------------------------ -- | Automatically generate the metaprogram command reference. writeDocumentation :: IO () writeDocumentation =-  writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $+  writeFile "COMMANDS.md" $     unlines       [ "# Wingman Metaprogram Command Reference"       , ""

@@ -0,0 +1,7 @@+module Wingman.Metaprogramming.Parser where++import Wingman.Metaprogramming.Lexer+import Wingman.Types++tactic :: Parser (TacticsM ())+

@@ -6,14 +6,16 @@ import           Data.List (sortOn) import           Data.String (IsString) import           Data.Text (Text)-import           Data.Text.Prettyprint.Doc+import           Data.Text.Prettyprint.Doc hiding (parens) 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.Metaprogramming.Lexer (Parser, identifier, variable, parens) import           Wingman.Types (TacticsM) +import {-# SOURCE #-} Wingman.Metaprogramming.Parser (tactic) + ------------------------------------------------------------------------------ -- | Is a tactic deterministic or not? data Determinism@@ -46,11 +48,13 @@   Nullary :: Syntax (Parser (TacticsM ()))   Ref     :: Count a -> Syntax (a -> Parser (TacticsM ()))   Bind    :: Count a -> Syntax (a -> Parser (TacticsM ()))+  Tactic  :: Syntax (TacticsM () -> Parser (TacticsM ()))  prettySyntax :: Syntax a -> Doc b prettySyntax Nullary   = "none" prettySyntax (Ref co)  = prettyCount co <+> "reference" prettySyntax (Bind co) = prettyCount co <+> "binding"+prettySyntax Tactic    = "tactic"   ------------------------------------------------------------------------------@@ -108,21 +112,24 @@ ------------------------------------------------------------------------------ -- | Run the 'Parser' of a 'MetaprogramCommand' makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())-makeMPParser (MC name Nullary _ _ tactic _) = do+makeMPParser (MC name Nullary _ _ t _) = do   identifier name-  tactic-makeMPParser (MC name (Ref One) _ _ tactic _) = do+  t+makeMPParser (MC name (Ref One) _ _ t _) = do   identifier name-  variable >>= tactic-makeMPParser (MC name (Ref Many) _ _ tactic _) = do+  variable >>= t+makeMPParser (MC name (Ref Many) _ _ t _) = do   identifier name-  P.many variable >>= tactic-makeMPParser (MC name (Bind One) _ _ tactic _) = do+  P.many variable >>= t+makeMPParser (MC name (Bind One) _ _ t _) = do   identifier name-  variable >>= tactic-makeMPParser (MC name (Bind Many) _ _ tactic _) = do+  variable >>= t+makeMPParser (MC name (Bind Many) _ _ t _) = do   identifier name-  P.many variable >>= tactic+  P.many variable >>= t+makeMPParser (MC name Tactic _ _ t _) = do+  identifier name+  parens tactic >>= t   ------------------------------------------------------------------------------@@ -143,6 +150,7 @@   , ">" <+> align (pretty desc)   , mempty   , vsep $ fmap (prettyExample name) exs+  , mempty   ]  

@@ -43,24 +43,26 @@ forceMarkdownNewlines :: String -> String forceMarkdownNewlines = unlines . fmap (<> "  ") . lines -layout :: Doc Ann -> String-layout+layout :: Bool -> Doc Ann -> String+layout use_styling   = forceMarkdownNewlines   . T.unpack   . renderSimplyDecorated id-    renderAnn-    renderUnann+    (renderAnn use_styling)+    (renderUnann use_styling)   . 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;'>"+renderAnn :: Bool -> Ann -> T.Text+renderAnn False _ = ""+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>"+renderUnann :: Bool -> Ann -> T.Text+renderUnann False _ = ""+renderUnann _ Goal = "</span>"+renderUnann _ Hypoth = "\n```\n"+renderUnann _ Status = "</span>"  proofState :: RunTacticResults -> Doc Ann proofState RunTacticResults{rtr_subgoals} =

@@ -8,7 +8,6 @@   , TacticCommand (..)   ) where -import           Control.Exception (evaluate) import           Control.Monad import           Control.Monad.Trans import           Control.Monad.Trans.Maybe@@ -32,6 +31,7 @@ import           Wingman.CaseSplit import           Wingman.EmptyCase import           Wingman.GHC+import           Wingman.Judgements (jNeedsToBindArgs) import           Wingman.LanguageServer import           Wingman.LanguageServer.Metaprogram (hoverProvider) import           Wingman.LanguageServer.TacticProviders@@ -40,7 +40,6 @@ import           Wingman.StaticPlugin import           Wingman.Tactics import           Wingman.Types-import Wingman.Metaprogramming.Lexer (ParserContext)   descriptor :: PluginId -> PluginDescriptor IdeState@@ -51,7 +50,7 @@               PluginCommand                 (tcCommandId tc)                 (tacticDesc $ tcCommandName tc)-                (tacticCmd (flip commandTactic tc) plId))+                (tacticCmd (commandTactic tc) plId))                 [minBound .. maxBound]           , pure $               PluginCommand@@ -101,8 +100,14 @@   pure $ Left $ mkErr InternalError $ T.pack $ show ufm  +mkUserFacingMessage :: [TacticError] -> UserFacingMessage+mkUserFacingMessage errs+  | elem OutOfGas errs = NotEnoughGas+mkUserFacingMessage _ = TacticErrors++ tacticCmd-    :: (ParserContext -> T.Text -> IO (TacticsM ()))+    :: (T.Text -> TacticsM ())     -> PluginId     -> CommandFunction IdeState TacticParams tacticCmd tac pId state (TacticParams uri range var_name)@@ -116,14 +121,14 @@         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+        let t = tac var_name -        timingOut (cfg_timeout_seconds cfg * seconds) $ join $-          case runTactic hj_ctx hj_jdg t of+        timingOut (cfg_timeout_seconds cfg * seconds) $ do+          res <- liftIO $ runTactic hj_ctx hj_jdg t+          pure $ join $ case res of             Left errs ->  do               traceMX "errs" errs-              Left TacticErrors+              Left $ mkUserFacingMessage errs             Right rtr ->               case rtr_extract rtr of                 L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->@@ -153,9 +158,9 @@  timingOut     :: Int  -- ^ Time in microseconds-    -> a    -- ^ Computation to run+    -> IO a    -- ^ Computation to run     -> MaybeT IO a-timingOut t m = MaybeT $ timeout t $ evaluate m+timingOut t m = MaybeT $ timeout t m   mkErr :: ErrorCode -> T.Text -> ResponseError@@ -191,18 +196,34 @@     -> Graft (Either String) ParsedSource graftHole span rtr   | _jIsTopHole (rtr_jdg rtr)-      = genericGraftWithSmallestM (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span $ \dflags ->-        everywhereM'-          $ mkBindListT $ \ix ->-            graftDecl dflags span ix $ \name pats ->-            splitToDecl (occName name)-          $ iterateSplit-          $ mkFirstAgda (fmap unXPat pats)-          $ unLoc-          $ rtr_extract rtr+      = genericGraftWithSmallestM+            (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span+      $ \dflags matches ->+          everywhereM'+            $ mkBindListT $ \ix ->+              graftDecl dflags span ix $ \name pats ->+              splitToDecl+                (case not $ jNeedsToBindArgs (rtr_jdg rtr) of+                   -- If the user has explicitly bound arguments, use the+                   -- fixity they wrote.+                   True -> matchContextFixity . m_ctxt . unLoc+                             =<< listToMaybe matches+                   -- Otherwise, choose based on the name of the function.+                   False -> Nothing+                )+                (occName name)+            $ iterateSplit+            $ mkFirstAgda (fmap unXPat pats)+            $ unLoc+            $ rtr_extract rtr graftHole span rtr   = graft span   $ rtr_extract rtr+++matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity+matchContextFixity (FunRhs _ l _) = Just l+matchContextFixity _ = Nothing   ------------------------------------------------------------------------------

@@ -19,9 +19,17 @@ staticPlugin = mempty   { dynFlagsModifyGlobal =       \df -> allowEmptyCaseButWithWarning+           $ flip gopt_unset Opt_SortBySubsumHoleFits+           $ flip gopt_unset Opt_ShowValidHoleFits            $ df+             { refLevelHoleFits = Just 0+             , maxRefHoleFits   = Just 0+             , maxValidHoleFits = Just 0 #if __GLASGOW_HASKELL__ >= 808-             { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] }+             , staticPlugins = staticPlugins df <> [metaprogrammingPlugin]+#endif+             }+#if __GLASGOW_HASKELL__ >= 808   , dynFlagsModifyParser = enableQuasiQuotes #endif   }

@@ -8,15 +8,17 @@ import           ConLike (ConLike(RealDataCon)) import           Control.Applicative (Alternative(empty)) import           Control.Lens ((&), (%~), (<>~))+import           Control.Monad (filterM) import           Control.Monad (unless)-import           Control.Monad.Except (throwError)+import           Control.Monad.Extra (anyM) import           Control.Monad.Reader.Class (MonadReader (ask))-import           Control.Monad.State.Strict (StateT(..), runStateT, gets)+import           Control.Monad.State.Strict (StateT(..), runStateT) import           Data.Bool (bool) import           Data.Foldable import           Data.Functor ((<&>)) import           Data.Generics.Labels () import           Data.List+import           Data.List.Extra (dropEnd, takeEnd) import qualified Data.Map as M import           Data.Maybe import           Data.Set (Set)@@ -34,7 +36,6 @@ 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@@ -64,28 +65,43 @@           { syn_trace = tracePrim $ "assume " <> occNameString name           , syn_used_vals = S.singleton name           }-    Nothing -> throwError $ UndefinedHypothesis name+    Nothing -> cut  +------------------------------------------------------------------------------+-- | Like 'apply', but uses an 'OccName' available in the context+-- or the module+use :: Saturation -> OccName -> TacticsM ()+use sat occ = do+  ctx <- ask+  ty <- case lookupNameInContext occ ctx of+    Just ty -> pure ty+    Nothing -> CType <$> getOccNameType occ+  apply sat $ createImportedHyInfo occ ty++ recursion :: TacticsM () -- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test, -- presumably due to running afoul of 'requireConcreteHole'. Look into this! recursion = requireConcreteHole $ tracing "recursion" $ do   defs <- getCurrentDefinitions   attemptOn (const defs) $ \(name, ty) -> markRecursion $ do+    jdg <- goal     -- Peek allows us to look at the extract produced by this block.-    peek $ \ext -> do-      jdg <- goal-      let pat_vals = jPatHypothesis jdg-      -- Make sure that the recursive call contains at least one already-bound-      -- pattern value. This ensures it is structurally smaller, and thus-      -- suggests termination.-      unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty--    let hy' = recursiveHypothesis defs-    ctx <- ask-    localTactic (apply $ HyInfo name RecursivePrv ty) (introduce ctx hy')-      <@> fmap (localTactic assumption . filterPosition name) [0..]+    peek+      ( do+          let hy' = recursiveHypothesis defs+          ctx <- ask+          localTactic (apply Saturated $ HyInfo name RecursivePrv ty) (introduce ctx hy')+            <@> fmap (localTactic assumption . filterPosition name) [0..]+      ) $ \ext -> do+        let pat_vals = jPatHypothesis jdg+        -- Make sure that the recursive call contains at least one already-bound+        -- pattern value. This ensures it is structurally smaller, and thus+        -- suggests termination.+        case (any (flip M.member pat_vals) $ syn_used_vals ext) of+          True -> Nothing+          False -> Just UnhelpfulRecursion   restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()@@ -112,22 +128,24 @@ intros' names = rule $ \jdg -> do   let g  = jGoal jdg   case tacticsSplitFunTy $ unCType g of-    (_, _, [], _) -> throwError $ GoalMismatch "intros" g-    (_, _, as, b) -> do+    (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g+    (_, _, args, res) -> do       ctx <- ask-      let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names-          num_args = length vs+      let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names+          num_occs = length occs           top_hole = isTopHole ctx jdg-          hy' = lambdaHypothesis top_hole $ zip vs $ coerce as+          bindings = zip occs $ coerce args+          bound_occs = fmap fst bindings+          hy' = lambdaHypothesis top_hole bindings           jdg' = introduce ctx hy'-               $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg+               $ withNewGoal (CType $ mkFunTys' (drop num_occs args) res) jdg       ext <- newSubgoal jdg'       pure $         ext-          & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}")+          & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show bound_occs) <> "}")                         . pure           & #syn_scoped <>~ hy'-          & #syn_val   %~ noLoc . lambda (fmap bvar' vs) . unLoc+          & #syn_val   %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc   ------------------------------------------------------------------------------@@ -184,10 +202,25 @@ ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: HyInfo CType -> TacticsM ()-homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->-  buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)+homo hi = requireConcreteHole . tracing "homo" $ do+  jdg <- goal+  let g = jGoal jdg +  -- Ensure that every data constructor in the domain type is covered in the+  -- codomain; otherwise 'homo' will produce an ill-typed program.+  case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of+    Just uncovered_dcs ->+      unless (S.null uncovered_dcs) $+        failure  $ TacticPanic "Can't cover every datacon in domain"+    _ -> failure $ TacticPanic "Unable to fetch datacons" +  rule+    $ destruct'+        False+        (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)+    $ hi++ ------------------------------------------------------------------------------ -- | LambdaCase split, and leave holes in the matches. destructLambdaCase :: TacticsM ()@@ -208,30 +241,39 @@         $ jGoal jdg  -apply :: HyInfo CType -> TacticsM ()-apply hi = tracing ("apply' " <> show (hi_name hi)) $ do+data Saturation = Unsaturated Int+  deriving (Eq, Ord, Show)++pattern Saturated :: Saturation+pattern Saturated = Unsaturated 0+++apply :: Saturation -> HyInfo CType -> TacticsM ()+apply (Unsaturated n) hi = tracing ("apply' " <> show (hi_name hi)) $ do   jdg <- goal   let g  = jGoal jdg       ty = unCType $ hi_type hi       func = hi_name hi   ty' <- freshTyvars ty-  let (_, _, args, ret) = tacticsSplitFunTy ty'+  let (_, _, all_args, ret) = tacticsSplitFunTy ty'+      saturated_args = dropEnd n all_args+      unsaturated_args = takeEnd n all_args   rule $ \jdg -> do-    unify g (CType ret)+    unify g (CType $ mkFunTys' unsaturated_args ret)     ext         <- fmap unzipTrace         $ traverse ( newSubgoal                     . blacklistingDestruct                     . flip withNewGoal jdg                     . CType-                    ) args+                    ) saturated_args     pure $       ext         & #syn_used_vals %~ S.insert func         & #syn_val       %~ mkApply func . fmap unLoc  application :: TacticsM ()-application = overFunctions apply+application = overFunctions $ apply Saturated   ------------------------------------------------------------------------------@@ -241,7 +283,7 @@   jdg <- goal   let g = jGoal jdg   case tacticsGetDataCons $ unCType g of-    Nothing -> throwError $ GoalMismatch "split" g+    Nothing -> failure $ GoalMismatch "split" g     Just (dcs, _) -> choice $ fmap splitDataCon dcs  @@ -254,7 +296,7 @@   jdg <- goal   let g = jGoal jdg   case tacticsGetDataCons $ unCType g of-    Nothing -> throwError $ GoalMismatch "split" g+    Nothing -> failure $ GoalMismatch "split" g     Just (dcs, _) -> do       case isSplitWhitelisted jdg of         True -> choice $ fmap splitDataCon dcs@@ -273,7 +315,7 @@   case tacticsGetDataCons $ unCType g of     Just ([dc], _) -> do       splitDataCon dc-    _ -> throwError $ GoalMismatch "splitSingle" g+    _ -> failure $ GoalMismatch "splitSingle" g  ------------------------------------------------------------------------------ -- | Like 'split', but prunes any data constructors which have holes.@@ -318,7 +360,7 @@     case splitTyConApp_maybe $ unCType g of       Just (_, apps) -> do         buildDataCon True (unwhitelistingSplit jdg) dc apps-      Nothing -> throwError $ GoalMismatch "splitDataCon" g+      Nothing -> cut -- failure $ GoalMismatch "splitDataCon" g  ------------------------------------------------------------------------------ -- | Attempt to instantiate the given data constructor to solve the goal.@@ -347,7 +389,7 @@            $ unHypothesis            $ jHypothesis jdg   for_ args $ \arg -> do-    subst <- gets ts_unifier+    subst <- getSubstForJudgement =<< goal     destruct $ fmap (coerce substTy subst) arg  --------------------------------------------------------------------------------@@ -364,8 +406,8 @@       case find (sloppyEqOccName occ . occName . dataConName)              $ tyConDataCons tc of         Just dc -> splitDataCon dc-        Nothing -> throwError $ NotInScope occ-    Nothing -> throwError $ NotInScope occ+        Nothing -> failure $ NotInScope occ+    Nothing -> failure $ NotInScope occ   ------------------------------------------------------------------------------@@ -390,13 +432,13 @@   auto' :: Int -> TacticsM ()-auto' 0 = throwError NoProgress+auto' 0 = failure OutOfGas auto' n = do   let loop = auto' (n - 1)   try intros   choice     [ overFunctions $ \fname -> do-        requireConcreteHole $ apply fname+        requireConcreteHole $ apply Saturated fname         loop     , overAlgebraicTerms $ \aname -> do         destructAuto aname@@ -427,8 +469,8 @@     Just method -> do       let (_, apps) = splitAppTys df       let ty = piResultTys (idType method) apps-      apply $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty-    Nothing -> throwError $ NotInScope method_name+      apply Saturated $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty+    Nothing -> failure $ NotInScope method_name   applyByName :: OccName -> TacticsM ()@@ -436,7 +478,7 @@   g <- goal   choice $ (unHypothesis (jHypothesis g)) <&> \hi ->     case hi_name hi == name of-      True  -> apply hi+      True  -> apply Saturated hi       False -> empty  @@ -475,22 +517,63 @@     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"+    Just (self, _) -> useNameFromContext (apply Saturated) self+    Nothing -> failure $ TacticPanic "no defining function"  +------------------------------------------------------------------------------+-- | Perform a catamorphism when destructing the given 'HyInfo'. This will+-- result in let binding, making values that call the defining function on each+-- destructed value. cata :: HyInfo CType -> TacticsM () cata hi = do+  (_, _, calling_args, _)+      <- tacticsSplitFunTy . unCType <$> getDefiningType+  freshened_args <- traverse freshTyvars calling_args   diff <- hyDiff $ destruct hi++  -- For for every destructed term, check to see if it can unify with any of+  -- the arguments to the calling function. If it doesn't, we don't try to+  -- perform a cata on it.+  unifiable_diff <- flip filterM (unHypothesis diff) $ \hi ->+    flip anyM freshened_args $ \ty ->+      canUnify (hi_type hi) $ CType ty+   rule $     letForEach       (mkVarOcc . flip mappend "_c" . occNameString)-      (\hi -> self >> commit (apply hi) assumption)-      diff+      (\hi -> self >> commit (assume $ hi_name hi) assumption)+      $ Hypothesis unifiable_diff ++------------------------------------------------------------------------------+-- | Deeply nest an unsaturated function onto itself+nested :: OccName -> TacticsM ()+nested = deepening . use (Unsaturated 1)+++------------------------------------------------------------------------------+-- | Repeatedly bind a tactic on its first hole+deep :: Int -> TacticsM () -> TacticsM ()+deep 0 _ = pure ()+deep n t = foldr1 bindOne $ replicate n t+++------------------------------------------------------------------------------+-- | Try 'deep' for arbitrary depths.+deepening :: TacticsM () -> TacticsM ()+deepening t =+  asum $ fmap (flip deep t) [0 .. 100]+++bindOne :: TacticsM a -> TacticsM a -> TacticsM a+bindOne t t1 = t <@> [t1]++ collapse :: TacticsM () collapse = do   g <- goal@@ -498,6 +581,15 @@   case terms of     [hi] -> assume $ hi_name hi     _    -> nary (length terms) <@> fmap (assume . hi_name) terms+++with_arg :: TacticsM ()+with_arg = rule $ \jdg -> do+  let g = jGoal jdg+  fresh_ty <- freshTyvars $ mkInvForAllTys [alphaTyVar] alphaTy+  a <- newSubgoal $ withNewGoal (CType fresh_ty) jdg+  f <- newSubgoal $ withNewGoal (coerce mkFunTys' [fresh_ty] g) jdg+  pure $ fmap noLoc $ (@@) <$> fmap unLoc f <*> fmap unLoc a   ------------------------------------------------------------------------------

@@ -1,5 +1,6 @@-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RecordWildCards   #-}+{-# LANGUAGE OverloadedStrings    #-}+{-# LANGUAGE RecordWildCards      #-}+{-# LANGUAGE UndecidableInstances #-}  {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -17,8 +18,11 @@ import           Control.Lens hiding (Context) import           Control.Monad.Reader import           Control.Monad.State+import qualified Control.Monad.State.Strict as Strict import           Data.Coerce import           Data.Function+import           Data.Generics (mkM, everywhereM, Data, Typeable)+import           Data.Generics.Labels () import           Data.Generics.Product (field) import           Data.List.NonEmpty (NonEmpty (..)) import           Data.Semigroup@@ -31,16 +35,21 @@ import           Development.IDE.GHC.Compat hiding (Node) import           Development.IDE.GHC.Orphans () import           FamInstEnv (FamInstEnvs)+import           GHC.Exts (fromString) import           GHC.Generics import           GHC.SourceGen (var)+import           GhcPlugins (GlobalRdrElt, mkRdrUnqual) import           InstEnv (InstEnvs(..)) import           OccName+import           Refinery.ProofState import           Refinery.Tactic+import           Refinery.Tactic.Internal (TacticT(TacticT), RuleT (RuleT)) import           System.IO.Unsafe (unsafePerformIO) import           Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst) import           UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)-import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)+import           Unique (nonDetCmpUnique, Uniquable, getUnique, Unique, mkUnique) import           Wingman.Debug+import Data.IORef   ------------------------------------------------------------------------------@@ -86,6 +95,7 @@   { cfg_max_use_ctor_actions :: Int   , cfg_timeout_seconds      :: Int   , cfg_auto_gas             :: Int+  , cfg_proofstate_styling   :: Bool   }   deriving (Eq, Ord, Show) @@ -94,11 +104,13 @@   { cfg_max_use_ctor_actions = 5   , cfg_timeout_seconds = 2   , cfg_auto_gas = 4+  , cfg_proofstate_styling = True   }  ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type }+  deriving stock (Data, Typeable)  instance Eq CType where   (==) = eqType `on` unCType@@ -109,9 +121,6 @@ instance Show CType where   show  = unsafeRender . unCType -instance Show OccName where-  show  = unsafeRender- instance Show Name where   show  = unsafeRender @@ -151,7 +160,10 @@ instance Show ConLike where   show  = unsafeRender +instance Show LexicalFixity where+  show  = unsafeRender + ------------------------------------------------------------------------------ -- | The state that should be shared between subgoals. Extracts move towards -- the root, judgments move towards the leaves, and the state moves *sideways*.@@ -170,7 +182,7 @@ -- | A 'UniqSupply' to use in 'defaultTacticState' unsafeDefaultUniqueSupply :: UniqSupply unsafeDefaultUniqueSupply =-  unsafePerformIO $ mkSplitUniqSupply '🚒'+  unsafePerformIO $ mkSplitUniqSupply 'w' {-# NOINLINE unsafeDefaultUniqueSupply #-}  @@ -219,7 +231,7 @@     -- to keep these in the hypothesis set, rather than filtering it, in order     -- to continue tracking downstream provenance.   | DisallowedPrv DisallowReason Provenance-  deriving stock (Eq, Show, Generic, Ord)+  deriving stock (Eq, Show, Generic, Ord, Data, Typeable)   ------------------------------------------------------------------------------@@ -229,7 +241,7 @@   | Shadowed   | RecursiveCall   | AlreadyDestructed-  deriving stock (Eq, Show, Generic, Ord)+  deriving stock (Eq, Show, Generic, Ord, Data, Typeable)   ------------------------------------------------------------------------------@@ -245,7 +257,7 @@     -- ^ The datacon which introduced this term.   , pv_position  :: Int     -- ^ The position of this binding in the datacon's arguments.-  } deriving stock (Eq, Show, Generic, Ord)+  } deriving stock (Eq, Show, Generic, Ord, Data, Typeable)   ------------------------------------------------------------------------------@@ -253,6 +265,7 @@ -- instances. newtype Uniquely a = Uniquely { getViaUnique :: a }   deriving Show via a+  deriving stock (Data, Typeable)  instance Uniquable a => Eq (Uniquely a) where   (==) = (==) `on` getUnique . getViaUnique@@ -268,7 +281,7 @@ newtype Hypothesis a = Hypothesis   { unHypothesis :: [HyInfo a]   }-  deriving stock (Functor, Eq, Show, Generic, Ord)+  deriving stock (Functor, Eq, Show, Generic, Ord, Data, Typeable)   deriving newtype (Semigroup, Monoid)  @@ -279,7 +292,7 @@   , hi_provenance :: Provenance   , hi_type       :: a   }-  deriving stock (Functor, Eq, Show, Generic, Ord)+  deriving stock (Functor, Eq, Show, Generic, Ord, Data, Typeable)   ------------------------------------------------------------------------------@@ -296,42 +309,71 @@   , _jWhitelistSplit    :: !Bool   , _jIsTopHole         :: !Bool   , _jGoal              :: !a+  , j_coercion          :: TCvSubst   }-  deriving stock (Eq, Generic, Functor, Show)+  deriving stock (Generic, Functor, Show)  type Judgement = Judgement' CType  -newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }+newtype ExtractM a = ExtractM { unExtractM :: ReaderT Context IO a }     deriving newtype (Functor, Applicative, Monad, MonadReader Context)  --------------------------------------------------------------------------------- | Orphan instance for producing holes when attempting to solve tactics.-instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where-  hole = pure . pure . noLoc $ var "_"+-- | Used to ensure hole names are unique across invocations of runTactic+globalHoleRef :: IORef Int+globalHoleRef = unsafePerformIO $ newIORef 10+{-# NOINLINE globalHoleRef #-} +instance MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM where+  hole = do+    u <- lift $ ExtractM $ lift $+          readIORef globalHoleRef <* modifyIORef' globalHoleRef (+ 1)+    pure+      ( u+      , pure . noLoc $ var $ fromString $ occNameString $ occName $ mkMetaHoleName u+      ) +  unsolvableHole _ = hole+++instance MonadReader r m => MonadReader r (TacticT jdg ext err s m) where+  ask = TacticT $ lift $ Effect $ fmap pure ask+  local f (TacticT m) = TacticT $ Strict.StateT $ \jdg ->+    Effect $ local f $ pure $ Strict.runStateT m jdg++instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where+  ask = RuleT $ Effect $ fmap Axiom ask+  local f (RuleT m) = RuleT $ Effect $ local f $ pure m++mkMetaHoleName :: Int -> RdrName+mkMetaHoleName u = mkRdrUnqual $ mkVarOcc $ "_" <> show (mkUnique 'w' u)++instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where+  -- TODO(sandy): This join is to combine the synthesizeds+  substMeta u val a =  join $ a <&>+    everywhereM (mkM $ \case+      (L _ (HsVar _ (L _ name)))+        | name == mkMetaHoleName u -> val+      (t :: LHsExpr GhcPs) -> pure t)++ ------------------------------------------------------------------------------ -- | Reasons a tactic might fail. data TacticError-  = UndefinedHypothesis OccName+  = OutOfGas   | GoalMismatch String CType-  | UnsolvedSubgoals [Judgement]-  | UnificationError CType CType   | NoProgress   | NoApplicableTactic-  | IncorrectDataCon DataCon-  | RecursionOnWrongParam OccName Int OccName+  | UnhelpfulRecursion   | UnhelpfulDestruct OccName-  | UnhelpfulSplit OccName   | TooPolymorphic   | NotInScope OccName   | TacticPanic String-  deriving stock (Eq)+  deriving (Eq)  instance Show TacticError where-    show (UndefinedHypothesis name) =-      occNameString name <> " is not available in the hypothesis."+    show OutOfGas = "Auto ran out of gas"     show (GoalMismatch tac (CType typ)) =       mconcat         [ "The tactic "@@ -339,34 +381,20 @@         , " doesn't apply to goal type "         , unsafeRender typ         ]-    show (UnsolvedSubgoals _) =-      "There were unsolved subgoals"-    show (UnificationError (CType t1) (CType t2)) =-        mconcat-          [ "Could not unify "-          , unsafeRender t1-          , " and "-          , unsafeRender t2-          ]     show NoProgress =       "Unable to make progress"     show NoApplicableTactic =       "No tactic could be applied"-    show (IncorrectDataCon dcon) =-      "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"-    show (RecursionOnWrongParam call p arg) =-      "Recursion on wrong param (" <> show call <> ") on arg"-        <> show p <> ": " <> show arg+    show UnhelpfulRecursion =+      "Recursion wasn't productive"     show (UnhelpfulDestruct n) =       "Destructing patval " <> show n <> " leads to no new types"-    show (UnhelpfulSplit n) =-      "Splitting constructor " <> show n <> " leads to no new goals"     show TooPolymorphic =       "The tactic isn't applicable because the goal is too polymorphic"     show (NotInScope name) =       "Tried to do something with the out of scope name " <> show name     show (TacticPanic err) =-      "PANIC: " <> err+      "Tactic panic: " <> err   ------------------------------------------------------------------------------@@ -394,8 +422,21 @@     -- ^ The number of recursive calls   , syn_val    :: a   }-  deriving (Eq, Show, Functor, Foldable, Traversable, Generic)+  deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic, Data, Typeable) +instance Monad Synthesized where+  return = pure+  Synthesized tr1 sc1 uv1 rc1 a >>= f =+    case f a of+      Synthesized tr2 sc2 uv2 rc2 b ->+        Synthesized+          { syn_trace = tr1 <> tr2+          , syn_scoped = sc1 <> sc2+          , syn_used_vals = uv1 <> uv2+          , syn_recursion_count = rc1 <> rc2+          , syn_val = b+          }+ mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a mapTrace f (Synthesized tr sc uv rc a) = Synthesized (f tr) sc uv rc a @@ -418,10 +459,12 @@   , ctxModuleFuncs   :: [(OccName, CType)]     -- ^ Everything defined in the current module   , ctxConfig        :: Config-  , ctxKnownThings   :: KnownThings   , ctxInstEnvs      :: InstEnvs   , ctxFamInstEnvs   :: FamInstEnvs   , ctxTheta         :: Set CType+  , ctx_hscEnv       :: HscEnv+  , ctx_occEnv       :: OccEnv [GlobalRdrElt]+  , ctx_module       :: Module   }  instance Show Context where@@ -435,14 +478,6 @@   --------------------------------------------------------------------------------- | Things we'd like to look up, that don't exist in TysWiredIn.-data KnownThings = KnownThings-  { kt_semigroup :: Class-  , kt_monoid    :: Class-  }--------------------------------------------------------------------------------- -- | An empty context emptyContext :: Context emptyContext@@ -450,15 +485,17 @@       { ctxDefiningFuncs = mempty       , ctxModuleFuncs = mempty       , ctxConfig = emptyConfig-      , ctxKnownThings = error "empty known things from emptyContext"       , ctxFamInstEnvs = mempty       , ctxInstEnvs = InstEnvs mempty mempty mempty       , ctxTheta = mempty+      , ctx_hscEnv = error "empty hsc env from emptyContext"+      , ctx_occEnv = emptyOccEnv+      , ctx_module = error "empty module from emptyContext"       }   newtype Rose a = Rose (Tree a)-  deriving stock (Eq, Functor, Generic)+  deriving stock (Eq, Functor, Generic, Data, Typeable)  instance Show (Rose String) where   show = unlines . dropEveryOther . lines . drawTree . coerce@@ -502,16 +539,18 @@   data UserFacingMessage-  = TacticErrors+  = NotEnoughGas+  | TacticErrors   | TimedOut   | NothingToDo   | InfrastructureError Text   deriving Eq  instance Show UserFacingMessage where-  show TacticErrors            = "Wingman couldn't find a solution"-  show TimedOut                = "Wingman timed out while trying to find a solution"-  show NothingToDo             = "Nothing to do"+  show NotEnoughGas = "Wingman ran out of gas when trying to find a solution.  \nTry increasing the `auto_gas` setting."+  show TacticErrors = "Wingman couldn't find a solution"+  show TimedOut     = "Wingman timed out while trying to find a solution"+  show NothingToDo  = "Nothing to do"   show (InfrastructureError t) = "Internal error: " <> T.unpack t  

@@ -2,17 +2,18 @@  module AutoTupleSpec where -import           Data.Either                  (isRight)-import           Wingman.Judgements (mkFirstJudgement)-import           Wingman.Machinery-import           Wingman.Tactics    (auto')-import           Wingman.Types-import           OccName                      (mkVarOcc)-import           Test.Hspec-import           Test.QuickCheck-import           Type                         (mkTyVarTy)-import           TysPrim                      (alphaTyVars)-import           TysWiredIn                   (mkBoxedTupleTy)+import Data.Either (isRight)+import OccName (mkVarOcc)+import System.IO.Unsafe+import Test.Hspec+import Test.QuickCheck+import Type (mkTyVarTy)+import TysPrim (alphaTyVars)+import TysWiredIn (mkBoxedTupleTy)+import Wingman.Judgements (mkFirstJudgement)+import Wingman.Machinery+import Wingman.Tactics (auto')+import Wingman.Types   spec :: Spec@@ -33,14 +34,15 @@               <$> randomGroups vars       pure $           -- We should always be able to find a solution-          runTactic-            emptyContext-            (mkFirstJudgement+          unsafePerformIO+            (runTactic               emptyContext-              (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type)-              True-              out_type)-            (auto' $ n * 2) `shouldSatisfy` isRight+              (mkFirstJudgement+                emptyContext+                (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type)+                True+                out_type)+              (auto' $ n * 2)) `shouldSatisfy` isRight   randomGroups :: [a] -> Gen [[a]]

@@ -47,6 +47,8 @@     autoTest  2 17 "AutoInfixApply"     autoTest  2 19 "AutoInfixApplyMany"     autoTest  2 25 "AutoInfixInfix"+    autoTest 19 12 "AutoTypeLevel"+    autoTest 11  9 "AutoForallClassMethod"      failing "flaky in CI" $       autoTest 2 11 "GoldenApplicativeThen"@@ -82,6 +84,7 @@     describe "messages" $ do-    mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors-    mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors+    mkShowMessageTest Auto ""  2 8 "MessageForallA"      TacticErrors+    mkShowMessageTest Auto ""  7 8 "MessageCantUnify"    TacticErrors+    mkShowMessageTest Auto "" 12 8 "MessageNotEnoughGas" NotEnoughGas 

@@ -35,3 +35,85 @@     destructTest "a"  7 17 "LayoutSplitPattern"     destructTest "a"  8 26 "LayoutSplitPatSyn" +  describe "providers" $ do+    mkTest+      "Produces destruct and homomorphism code actions"+      "T2" 2 21+      [ (id, Destruct, "eab")+      , (id, Homomorphism, "eab")+      , (not, DestructPun, "eab")+      ]++    mkTest+      "Won't suggest homomorphism on the wrong type"+      "T2" 8 8+      [ (not, Homomorphism, "global")+      ]++    mkTest+      "Produces (homomorphic) lambdacase code actions"+      "T3" 4 24+      [ (id, HomomorphismLambdaCase, "")+      , (id, DestructLambdaCase, "")+      ]++    mkTest+      "Produces lambdacase code actions"+      "T3" 7 13+      [ (id, DestructLambdaCase, "")+      ]++    mkTest+      "Doesn't suggest lambdacase without -XLambdaCase"+      "T2" 11 25+      [ (not, DestructLambdaCase, "")+      ]++    mkTest+      "Doesn't suggest destruct if already destructed"+      "ProvideAlreadyDestructed" 6 18+      [ (not, Destruct, "x")+      ]++    mkTest+      "...but does suggest destruct if destructed in a different branch"+      "ProvideAlreadyDestructed" 9 7+      [ (id, Destruct, "x")+      ]++    mkTest+      "Doesn't suggest destruct on class methods"+      "ProvideLocalHyOnly" 2 12+      [ (not, Destruct, "mempty")+      ]++    mkTest+      "Suggests homomorphism if the domain is bigger than the codomain"+      "ProviderHomomorphism" 12 13+      [ (id, Homomorphism, "g")+      ]++    mkTest+      "Doesn't suggest homomorphism if the domain is smaller than the codomain"+      "ProviderHomomorphism" 15 14+      [ (not, Homomorphism, "g")+      , (id, Destruct, "g")+      ]++    mkTest+      "Suggests lambda homomorphism if the domain is bigger than the codomain"+      "ProviderHomomorphism" 18 14+      [ (id, HomomorphismLambdaCase, "")+      ]++    mkTest+      "Doesn't suggest lambda homomorphism if the domain is smaller than the codomain"+      "ProviderHomomorphism" 21 15+      [ (not, HomomorphismLambdaCase, "")+      , (id, DestructLambdaCase, "")+      ]++    -- test layouts that maintain user-written fixities+    destructTest "b"  3 13 "LayoutInfixKeep"+    destructTest "b"  2 12 "LayoutPrefixKeep"+

@@ -20,6 +20,7 @@ #if __GLASGOW_HASKELL__ >= 808   describe "beginMetaprogram" $ do     goldenTest BeginMetaprogram ""  1  7 "MetaBegin"+    goldenTest BeginMetaprogram ""  1  9 "MetaBeginNoWildify" #endif    describe "golden" $ do@@ -33,4 +34,10 @@     metaTest 11 11 "MetaUseMethod"     metaTest  9 38 "MetaCataCollapse"     metaTest  7 16 "MetaCataCollapseUnary"+    metaTest 10 32 "MetaCataAST"+    metaTest  6 46 "MetaPointwise"+    metaTest  4 28 "MetaUseSymbol"+    metaTest  7 53 "MetaDeepOf"+    metaTest  2 34 "MetaWithArg"+    metaTest  2 12 "IntrosTooMany" 

@@ -9,6 +9,7 @@ spec :: Spec spec = do   let test = mkCodeLensTest+      noTest = mkNoCodeLensTest    describe "golden" $ do     test "EmptyCaseADT"@@ -17,4 +18,8 @@     test "EmptyCaseNested"     test "EmptyCaseApply"     test "EmptyCaseGADT"+    test "EmptyCaseLamCase"++  describe "no code lenses" $ do+    noTest "EmptyCaseSpuriousGADT" 

@@ -14,55 +14,9 @@     "T1" 2 14     [ (id, Intros, "")     ]-  mkTest-    "Produces destruct and homomorphism code actions"-    "T2" 2 21-    [ (id, Destruct, "eab")-    , (id, Homomorphism, "eab")-    , (not, DestructPun, "eab")-    ]-  mkTest-    "Won't suggest homomorphism on the wrong type"-    "T2" 8 8-    [ (not, Homomorphism, "global")-    ]+   mkTest     "Won't suggest intros on the wrong type"     "T2" 8 8     [ (not, Intros, "")     ]-  mkTest-    "Produces (homomorphic) lambdacase code actions"-    "T3" 4 24-    [ (id, HomomorphismLambdaCase, "")-    , (id, DestructLambdaCase, "")-    ]-  mkTest-    "Produces lambdacase code actions"-    "T3" 7 13-    [ (id, DestructLambdaCase, "")-    ]-  mkTest-    "Doesn't suggest lambdacase without -XLambdaCase"-    "T2" 11 25-    [ (not, DestructLambdaCase, "")-    ]--  mkTest-    "Doesn't suggest destruct if already destructed"-    "ProvideAlreadyDestructed" 6 18-    [ (not, Destruct, "x")-    ]--  mkTest-    "...but does suggest destruct if destructed in a different branch"-    "ProvideAlreadyDestructed" 9 7-    [ (id, Destruct, "x")-    ]--  mkTest-    "Doesn't suggest destruct on class methods"-    "ProvideLocalHyOnly" 2 12-    [ (not, Destruct, "mempty")-    ]-

@@ -16,7 +16,7 @@ import           Type (mkTyVarTy) import           TysPrim (alphaTyVars) import           TysWiredIn (mkBoxedTupleTy)-import           Wingman.Machinery+import           Wingman.GHC import           Wingman.Types  

@@ -15,12 +15,11 @@ import           Data.Aeson import           Data.Foldable import           Data.Function (on)-import qualified Data.Map as M+import           Data.IORef (writeIORef) import           Data.Maybe import           Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as T-import qualified Ide.Plugin.Config as Plugin import           Ide.Plugin.Tactic as Tactic import           Language.LSP.Types import           Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title)@@ -55,6 +54,19 @@ codeActionTitle (InR(CodeAction title _ _ _ _ _ _ _)) = Just title  +resetGlobalHoleRef :: IO ()+resetGlobalHoleRef = writeIORef globalHoleRef 0+++runSessionForTactics :: Session a -> IO a+runSessionForTactics =+  runSessionWithServer'+    [plugin]+    def+    (def { messageTimeout = 5 } )+    fullCaps+    tacticPath+ ------------------------------------------------------------------------------ -- | Make a tactic unit test. mkTest@@ -69,7 +81,8 @@          ) -- ^ A collection of (un)expected code actions.     -> SpecWith (Arg Bool) mkTest name fp line col ts = it name $ do-  runSessionWithServer plugin tacticPath $ do+  resetGlobalHoleRef+  runSessionForTactics $ do     doc <- openDoc (fp <.> "hs") "haskell"     _ <- waitForDiagnostics     actions <- getCodeActions doc $ pointRange line col@@ -91,7 +104,8 @@     -> SpecWith () mkGoldenTest eq tc occ line col input =   it (input <> " (golden)") $ do-    runSessionWithServer plugin tacticPath $ do+    resetGlobalHoleRef+    runSessionForTactics $ do       doc <- openDoc (input <.> "hs") "haskell"       _ <- waitForDiagnostics       actions <- getCodeActions doc $ pointRange line col@@ -113,7 +127,8 @@     -> SpecWith () mkCodeLensTest input =   it (input <> " (golden)") $ do-    runSessionWithServer plugin tacticPath $ do+    resetGlobalHoleRef+    runSessionForTactics $ do       doc <- openDoc (input <.> "hs") "haskell"       _ <- waitForDiagnostics       lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc@@ -129,7 +144,22 @@       liftIO $ edited `shouldBe` expected  +------------------------------------------------------------------------------+-- | A test that no code lenses can be run in the file+mkNoCodeLensTest+    :: FilePath+    -> SpecWith ()+mkNoCodeLensTest input =+  it (input <> " (no code lenses)") $ do+    resetGlobalHoleRef+    runSessionForTactics $ do+      doc <- openDoc (input <.> "hs") "haskell"+      _ <- waitForDiagnostics+      lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc+      liftIO $ lenses `shouldBe` [] ++ isWingmanLens :: CodeLens -> Bool isWingmanLens (CodeLens _ (Just (Command _ cmd _)) _)     = T.isInfixOf ":tactics:" cmd@@ -146,7 +176,8 @@     -> SpecWith () mkShowMessageTest tc occ line col input ufm =   it (input <> " (golden)") $ do-    runSessionWithServer plugin tacticPath $ do+    resetGlobalHoleRef+    runSessionForTactics $ do       doc <- openDoc (input <.> "hs") "haskell"       _ <- waitForDiagnostics       actions <- getCodeActions doc $ pointRange line col

@@ -0,0 +1,12 @@+{-# LANGUAGE ExplicitForAll        #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE MultiParamTypeClasses #-}++import Data.Functor.Contravariant++class Semigroupal cat t1 t2 to f where+  combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))++comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d)+comux = case combine of { (Op f) -> f }+

@@ -0,0 +1,12 @@+{-# LANGUAGE ExplicitForAll        #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE MultiParamTypeClasses #-}++import Data.Functor.Contravariant++class Semigroupal cat t1 t2 to f where+  combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))++comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d)+comux = _+

@@ -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 _ hl') = lookMeUp ea' 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 = _+

@@ -1,5 +1,5 @@ and :: Bool -> Bool -> Bool-and False False = _-and False True = _-and True False = _-and True True = _+and False False = _w0+and False True = _w1+and True False = _w2+and True True = _w3

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

@@ -16,6 +16,6 @@   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') = _+lookMeUp AtZ (HCons t hl') = _w0+lookMeUp (AtS ea') (HCons t hl') = _w1 

@@ -1,27 +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 = _+many () (Left a) False Nothing A = _w0+many () (Left a) False Nothing B = _w1+many () (Left a) False Nothing C = _w2+many () (Left a) False (Just abc') A = _w3+many () (Left a) False (Just abc') B = _w4+many () (Left a) False (Just abc') C = _w5+many () (Left a) True Nothing A = _w6+many () (Left a) True Nothing B = _w7+many () (Left a) True Nothing C = _w8+many () (Left a) True (Just abc') A = _w9+many () (Left a) True (Just abc') B = _wa+many () (Left a) True (Just abc') C = _wb+many () (Right b') False Nothing A = _wc+many () (Right b') False Nothing B = _wd+many () (Right b') False Nothing C = _we+many () (Right b') False (Just abc') A = _wf+many () (Right b') False (Just abc') B = _wg+many () (Right b') False (Just abc') C = _wh+many () (Right b') True Nothing A = _wi+many () (Right b') True Nothing B = _wj+many () (Right b') True Nothing C = _wk+many () (Right b') True (Just abc') A = _wl+many () (Right b') True (Just abc') B = _wm+many () (Right b') True (Just abc') C = _wn

@@ -1,6 +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 = _+and (a, b) False False = _w0+and (a, b) False True = _w1+and (a, b) True False = _w2+and (a, b) True True = _w3 

@@ -28,27 +28,27 @@   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') = _+cthulhu ID = _w0+cthulhu (Comp fp' fp_rcyb) = _w1+cthulhu Copy = _w2+cthulhu Consume = _w3+cthulhu Swap = _w4+cthulhu SwapE = _w5+cthulhu Fst = _w6+cthulhu Snd = _w7+cthulhu InjectL = _w8+cthulhu InjectR = _w9+cthulhu Unify = _wa+cthulhu (First fp') = _wb+cthulhu (Second fp') = _wc+cthulhu (Alongside fp' fp_rca'b') = _wd+cthulhu (Fanout fp' fp_rcab') = _we+cthulhu (Left' fp') = _wf+cthulhu (Right' fp') = _wg+cthulhu (EitherOf fp' fp_rca'b') = _wh+cthulhu (Fanin fp' fp_rca'b) = _wi+cthulhu (LiftC cab) = _wj+cthulhu Zero = _wk+cthulhu (Plus fp' fp_rcab) = _wl+cthulhu (Unleft fp') = _wm+cthulhu (Unright fp') = _wn

@@ -4,5 +4,5 @@ data instance Yo = Heya Int  test :: Yo -> Int-test (Heya n) = _+test (Heya n) = _w0 

@@ -3,6 +3,6 @@  data Foo = Foo { a :: Bool, b :: Bool } -foo Foo {a = False, b} = _-foo Foo {a = True, b} = _+foo Foo {a = False, b} = _w0+foo Foo {a = True, b} = _w1 

@@ -4,6 +4,6 @@   Yo = Bool  test :: Yo -> Int-test False = _-test True = _+test False = _w0+test True = _w1 

@@ -14,5 +14,5 @@ data instance Yo = Heya Int  test :: T1 Bool -> Int-test (Heya n) = _+test (Heya n) = _w0 

@@ -0,0 +1,6 @@+{-# LANGUAGE LambdaCase #-}++test :: Bool -> Bool+test = \case+  False -> _+  True -> _

@@ -0,0 +1,4 @@+{-# LANGUAGE LambdaCase #-}++test :: Bool -> Bool+test = \case

@@ -0,0 +1,8 @@+{-# LANGUAGE GADTs #-}++data Foo a where+  Foo :: Foo Int++foo :: Foo Bool -> ()+foo x = case x of+

@@ -4,4 +4,4 @@   MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT  ctxGADT :: CtxGADT -> String-ctxGADT (MkCtxGADT a) = _+ctxGADT (MkCtxGADT a) = _w0

@@ -5,4 +5,4 @@   E :: forall a b. (b ~ a, Ord a) => b -> E a [a]  ctxGADT :: E a b -> String-ctxGADT (E b) = _+ctxGADT (E b) = _w0

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

@@ -0,0 +1,2 @@+too_many :: a -> b -> c+too_many a b = _w0

@@ -0,0 +1,2 @@+too_many :: a -> b -> c+too_many = [wingman| intros a b c d e f g h i j k l m n o p q r s t u v w x y z |]

@@ -3,7 +3,7 @@ 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 sum s en any) <> (Big bs' sum' str en' any')     = Big         (bs <> bs') (sum <> sum') (s <> str) (en <> en') (any <> any') 

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

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

@@ -4,5 +4,5 @@   (<>) = undefined  instance Monoid (Mono a) where-  mempty = Monoid mempty _+  mempty = Monoid mempty _w0 

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

@@ -7,6 +7,6 @@ data Bar = Bar Foo Foo  instance Semigroup Bar where-  (<>) (Bar foo foo') (Bar foo2 foo3)+  (Bar foo foo') <> (Bar foo2 foo3)     = Bar (foo <> foo2) (foo' <> foo3) 

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

@@ -2,7 +2,7 @@ test b = do   putStrLn "hello"   case b of-    False -> _-    True -> _+    False -> _w0+    True -> _w1   pure () 

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

@@ -0,0 +1,5 @@+-- keep layout that was written by the user in infix+foo :: Bool -> a -> a+False `foo` a = _w0+True `foo` a = _w1+

@@ -0,0 +1,4 @@+-- keep layout that was written by the user in infix+foo :: Bool -> a -> a+b `foo` a = _+

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

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

@@ -0,0 +1,4 @@+(-/) :: Bool -> a -> a+(-/) False a = _w0+(-/) True a = _w1+

@@ -0,0 +1,3 @@+(-/) :: Bool -> a -> a+(-/) b a = _+

@@ -1,5 +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 -> _}+p = Pair {pa = _, pb = \ a b c -> _w0} 

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

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

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

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

@@ -5,7 +5,7 @@   test :: Maybe [Bool] -> Maybe Bool-test (JustSingleton False) = _-test (JustSingleton True) = _+test (JustSingleton False) = _w0+test (JustSingleton True) = _w1  

@@ -4,6 +4,6 @@ pattern Blah a = Just a  test :: Maybe Bool -> a-test (Blah False) = _-test (Blah True) = _+test (Blah False) = _w0+test (Blah True) = _w1 

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

@@ -8,7 +8,7 @@       foo = putStrLn "Hi"        bar :: A -> IO ()-      bar A = _-      bar B = _-      bar C = _+      bar A = _w0+      bar B = _w1+      bar C = _w2 

@@ -0,0 +1,13 @@+test+   :: (a1 -> a2)+   -> (a2 -> a3)+   -> (a3 -> a4)+   -> (a4 -> a5)+   -> (a5 -> a6)+   -> (a6 -> a7)+   -> (a7 -> a8)+   -> (a8 -> a9)+   -> (a9 -> a10)+   -> a1 -> a10+test = _+

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

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

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

@@ -0,0 +1,23 @@+{-# LANGUAGE GADTs #-}++data AST a where+    BoolLit :: Bool -> AST Bool+    IntLit :: Int -> AST Int+    If :: AST Bool -> AST a -> AST a -> AST a+    Equal :: AST a -> AST a -> AST Bool++eval :: AST a -> a+eval (BoolLit b) = b+eval (IntLit n) = n+eval (If ast ast' ast_a)+  = let+      ast_c = eval ast+      ast'_c = eval ast'+      ast_a_c = eval ast_a+    in _w0 ast_c ast'_c ast_a_c+eval (Equal ast ast')+  = let+      ast_c = eval ast+      ast'_c = eval ast'+    in _w1 ast_c ast'_c+

@@ -0,0 +1,11 @@+{-# LANGUAGE GADTs #-}++data AST a where+    BoolLit :: Bool -> AST Bool+    IntLit :: Int -> AST Int+    If :: AST Bool -> AST a -> AST a -> AST a+    Equal :: AST a -> AST a -> AST Bool++eval :: AST a -> a+eval = [wingman| intros x, cata x; collapse |]+

@@ -10,5 +10,5 @@     = let         fx_c = yo fx         gx_c = yo gx-      in _ fx_c gx_c+      in _w0 fx_c gx_c 

@@ -0,0 +1,8 @@+whats_it_deep_of+    :: (a -> a)+    -> [(Int, Either Bool (Maybe [a]))]+    -> [(Int, Either Bool (Maybe [a]))]+-- The assumption here is necessary to tie-break in favor of the longest+-- nesting of fmaps.+whats_it_deep_of f = fmap (fmap (fmap (fmap (fmap f))))+

@@ -0,0 +1,8 @@+whats_it_deep_of+    :: (a -> a)+    -> [(Int, Either Bool (Maybe [a]))]+    -> [(Int, Either Bool (Maybe [a]))]+-- The assumption here is necessary to tie-break in favor of the longest+-- nesting of fmaps.+whats_it_deep_of f = [wingman| nested fmap, assumption |]+

@@ -0,0 +1,8 @@+import Data.Monoid++data Foo = Foo (Sum Int) (Sum Int)++mappend2 :: Foo -> Foo -> Foo+mappend2 (Foo sum sum') (Foo sum2 sum3)+  = Foo (mappend sum sum2) (mappend sum' sum3)+

@@ -0,0 +1,7 @@+import Data.Monoid++data Foo = Foo (Sum Int) (Sum Int)++mappend2 :: Foo -> Foo -> Foo+mappend2 = [wingman| intros f1 f2, destruct_all, ctor Foo; pointwise (use mappend); assumption|]+

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

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

@@ -0,0 +1,4 @@+import Data.Monoid++resolve :: Sum Int+resolve = _w0 <> _w1

@@ -0,0 +1,4 @@+import Data.Monoid++resolve :: Sum Int+resolve = [wingman| use (<>) |]

@@ -0,0 +1,2 @@+wat :: a -> b+wat a = _w0 a

@@ -0,0 +1,2 @@+wat :: a -> b+wat a = [wingman| with_arg, assumption |]

@@ -0,0 +1,22 @@+{-# LANGUAGE GADTs      #-}+{-# LANGUAGE LambdaCase #-}++data GADT a where+  B1 :: GADT Bool+  B2 :: GADT Bool+  Int :: GADT Int+  Var :: GADT a+++hasHomo :: GADT Bool -> GADT a+hasHomo g = _++cantHomo :: GADT a -> GADT Int+cantHomo g = _++hasHomoLam :: GADT Bool -> GADT a+hasHomoLam = _++cantHomoLam :: GADT a -> GADT Int+cantHomoLam = _+

@@ -8,5 +8,5 @@   split :: GADT a -> a-split GADT {blah, bar} = _+split GADT {blah, bar} = _w0 

@@ -3,6 +3,6 @@   | Goodbye { a :: Int, b :: Bool, c :: Many }  test :: Many -> Many-test Hello {world} = _-test Goodbye {a, b, c} = _+test Hello {world} = _w0+test Goodbye {a, b, c} = _w1 

@@ -14,6 +14,6 @@   split :: GADT Bool -> a-split GADT {blah, bar} = _-split Bar {zoo, baxter, another} = _+split GADT {blah, bar} = _w0+split Bar {zoo, baxter, another} = _w1 

@@ -1,5 +1,5 @@ data Bar = Bar { ax :: Int, bax :: Bool }  bar :: () -> Bar -> Int-bar ax Bar {ax = n, bax} = _+bar ax Bar {ax = n, bax} = _w0 

@@ -1,5 +1,5 @@ data Bar = Bar { ax :: Int, bax :: Bool }  bar :: Bar -> Int-bar Bar {ax, bax} = _+bar Bar {ax, bax} = _w0 

@@ -1,3 +1,3 @@ test :: ((), (b, c), d)-test = (_, _, _)+test = (_w0, _w1, _w2) 

@@ -5,5 +5,5 @@   Two :: GADT Bool  test :: z -> GADT Int-test z = One _+test z = One _w0 

@@ -1,2 +1,2 @@ test :: a -> Either a b-test a = _+test a = _w0

@@ -1,5 +1,5 @@ newtype Reader r a = Reader (r -> a)  test :: b -> Reader r a-test b = Reader _+test b = Reader _w0 

@@ -4,9 +4,9 @@ case_split One        = _ case_split (Two i)    = _ case_split Three      = _-case_split (Four b One) = _-case_split (Four b (Two n)) = _-case_split (Four b Three) = _-case_split (Four b (Four b' adt)) = _-case_split (Four b Five) = _+case_split (Four b One) = _w0+case_split (Four b (Two n)) = _w1+case_split (Four b Three) = _w2+case_split (Four b (Four b' adt)) = _w3+case_split (Four b Five) = _w4 case_split Five       = _

@@ -1,3 +1,3 @@ test :: Either a b-test = Left _+test = Left _w0 

@@ -1,2 +1,2 @@ test :: (a, b)-test = (_, _)+test = (_w0, _w1)

@@ -1,3 +1,3 @@ test :: Either a b-test = Right _+test = Right _w0