hls-tactics-plugin 1.5.0.1 → 1.6.0.0
raw patch · 45 files changed
+465/−215 lines, 45 filesdep ~ghcidedep ~hls-plugin-apidep ~hls-test-utils
Dependency ranges changed: ghcide, hls-plugin-api, hls-test-utils
Files
- hls-tactics-plugin.cabal +4/−4
- src/Refinery/Future.hs +3/−3
- src/Wingman/AbstractLSP.hs +22/−26
- src/Wingman/AbstractLSP/TacticActions.hs +5/−4
- src/Wingman/AbstractLSP/Types.hs +5/−7
- src/Wingman/CaseSplit.hs +1/−1
- src/Wingman/CodeGen.hs +24/−9
- src/Wingman/Context.hs +6/−0
- src/Wingman/Debug.hs +2/−1
- src/Wingman/EmptyCase.hs +9/−9
- src/Wingman/GHC.hs +32/−17
- src/Wingman/Judgements.hs +11/−10
- src/Wingman/Judgements/SYB.hs +2/−2
- src/Wingman/Judgements/Theta.hs +28/−3
- src/Wingman/LanguageServer.hs +13/−6
- src/Wingman/LanguageServer/Metaprogram.hs +1/−2
- src/Wingman/LanguageServer/TacticProviders.hs +6/−7
- src/Wingman/Machinery.hs +34/−9
- src/Wingman/Metaprogramming/Lexer.hs +0/−2
- src/Wingman/Metaprogramming/Parser.hs +14/−3
- src/Wingman/Metaprogramming/Parser/Documentation.hs +1/−0
- src/Wingman/Metaprogramming/ProofState.hs +2/−0
- src/Wingman/Naming.hs +9/−4
- src/Wingman/Plugin.hs +0/−3
- src/Wingman/Range.hs +2/−3
- src/Wingman/Simplify.hs +10/−10
- src/Wingman/StaticPlugin.hs +15/−13
- src/Wingman/Tactics.hs +68/−18
- src/Wingman/Types.hs +3/−4
- test/AutoTupleSpec.hs +1/−2
- test/CodeAction/AutoSpec.hs +1/−1
- test/CodeAction/RunMetaprogramSpec.hs +4/−0
- test/ProviderSpec.hs +6/−0
- test/UnificationSpec.hs +9/−2
- test/Utils.hs +40/−28
- test/golden/AutoThetaRankN.expected.hs +1/−1
- test/golden/AutoThetaRankN.hs +1/−1
- test/golden/MetaFundeps.expected.hs +16/−0
- test/golden/MetaFundeps.hs +16/−0
- test/golden/MetaIdiom.expected.hs +6/−0
- test/golden/MetaIdiom.hs +6/−0
- test/golden/MetaIdiomRecord.expected.hs +8/−0
- test/golden/MetaIdiomRecord.hs +8/−0
- test/golden/SubsequentTactics.expected.hs +5/−0
- test/golden/SubsequentTactics.hs +5/−0
hls-tactics-plugin.cabal view
@@ -1,7 +1,7 @@ cabal-version: 2.4 category: Development name: hls-tactics-plugin-version: 1.5.0.1+version: 1.6.0.0 synopsis: Wingman plugin for Haskell Language Server description: Please see the README on GitHub at <https://github.com/haskell/haskell-language-server#readme>@@ -82,9 +82,9 @@ , ghc-boot-th , ghc-exactprint , ghc-source-gen ^>=0.4.1- , ghcide ^>=1.5.0+ , ghcide ^>=1.6 , hls-graph- , hls-plugin-api >=1.1 && <1.3+ , hls-plugin-api ^>=1.3 , hyphenation , lens , lsp@@ -160,7 +160,7 @@ , ghcide , hls-plugin-api , hls-tactics-plugin- , hls-test-utils >=1.0 && <1.2+ , hls-test-utils ^>=1.2 , hspec , hspec-expectations , lens
src/Refinery/Future.hs view
@@ -113,7 +113,7 @@ -- This would happen when we had a handler that wasn't followed by an error call. -- pair >> goal >>= \g -> (handler_ $ \_ -> traceM $ "Handling " <> show g) <|> failure "Error" -- We would see the "Handling a" message when solving for b.- (go s' (goals ++ [(meta, goal)]) pure $ k h)+ go s' (goals ++ [(meta, goal)]) pure $ k h go s goals handlers (Effect m) = m >>= go s goals handlers go s goals handlers (Stateful f) = let (s', p) = f s@@ -121,10 +121,10 @@ go s goals handlers (Alt p1 p2) = unListT $ ListT (go s goals handlers p1) <|> ListT (go s goals handlers p2) go s goals handlers (Interleave p1 p2) =- interleaveT <$> (go s goals handlers p1) <*> (go s goals handlers p2)+ interleaveT <$> go s goals handlers p1 <*> go s goals handlers p2 go s goals handlers (Commit p1 p2) = do solns <- force =<< go s goals handlers p1- if (any isRight solns) then pure $ ofList solns else go s goals handlers p2+ if any isRight solns then pure $ ofList solns else go s goals handlers p2 go _ _ _ Empty = pure Done go _ _ handlers (Failure err _) = do annErr <- handlers err
src/Wingman/AbstractLSP.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE NoMonoLocalBinds #-} @@ -30,6 +29,7 @@ import Wingman.AbstractLSP.Types import Wingman.EmptyCase (fromMaybeT) import Wingman.LanguageServer (getTacticConfig, getIdeDynflags, mkWorkspaceEdits, runStaleIde, showLspMessage, mkShowMessageParams)+import Wingman.StaticPlugin (enableQuasiQuotes) import Wingman.Types @@ -94,12 +94,13 @@ , _xdata = Nothing } ) $ do env@LspEnv{..} <- buildEnv state plId fc- let stale a = runStaleIde "runContinuation" state (fc_nfp le_fileContext) a+ nfp <- getNfp $ fc_uri le_fileContext+ let stale a = runStaleIde "runContinuation" state nfp a args <- fetchTargetArgs @a env res <- c_runCommand cont env args fc b -- This block returns a maybe error.- fmap (maybe (Right $ A.Null) Left . coerce . foldMap Last) $+ fmap (maybe (Right A.Null) Left . coerce . foldMap Last) $ for res $ \case ErrorMessages errs -> do traverse_ showUserFacingMessage errs@@ -110,7 +111,7 @@ GraftEdit gr -> do ccs <- lift getClientCapabilities TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource- case mkWorkspaceEdits le_dflags ccs (fc_uri le_fileContext) (unTrack pm) gr of+ case mkWorkspaceEdits (enableQuasiQuotes le_dflags) ccs (fc_uri le_fileContext) (unTrack pm) gr of Left errs -> pure $ Just $ ResponseError { _code = InternalError@@ -119,7 +120,7 @@ } Right edits -> do sendEdits edits- pure $ Nothing+ pure Nothing ------------------------------------------------------------------------------@@ -152,7 +153,8 @@ -> MaybeT (LspM Plugin.Config) LspEnv buildEnv state plId fc = do cfg <- lift $ getTacticConfig plId- dflags <- mapMaybeT liftIO $ getIdeDynflags state $ fc_nfp fc+ nfp <- getNfp $ fc_uri fc+ dflags <- mapMaybeT liftIO $ getIdeDynflags state nfp pure $ LspEnv { le_ideState = state , le_pluginId = plId@@ -174,22 +176,19 @@ ) -> PluginMethodHandler IdeState TextDocumentCodeAction codeActionProvider sort k state plId- (CodeActionParams _ _ (TextDocumentIdentifier uri) range _)- | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do- fromMaybeT (Right $ List []) $ do- let fc = FileContext- { fc_uri = uri- , fc_nfp = nfp- , fc_range = Just $ unsafeMkCurrent range- }- env <- buildEnv state plId fc- args <- fetchTargetArgs @target env- actions <- k env args- pure- $ Right- $ List- $ fmap (InR . uncurry (makeCodeAction plId fc sort)) actions-codeActionProvider _ _ _ _ _ = pure $ Right $ List []+ (CodeActionParams _ _ (TextDocumentIdentifier uri) range _) = do+ fromMaybeT (Right $ List []) $ do+ let fc = FileContext+ { fc_uri = uri+ , fc_range = Just $ unsafeMkCurrent range+ }+ env <- buildEnv state plId fc+ args <- fetchTargetArgs @target env+ actions <- k env args+ pure+ $ Right+ $ List+ $ fmap (InR . uncurry (makeCodeAction plId fc sort)) actions ------------------------------------------------------------------------------@@ -204,12 +203,10 @@ ) -> PluginMethodHandler IdeState TextDocumentCodeLens codeLensProvider sort k state plId- (CodeLensParams _ _ (TextDocumentIdentifier uri))- | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do+ (CodeLensParams _ _ (TextDocumentIdentifier uri)) = do fromMaybeT (Right $ List []) $ do let fc = FileContext { fc_uri = uri- , fc_nfp = nfp , fc_range = Nothing } env <- buildEnv state plId fc@@ -219,7 +216,6 @@ $ Right $ List $ fmap (uncurry3 $ makeCodeLens plId sort fc) actions-codeLensProvider _ _ _ _ _ = pure $ Right $ List [] ------------------------------------------------------------------------------
src/Wingman/AbstractLSP/TacticActions.hs view
@@ -45,9 +45,10 @@ } ) $ \LspEnv{..} HoleJudgment{..} FileContext{..} var_name -> do- let stale a = runStaleIde "tacticCmd" le_ideState fc_nfp a+ nfp <- getNfp fc_uri+ let stale a = runStaleIde "tacticCmd" le_ideState nfp a - let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath fc_nfp)) hj_range+ let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range TrackedStale _ pmmap <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource pm_span <- liftMaybe $ mapAgeFrom pmmap span IdeOptions{optTesting = IdeTesting isTesting} <-@@ -161,8 +162,8 @@ | dst `isSubspanOf` src = do L _ dec <- annotateDecl dflags $ make_decl name pats case dec of- ValD _ (FunBind { fun_matches = MG { mg_alts = L _ alts@(first_match : _)}- }) -> do+ ValD _ FunBind{ fun_matches = MG { mg_alts = L _ alts@(first_match : _)}+ } -> do -- For whatever reason, ExactPrint annotates newlines to the ends of -- case matches and type signatures, but only allows us to insert -- them at the beginning of those things. Thus, we need want to
src/Wingman/AbstractLSP/Types.hs view
@@ -121,7 +121,6 @@ -- | What file are we looking at, and what bit of it? data FileContext = FileContext { fc_uri :: Uri- , fc_nfp :: NormalizedFilePath , fc_range :: Maybe (Tracked 'Current Range) -- ^ For code actions, this is 'Just'. For code lenses, you'll get -- a 'Nothing' in the request, and a 'Just' in the response.@@ -129,12 +128,7 @@ deriving stock (Eq, Ord, Show, Generic) deriving anyclass (A.ToJSON, A.FromJSON) -deriving anyclass instance A.ToJSON NormalizedFilePath-deriving anyclass instance A.ToJSON NormalizedUri-deriving anyclass instance A.FromJSON NormalizedFilePath-deriving anyclass instance A.FromJSON NormalizedUri - ------------------------------------------------------------------------------ -- | Everything we need to resolve continuations. data LspEnv = LspEnv@@ -162,10 +156,14 @@ data HoleTarget = HoleTarget deriving stock (Eq, Ord, Show, Enum, Bounded) +getNfp :: Applicative m => Uri -> MaybeT m NormalizedFilePath+getNfp = MaybeT . pure . uriToNormalizedFilePath . toNormalizedUri+ instance IsTarget HoleTarget where type TargetArgs HoleTarget = HoleJudgment fetchTargetArgs LspEnv{..} = do let FileContext{..} = le_fileContext range <- MaybeT $ pure fc_range- mapMaybeT liftIO $ judgementForHole le_ideState fc_nfp range le_config+ nfp <- getNfp fc_uri+ mapMaybeT liftIO $ judgementForHole le_ideState nfp range le_config
src/Wingman/CaseSplit.hs view
@@ -105,5 +105,5 @@ iterateSplit :: AgdaMatch -> [AgdaMatch] iterateSplit am = let iterated = iterate (agdaSplit =<<) $ pure am- in fmap wildify . head . drop 5 $ iterated+ in fmap wildify . (!! 5) $ iterated
src/Wingman/CodeGen.hs view
@@ -1,8 +1,8 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedLabels #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-}-{-# LANGUAGE TypeApplications #-} module Wingman.CodeGen ( module Wingman.CodeGen@@ -57,7 +57,7 @@ Just (dcs, apps) -> fmap unzipTrace $ for dcs $ \dc -> do let con = RealDataCon dc- ev = concatMap mkEvidence $ dataConInstArgTys dc apps+ ev = concatMap (mkEvidence . scaledThing) $ dataConInstArgTys dc apps -- We explicitly do not need to add the method hypothesis to -- #syn_scoped method_hy = foldMap evidenceToHypothesis ev@@ -141,8 +141,7 @@ in (names', ) $ ConPatIn (noLoc $ Unqual $ occName $ conLikeName con) $ RecCon- $ HsRecFields rec_fields- $ Nothing+ $ HsRecFields rec_fields Nothing | otherwise = (names, ) $ infixifyPatIfNecessary con $ conP@@ -186,7 +185,7 @@ -- ^ Types of arguments to the ConLike with returned type is instantiated with the second argument. conLikeInstOrigArgTys' con uniTys = let exvars = conLikeExTys con- in conLikeInstOrigArgTys con $+ in fmap scaledThing $ conLikeInstOrigArgTys con $ uniTys ++ fmap mkTyVarTy exvars -- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys' -- unifies the second argument with DataCon's universals followed by existentials.@@ -208,7 +207,7 @@ destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule destruct' use_field_puns f hi jdg = do- when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic+ when (isDestructBlacklisted jdg) cut -- throwError NoApplicableTactic let term = hi_name hi ext <- destructMatches@@ -227,10 +226,14 @@ -- resulting matches. destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule destructLambdaCase' use_field_puns f jdg = do- when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic+ when (isDestructBlacklisted jdg) cut -- throwError NoApplicableTactic let g = jGoal jdg case splitFunTy_maybe (unCType g) of+#if __GLASGOW_HASKELL__ >= 900+ Just (_multiplicity, arg, _) | isAlgType arg ->+#else Just (arg, _) | isAlgType arg ->+#endif fmap (fmap noLoc lambdaCase) <$> destructMatches use_field_puns f Nothing (CType arg) jdg _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g@@ -320,12 +323,24 @@ occexts <- traverse newSubgoal $ fmap snd occjdgs ctx <- ask ext <- newSubgoal- $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs)- $ jdg+ $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs) jdg pure $ fmap noLoc $ let' <$> traverse (\(occ, ext) -> valBind (occNameToStr occ) <$> fmap unLoc ext) (zip (fmap fst occjdgs) occexts) <*> fmap unLoc ext+++------------------------------------------------------------------------------+-- | Converts a function application into applicative form+idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs+idiomize x = noLoc $ case unLoc x of+ HsApp _ (L _ (HsVar _ (L _ x))) gshgp3 ->+ op (bvar' $ occName x) "<$>" (unLoc gshgp3)+ HsApp _ gsigp gshgp3 ->+ op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3)+ RecordCon _ con flds ->+ unLoc $ idiomize $ noLoc $ foldl' (@@) (HsVar noExtField con) $ fmap unLoc flds+ y -> y
src/Wingman/Context.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Wingman.Context where import Control.Arrow@@ -11,6 +13,10 @@ import Wingman.GHC (normalizeType) import Wingman.Judgements.Theta import Wingman.Types++#if __GLASGOW_HASKELL__ >= 900+import GHC.Tc.Utils.TcType+#endif mkContext
src/Wingman/Debug.hs view
@@ -17,6 +17,7 @@ import Control.DeepSeq import Control.Exception+import Data.Either (fromRight) import qualified Debug.Trace import Development.IDE.GHC.Compat (PlainGhcException, Outputable(..), SDoc, showSDocUnsafe) import System.IO.Unsafe (unsafePerformIO)@@ -33,7 +34,7 @@ -- We might not have unsafeGlobalDynFlags (like during testing), in which -- case GHC panics. Instead of crashing, let's just fail to print. !res <- try @PlainGhcException $ evaluate $ deepseq z z- pure $ either (const "<unsafeRender'>") id res+ pure $ fromRight "<unsafeRender'>" res {-# NOINLINE unsafeRender' #-} traceMX :: (Monad m, Show a) => String -> a -> m ()
src/Wingman/EmptyCase.hs view
@@ -17,8 +17,7 @@ import Data.Monoid import qualified Data.Text as T import Data.Traversable-import Development.IDE (hscEnv)-import Development.IDE (realSrcSpanToRange)+import Development.IDE (hscEnv, realSrcSpanToRange) import Development.IDE.Core.RuleTypes import Development.IDE.Core.Shake (IdeState (..)) import Development.IDE.Core.UseStale@@ -51,13 +50,14 @@ Continuation @EmptyCaseT @EmptyCaseT @WorkspaceEdit EmptyCaseT (SynthesizeCodeLens $ \LspEnv{..} _ -> do let FileContext{..} = le_fileContext+ nfp <- getNfp fc_uri - let stale a = runStaleIde "codeLensProvider" le_ideState fc_nfp a+ let stale a = runStaleIde "codeLensProvider" le_ideState nfp a ccs <- lift getClientCapabilities TrackedStale pm _ <- mapMaybeT liftIO $ stale GetAnnotatedParsedSource TrackedStale binds bind_map <- mapMaybeT liftIO $ stale GetBindings- holes <- mapMaybeT liftIO $ emptyCaseScrutinees le_ideState fc_nfp+ holes <- mapMaybeT liftIO $ emptyCaseScrutinees le_ideState nfp for holes $ \(ss, ty) -> do binds_ss <- liftMaybe $ mapAgeFrom bind_map ss@@ -81,14 +81,14 @@ , edits ) )- $ (\ _ _ _ we -> pure $ pure $ RawEdit we)+ (\ _ _ _ we -> pure $ pure $ RawEdit we) scrutinzedType :: EmptyCaseSort Type -> Maybe Type scrutinzedType (EmptyCase ty) = pure ty scrutinzedType (EmptyLamCase ty) = case tacticsSplitFunTy ty of- (_, _, tys, _) -> listToMaybe tys+ (_, _, tys, _) -> listToMaybe $ fmap scaledThing tys ------------------------------------------------------------------------------@@ -115,9 +115,9 @@ -> Graft (Either String) ParsedSource graftMatchGroup ss l = hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case- L span (HsCase ext scrut mg@_) -> do+ L span (HsCase ext scrut mg) -> do pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l }- L span (HsLamCase ext mg@_) -> do+ L span (HsLamCase ext mg) -> do pure $ Just $ L span $ HsLamCase ext $ mg { mg_alts = l } (_ :: LHsExpr GhcPs) -> pure Nothing @@ -165,6 +165,6 @@ emptyCaseQ :: GenericQ [(SrcSpan, EmptyCaseSort (HsExpr GhcTc))] emptyCaseQ = everything (<>) $ mkQ mempty $ \case L new_span (Case scrutinee []) -> pure (new_span, EmptyCase scrutinee)- L new_span (expr@(LamCase [])) -> pure (new_span, EmptyLamCase expr)+ L new_span expr@(LamCase []) -> pure (new_span, EmptyLamCase expr) (_ :: LHsExpr GhcTc) -> mempty
src/Wingman/GHC.hs view
@@ -6,6 +6,7 @@ import Control.Monad.State import Control.Monad.Trans.Maybe (MaybeT(..)) import Data.Bool (bool)+import Data.Coerce (coerce) import Data.Function (on) import Data.Functor ((<&>)) import Data.List (isPrefixOf)@@ -21,7 +22,11 @@ import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types +#if __GLASGOW_HASKELL__ >= 900+import GHC.Tc.Utils.TcType+#endif + tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty -- look through casts, as@@ -57,7 +62,7 @@ ------------------------------------------------------------------------------ -- | Split a function, also splitting out its quantified variables and theta -- context.-tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)+tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Scaled Type], Type) tacticsSplitFunTy t = let (vars, theta, t') = tcSplitNestedSigmaTys t (args, res) = tcSplitFunTys t'@@ -96,10 +101,7 @@ pure (tv, setTyVarUnique tv uniq) pure $ everywhere- (mkT $ \tv ->- case M.lookup tv reps of- Just tv' -> tv'- Nothing -> tv+ (mkT $ \tv -> M.findWithDefault tv tv reps ) $ snd $ tcSplitForAllTyVars t @@ -182,7 +184,11 @@ ------------------------------------------------------------------------------ -- | Unpack the relevant parts of a 'Match'+#if __GLASGOW_HASKELL__ >= 900+pattern AMatch :: HsMatchContext (NoGhcTc GhcPs) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)+#else pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)+#endif pattern AMatch ctx pats body <- Match { m_ctxt = ctx , m_pats = fmap fromPatCompat -> pats@@ -193,9 +199,9 @@ pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs pattern SingleLet bind pats val expr <- HsLet _- (L _ (HsValBinds _+ (HsValBinds _ (ValBinds _ (bagToList ->- [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _)))+ [L _ (FunBind {fun_id = (L _ bind), fun_matches = (MG _ (L _ [L _ (AMatch _ pats val)]) _)})]) _)) (L _ expr) @@ -204,7 +210,7 @@ pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs pattern Lambda pats body <- HsLam _- (MG {mg_alts = L _ [L _ (AMatch _ pats body) ]})+ MG {mg_alts = L _ [L _ (AMatch _ pats body) ]} where -- If there are no patterns to bind, just stick in the body Lambda [] body = body@@ -232,7 +238,7 @@ unpackMatches :: PatCompattable p => [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)] unpackMatches [] = Just [] unpackMatches (SinglePatMatch pat body : matches) =- (:) <$> pure (pat, body) <*> unpackMatches matches+ ((pat, body):) <$> unpackMatches matches unpackMatches _ = Nothing @@ -241,14 +247,14 @@ pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p pattern Case scrutinee matches <- HsCase _ (L _ scrutinee)- (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})+ 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)})+ MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)} ------------------------------------------------------------------------------@@ -258,7 +264,11 @@ -- @Just False@ if it can't be homomorphic -- @Just True@ if it can lambdaCaseable :: Type -> Maybe Bool+#if __GLASGOW_HASKELL__ >= 900+lambdaCaseable (splitFunTy_maybe -> Just (_multiplicity, arg, res))+#else lambdaCaseable (splitFunTy_maybe -> Just (arg, res))+#endif | isJust (algebraicTyCon arg) = Just $ isJust $ algebraicTyCon res lambdaCaseable _ = Nothing@@ -350,12 +360,17 @@ -- | 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+ tryUnifyUnivarsButNotSkolemsMany skolems $ coerce [(goal, inst)]++------------------------------------------------------------------------------+-- | Like 'tryUnifyUnivarsButNotSkolems', but takes a list+-- of pairs of types to unify.+tryUnifyUnivarsButNotSkolemsMany :: Set TyVar -> [(Type, Type)] -> Maybe TCvSubst+tryUnifyUnivarsButNotSkolemsMany skolems (unzip -> (goal, inst)) =+ tcUnifyTys+ (bool BindMe Skolem . flip S.member skolems)+ inst+ goal updateSubst :: TCvSubst -> TacticState -> TacticState
src/Wingman/Judgements.hs view
@@ -66,7 +66,13 @@ withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t +------------------------------------------------------------------------------+-- | Like 'withNewGoal' but allows you to modify the goal rather than replacing+-- it.+withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a+withModifiedGoal f = field @"_jGoal" %~ f + ------------------------------------------------------------------------------ -- | Add some new type equalities to the local judgement. withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement@@ -140,7 +146,7 @@ -- otherwise nothing hasPositionalAncestry ancestors jdg name | not $ null ancestors- = case any (== name) ancestors of+ = case name `elem` ancestors of True -> Just True False -> case M.lookup name $ jAncestryMap jdg of@@ -162,8 +168,7 @@ disallowing reason (M.keysSet $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg where go name _- = not- . isJust+ = isNothing $ hasPositionalAncestry ancestry jdg name @@ -233,14 +238,12 @@ -- | Return the ancestry of a 'PatVal', or 'mempty' otherwise. getAncestry :: Judgement' a -> OccName -> Set OccName getAncestry jdg name =- case M.lookup name $ jPatHypothesis jdg of- Just pv -> pv_ancestry pv- Nothing -> mempty+ maybe mempty pv_ancestry . M.lookup name $ jPatHypothesis jdg jAncestryMap :: Judgement' a -> Map OccName (Set OccName) jAncestryMap jdg =- flip M.map (jPatHypothesis jdg) pv_ancestry+ M.map pv_ancestry (jPatHypothesis jdg) provAncestryOf :: Provenance -> Set OccName@@ -365,9 +368,7 @@ -- | Are there any top-level function argument bindings in this judgement? jHasBoundArgs :: Judgement' a -> Bool jHasBoundArgs- = not- . null- . filter (isTopLevel . hi_provenance)+ = any (isTopLevel . hi_provenance) . unHypothesis . jLocalHypothesis
src/Wingman/Judgements/SYB.hs view
@@ -87,12 +87,12 @@ metaprogramAtQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)] metaprogramAtQ ss = everythingContaining ss $ mkQ mempty $ \case- L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)+ L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS program) (_ :: LHsExpr GhcTc) -> mempty metaprogramQ :: GenericQ [(SrcSpan, T.Text)] metaprogramQ = everything (<>) $ mkQ mempty $ \case- L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)+ L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS program) (_ :: LHsExpr GhcTc) -> mempty
src/Wingman/Judgements/Theta.hs view
@@ -26,7 +26,11 @@ import Wingman.GHC import Wingman.Types +#if __GLASGOW_HASKELL__ >= 900+import GHC.Tc.Utils.TcType+#endif + ------------------------------------------------------------------------------ -- | Something we've learned about the type environment. data Evidence@@ -172,16 +176,32 @@ ------------------------------------------------------------------------------ -- | Extract evidence from 'AbsBinds' in scope. absBinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]+#if __GLASGOW_HASKELL__ >= 900+absBinds dst (L src (FunBind w _ _ _))+ | dst `isSubspanOf` src+ = wrapper w+absBinds dst (L src (AbsBinds _ _ h _ _ z _))+#else absBinds dst (L src (AbsBinds _ _ h _ _ _ _))- | dst `isSubspanOf` src = fmap idType h+#endif+ | dst `isSubspanOf` src+ = fmap idType h+#if __GLASGOW_HASKELL__ >= 900+ <> foldMap (absBinds dst) z+#endif absBinds _ _ = [] ------------------------------------------------------------------------------ -- | Extract evidence from 'HsWrapper's in scope wrapperBinds :: SrcSpan -> LHsExpr GhcTc -> [PredType]+#if __GLASGOW_HASKELL__ >= 900+wrapperBinds dst (L src (XExpr (WrapExpr (HsWrap h _))))+#else wrapperBinds dst (L src (HsWrap _ h _))- | dst `isSubspanOf` src = wrapper h+#endif+ | dst `isSubspanOf` src+ = wrapper h wrapperBinds _ _ = [] @@ -189,14 +209,19 @@ -- | Extract evidence from the 'ConPatOut's bound in this 'Match'. matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType] matchBinds dst (L src (Match _ _ pats _))- | dst `isSubspanOf` src = everything (<>) (mkQ mempty patBinds) pats+ | dst `isSubspanOf` src+ = everything (<>) (mkQ mempty patBinds) pats matchBinds _ _ = [] ------------------------------------------------------------------------------ -- | Extract evidence from a 'ConPatOut'. patBinds :: Pat GhcTc -> [PredType]+#if __GLASGOW_HASKELL__ >= 900+patBinds (ConPat{ pat_con_ext = ConPatTc { cpt_dicts = dicts }})+#else patBinds (ConPatOut { pat_dicts = dicts })+#endif = fmap idType dicts patBinds _ = []
src/Wingman/LanguageServer.hs view
@@ -1,7 +1,6 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE NoMonoLocalBinds #-}@@ -230,7 +229,7 @@ -- KnownThings is just the instances in scope. There are no ranges -- involved, so it's not crucial to track ages.- let henv = untrackedStaleValue $ hscenv+ let henv = untrackedStaleValue hscenv eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps@@ -279,7 +278,7 @@ evidence = getEvidenceAtHole (fmap (`RealSrcSpan` Nothing) tcg_rss) tcs cls_hy = foldMap evidenceToHypothesis evidence subst = ts_unifier $ evidenceToSubst evidence defaultTacticState- pure $+ pure ( disallowing AlreadyDestructed already_destructed $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement@@ -309,8 +308,8 @@ getSpanAndTypeAtHole :: Tracked age Range- -> Tracked age (HieASTs b)- -> Maybe (Tracked age RealSrcSpan, b)+ -> Tracked age (HieASTs Type)+ -> Maybe (Tracked age RealSrcSpan, Type) getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast -> case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range) ast of@@ -403,7 +402,11 @@ (RealDataCon $ tupleDataCon boxity $ length pats) tys $ zip [0.. ] pats- ConPatOut (L _ con) args _ _ _ f _ ->+#if __GLASGOW_HASKELL__ >= 900+ ConPat {pat_con = (L _ con), pat_con_ext = ConPatTc {cpt_arg_tys = args}, pat_args = f} ->+#else+ ConPatOut {pat_con = (L _ con), pat_arg_tys = args, pat_args = f} ->+#endif case f of PrefixCon l_pgt -> mkDerivedConHypothesis prov con args $ zip [0..] l_pgt@@ -564,7 +567,11 @@ L span (HsVar _ (L _ name)) | isHole (occName name) -> maybeToList $ srcSpanToRange span+#if __GLASGOW_HASKELL__ >= 900+ L span (HsUnboundVar _ occ)+#else L span (HsUnboundVar _ (TrueExprHole occ))+#endif | isHole occ -> maybeToList $ srcSpanToRange span #if __GLASGOW_HASKELL__ <= 808
src/Wingman/LanguageServer/Metaprogram.hs view
@@ -15,8 +15,7 @@ import Data.List (find) import Data.Maybe import qualified Data.Text as T-import Development.IDE (positionToRealSrcLoc)-import Development.IDE (realSrcSpanToRange)+import Development.IDE (positionToRealSrcLoc, realSrcSpanToRange) import Development.IDE.Core.Shake (IdeState (..)) import Development.IDE.Core.UseStale import Development.IDE.GHC.Compat hiding (empty)
src/Wingman/LanguageServer/TacticProviders.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wno-orphans #-} module Wingman.LanguageServer.TacticProviders@@ -139,8 +138,7 @@ withConfig $ \cfg -> filterTypeProjection ( guardLength (<= cfg_max_use_ctor_actions cfg)- . fromMaybe []- . fmap fst+ . maybe [] fst . tacticsGetDataCons ) $ \dcon -> provide UseDataCon@@ -162,10 +160,11 @@ requireGHC88OrHigher :: TacticProvider -> TacticProvider-requireGHC88OrHigher tp tpd = #if __GLASGOW_HASKELL__ >= 808+requireGHC88OrHigher tp tpd = tp tpd #else+requireGHC88OrHigher _ _= mempty #endif @@ -272,7 +271,7 @@ -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider provide tc name _ =- pure $ (Metadata (tacticTitle tc name) (mkTacticKind tc) (tacticPreferred tc), name)+ pure (Metadata (tacticTitle tc name) (mkTacticKind tc) (tacticPreferred tc), name) ------------------------------------------------------------------------------@@ -296,7 +295,7 @@ liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r liftLambdaCase nil f t = case tacticsSplitFunTy t of- (_, _, arg : _, res) -> f res arg+ (_, _, arg : _, res) -> f res $ scaledThing arg _ -> nil @@ -314,7 +313,7 @@ -- usual algebraic types, and when any of their data constructors are records. destructPunFilter :: Type -> Type -> Bool destructPunFilter _ (algebraicTyCon -> Just tc) =- any (not . null . dataConFieldLabels) $ tyConDataCons tc+ not . all (null . dataConFieldLabels) $ tyConDataCons tc destructPunFilter _ _ = False
src/Wingman/Machinery.hs view
@@ -1,6 +1,6 @@-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TupleSections #-} module Wingman.Machinery where @@ -18,7 +18,7 @@ import Data.Generics.Product (field') import Data.List (sortBy) import qualified Data.Map as M-import Data.Maybe (mapMaybe, isJust)+import Data.Maybe (mapMaybe, isNothing) import Data.Monoid (getSum) import Data.Ord (Down (..), comparing) import qualified Data.Set as S@@ -31,12 +31,20 @@ import Refinery.Tactic.Internal import System.Timeout (timeout) import Wingman.Context (getInstance)-import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars)+import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons, freshTyvars, tryUnifyUnivarsButNotSkolemsMany) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types +#if __GLASGOW_HASKELL__ < 900+import FunDeps (fd_eqs, improveFromInstEnv)+import Pair (unPair)+#else+import GHC.Tc.Instance.FunDeps (fd_eqs, improveFromInstEnv)+import GHC.Data.Pair (unPair)+#endif + substCTy :: TCvSubst -> CType -> CType substCTy subst = coerce . substTy subst . coerce @@ -69,14 +77,14 @@ tacticToRule :: Judgement -> TacticsM () -> Rule-tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom+tacticToRule jdg (TacticT tt) = RuleT $ execStateT tt jdg >>= flip Subgoal Axiom consumeChan :: OutChan (Maybe a) -> IO [a] consumeChan chan = do tryReadChan chan >>= tryRead >>= \case Nothing -> pure []- Just (Just a) -> (:) <$> pure a <*> consumeChan chan+ Just (Just a) -> (a:) <$> consumeChan chan Just Nothing -> pure [] @@ -107,7 +115,7 @@ (in_proofs, out_proofs) <- newChan (in_errs, out_errs) <- newChan timed_out <-- fmap (not. isJust) $ timeout duration $ consume stream $ \case+ fmap isNothing $ timeout duration $ consume stream $ \case Left err -> writeChan in_errs $ Just err Right proof -> writeChan in_proofs $ Just proof writeChan in_proofs Nothing@@ -246,6 +254,23 @@ modify $ updateSubst subst Nothing -> cut +------------------------------------------------------------------------------+-- | Get a substition out of a theta's fundeps+learnFromFundeps+ :: ThetaType+ -> RuleM ()+learnFromFundeps theta = do+ inst_envs <- asks ctxInstEnvs+ skolems <- gets ts_skolems+ subst <- gets ts_unifier+ let theta' = substTheta subst theta+ fundeps = foldMap (foldMap fd_eqs . improveFromInstEnv inst_envs (\_ _ -> ())) theta'+ case tryUnifyUnivarsButNotSkolemsMany skolems $ fmap unPair fundeps of+ Just subst ->+ modify $ updateSubst subst+ Nothing -> cut++ cut :: RuleT jdg ext err s m a cut = RuleT Empty @@ -342,7 +367,7 @@ getDefiningType :: TacticsM CType getDefiningType = do- calling_fun_name <- fst . head <$> asks ctxDefiningFuncs+ calling_fun_name <- asks (fst . head . ctxDefiningFuncs) maybe (failure $ NotInScope calling_fun_name) pure
src/Wingman/Metaprogramming/Lexer.hs view
@@ -1,7 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeApplications #-} module Wingman.Metaprogramming.Lexer where
src/Wingman/Metaprogramming/Parser.hs view
@@ -1,12 +1,12 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeApplications #-} module Wingman.Metaprogramming.Parser where import qualified Control.Monad.Combinators.Expr as P+import Data.Either (fromRight) import Data.Functor import Data.Maybe (listToMaybe) import qualified Data.Text as T@@ -98,6 +98,17 @@ "\\x y z -> (_ :: d)" ] + , command "idiom" Deterministic Tactic+ "Lift a tactic into idiom brackets."+ (pure . idiom)+ [ Example+ Nothing+ ["(apply f)"]+ [EHI "f" "a -> b -> Int"]+ (Just "Maybe Int")+ "f <$> (_ :: Maybe a) <*> (_ :: Maybe b)"+ ]+ , command "intro" Deterministic (Bind One) "Construct a lambda expression, binding an argument with the given name." (pure . intros' . IntroduceOnlyNamed . pure)@@ -415,7 +426,7 @@ tactic :: Parser (TacticsM ())-tactic = flip P.makeExprParser operators oneTactic+tactic = P.makeExprParser oneTactic operators operators :: [[P.Operator Parser (TacticsM ())]] operators =@@ -473,7 +484,7 @@ parseMetaprogram :: T.Text -> TacticsM () parseMetaprogram- = either (const $ pure ()) id+ = fromRight (pure ()) . P.runParser tacticProgram "<splice>"
src/Wingman/Metaprogramming/Parser/Documentation.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-deprecations #-} module Wingman.Metaprogramming.Parser.Documentation where
src/Wingman/Metaprogramming/ProofState.hs view
@@ -1,5 +1,7 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -Wno-deprecations #-} module Wingman.Metaprogramming.ProofState where
src/Wingman/Naming.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Wingman.Naming where import Control.Arrow@@ -18,7 +20,11 @@ import Text.Hyphenation (hyphenate, english_US) import Wingman.GHC (tcTyVar_maybe) +#if __GLASGOW_HASKELL__ >= 900+import GHC.Tc.Utils.TcType+#endif + ------------------------------------------------------------------------------ -- | A classification of a variable, for which we have specific naming rules. -- A variable can have multiple purposes simultaneously.@@ -38,11 +44,11 @@ pattern IsPredicate :: Type pattern IsPredicate <-- (tcSplitFunTys -> ([isFunTy -> False], isBoolTy -> True))+ (tcSplitFunTys -> ([isFunTy . scaledThing -> False], isBoolTy -> True)) pattern IsFunction :: [Type] -> Type -> Type pattern IsFunction args res <-- (tcSplitFunTys -> (args@(_:_), res))+ (first (map scaledThing) . tcSplitFunTys -> (args@(_:_), res)) pattern IsString :: Type pattern IsString <-@@ -156,8 +162,7 @@ = foldMap (fmap toLower . take 1) camels | otherwise = getStem- $ fmap toLower- $ name+ $ fmap toLower name where occ = getOccName tc name = occNameString occ
src/Wingman/Plugin.hs view
@@ -1,6 +1,3 @@-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RecordWildCards #-}- -- | A plugin that uses tactics to synthesize code module Wingman.Plugin where
src/Wingman/Range.hs view
@@ -19,6 +19,5 @@ rangeToRealSrcSpan :: String -> Range -> RealSrcSpan rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = mkRealSrcSpan- (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1))- (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1))-+ (mkRealSrcLoc (FS.fsLit file) (fromIntegral $ startLn + 1) (fromIntegral $ startCh + 1))+ (mkRealSrcLoc (FS.fsLit file) (fromIntegral $ endLn + 1) (fromIntegral $ endCh + 1))
src/Wingman/Simplify.hs view
@@ -19,11 +19,12 @@ pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs pattern Lambda pats body <- HsLam _- (MG {mg_alts = L _ [L _- (Match { m_pats = fmap fromPatCompat -> pats- , m_grhss = GRHSs {grhssGRHSs = [L _ (+ MG {mg_alts = L _ [L _+ Match { m_pats = fmap fromPatCompat -> pats+ , m_grhss = GRHSs {grhssGRHSs = [L _ ( GRHS _ [] (L _ body))]}- })]})+ }]+ } where -- If there are no patterns to bind, just stick in the body Lambda [] body = body@@ -35,9 +36,8 @@ -- | Simlify an expression. simplify :: LHsExpr GhcPs -> LHsExpr GhcPs simplify- = head- . drop 3 -- Do three passes; this should be good enough for the limited- -- amount of gas we give to auto+ = (!!3) -- Do three passes; this should be good enough for the limited+ -- amount of gas we give to auto . iterate (everywhere $ foldEndo [ simplifyEtaReduce , simplifyRemoveParens@@ -62,7 +62,7 @@ (HsVar _ (L _ a)) | pat == a -> var "id" Lambda- (unsnoc -> Just (pats, (VarPat _ (L _ pat))))+ (unsnoc -> Just (pats, VarPat _ (L _ pat))) (HsApp _ (L _ f) (L _ (HsVar _ (L _ a)))) | pat == a -- We can only perform this simplifiation if @pat@ is otherwise unused.@@ -84,8 +84,8 @@ simplifyCompose :: GenericT simplifyCompose = mkT $ \case Lambda- (unsnoc -> Just (pats, (VarPat _ (L _ pat))))- (unroll -> (fs@(_:_), (HsVar _ (L _ a))))+ (unsnoc -> Just (pats, VarPat _ (L _ pat)))+ (unroll -> (fs@(_:_), HsVar _ (L _ a))) | pat == a -- We can only perform this simplifiation if @pat@ is otherwise unused. , not (containsHsVar pat fs) ->
src/Wingman/StaticPlugin.hs view
@@ -3,17 +3,26 @@ module Wingman.StaticPlugin ( staticPlugin , metaprogramHoleName+ , enableQuasiQuotes , pattern WingmanMetaprogram , pattern MetaprogramSyntax ) where -import Data.Data import Development.IDE.GHC.Compat import Development.IDE.GHC.Compat.Util import GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes))-import Generics.SYB+ import Ide.Types++#if __GLASGOW_HASKELL__ >= 808+import Data.Data+import Generics.SYB+#if __GLASGOW_HASKELL__ >= 900+import GHC.Driver.Plugins (purePlugin)+#else import Plugins (purePlugin)+#endif+#endif staticPlugin :: DynFlagsModifications staticPlugin = mempty@@ -39,7 +48,6 @@ pattern MetaprogramSourceText = SourceText "wingman-meta-program" - pattern WingmanMetaprogram :: FastString -> HsExpr p pattern WingmanMetaprogram mp <- #if __GLASGOW_HASKELL__ >= 900@@ -51,7 +59,6 @@ #endif - enableQuasiQuotes :: DynFlags -> DynFlags enableQuasiQuotes = flip xopt_set QuasiQuotes @@ -75,12 +82,7 @@ } worker :: Monad m => [CommandLineOption] -> ModSummary -> HsParsedModule -> m HsParsedModule worker _ _ pm = pure $ pm { hpm_module = addMetaprogrammingSyntax $ hpm_module pm }-#endif -metaprogramHoleName :: OccName-metaprogramHoleName = mkVarOcc "_$metaprogram"-- mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs mkMetaprogram ss mp = #if __GLASGOW_HASKELL__ >= 900@@ -91,9 +93,7 @@ $ L ss $ HsVar noExtField $ L ss- $ mkRdrUnqual- $ metaprogramHoleName-+ $ mkRdrUnqual metaprogramHoleName addMetaprogrammingSyntax :: Data a => a -> a addMetaprogrammingSyntax =@@ -101,7 +101,10 @@ L ss (MetaprogramSyntax mp) -> L ss $ mkMetaprogram ss mp (x :: LHsExpr GhcPs) -> x+#endif +metaprogramHoleName :: OccName+metaprogramHoleName = mkVarOcc "_$metaprogram" pattern MetaprogramSyntax :: FastString -> HsExpr GhcPs pattern MetaprogramSyntax mp <-@@ -115,4 +118,3 @@ (mkRdrUnqual $ mkVarOcc "wingman") noSrcSpan mp-
src/Wingman/Tactics.hs view
@@ -8,11 +8,11 @@ import Control.Applicative (Alternative(empty), (<|>)) import Control.Lens ((&), (%~), (<>~))-import Control.Monad (filterM)-import Control.Monad (unless)+import Control.Monad (filterM, unless)+import Control.Monad (when) import Control.Monad.Extra (anyM) import Control.Monad.Reader.Class (MonadReader (ask))-import Control.Monad.State.Strict (StateT(..), runStateT)+import Control.Monad.State.Strict (StateT(..), runStateT, execStateT) import Data.Bool (bool) import Data.Foldable import Data.Functor ((<&>))@@ -24,7 +24,6 @@ import Data.Set (Set) import qualified Data.Set as S import Data.Traversable (for)-import DataCon import Development.IDE.GHC.Compat hiding (empty) import GHC.Exts import GHC.SourceGen ((@@))@@ -95,7 +94,7 @@ -- 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+ case any (flip M.member pat_vals) $ syn_used_vals ext of True -> Nothing False -> Just UnhelpfulRecursion @@ -132,7 +131,8 @@ let g = jGoal jdg case tacticsSplitFunTy $ unCType g of (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g- (_, _, args, res) -> do+ (_, _, scaledArgs, res) -> do+ let args = fmap scaledThing scaledArgs ctx <- ask let gen_names = mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args occs = case params of@@ -145,7 +145,7 @@ bound_occs = fmap fst bindings hy' = lambdaHypothesis top_hole bindings jdg' = introduce ctx hy'- $ withNewGoal (CType $ mkVisFunTys (drop num_occs args) res) jdg+ $ withNewGoal (CType $ mkVisFunTys (drop num_occs scaledArgs) res) jdg ext <- newSubgoal jdg' pure $ ext@@ -233,7 +233,7 @@ -- 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+ 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"@@ -243,7 +243,7 @@ $ destruct' False (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)- $ hi+ hi ------------------------------------------------------------------------------@@ -266,7 +266,7 @@ $ jGoal jdg -data Saturation = Unsaturated Int+newtype Saturation = Unsaturated Int deriving (Eq, Ord, Show) pattern Saturated :: Saturation@@ -280,17 +280,19 @@ ty = unCType $ hi_type hi func = hi_name hi ty' <- freshTyvars ty- let (_, _, all_args, ret) = tacticsSplitFunTy ty'+ let (_, theta, all_args, ret) = tacticsSplitFunTy ty' saturated_args = dropEnd n all_args unsaturated_args = takeEnd n all_args rule $ \jdg -> do unify g (CType $ mkVisFunTys unsaturated_args ret)+ learnFromFundeps theta ext <- fmap unzipTrace $ traverse ( newSubgoal . blacklistingDestruct . flip withNewGoal jdg . CType+ . scaledThing ) saturated_args pure $ ext@@ -443,7 +445,7 @@ attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()-attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames)+attemptOn getNames tac = matching (choice . fmap tac . getNames) localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a@@ -501,7 +503,7 @@ applyByName :: OccName -> TacticsM () applyByName name = do g <- goal- choice $ (unHypothesis (jHypothesis g)) <&> \hi ->+ choice $ unHypothesis (jHypothesis g) <&> \hi -> case hi_name hi == name of True -> apply Saturated hi False -> empty@@ -524,6 +526,7 @@ . blacklistingDestruct . flip withNewGoal jdg . CType+ . scaledThing ) args app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg pure $@@ -540,7 +543,7 @@ nary n = do a <- newUnivar b <- newUnivar- applyByType $ mkVisFunTys (replicate n a) b+ applyByType $ mkVisFunTys (replicate n $ unrestricted a) b self :: TacticsM ()@@ -558,7 +561,7 @@ cata hi = do (_, _, calling_args, _) <- tacticsSplitFunTy . unCType <$> getDefiningType- freshened_args <- traverse freshTyvars calling_args+ freshened_args <- traverse (freshTyvars . scaledThing) calling_args diff <- hyDiff $ destruct hi -- For for every destructed term, check to see if it can unify with any of@@ -582,8 +585,7 @@ $ \occ -> fmap (occ, ) $ fmap (<$ jdg)- $ fmap CType- $ newUnivar+ $ fmap CType newUnivar rule $ nonrecLet occ_tys @@ -625,7 +627,7 @@ let g = jGoal jdg fresh_ty <- newUnivar a <- newSubgoal $ withNewGoal (CType fresh_ty) jdg- f <- newSubgoal $ withNewGoal (coerce mkVisFunTys [fresh_ty] g) jdg+ f <- newSubgoal $ withNewGoal (coerce mkVisFunTys [unrestricted fresh_ty] g) jdg pure $ fmap noLoc $ (@@) <$> fmap unLoc f <*> fmap unLoc a @@ -639,4 +641,52 @@ m g' <- unHypothesis . jEntireHypothesis <$> goal pure $ Hypothesis $ take (length g' - g_len) g'+++------------------------------------------------------------------------------+-- | Attempt to run the given tactic in "idiom bracket" mode. For example, if+-- the current goal is+--+-- (_ :: [r])+--+-- then @idiom apply@ will remove the applicative context, resulting in a hole:+--+-- (_ :: r)+--+-- and then use @apply@ to solve it. Let's say this results in:+--+-- (f (_ :: a) (_ :: b))+--+-- Finally, @idiom@ lifts this back into the original applicative:+--+-- (f <$> (_ :: [a]) <*> (_ :: [b]))+--+-- Idiom will fail fast if the current goal doesn't have an applicative+-- instance.+idiom :: TacticsM () -> TacticsM ()+idiom m = do+ jdg <- goal+ let hole = unCType $ jGoal jdg+ when (isFunction hole) $+ failure $ GoalMismatch "idiom" $ jGoal jdg+ case splitAppTy_maybe hole of+ Just (applic, ty) -> do+ minst <- getKnownInstance (mkClsOcc "Applicative")+ . pure+ $ applic+ case minst of+ Nothing -> failure $ GoalMismatch "idiom" $ CType applic+ Just (_, _) -> do+ rule $ \jdg -> do+ expr <- subgoalWith (withNewGoal (CType ty) jdg) m+ case unLoc $ syn_val expr of+ HsApp{} -> pure $ fmap idiomize expr+ RecordCon{} -> pure $ fmap idiomize expr+ _ -> unsolvable $ GoalMismatch "idiom" $ jGoal jdg+ rule $ newSubgoal . withModifiedGoal (CType . mkAppTy applic . unCType)+ Nothing ->+ failure $ GoalMismatch "idiom" $ jGoal jdg++subgoalWith :: Judgement -> TacticsM () -> RuleM (Synthesized (LHsExpr GhcPs))+subgoalWith jdg t = RuleT $ flip execStateT jdg $ unTacticT t
src/Wingman/Types.hs view
@@ -38,7 +38,6 @@ import GHC.Generics import GHC.SourceGen (var) import Refinery.ProofState-import Refinery.Tactic import Refinery.Tactic.Internal (TacticT(TacticT), RuleT (RuleT)) import System.IO.Unsafe (unsafePerformIO) import Wingman.Debug@@ -333,12 +332,12 @@ instance MonadReader r m => MonadReader r (TacticT jdg ext err s m) where- ask = TacticT $ lift $ Effect $ fmap pure ask+ ask = TacticT $ lift $ Effect $ asks pure 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+ ask = RuleT $ Effect $ asks Axiom local f (RuleT m) = RuleT $ Effect $ local f $ pure m mkMetaHoleName :: Int -> RdrName@@ -463,7 +462,7 @@ } instance Show Context where- show (Context {..}) = mconcat+ show Context{..} = mconcat [ "Context " , showsPrec 10 ctxDefiningFuncs "" , showsPrec 10 ctxModuleFuncs ""
test/AutoTupleSpec.hs view
@@ -7,11 +7,10 @@ import Control.Monad (replicateM) import Control.Monad.State (evalState) import Data.Either (isRight)-import OccName (mkVarOcc)+import Development.IDE.GHC.Compat.Core ( mkVarOcc, mkBoxedTupleTy ) import System.IO.Unsafe import Test.Hspec import Test.QuickCheck-import TysWiredIn (mkBoxedTupleTy) import Wingman.Judgements (mkFirstJudgement) import Wingman.Machinery import Wingman.Tactics (auto')
test/CodeAction/AutoSpec.hs view
@@ -59,7 +59,7 @@ describe "theta" $ do autoTest 12 10 "AutoThetaFix"- autoTest 7 20 "AutoThetaRankN"+ autoTest 7 27 "AutoThetaRankN" autoTest 6 10 "AutoThetaGADT" autoTest 6 8 "AutoThetaGADTDestruct" autoTest 4 8 "AutoThetaEqCtx"
test/CodeAction/RunMetaprogramSpec.hs view
@@ -40,6 +40,10 @@ metaTest 7 53 "MetaDeepOf" metaTest 2 34 "MetaWithArg" metaTest 2 18 "MetaLetSimple"+ metaTest 5 9 "MetaIdiom"+ metaTest 7 9 "MetaIdiomRecord"++ metaTest 14 10 "MetaFundeps" metaTest 2 12 "IntrosTooMany"
test/ProviderSpec.hs view
@@ -20,3 +20,9 @@ "T2" 8 8 [ (not, Intros, "") ]++ goldenTestMany "SubsequentTactics"+ [ InvokeTactic Intros "" 4 5+ , InvokeTactic Destruct "du" 4 8+ , InvokeTactic Auto "" 4 15+ ]
test/UnificationSpec.hs view
@@ -1,4 +1,6 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE ViewPatterns #-}+ {-# OPTIONS_GHC -fno-warn-orphans #-} module UnificationSpec where@@ -12,13 +14,18 @@ import qualified Data.Set as S import Data.Traversable import Data.Tuple (swap)-import TcType (substTy, tcGetTyVar_maybe)+import Development.IDE.GHC.Compat.Core (substTy, mkBoxedTupleTy) import Test.Hspec import Test.QuickCheck-import TysWiredIn (mkBoxedTupleTy) import Wingman.GHC import Wingman.Machinery (newUnivar) import Wingman.Types++#if __GLASGOW_HASKELL__ >= 900+import GHC.Tc.Utils.TcType (tcGetTyVar_maybe)+#else+import TcType (tcGetTyVar_maybe)+#endif spec :: Spec
test/Utils.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE RecordWildCards #-} module Utils where @@ -23,6 +24,7 @@ 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)+import qualified Language.LSP.Types.Lens as J import System.Directory (doesFileExist) import System.FilePath import Test.Hls@@ -42,8 +44,8 @@ -- NB: These coordinates are in "file space", ie, 1-indexed. pointRange :: Int -> Int -> Range pointRange- (subtract 1 -> line)- (subtract 1 -> col) =+ (subtract 1 -> fromIntegral -> line)+ (subtract 1 -> fromIntegral -> col) = Range (Position line col) (Position line $ col + 1) @@ -63,7 +65,7 @@ runSessionWithServer' [plugin] def- (def { messageTimeout = 5 } )+ (def { messageTimeout = 20 } ) fullCaps tacticPath @@ -96,40 +98,47 @@ liftIO $ (title `elem` titles) `shouldSatisfy` f +data InvokeTactic = InvokeTactic+ { it_command :: TacticCommand+ , it_argument :: Text+ , it_line :: Int+ , it_col :: Int+ } +invokeTactic :: TextDocumentIdentifier -> InvokeTactic -> Session ()+invokeTactic doc InvokeTactic{..} = do+ -- wait for the entire build to finish, so that Tactics code actions that+ -- use stale data will get uptodate stuff+ void waitForDiagnostics+ void $ waitForTypecheck doc+ actions <- getCodeActions doc $ pointRange it_line it_col+ case find ((== Just (tacticTitle it_command it_argument)) . codeActionTitle) actions of+ Just (InR CodeAction {_command = Just c}) -> do+ executeCommand c+ void $ skipManyTill anyMessage $ message SWorkspaceApplyEdit+ _ -> error $ show actions + mkGoldenTest :: (Text -> Text -> Assertion)- -> TacticCommand- -> Text- -> Int- -> Int+ -> [InvokeTactic] -> FilePath -> SpecWith ()-mkGoldenTest eq tc occ line col input =+mkGoldenTest eq invocations input = it (input <> " (golden)") $ do resetGlobalHoleRef runSessionForTactics $ do doc <- openDoc (input <.> "hs") "haskell"- -- wait for diagnostics to start coming- void waitForDiagnostics- -- wait for the entire build to finish, so that Tactics code actions that- -- use stale data will get uptodate stuff- void $ waitForTypecheck doc- actions <- getCodeActions doc $ pointRange line col- case find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions of- Just (InR CodeAction {_command = Just c}) -> do- executeCommand c- _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit)- edited <- documentContents doc- let expected_name = input <.> "expected" <.> "hs"- -- Write golden tests if they don't already exist- liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do- T.writeFile expected_name edited- expected <- liftIO $ T.readFile expected_name- liftIO $ edited `eq` expected- _ -> error $ show actions+ traverse_ (invokeTactic doc) invocations+ edited <- documentContents doc+ let expected_name = input <.> "expected" <.> "hs"+ -- Write golden tests if they don't already exist+ liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do+ T.writeFile expected_name edited+ expected <- liftIO $ T.readFile expected_name+ liftIO $ edited `eq` expected + mkCodeLensTest :: FilePath -> SpecWith ()@@ -197,10 +206,13 @@ goldenTest :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()-goldenTest = mkGoldenTest shouldBe+goldenTest tc occ line col = mkGoldenTest shouldBe [InvokeTactic tc occ line col] +goldenTestMany :: FilePath -> [InvokeTactic] -> SpecWith ()+goldenTestMany = flip $ mkGoldenTest shouldBe+ goldenTestNoWhitespace :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()-goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces+goldenTestNoWhitespace tc occ line col = mkGoldenTest shouldBeIgnoringSpaces [InvokeTactic tc occ line col] shouldBeIgnoringSpaces :: Text -> Text -> Assertion
test/golden/AutoThetaRankN.expected.hs view
@@ -4,5 +4,5 @@ showMe f = f showedYou :: Int -> String-showedYou = showMe show+showedYou = showMe (\x -> show x)
test/golden/AutoThetaRankN.hs view
@@ -4,5 +4,5 @@ showMe f = f showedYou :: Int -> String-showedYou = showMe _+showedYou = showMe (\x -> _)
+ test/golden/MetaFundeps.expected.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}++class Blah a b | a -> b, b -> a+instance Blah Int Bool++foo :: Int+foo = 10++bar :: Blah a b => a -> b+bar = undefined++qux :: Bool+qux = bar foo++
+ test/golden/MetaFundeps.hs view
@@ -0,0 +1,16 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}++class Blah a b | a -> b, b -> a+instance Blah Int Bool++foo :: Int+foo = 10++bar :: Blah a b => a -> b+bar = undefined++qux :: Bool+qux = [wingman| use bar, use foo |]++
+ test/golden/MetaIdiom.expected.hs view
@@ -0,0 +1,6 @@+foo :: Int -> Int -> Int+foo = undefined++test :: Maybe Int+test = (foo <$> _w0) <*> _w1+
+ test/golden/MetaIdiom.hs view
@@ -0,0 +1,6 @@+foo :: Int -> Int -> Int+foo = undefined++test :: Maybe Int+test = [wingman| idiom (use foo) |]+
+ test/golden/MetaIdiomRecord.expected.hs view
@@ -0,0 +1,8 @@+data Rec = Rec+ { a :: Int+ , b :: Bool+ }++test :: Maybe Rec+test = (Rec <$> _w0) <*> _w1+
+ test/golden/MetaIdiomRecord.hs view
@@ -0,0 +1,8 @@+data Rec = Rec+ { a :: Int+ , b :: Bool+ }++test :: Maybe Rec+test = [wingman| idiom (ctor Rec) |]+
+ test/golden/SubsequentTactics.expected.hs view
@@ -0,0 +1,5 @@+data Dummy a = Dummy a++f :: Dummy Int -> Int+f (Dummy n) = n+
+ test/golden/SubsequentTactics.hs view
@@ -0,0 +1,5 @@+data Dummy a = Dummy a++f :: Dummy Int -> Int+f = _+