From 34cfa1df5f987eeae82bee39968bf3b0043d9964 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Thu, 24 Sep 2020 18:05:36 -0700 Subject: [PATCH 01/64] [WIP] Start work on 'auto' --- plugins/default/src/Ide/Plugin/Tactic.hs | 2 +- .../src/Ide/Plugin/Tactic/Machinery.hs | 42 +++++++++---- .../default/src/Ide/Plugin/Tactic/Tactics.hs | 60 +++++++++++++++---- stack.yaml | 4 +- 4 files changed, 86 insertions(+), 22 deletions(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index 6629a29471..d42171dbe4 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -63,7 +63,7 @@ tacticDesc name = "fill the hole using the " <> name <> " tactic" ------------------------------------------------------------------------------ enabledTactics :: [TacticCommand] -enabledTactics = [Intros, Destruct, Homomorphism] +enabledTactics = [Intros, Destruct, Homomorphism, Auto] ------------------------------------------------------------------------------ -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs index 51ef83e6cd..c2f2ce0a02 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -9,9 +9,12 @@ module Ide.Plugin.Tactic.Machinery where +import Control.Monad.Except (throwError) import Control.Monad.State (get, modify, evalStateT) import Data.Char +import Data.Either import Data.Function +import Data.Functor.Identity import Data.List import Data.Map (Map) import qualified Data.Map as M @@ -30,6 +33,7 @@ import Refinery.Tactic import TcType import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) +import Unify import Data.Maybe import SrcLoc @@ -87,7 +91,9 @@ data TacticError = UndefinedHypothesis OccName | GoalMismatch String CType | UnsolvedSubgoals [Judgement] + | UnificationError CType CType | NoProgress + | NoApplicableTactic instance Show TacticError where show (UndefinedHypothesis name) = @@ -101,14 +107,22 @@ instance Show TacticError where ] 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" - -type ProvableM = ProvableT Judgement (Either TacticError) -type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM -type RuleM = RuleT Judgement (LHsExpr GhcPs) ProvableM -type Rule = RuleM (LHsExpr GhcPs) +type ProvableM = ProvableT Judgement Identity +type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError ProvableM +type Rule = RuleM (LHsExpr GhcPs) ------------------------------------------------------------------------------ @@ -215,11 +229,12 @@ mkTyConName tc runTactic :: Judgement -> TacticsM () -- ^ Tactic to use - -> Either TacticError (LHsExpr GhcPs) -runTactic jdg t - = fmap (fst) - . runProvableT - $ runTacticT t jdg + -> Either [TacticError] (LHsExpr GhcPs) +runTactic jdg t = case partitionEithers $ runProvable $ runTacticT t jdg of + (errs, []) -> Left $ errs + (_, solns) -> + let soln = listToMaybe $ filter (null . snd) solns + in Right $ fst $ fromMaybe (head solns) soln ------------------------------------------------------------------------------ @@ -244,6 +259,13 @@ buildDataCon hy dc apps = do (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs +------------------------------------------------------------------------------ +-- | Attempt to unify two types. +unify :: CType -> CType -> RuleM TCvSubst +unify (CType t1) (CType t2) = case tcUnifyTy t1 t2 of + Just unifier -> pure unifier + Nothing -> throwError (UnificationError (CType t1) (CType t2)) + ------------------------------------------------------------------------------ -- | Convert a DAML compiler Range to a GHC SrcSpan diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs index a86e668568..256e9c1c12 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -9,8 +9,13 @@ module Ide.Plugin.Tactic.Tactics , runTactic ) where + +import Control.Applicative +import Control.Monad.State.Strict (StateT(..), runStateT) import Control.Monad.Except (throwError) +import Data.Function import Data.List +import Data.Maybe import qualified Data.Map as M import Data.Traversable import DataCon @@ -23,6 +28,7 @@ import GHC.SourceGen.Pat import Ide.Plugin.Tactic.Machinery import Name import Refinery.Tactic +import Refinery.Tactic.Internal import TcType import Type hiding (Var) @@ -116,10 +122,9 @@ homo = destruct' $ \dc (Judgement hy (CType g)) -> ------------------------------------------------------------------------------ -- | Ensure a tactic produces no subgoals. Useful when working with -- backtracking. -solve :: TacticsM () -> TacticsM () +solve :: TacticsM () -> TacticsM () solve t = t >> throwError NoProgress - ------------------------------------------------------------------------------ -- | Apply a function from the hypothesis. apply :: TacticsM () @@ -133,6 +138,20 @@ apply = rule $ \(Judgement hy g) -> do $ fmap unLoc sgs Nothing -> throwError $ GoalMismatch "apply" g +apply' :: OccName -> TacticsM () +apply' fname = rule $ \(Judgement hy g) -> + case M.lookup fname hy of + Just (CType fty) -> do + let (args, r) = splitFunTys fty + -- FIXME Need to use the unifier + subst <- unify g (CType r) + let hy' = fmap (CType . substTy subst . unCType) hy + sgs <- traverse (newSubgoal hy' . CType . substTy subst) args + pure . noLoc + . foldl' (@@) (var' fname) + $ fmap unLoc sgs + Nothing -> throwError $ GoalMismatch "apply'" g + ------------------------------------------------------------------------------ -- | Introduce a data constructor, splitting a goal into the datacon's @@ -155,26 +174,47 @@ deepen depth = do one deepen $ depth - 1 +------------------------------------------------------------------------------ +-- | @matching f@ takes a function from a judgement to a @Tactic@, and +-- then applies the resulting @Tactic@. +matching :: (Judgement -> TacticsM ()) -> TacticsM () +matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f $ s) s + +attemptOn :: (a -> TacticsM ()) -> (Judgement -> [a]) -> TacticsM () +attemptOn tac getNames = matching (choice . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------ -- | Automatically solve a goal. auto :: TacticsM () -auto = (intro >> auto) - (assumption >> auto) - (split >> auto) - (apply >> auto) - pure () - +auto = TacticT $ StateT $ \(Judgement _ goal) -> runStateT (unTacticT $ auto' 5) (Judgement M.empty goal) + -- auto' 5 + +auto' :: Int -> TacticsM () +auto' 0 = throwError NoProgress +auto' n = do + many_ intro + choice + [ split >> (auto' $ n - 1) + , attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames + , attemptOn (\aname -> progress ((==) `on` jGoal) NoProgress (destruct aname) >> (auto' $ n - 1)) algebraicNames + , assumption >> (auto' $ n - 1) + ] + where + functionNames :: Judgement -> [OccName] + functionNames (Judgement hys _) = M.keys $ M.filter (isFunction . unCType) hys + + algebraicNames :: Judgement -> [OccName] + algebraicNames (Judgement hys _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys ------------------------------------------------------------------------------ -- | Run a tactic, and subsequently apply auto if it completes. If not, just -- run the first tactic, leaving its subgoals as holes. autoIfPossible :: TacticsM () -> TacticsM () -autoIfPossible t = (t >> solve auto) t +autoIfPossible t = (t >> solve auto) <|> t ------------------------------------------------------------------------------ -- | Do one obvious thing. one :: TacticsM () -one = intro assumption split apply pure () +one = intro <|> assumption <|> split <|> apply <|> pure () diff --git a/stack.yaml b/stack.yaml index 48f52f1bcc..d6f7c1e3d0 100644 --- a/stack.yaml +++ b/stack.yaml @@ -45,7 +45,9 @@ extra-deps: - ormolu-0.1.2.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- refinery-0.1.0.0 +- github: totbwf/refinery + commit: 2eb856d1c582a7df7eb184f8cec1ca5e5aa4a82b + - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 From 005bf87b87514ae826ff6b85a2d26d34f9ba8f00 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 25 Sep 2020 12:55:33 -0700 Subject: [PATCH 02/64] Get current binding --- plugins/default/src/Ide/Plugin/Tactic.hs | 19 ++++++---- .../src/Ide/Plugin/Tactic/Machinery.hs | 38 +++++++++++++++++-- 2 files changed, 46 insertions(+), 11 deletions(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index d42171dbe4..bd9355fe5e 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -137,7 +137,7 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right $ List []) $ do - (_, span, jdg) <- MaybeT $ judgementForHole state nfp range + (_, _, span, jdg) <- MaybeT $ judgementForHole state nfp range actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider enabledTactics @@ -207,33 +207,33 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (Maybe (PositionMapping, Range, Judgement)) + -> IO (Maybe (PositionMapping, HieAST Type, Range, Judgement)) judgementForHole state nfp range = runMaybeT $ do (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp range' <- liftMaybe $ fromCurrentRange amapping range (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp - (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> + (ast, rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of Nothing -> Nothing Just ast' -> do let info = nodeInfo ast' ty <- listToMaybe $ nodeType info guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info - pure (nodeSpan ast', ty) + pure (ast, nodeSpan ast', ty) resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (amapping, resulting_range, Judgement hyps $ CType goal) + pure (amapping, ast, resulting_range, Judgement hyps $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do - (pos, _, jdg) <- MaybeT $ judgementForHole state nfp range + (pos, ast, _, jdg) <- MaybeT $ judgementForHole state nfp range -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp @@ -249,8 +249,11 @@ tacticCmd tac lf state (TacticParams uri range var_name) $ ResponseError InvalidRequest (T.pack $ show err) Nothing Right res -> do range' <- liftMaybe $ toCurrentRange pos range - let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' - g = graft span res + let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' + g = graft (RealSrcSpan span) res + -- TODO(sandy): unclear if this span is correct; might be + -- pointing to the wrong version + _this_name = currentBindingName ast span let response = transform dflags (clientCapabilities lf) uri g pm pure $ case response of Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs index c2f2ce0a02..0633eaf666 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -18,24 +18,26 @@ import Data.Functor.Identity import Data.List import Data.Map (Map) import qualified Data.Map as M +import Data.Maybe +import Data.Monoid +import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat +import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics import GHC.SourceGen.Overloaded -import Development.IDE.Spans.LocalBindings import Name import Outputable hiding ((<>)) import Refinery.Tactic +import SrcLoc import TcType import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unify -import Data.Maybe -import SrcLoc ------------------------------------------------------------------------------ @@ -284,3 +286,33 @@ rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh) unsafeRender :: Outputable a => a -> String unsafeRender = showSDoc unsafeGlobalDynFlags . ppr +currentBindingName :: HieAST a -> Span -> Maybe Name +currentBindingName ast s = firstContainingMap s isDefining ast + + +isDefining :: HieAST a -> Maybe Name +isDefining t = getFirst $ foldMap pure $ do + (Right name, details) <- M.toList . nodeIdentifiers $ nodeInfo t + ValBind _ ModuleScope _ <- S.toList $ identInfo details + pure name + +firstContainingMap + :: Span + -> (HieAST a -> Maybe b) + -> HieAST a + -> Maybe b +firstContainingMap sp cond node + | nodeSpan node `containsSpan` sp = firstMap cond node + | sp `containsSpan` nodeSpan node = Nothing + | otherwise = Nothing + +firstMap + :: (HieAST a -> Maybe b) + -> HieAST a + -> Maybe b +firstMap cond node = getFirst $ mconcat + [ First $ cond node + , foldMap (First . firstMap cond) $ + nodeChildren node + ] + From c2df687407c7656b037b7c486307c00959216866 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 25 Sep 2020 13:14:33 -0700 Subject: [PATCH 03/64] Fix currentBindingName for class methods --- plugins/default/src/Ide/Plugin/Tactic.hs | 2 +- plugins/default/src/Ide/Plugin/Tactic/Machinery.hs | 9 +++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index bd9355fe5e..9ffd93afb4 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -252,7 +252,7 @@ tacticCmd tac lf state (TacticParams uri range var_name) let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' g = graft (RealSrcSpan span) res -- TODO(sandy): unclear if this span is correct; might be - -- pointing to the wrong version + -- pointing to the wrong version of the file _this_name = currentBindingName ast span let response = transform dflags (clientCapabilities lf) uri g pm pure $ case response of diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs index 0633eaf666..953a477eb6 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -284,7 +284,10 @@ rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh) ------------------------------------------------------------------------------ -- | Print something unsafeRender :: Outputable a => a -> String -unsafeRender = showSDoc unsafeGlobalDynFlags . ppr +unsafeRender = unsafeRender' . ppr + +unsafeRender' :: SDoc -> String +unsafeRender' = showSDoc unsafeGlobalDynFlags currentBindingName :: HieAST a -> Span -> Maybe Name currentBindingName ast s = firstContainingMap s isDefining ast @@ -293,7 +296,9 @@ currentBindingName ast s = firstContainingMap s isDefining ast isDefining :: HieAST a -> Maybe Name isDefining t = getFirst $ foldMap pure $ do (Right name, details) <- M.toList . nodeIdentifiers $ nodeInfo t - ValBind _ ModuleScope _ <- S.toList $ identInfo details + -- Find anything in module scope that has a real source span; that is, only + -- things that actually appear in the source, and not default methods. + ValBind _ ModuleScope (Just _) <- S.toList $ identInfo details pure name firstContainingMap From 1d7a17e1152934d912d7dc916fbb6f54452d158f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 25 Sep 2020 14:07:59 -0700 Subject: [PATCH 04/64] Proper impl of getDefiningBindings --- haskell-language-server.cabal | 1 + plugins/default/src/Ide/Plugin/Tactic.hs | 19 +++++----- .../src/Ide/Plugin/Tactic/Machinery.hs | 35 +------------------ 3 files changed, 13 insertions(+), 42 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 46a48386ce..a618e63b63 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -149,6 +149,7 @@ executable haskell-language-server , ghc-source-gen , refinery , ghc-exactprint + , fingertree if flag(agpl) build-depends: brittany diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index 9ffd93afb4..3fcef7e709 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -19,8 +19,8 @@ import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce import qualified Data.Map as M -import qualified Data.Set as S import Data.Maybe +import qualified Data.Set as S import qualified Data.Text as T import Data.Traversable import Development.IDE.Core.PositionMapping @@ -31,9 +31,11 @@ import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (realSrcSpanToRange) import Development.IDE.GHC.Util (hscEnv) import Development.Shake (Action) +import qualified FastString import GHC.Generics (Generic) import HscTypes (hsc_dflags) import Ide.Plugin (mkLspCommand) +import Ide.Plugin.Tactic.BindSites import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Tactics import Ide.Plugin.Tactic.Types @@ -42,7 +44,6 @@ import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) import Language.Haskell.LSP.Types import OccName -import qualified FastString descriptor :: PluginId -> PluginDescriptor @@ -207,33 +208,35 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (Maybe (PositionMapping, HieAST Type, Range, Judgement)) + -> IO (Maybe (PositionMapping, BindSites, Range, Judgement)) judgementForHole state nfp range = runMaybeT $ do (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp range' <- liftMaybe $ fromCurrentRange amapping range (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp + (har, _) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp + let b2 = bindSites $ refMap har - (ast, rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> + (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of Nothing -> Nothing Just ast' -> do let info = nodeInfo ast' ty <- listToMaybe $ nodeType info guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info - pure (ast, nodeSpan ast', ty) + pure (nodeSpan ast', ty) resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (amapping, ast, resulting_range, Judgement hyps $ CType goal) + pure (amapping, b2, resulting_range, Judgement hyps $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do - (pos, ast, _, jdg) <- MaybeT $ judgementForHole state nfp range + (pos, b2, _, jdg) <- MaybeT $ judgementForHole state nfp range -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp @@ -253,7 +256,7 @@ tacticCmd tac lf state (TacticParams uri range var_name) g = graft (RealSrcSpan span) res -- TODO(sandy): unclear if this span is correct; might be -- pointing to the wrong version of the file - _this_name = currentBindingName ast span + _this_name = getDefiningBindings b2 span let response = transform dflags (clientCapabilities lf) uri g pm pure $ case response of Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs index 953a477eb6..09303de641 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} @@ -19,8 +20,6 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import Data.Monoid -import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat @@ -289,35 +288,3 @@ unsafeRender = unsafeRender' . ppr unsafeRender' :: SDoc -> String unsafeRender' = showSDoc unsafeGlobalDynFlags -currentBindingName :: HieAST a -> Span -> Maybe Name -currentBindingName ast s = firstContainingMap s isDefining ast - - -isDefining :: HieAST a -> Maybe Name -isDefining t = getFirst $ foldMap pure $ do - (Right name, details) <- M.toList . nodeIdentifiers $ nodeInfo t - -- Find anything in module scope that has a real source span; that is, only - -- things that actually appear in the source, and not default methods. - ValBind _ ModuleScope (Just _) <- S.toList $ identInfo details - pure name - -firstContainingMap - :: Span - -> (HieAST a -> Maybe b) - -> HieAST a - -> Maybe b -firstContainingMap sp cond node - | nodeSpan node `containsSpan` sp = firstMap cond node - | sp `containsSpan` nodeSpan node = Nothing - | otherwise = Nothing - -firstMap - :: (HieAST a -> Maybe b) - -> HieAST a - -> Maybe b -firstMap cond node = getFirst $ mconcat - [ First $ cond node - , foldMap (First . firstMap cond) $ - nodeChildren node - ] - From 18df4e687a4a9d0e88838f166f6a8026da381946 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 25 Sep 2020 15:37:06 -0700 Subject: [PATCH 05/64] Forgot to checkin bindsites --- .../src/Ide/Plugin/Tactic/BindSites.hs | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 plugins/default/src/Ide/Plugin/Tactic/BindSites.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/BindSites.hs b/plugins/default/src/Ide/Plugin/Tactic/BindSites.hs new file mode 100644 index 0000000000..568f1c2ede --- /dev/null +++ b/plugins/default/src/Ide/Plugin/Tactic/BindSites.hs @@ -0,0 +1,55 @@ +module Ide.Plugin.Tactic.BindSites + ( BindSites () + , bindSites + , getDefiningBindings + ) where + +import Data.IntervalMap.FingerTree (IntervalMap, Interval (..)) +import qualified Data.IntervalMap.FingerTree as IM +import qualified Data.Map as M +import qualified Data.Set as S +import Development.IDE.GHC.Compat +import Development.IDE.GHC.Error +import Development.IDE.Types.Location +import NameEnv +import SrcLoc + + +-- TODO(sandy): Consolidate this with LocalBindings +data BindSites = BindSites + { unBindSites :: IntervalMap Position (NameEnv (Name, Maybe Type)) + } + +------------------------------------------------------------------------------ +-- | Turn a 'RealSrcSpan' into an 'Interval'. +realSrcSpanToInterval :: RealSrcSpan -> Interval Position +realSrcSpanToInterval rss = + Interval + (realSrcLocToPosition $ realSrcSpanStart rss) + (realSrcLocToPosition $ realSrcSpanEnd rss) + +------------------------------------------------------------------------------ +-- | Compute which identifiers are in scope at every point in the AST. Use +-- 'getDefiningBindings' to find the results. +bindSites :: RefMap -> BindSites +bindSites refmap = BindSites $ foldr (uncurry IM.insert) mempty $ do + (ident, refs) <- M.toList refmap + Right name <- pure ident + (_, ident_details) <- refs + let ty = identType ident_details + info <- S.toList $ identInfo ident_details + Just scope <- pure $ getBindSiteFromContext info + pure ( realSrcSpanToInterval scope + , unitNameEnv name (name,ty) + ) + +------------------------------------------------------------------------------ +-- | Given a 'BindSites', get every binding currently active at a given +-- 'RealSrcSpan', +getDefiningBindings :: BindSites -> RealSrcSpan -> [(Name, Maybe Type)] +getDefiningBindings bs rss + = nameEnvElts + $ foldMap snd + $ IM.dominators (realSrcSpanToInterval rss) + $ unBindSites bs + From 646ff64a73ab7390de88fe7669cecb8e8c1e3eeb Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Fri, 25 Sep 2020 15:39:17 -0700 Subject: [PATCH 06/64] [WIP] Update version of refinery --- plugins/default/src/Ide/Plugin/Tactic/Tactics.hs | 4 ++-- stack.yaml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs index 256e9c1c12..b3a4effc12 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -194,9 +194,9 @@ auto' 0 = throwError NoProgress auto' n = do many_ intro choice - [ split >> (auto' $ n - 1) - , attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames + [ attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames , attemptOn (\aname -> progress ((==) `on` jGoal) NoProgress (destruct aname) >> (auto' $ n - 1)) algebraicNames + , split >> (auto' $ n - 1) , assumption >> (auto' $ n - 1) ] where diff --git a/stack.yaml b/stack.yaml index d6f7c1e3d0..58dd01134b 100644 --- a/stack.yaml +++ b/stack.yaml @@ -46,7 +46,7 @@ extra-deps: - parser-combinators-1.2.1 - primitive-0.7.1.0 - github: totbwf/refinery - commit: 2eb856d1c582a7df7eb184f8cec1ca5e5aa4a82b + commit: 5709a3f10645dd49af20912aec5eb06e72990849 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 From 3dd9955cd099fb9d288fa1149d5133bce07877fc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 25 Sep 2020 16:18:39 -0700 Subject: [PATCH 07/64] Bind all tyvars if possible --- plugins/default/src/Ide/Plugin/Tactic/Tactics.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs index b3a4effc12..d4d1905ef7 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -192,7 +192,7 @@ auto = TacticT $ StateT $ \(Judgement _ goal) -> runStateT (unTacticT $ auto' 5) auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress auto' n = do - many_ intro + intros <|> many_ intro choice [ attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames , attemptOn (\aname -> progress ((==) `on` jGoal) NoProgress (destruct aname) >> (auto' $ n - 1)) algebraicNames From 73f1654f2e119e70313b7516cd29547e53e7ed3b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 26 Sep 2020 11:20:57 -0700 Subject: [PATCH 08/64] WIP: Instantiate polymorphic functions --- plugins/default/src/Ide/Plugin/Tactic/GHC.hs | 47 +++++++++++++++++++ .../default/src/Ide/Plugin/Tactic/Tactics.hs | 32 ++++++++++--- 2 files changed, 72 insertions(+), 7 deletions(-) create mode 100644 plugins/default/src/Ide/Plugin/Tactic/GHC.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/GHC.hs b/plugins/default/src/Ide/Plugin/Tactic/GHC.hs new file mode 100644 index 0000000000..104077e390 --- /dev/null +++ b/plugins/default/src/Ide/Plugin/Tactic/GHC.hs @@ -0,0 +1,47 @@ +module Ide.Plugin.Tactic.GHC where + +import TcType +import TyCoRep +import Var +import Unique + +tcTyVar_maybe :: Type -> Maybe Var +tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' +tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty -- look through casts, as + -- this is only used for + -- e.g., FlexibleContexts +tcTyVar_maybe (TyVarTy v) = Just v +tcTyVar_maybe _ = Nothing + + +oneWayUnify + :: [TyVar] -- ^ binders + -> Type -- ^ type to instiate + -> Type -- ^ at this type + -> Maybe TCvSubst +oneWayUnify binders toinst res = + case tcTyVar_maybe toinst of + Just var -> + case elem var binders of + True -> pure $ mkTvSubstPrs $ pure (var, res) + False -> Nothing + Nothing -> + case eqType toinst res of + True -> pure emptyTCvSubst + False -> Nothing + + +instantiateType :: Type -> Type +instantiateType t = do + let vs = tyCoVarsOfTypeList t + vs' = fmap cloneTyVar vs + subst = foldr (\(v,t) a -> extendTCvSubst a v t) emptyTCvSubst $ zip vs vs' + in substTy subst t + + +cloneTyVar :: TyVar -> Type +cloneTyVar t = + let uniq = getUnique t + some_magic_number = 49 + in TyVarTy $ setVarUnique t (deriveUnique uniq some_magic_number) + diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs index d4d1905ef7..7f7407d646 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -26,6 +26,7 @@ import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.GHC import Name import Refinery.Tactic import Refinery.Tactic.Internal @@ -128,14 +129,9 @@ solve t = t >> throwError NoProgress ------------------------------------------------------------------------------ -- | Apply a function from the hypothesis. apply :: TacticsM () -apply = rule $ \(Judgement hy g) -> do +apply = rule $ \jdg@(Judgement hy g) -> do case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of - Just (func, CType ty) -> do - let (args, _) = splitFunTys ty - sgs <- traverse (newSubgoal hy . CType) args - pure . noLoc - . foldl' (@@) (var' func) - $ fmap unLoc sgs + Just (func, ty) -> applySpecific func ty jdg Nothing -> throwError $ GoalMismatch "apply" g apply' :: OccName -> TacticsM () @@ -153,6 +149,28 @@ apply' fname = rule $ \(Judgement hy g) -> Nothing -> throwError $ GoalMismatch "apply'" g +applySpecific :: OccName -> CType -> Judgement -> RuleM (LHsExpr GhcPs) +applySpecific func (CType ty) (Judgement hy _) = do + let (args, _) = splitFunTys ty + sgs <- traverse (newSubgoal hy . CType) args + pure . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs + + +instantiate :: OccName -> Type -> TacticsM () +instantiate func ty = rule $ \jdg@(Judgement _ (CType g)) -> do + -- TODO(sandy): We need to get available from the type sig and compare + -- against _ctx + let (binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty + case oneWayUnify binders res g of + Just subst -> + -- TODO(sandy): How does this affect the judgment wrt our new ununified + -- tyvars? + applySpecific func (CType $ instantiateType $ substTy subst ty) jdg + Nothing -> throwError $ GoalMismatch "instantiate" $ CType g + + ------------------------------------------------------------------------------ -- | Introduce a data constructor, splitting a goal into the datacon's -- constituent sub-goals. From 46df1a4471d7e5f0e00f45712c32ebf74c3210a8 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 26 Sep 2020 12:23:06 -0700 Subject: [PATCH 09/64] Split out fresh type variables when instantiating --- plugins/default/src/Ide/Plugin/Tactic/GHC.hs | 11 ++++++----- plugins/default/src/Ide/Plugin/Tactic/Tactics.hs | 3 ++- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic/GHC.hs b/plugins/default/src/Ide/Plugin/Tactic/GHC.hs index 104077e390..337c3b6ab9 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/GHC.hs @@ -31,17 +31,18 @@ oneWayUnify binders toinst res = False -> Nothing -instantiateType :: Type -> Type +instantiateType :: Type -> ([TyVar], Type) instantiateType t = do let vs = tyCoVarsOfTypeList t vs' = fmap cloneTyVar vs - subst = foldr (\(v,t) a -> extendTCvSubst a v t) emptyTCvSubst $ zip vs vs' - in substTy subst t + subst = foldr (\(v,t) a -> extendTCvSubst a v $ TyVarTy t) emptyTCvSubst + $ zip vs vs' + in (vs', substTy subst t) -cloneTyVar :: TyVar -> Type +cloneTyVar :: TyVar -> TyVar cloneTyVar t = let uniq = getUnique t some_magic_number = 49 - in TyVarTy $ setVarUnique t (deriveUnique uniq some_magic_number) + in setVarUnique t $ deriveUnique uniq some_magic_number diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs index 7f7407d646..bd1910e6f7 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -167,7 +167,8 @@ instantiate func ty = rule $ \jdg@(Judgement _ (CType g)) -> do Just subst -> -- TODO(sandy): How does this affect the judgment wrt our new ununified -- tyvars? - applySpecific func (CType $ instantiateType $ substTy subst ty) jdg + let (_fresh_vars, ty') = instantiateType $ substTy subst ty + in applySpecific func (CType ty') jdg Nothing -> throwError $ GoalMismatch "instantiate" $ CType g From 916360591511c2369f80cee0354df85b7ea97feb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 27 Sep 2020 00:27:40 -0700 Subject: [PATCH 10/64] Make everything compile --- haskell-language-server.cabal | 2 ++ plugins/default/src/Ide/Plugin/Tactic/Machinery.hs | 6 +++--- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index a618e63b63..ecb043b07e 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -96,6 +96,8 @@ executable haskell-language-server Ide.Plugin.Tactic.Types Ide.Plugin.Tactic.Machinery Ide.Plugin.Tactic.Tactics + Ide.Plugin.Tactic.BindSites + Ide.Plugin.Tactic.GHC Ide.TreeTransform ghc-options: diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs index 09303de641..25b827f090 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -121,8 +121,8 @@ instance Show TacticError where "No tactic could be applied" type ProvableM = ProvableT Judgement Identity -type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError ProvableM -type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError ProvableM +type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError () ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError () ProvableM type Rule = RuleM (LHsExpr GhcPs) @@ -231,7 +231,7 @@ runTactic :: Judgement -> TacticsM () -- ^ Tactic to use -> Either [TacticError] (LHsExpr GhcPs) -runTactic jdg t = case partitionEithers $ runProvable $ runTacticT t jdg of +runTactic jdg t = case partitionEithers $ runProvable $ runTacticT t jdg () of (errs, []) -> Left $ errs (_, solns) -> let soln = listToMaybe $ filter (null . snd) solns From 16932da3c9c9b8e9fef07654bf18f9c4ae6d0ce2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 27 Sep 2020 18:29:00 -0700 Subject: [PATCH 11/64] Separate out tactics --- haskell-language-server.cabal | 48 +++++++++++++++---- .../src/Ide/Plugin/Tactic.hs | 0 .../src/Ide/Plugin/Tactic/BindSites.hs | 0 .../src/Ide/Plugin/Tactic/GHC.hs | 0 .../src/Ide/Plugin/Tactic/Machinery.hs | 0 .../src/Ide/Plugin/Tactic/Tactics.hs | 0 .../src/Ide/Plugin/Tactic/Types.hs | 0 .../src/Ide/TreeTransform.hs | 1 - 8 files changed, 40 insertions(+), 9 deletions(-) rename plugins/{default => tactics}/src/Ide/Plugin/Tactic.hs (100%) rename plugins/{default => tactics}/src/Ide/Plugin/Tactic/BindSites.hs (100%) rename plugins/{default => tactics}/src/Ide/Plugin/Tactic/GHC.hs (100%) rename plugins/{default => tactics}/src/Ide/Plugin/Tactic/Machinery.hs (100%) rename plugins/{default => tactics}/src/Ide/Plugin/Tactic/Tactics.hs (100%) rename plugins/{default => tactics}/src/Ide/Plugin/Tactic/Types.hs (100%) rename plugins/{default => tactics}/src/Ide/TreeTransform.hs (99%) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index ecb043b07e..81095dfc73 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -77,6 +77,43 @@ library default-language: Haskell2010 +library hls-tactics + import: agpl, common-deps + hs-source-dirs: plugins/tactics/src + exposed-modules: + Ide.Plugin.Tactic + Ide.Plugin.Tactic.Types + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Tactics + Ide.Plugin.Tactic.BindSites + Ide.Plugin.Tactic.GHC + Ide.TreeTransform + + ghc-options: + -Wall -Wno-name-shadowing -Wredundant-constraints + if flag(pedantic) + ghc-options: -Werror + + build-depends: + , aeson + , containers + , fingertree + , ghc + , ghc-exactprint + , ghc-source-gen + , ghcide >=0.1 + , haskell-lsp ^>=0.22 + , hls-plugin-api + , mtl + , refinery + , retrie >=0.1.1.0 + , shake + , syb + , text + , transformers + + default-language: Haskell2010 + executable haskell-language-server import: agpl, common-deps main-is: Main.hs @@ -92,13 +129,6 @@ executable haskell-language-server Ide.Plugin.Pragmas Ide.Plugin.Retrie Ide.Plugin.StylishHaskell - Ide.Plugin.Tactic - Ide.Plugin.Tactic.Types - Ide.Plugin.Tactic.Machinery - Ide.Plugin.Tactic.Tactics - Ide.Plugin.Tactic.BindSites - Ide.Plugin.Tactic.GHC - Ide.TreeTransform ghc-options: -threaded -Wall -Wno-name-shadowing -Wredundant-constraints @@ -131,6 +161,7 @@ executable haskell-language-server , regex-tdfa , retrie >=0.1.1.0 , hslogger + , hls-tactics , optparse-applicative , haskell-lsp ^>=0.22 , hls-plugin-api @@ -233,6 +264,7 @@ test-suite func-test build-depends: , bytestring , data-default + , hls-tactics , lens , tasty , tasty-ant-xml >=1.1.6 @@ -240,7 +272,7 @@ test-suite func-test , tasty-golden , tasty-rerun - hs-source-dirs: test/functional plugins/default/src + hs-source-dirs: test/functional main-is: Main.hs other-modules: Command diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs similarity index 100% rename from plugins/default/src/Ide/Plugin/Tactic.hs rename to plugins/tactics/src/Ide/Plugin/Tactic.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/BindSites.hs b/plugins/tactics/src/Ide/Plugin/Tactic/BindSites.hs similarity index 100% rename from plugins/default/src/Ide/Plugin/Tactic/BindSites.hs rename to plugins/tactics/src/Ide/Plugin/Tactic/BindSites.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs similarity index 100% rename from plugins/default/src/Ide/Plugin/Tactic/GHC.hs rename to plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs similarity index 100% rename from plugins/default/src/Ide/Plugin/Tactic/Machinery.hs rename to plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs similarity index 100% rename from plugins/default/src/Ide/Plugin/Tactic/Tactics.hs rename to plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs similarity index 100% rename from plugins/default/src/Ide/Plugin/Tactic/Types.hs rename to plugins/tactics/src/Ide/Plugin/Tactic/Types.hs diff --git a/plugins/default/src/Ide/TreeTransform.hs b/plugins/tactics/src/Ide/TreeTransform.hs similarity index 99% rename from plugins/default/src/Ide/TreeTransform.hs rename to plugins/tactics/src/Ide/TreeTransform.hs index 996c552c43..012426de68 100644 --- a/plugins/default/src/Ide/TreeTransform.hs +++ b/plugins/tactics/src/Ide/TreeTransform.hs @@ -26,7 +26,6 @@ import Language.Haskell.LSP.Types import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) import Outputable import Retrie.ExactPrint hiding (parseExpr) -import Text.Regex.TDFA.Text() ------------------------------------------------------------------------------ From 262e8e1aed6bb8ad87d5ac10acd3289efde57b02 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 11:27:14 -0700 Subject: [PATCH 12/64] oneWayUnifyRule --- plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 25b827f090..278aef5bed 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -29,6 +29,7 @@ import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics import GHC.SourceGen.Overloaded +import Ide.Plugin.Tactic.GHC (oneWayUnify) import Name import Outputable hiding ((<>)) import Refinery.Tactic @@ -267,6 +268,16 @@ unify (CType t1) (CType t2) = case tcUnifyTy t1 t2 of Just unifier -> pure unifier Nothing -> throwError (UnificationError (CType t1) (CType t2)) +oneWayUnifyRule + :: [TyVar] -- ^ binders + -> CType -- ^ type to instiate + -> CType -- ^ at this type + -> RuleM TCvSubst +oneWayUnifyRule binders t1 t2 = + case oneWayUnify binders (unCType t1) (unCType t2) of + Just subst -> pure subst + Nothing -> throwError $ UnificationError t1 t2 + ------------------------------------------------------------------------------ -- | Convert a DAML compiler Range to a GHC SrcSpan From 607e1d635db3e75b5d130e243bb98de32afe1bee Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 28 Sep 2020 11:27:16 -0700 Subject: [PATCH 13/64] [WIP] Add 'TacticState' --- .../src/Ide/Plugin/Tactic/Machinery.hs | 31 +++++++++++++++---- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 21 +++---------- 2 files changed, 30 insertions(+), 22 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 25b827f090..80ecad720c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -11,7 +11,7 @@ module Ide.Plugin.Tactic.Machinery where import Control.Monad.Except (throwError) -import Control.Monad.State (get, modify, evalStateT) +import Control.Monad.State (gets, get, modify, evalStateT) import Data.Char import Data.Either import Data.Function @@ -25,6 +25,7 @@ import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location +import Ide.Plugin.Tactic.GHC import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics @@ -39,6 +40,17 @@ import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleT import Unify +data TacticState = TacticState + { ts_skolems :: [TyVar] + , ts_unifier :: TCvSubst + } + +initialTacticState :: TacticState +initialTacticState = TacticState + { ts_skolems = [] + , ts_unifier = emptyTCvSubst + } + ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. instance MonadExtract (LHsExpr GhcPs) ProvableM where @@ -55,6 +67,8 @@ instance Eq CType where instance Ord CType where compare = nonDetCmpType `on` unCType +substCTy :: TCvSubst -> CType -> CType +substCTy subst = CType . substTy subst . unCType ------------------------------------------------------------------------------ -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. @@ -86,6 +100,9 @@ data Judgement = Judgement deriving (Eq, Ord, Generic) +substJdg :: TCvSubst -> Judgement -> Judgement +substJdg subst (Judgement hys goal) = Judgement (fmap (substCTy subst) hys) (substCTy subst goal) + ------------------------------------------------------------------------------ -- | Reasons a tactic might fail. data TacticError @@ -121,8 +138,8 @@ instance Show TacticError where "No tactic could be applied" type ProvableM = ProvableT Judgement Identity -type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError () ProvableM -type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError () ProvableM +type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM type Rule = RuleM (LHsExpr GhcPs) @@ -133,8 +150,10 @@ newSubgoal :: Map OccName CType -- ^ Available bindings -> CType -- ^ Sub-goal type -> RuleM (LHsExpr GhcPs) -newSubgoal hy g = subgoal =<< newJudgement hy g - +newSubgoal hy g = do + j <- newJudgement hy g + unifier <- gets ts_unifier + subgoal $ substJdg unifier j ------------------------------------------------------------------------------ -- | Create a new judgment @@ -231,7 +250,7 @@ runTactic :: Judgement -> TacticsM () -- ^ Tactic to use -> Either [TacticError] (LHsExpr GhcPs) -runTactic jdg t = case partitionEithers $ runProvable $ runTacticT t jdg () of +runTactic jdg t = case partitionEithers $ runProvable $ runTacticT t jdg initialTacticState of (errs, []) -> Left $ errs (_, solns) -> let soln = listToMaybe $ filter (null . snd) solns diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index bd1910e6f7..118b88a28a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -135,19 +135,9 @@ apply = rule $ \jdg@(Judgement hy g) -> do Nothing -> throwError $ GoalMismatch "apply" g apply' :: OccName -> TacticsM () -apply' fname = rule $ \(Judgement hy g) -> - case M.lookup fname hy of - Just (CType fty) -> do - let (args, r) = splitFunTys fty - -- FIXME Need to use the unifier - subst <- unify g (CType r) - let hy' = fmap (CType . substTy subst . unCType) hy - sgs <- traverse (newSubgoal hy' . CType . substTy subst) args - pure . noLoc - . foldl' (@@) (var' fname) - $ fmap unLoc sgs - Nothing -> throwError $ GoalMismatch "apply'" g - +apply' fname = do + (Judgement _ ty) <- goal + instantiate fname ty applySpecific :: OccName -> CType -> Judgement -> RuleM (LHsExpr GhcPs) applySpecific func (CType ty) (Judgement hy _) = do @@ -158,8 +148,8 @@ applySpecific func (CType ty) (Judgement hy _) = do $ fmap unLoc sgs -instantiate :: OccName -> Type -> TacticsM () -instantiate func ty = rule $ \jdg@(Judgement _ (CType g)) -> do +instantiate :: OccName -> CType -> TacticsM () +instantiate func (CType ty) = rule $ \jdg@(Judgement _ (CType g)) -> do -- TODO(sandy): We need to get available from the type sig and compare -- against _ctx let (binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty @@ -206,7 +196,6 @@ attemptOn tac getNames = matching (choice . fmap (\s -> tac s) . getNames) -- | Automatically solve a goal. auto :: TacticsM () auto = TacticT $ StateT $ \(Judgement _ goal) -> runStateT (unTacticT $ auto' 5) (Judgement M.empty goal) - -- auto' 5 auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress From 2fc23ee1d93e6c56686bfa29325f5ed49bf44c82 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 28 Sep 2020 11:57:43 -0700 Subject: [PATCH 14/64] [WIP] Tweak 'unify' and 'unifyOneWayRule' --- .../src/Ide/Plugin/Tactic/Machinery.hs | 35 +++++++++++++++---- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 16 +++++---- 2 files changed, 38 insertions(+), 13 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index f8be70c6c0..bd9e474a13 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -280,21 +280,44 @@ buildDataCon hy dc apps = do (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs + +-- | We need to make sure that we don't try to unify any skolems. +-- To see why, consider the case: +-- +-- uhh :: (Int -> Int) -> a +-- uhh f = _ +-- +-- If we were to apply 'f', then we would try to unify 'Int' and 'a'. +-- This is fine from the perspective of 'tcUnifyTy', but will cause obvious +-- type errors in our use case. Therefore, we need to ensure that our +-- 'TCvSubst' doesn't try to unify skolems. +checkSkolemUnification :: CType -> CType -> TCvSubst -> RuleM () +checkSkolemUnification t1 t2 subst = do + skolems <- gets ts_skolems + case traverse (lookupTyVar subst) skolems of + Just _ -> throwError (UnificationError t1 t2) + Nothing -> pure () + ------------------------------------------------------------------------------ -- | Attempt to unify two types. -unify :: CType -> CType -> RuleM TCvSubst -unify (CType t1) (CType t2) = case tcUnifyTy t1 t2 of - Just unifier -> pure unifier - Nothing -> throwError (UnificationError (CType t1) (CType t2)) +unify :: CType -> CType -> RuleM () +unify t1 t2 = + case tcUnifyTy (unCType t1) (unCType t2) of + Just subst -> do + checkSkolemUnification t1 t2 subst + modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) }) + Nothing -> throwError (UnificationError t1 t2) oneWayUnifyRule :: [TyVar] -- ^ binders -> CType -- ^ type to instiate -> CType -- ^ at this type - -> RuleM TCvSubst + -> RuleM () oneWayUnifyRule binders t1 t2 = case oneWayUnify binders (unCType t1) (unCType t2) of - Just subst -> pure subst + Just subst -> do + checkSkolemUnification t1 t2 subst + modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) }) Nothing -> throwError $ UnificationError t1 t2 diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 118b88a28a..1593956391 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -153,13 +153,15 @@ instantiate func (CType ty) = rule $ \jdg@(Judgement _ (CType g)) -> do -- TODO(sandy): We need to get available from the type sig and compare -- against _ctx let (binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty - case oneWayUnify binders res g of - Just subst -> - -- TODO(sandy): How does this affect the judgment wrt our new ununified - -- tyvars? - let (_fresh_vars, ty') = instantiateType $ substTy subst ty - in applySpecific func (CType ty') jdg - Nothing -> throwError $ GoalMismatch "instantiate" $ CType g + oneWayUnifyRule binders (CType res) (CType g) + applySpecific func (CType ty) jdg + -- case oneWayUnify binders res g of + -- Just subst -> + -- -- TODO(sandy): How does this affect the judgment wrt our new ununified + -- -- tyvars? + -- let (_fresh_vars, ty') = instantiateType $ substTy subst ty + -- in applySpecific func (CType ty') jdg + -- Nothing -> throwError $ GoalMismatch "instantiate" $ CType g ------------------------------------------------------------------------------ From d03449d489dcd47abc64078af83a54005620fe90 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 28 Sep 2020 13:47:30 -0700 Subject: [PATCH 15/64] [WIP] Start work on skolem tracking --- .../src/Ide/Plugin/Tactic/Machinery.hs | 16 ++++++++++------ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 19 +++++++++++++------ 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index bd9e474a13..dc9115b5a0 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -25,7 +25,7 @@ import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location -import Ide.Plugin.Tactic.GHC + import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics @@ -251,11 +251,15 @@ runTactic :: Judgement -> TacticsM () -- ^ Tactic to use -> Either [TacticError] (LHsExpr GhcPs) -runTactic jdg t = case partitionEithers $ runProvable $ runTacticT t jdg initialTacticState of - (errs, []) -> Left $ errs - (_, solns) -> - let soln = listToMaybe $ filter (null . snd) solns - in Right $ fst $ fromMaybe (head solns) soln +runTactic jdg t = + -- FIXME [Reed] This code does not work + let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg + tacticState = initialTacticState { ts_skolems = skolems } + in case partitionEithers $ runProvable $ runTacticT t jdg tacticState of + (errs, []) -> Left $ errs + (_, solns) -> + let soln = listToMaybe $ filter (null . snd) solns + in Right $ fst $ fromMaybe (head solns) soln ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 1593956391..c7180b47d1 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -26,7 +26,7 @@ import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat import Ide.Plugin.Tactic.Machinery -import Ide.Plugin.Tactic.GHC + import Name import Refinery.Tactic import Refinery.Tactic.Internal @@ -135,9 +135,16 @@ apply = rule $ \jdg@(Judgement hy g) -> do Nothing -> throwError $ GoalMismatch "apply" g apply' :: OccName -> TacticsM () -apply' fname = do - (Judgement _ ty) <- goal - instantiate fname ty +apply' func = rule $ \(Judgement hys g) -> + case M.lookup func hys of + Just (CType ty) -> do + let (args, ret) = splitFunTys ty + unify g (CType ret) + sgs <- traverse (newSubgoal hys . CType) args + pure . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs + Nothing -> throwError $ GoalMismatch "apply" g applySpecific :: OccName -> CType -> Judgement -> RuleM (LHsExpr GhcPs) applySpecific func (CType ty) (Judgement hy _) = do @@ -152,8 +159,8 @@ instantiate :: OccName -> CType -> TacticsM () instantiate func (CType ty) = rule $ \jdg@(Judgement _ (CType g)) -> do -- TODO(sandy): We need to get available from the type sig and compare -- against _ctx - let (binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty - oneWayUnifyRule binders (CType res) (CType g) + let (_binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty + unify (CType res) (CType g) applySpecific func (CType ty) jdg -- case oneWayUnify binders res g of -- Just subst -> From ff36b39bbc03fda5fbaab4bf2134e8b033a1867c Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 28 Sep 2020 14:11:16 -0700 Subject: [PATCH 16/64] [WIP] Fix 'checkSkolemUnification' --- .../src/Ide/Plugin/Tactic/Machinery.hs | 31 ++++++------------- 1 file changed, 10 insertions(+), 21 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index dc9115b5a0..9c5e0c5b0c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -10,6 +10,7 @@ module Ide.Plugin.Tactic.Machinery where +import Control.Monad (unless) import Control.Monad.Except (throwError) import Control.Monad.State (gets, get, modify, evalStateT) import Data.Char @@ -40,7 +41,6 @@ import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unify - data TacticState = TacticState { ts_skolems :: [TyVar] , ts_unifier :: TCvSubst @@ -298,31 +298,20 @@ buildDataCon hy dc apps = do checkSkolemUnification :: CType -> CType -> TCvSubst -> RuleM () checkSkolemUnification t1 t2 subst = do skolems <- gets ts_skolems - case traverse (lookupTyVar subst) skolems of - Just _ -> throwError (UnificationError t1 t2) - Nothing -> pure () + unless (all (flip notElemTCvSubst subst) skolems) $ + throwError (UnificationError t1 t2) ------------------------------------------------------------------------------ -- | Attempt to unify two types. -unify :: CType -> CType -> RuleM () -unify t1 t2 = - case tcUnifyTy (unCType t1) (unCType t2) of +unify :: CType -- ^ The goal type + -> CType -- ^ The type we are trying unify the goal type with + -> RuleM () +unify goal inst = + case tcUnifyTy (unCType inst) (unCType goal) of Just subst -> do - checkSkolemUnification t1 t2 subst + checkSkolemUnification inst goal subst modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) }) - Nothing -> throwError (UnificationError t1 t2) - -oneWayUnifyRule - :: [TyVar] -- ^ binders - -> CType -- ^ type to instiate - -> CType -- ^ at this type - -> RuleM () -oneWayUnifyRule binders t1 t2 = - case oneWayUnify binders (unCType t1) (unCType t2) of - Just subst -> do - checkSkolemUnification t1 t2 subst - modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) }) - Nothing -> throwError $ UnificationError t1 t2 + Nothing -> throwError (UnificationError inst goal) ------------------------------------------------------------------------------ From 8709694a945a4cfff0c2a91f892f76fd567eee25 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 14:20:02 -0700 Subject: [PATCH 17/64] Update judgement type --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 6 ++--- .../src/Ide/Plugin/Tactic/Machinery.hs | 26 ++++++++++++++----- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 26 +++++++++---------- 3 files changed, 36 insertions(+), 22 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 3fcef7e709..20e8059b06 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -173,7 +173,7 @@ provide tc name plId uri range _ = do -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider -filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) = +filterGoalType p tp plId uri range jdg@(Judgement _ _ (CType g)) = case p g of True -> tp plId uri range jdg False -> pure [] @@ -186,7 +186,7 @@ filterBindingType :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider -filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = +filterBindingType p tp plId uri range jdg@(Judgement hys _ (CType g)) = fmap join $ for (M.toList hys) $ \(occ, CType ty) -> case p g ty of True -> tp occ ty plId uri range jdg @@ -229,7 +229,7 @@ judgementForHole state nfp range = runMaybeT $ do resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (amapping, b2, resulting_range, Judgement hyps $ CType goal) + pure (amapping, b2, resulting_range, Judgement hyps mempty $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index dc9115b5a0..8d5fbf6141 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -20,11 +22,14 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe +import Data.Set (Set) +import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location +import GHC.Generics import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS @@ -94,15 +99,24 @@ buildHypothesis ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. -data Judgement = Judgement - { jHypothesis :: Map OccName CType - , jGoal :: CType +data Judgement' a = Judgement + { _jHypothesis :: Map OccName a + , _jDestructed :: Set OccName + , _jGoal :: a } - deriving (Eq, Ord, Generic) + deriving stock (Eq, Ord, Generic, Functor) + +jHypothesis :: Judgement' a -> Map OccName a +jHypothesis = _jHypothesis + +jGoal :: Judgement' a -> a +jGoal = _jGoal + +type Judgement = Judgement' CType substJdg :: TCvSubst -> Judgement -> Judgement -substJdg subst (Judgement hys goal) = Judgement (fmap (substCTy subst) hys) (substCTy subst goal) +substJdg = fmap . substCTy ------------------------------------------------------------------------------ -- | Reasons a tactic might fail. @@ -164,7 +178,7 @@ newJudgement -> CType -- ^ Sub-goal type -> m Judgement newJudgement hy g = do - pure $ Judgement hy g + pure $ Judgement hy mempty g ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index c7180b47d1..b131018523 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -48,7 +48,7 @@ bvar' = bvar . fromString . occNameString ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () -assumption = rule $ \(Judgement hy g) -> +assumption = rule $ \(Judgement hy _ g) -> case find ((== g) . snd) $ toList hy of Just (v, _) -> pure $ noLoc $ var' v Nothing -> throwError $ GoalMismatch "assumption" g @@ -57,7 +57,7 @@ assumption = rule $ \(Judgement hy g) -> ------------------------------------------------------------------------------ -- | Introduce a lambda. intro :: TacticsM () -intro = rule $ \(Judgement hy g) -> +intro = rule $ \(Judgement hy _ g) -> case splitFunTy_maybe $ unCType g of Just (a, b) -> do v <- pure $ mkGoodName (getInScope hy) a @@ -68,7 +68,7 @@ intro = rule $ \(Judgement hy g) -> ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros :: TacticsM () -intros = rule $ \(Judgement hy g) -> +intros = rule $ \(Judgement hy _ g) -> case tcSplitFunTys $ unCType g of ([], _) -> throwError $ GoalMismatch "intro" g (as, b) -> do @@ -84,7 +84,7 @@ intros = rule $ \(Judgement hy g) -> -- | Combinator for performign case splitting, and running sub-rules on the -- resulting matches. destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM () -destruct' f term = rule $ \(Judgement hy g) -> do +destruct' f term = rule $ \(Judgement hy _ g) -> do case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term Just (_, t) -> @@ -116,7 +116,7 @@ destruct = destruct' $ const subgoal ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () -homo = destruct' $ \dc (Judgement hy (CType g)) -> +homo = destruct' $ \dc (Judgement hy _ (CType g)) -> buildDataCon hy dc (snd $ splitAppTys g) @@ -129,13 +129,13 @@ solve t = t >> throwError NoProgress ------------------------------------------------------------------------------ -- | Apply a function from the hypothesis. apply :: TacticsM () -apply = rule $ \jdg@(Judgement hy g) -> do +apply = rule $ \jdg@(Judgement hy _ g) -> do case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of Just (func, ty) -> applySpecific func ty jdg Nothing -> throwError $ GoalMismatch "apply" g apply' :: OccName -> TacticsM () -apply' func = rule $ \(Judgement hys g) -> +apply' func = rule $ \(Judgement hys _ g) -> case M.lookup func hys of Just (CType ty) -> do let (args, ret) = splitFunTys ty @@ -147,7 +147,7 @@ apply' func = rule $ \(Judgement hys g) -> Nothing -> throwError $ GoalMismatch "apply" g applySpecific :: OccName -> CType -> Judgement -> RuleM (LHsExpr GhcPs) -applySpecific func (CType ty) (Judgement hy _) = do +applySpecific func (CType ty) (Judgement hy _ _) = do let (args, _) = splitFunTys ty sgs <- traverse (newSubgoal hy . CType) args pure . noLoc @@ -156,7 +156,7 @@ applySpecific func (CType ty) (Judgement hy _) = do instantiate :: OccName -> CType -> TacticsM () -instantiate func (CType ty) = rule $ \jdg@(Judgement _ (CType g)) -> do +instantiate func (CType ty) = rule $ \jdg@(Judgement _ _ (CType g)) -> do -- TODO(sandy): We need to get available from the type sig and compare -- against _ctx let (_binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty @@ -175,7 +175,7 @@ instantiate func (CType ty) = rule $ \jdg@(Judgement _ (CType g)) -> do -- | Introduce a data constructor, splitting a goal into the datacon's -- constituent sub-goals. split :: TacticsM () -split = rule $ \(Judgement hy g) -> +split = rule $ \(Judgement hy _ g) -> case splitTyConApp_maybe $ unCType g of Just (tc, apps) -> case tyConDataCons tc of @@ -204,7 +204,7 @@ attemptOn tac getNames = matching (choice . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------ -- | Automatically solve a goal. auto :: TacticsM () -auto = TacticT $ StateT $ \(Judgement _ goal) -> runStateT (unTacticT $ auto' 5) (Judgement M.empty goal) +auto = TacticT $ StateT $ \(Judgement _ _ goal) -> runStateT (unTacticT $ auto' 5) (Judgement mempty mempty goal) auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress @@ -218,10 +218,10 @@ auto' n = do ] where functionNames :: Judgement -> [OccName] - functionNames (Judgement hys _) = M.keys $ M.filter (isFunction . unCType) hys + functionNames (Judgement hys _ _) = M.keys $ M.filter (isFunction . unCType) hys algebraicNames :: Judgement -> [OccName] - algebraicNames (Judgement hys _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys + algebraicNames (Judgement hys _ _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys ------------------------------------------------------------------------------ -- | Run a tactic, and subsequently apply auto if it completes. If not, just From 8751bb522a6854bdea6077fb444aeaa64560552f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 14:27:32 -0700 Subject: [PATCH 18/64] Add a Context to TacticM --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 19 ++++++++++--------- .../src/Ide/Plugin/Tactic/Machinery.hs | 17 +++++++++++++---- 2 files changed, 23 insertions(+), 13 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 20e8059b06..41f204fc96 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -13,6 +13,7 @@ module Ide.Plugin.Tactic , TacticCommand (..) ) where +import Control.Arrow import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe @@ -240,9 +241,14 @@ tacticCmd tac lf state (TacticParams uri range var_name) -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp - let dflags = hsc_dflags $ hscEnv hscenv + range' <- liftMaybe $ toCurrentRange pos range + let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' + -- TODO(sandy): unclear if this span is correct; might be + -- pointing to the wrong version of the file + dflags = hsc_dflags $ hscEnv hscenv + ctx = mkContext $ mapMaybe (sequenceA . first occName) $ getDefiningBindings b2 span pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp - case runTactic jdg + case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of @@ -251,13 +257,8 @@ tacticCmd tac lf state (TacticParams uri range var_name) $ Left $ ResponseError InvalidRequest (T.pack $ show err) Nothing Right res -> do - range' <- liftMaybe $ toCurrentRange pos range - let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' - g = graft (RealSrcSpan span) res - -- TODO(sandy): unclear if this span is correct; might be - -- pointing to the wrong version of the file - _this_name = getDefiningBindings b2 span - let response = transform dflags (clientCapabilities lf) uri g pm + let g = graft (RealSrcSpan span) res + response = transform dflags (clientCapabilities lf) uri g pm pure $ case response of Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index e443b65345..5e0ccdafa6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -15,6 +15,7 @@ module Ide.Plugin.Tactic.Machinery where import Control.Monad (unless) import Control.Monad.Except (throwError) import Control.Monad.State (gets, get, modify, evalStateT) +import Control.Monad.Reader import Data.Char import Data.Either import Data.Function @@ -152,7 +153,14 @@ instance Show TacticError where show NoApplicableTactic = "No tactic could be applied" -type ProvableM = ProvableT Judgement Identity +mkContext :: [(OccName, Type)] -> Context +mkContext = Context + +data Context = Context + { ctxDefiningFuncs :: [(OccName, Type)] + } + +type ProvableM = ProvableT Judgement (Reader Context) type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM type Rule = RuleM (LHsExpr GhcPs) @@ -262,14 +270,15 @@ mkTyConName tc -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. runTactic - :: Judgement + :: Context + -> Judgement -> TacticsM () -- ^ Tactic to use -> Either [TacticError] (LHsExpr GhcPs) -runTactic jdg t = +runTactic ctx jdg t = -- FIXME [Reed] This code does not work let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg tacticState = initialTacticState { ts_skolems = skolems } - in case partitionEithers $ runProvable $ runTacticT t jdg tacticState of + in case partitionEithers $ flip runReader ctx $ runProvableT $ runTacticT t jdg tacticState of (errs, []) -> Left $ errs (_, solns) -> let soln = listToMaybe $ filter (null . snd) solns From b0f233ab906ae66640c5aa91d465cebbff2257e3 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 14:49:39 -0700 Subject: [PATCH 19/64] Don't destruct already destructed --- .../src/Ide/Plugin/Tactic/Machinery.hs | 27 +++++++++++++++++-- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 13 ++++++--- 2 files changed, 35 insertions(+), 5 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 5e0ccdafa6..e4a187d307 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -1,11 +1,12 @@ -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ViewPatterns #-} @@ -107,6 +108,24 @@ data Judgement' a = Judgement } deriving stock (Eq, Ord, Generic, Functor) +hasDestructed :: Judgement -> OccName -> Bool +hasDestructed j n = S.member n $ _jDestructed j + +destructing :: OccName -> Judgement -> Judgement +destructing n jdg@Judgement{..} = jdg + { _jDestructed = _jDestructed <> S.singleton n + } + +withNewGoal :: a -> Judgement' a -> Judgement' a +withNewGoal t jdg = jdg + { _jGoal = t + } + +introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a +introducing ns jdg@Judgement{..} = jdg + { _jHypothesis = M.fromList ns <> _jHypothesis + } + jHypothesis :: Judgement' a -> Map OccName a jHypothesis = _jHypothesis @@ -128,6 +147,7 @@ data TacticError | UnificationError CType CType | NoProgress | NoApplicableTactic + | AlreadyDestructed OccName instance Show TacticError where show (UndefinedHypothesis name) = @@ -156,6 +176,9 @@ instance Show TacticError where mkContext :: [(OccName, Type)] -> Context mkContext = Context +getCurrentDefinitions :: MonadReader Context m => m [OccName] +getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs + data Context = Context { ctxDefiningFuncs :: [(OccName, Type)] } diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index b131018523..89511fd6e0 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -13,6 +13,7 @@ module Ide.Plugin.Tactic.Tactics import Control.Applicative import Control.Monad.State.Strict (StateT(..), runStateT) import Control.Monad.Except (throwError) +import Data.Coerce import Data.Function import Data.List import Data.Maybe @@ -84,7 +85,7 @@ intros = rule $ \(Judgement hy _ g) -> -- | Combinator for performign case splitting, and running sub-rules on the -- resulting matches. destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM () -destruct' f term = rule $ \(Judgement hy _ g) -> do +destruct' f term = rule $ \jdg@(Judgement hy _ g) -> do case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term Just (_, t) -> @@ -102,7 +103,9 @@ destruct' f term = rule $ \(Judgement hy _ g) -> do pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) $ fmap bvar' names - j <- newJudgement (M.fromList (zip names (fmap CType args)) <> hy) g + let j = destructing term + $ introducing (zip names $ coerce args) + $ withNewGoal g jdg sg <- f dc j pure $ match [pat] $ unLoc sg @@ -110,7 +113,11 @@ destruct' f term = rule $ \(Judgement hy _ g) -> do ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. destruct :: OccName -> TacticsM () -destruct = destruct' $ const subgoal +destruct name = do + jdg <- goal + case hasDestructed jdg name of + True -> throwError $ AlreadyDestructed name + False -> destruct' (const subgoal) name ------------------------------------------------------------------------------ From d5112be08a0079de0f0605128e6c07817566cbf1 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 14:51:44 -0700 Subject: [PATCH 20/64] Remove the internal lib --- haskell-language-server.cabal | 48 ++++++----------------------------- 1 file changed, 8 insertions(+), 40 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 81095dfc73..d7d9b7c03c 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -77,47 +77,10 @@ library default-language: Haskell2010 -library hls-tactics - import: agpl, common-deps - hs-source-dirs: plugins/tactics/src - exposed-modules: - Ide.Plugin.Tactic - Ide.Plugin.Tactic.Types - Ide.Plugin.Tactic.Machinery - Ide.Plugin.Tactic.Tactics - Ide.Plugin.Tactic.BindSites - Ide.Plugin.Tactic.GHC - Ide.TreeTransform - - ghc-options: - -Wall -Wno-name-shadowing -Wredundant-constraints - if flag(pedantic) - ghc-options: -Werror - - build-depends: - , aeson - , containers - , fingertree - , ghc - , ghc-exactprint - , ghc-source-gen - , ghcide >=0.1 - , haskell-lsp ^>=0.22 - , hls-plugin-api - , mtl - , refinery - , retrie >=0.1.1.0 - , shake - , syb - , text - , transformers - - default-language: Haskell2010 - executable haskell-language-server import: agpl, common-deps main-is: Main.hs - hs-source-dirs: exe plugins/default/src + hs-source-dirs: exe plugins/default/src plugins/tactics/src other-modules: Ide.Plugin.Eval Ide.Plugin.Example @@ -129,6 +92,13 @@ executable haskell-language-server Ide.Plugin.Pragmas Ide.Plugin.Retrie Ide.Plugin.StylishHaskell + Ide.Plugin.Tactic + Ide.Plugin.Tactic.Types + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Tactics + Ide.Plugin.Tactic.BindSites + Ide.Plugin.Tactic.GHC + Ide.TreeTransform ghc-options: -threaded -Wall -Wno-name-shadowing -Wredundant-constraints @@ -161,7 +131,6 @@ executable haskell-language-server , regex-tdfa , retrie >=0.1.1.0 , hslogger - , hls-tactics , optparse-applicative , haskell-lsp ^>=0.22 , hls-plugin-api @@ -264,7 +233,6 @@ test-suite func-test build-depends: , bytestring , data-default - , hls-tactics , lens , tasty , tasty-ant-xml >=1.1.6 From 34da9ef929af353ac13412be4beb2066ab665dca Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 14:53:10 -0700 Subject: [PATCH 21/64] Cleanup warnings --- plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index e4a187d307..1052ae27dc 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -13,14 +13,12 @@ module Ide.Plugin.Tactic.Machinery where -import Control.Monad (unless) import Control.Monad.Except (throwError) import Control.Monad.State (gets, get, modify, evalStateT) import Control.Monad.Reader import Data.Char import Data.Either import Data.Function -import Data.Functor.Identity import Data.List import Data.Map (Map) import qualified Data.Map as M @@ -32,13 +30,11 @@ import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location -import GHC.Generics import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics import GHC.SourceGen.Overloaded -import Ide.Plugin.Tactic.GHC (oneWayUnify) import Name import Outputable hiding ((<>)) import Refinery.Tactic @@ -172,6 +168,8 @@ instance Show TacticError where "Unable to make progress" show NoApplicableTactic = "No tactic could be applied" + show (AlreadyDestructed name) = + "Aleady destructed " <> unsafeRender name mkContext :: [(OccName, Type)] -> Context mkContext = Context From 05301ca79edf4dd3aa693f24bf9908ca2856c6db Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 14:58:11 -0700 Subject: [PATCH 22/64] Move debug machinery into *.Debug --- haskell-language-server.cabal | 1 + .../tactics/src/Ide/Plugin/Tactic/Debug.hs | 19 +++++++++++++++++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 18 ++++++------------ 3 files changed, 26 insertions(+), 12 deletions(-) create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index d7d9b7c03c..0a6ce0be77 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -93,6 +93,7 @@ executable haskell-language-server Ide.Plugin.Retrie Ide.Plugin.StylishHaskell Ide.Plugin.Tactic + Ide.Plugin.Tactic.Debug Ide.Plugin.Tactic.Types Ide.Plugin.Tactic.Machinery Ide.Plugin.Tactic.Tactics diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs new file mode 100644 index 0000000000..87b4a1c17c --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs @@ -0,0 +1,19 @@ +module Ide.Plugin.Tactic.Debug + ( module Ide.Plugin.Tactic.Debug + , traceM + , traceShowId + , trace + ) where + +import Debug.Trace +import DynFlags (unsafeGlobalDynFlags) +import Outputable hiding ((<>)) + +------------------------------------------------------------------------------ +-- | Print something +unsafeRender :: Outputable a => a -> String +unsafeRender = unsafeRender' . ppr + +unsafeRender' :: SDoc -> String +unsafeRender' = showSDoc unsafeGlobalDynFlags + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 1052ae27dc..35a1e0a37d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -11,11 +11,14 @@ {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ViewPatterns #-} -module Ide.Plugin.Tactic.Machinery where +module Ide.Plugin.Tactic.Machinery + ( module Ide.Plugin.Tactic.Machinery + , module Ide.Plugin.Tactic.Debug + ) where import Control.Monad.Except (throwError) -import Control.Monad.State (gets, get, modify, evalStateT) import Control.Monad.Reader +import Control.Monad.State (gets, get, modify, evalStateT) import Data.Char import Data.Either import Data.Function @@ -30,13 +33,12 @@ import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location +import Ide.Plugin.Tactic.Debug -import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics import GHC.SourceGen.Overloaded import Name -import Outputable hiding ((<>)) import Refinery.Tactic import SrcLoc import TcType @@ -370,11 +372,3 @@ rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh) (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) ------------------------------------------------------------------------------- --- | Print something -unsafeRender :: Outputable a => a -> String -unsafeRender = unsafeRender' . ppr - -unsafeRender' :: SDoc -> String -unsafeRender' = showSDoc unsafeGlobalDynFlags - From 2034717b1d0a5d92bded5fb69ec44cc4688c7c4a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:06:59 -0700 Subject: [PATCH 23/64] Rip types out of machinery --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 2 +- .../src/Ide/Plugin/Tactic/Machinery.hs | 87 +------------- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 112 +++++++++++++++++- 3 files changed, 113 insertions(+), 88 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 41f204fc96..5a52cc981a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -246,7 +246,7 @@ tacticCmd tac lf state (TacticParams uri range var_name) -- TODO(sandy): unclear if this span is correct; might be -- pointing to the wrong version of the file dflags = hsc_dflags $ hscEnv hscenv - ctx = mkContext $ mapMaybe (sequenceA . first occName) $ getDefiningBindings b2 span + ctx = mkContext $ mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings b2 span pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic ctx jdg $ tac diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 35a1e0a37d..a900cba451 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -14,6 +14,7 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery , module Ide.Plugin.Tactic.Debug + , module Ide.Plugin.Tactic.Types ) where import Control.Monad.Except (throwError) @@ -21,7 +22,6 @@ import Control.Monad.Reader import Control.Monad.State (gets, get, modify, evalStateT) import Data.Char import Data.Either -import Data.Function import Data.List import Data.Map (Map) import qualified Data.Map as M @@ -34,6 +34,7 @@ import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location import Ide.Plugin.Tactic.Debug +import Ide.Plugin.Tactic.Types import qualified FastString as FS import GHC.Generics @@ -46,33 +47,11 @@ import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unify -data TacticState = TacticState - { ts_skolems :: [TyVar] - , ts_unifier :: TCvSubst - } - -initialTacticState :: TacticState -initialTacticState = TacticState - { ts_skolems = [] - , ts_unifier = emptyTCvSubst - } - ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. instance MonadExtract (LHsExpr GhcPs) ProvableM where hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" - ------------------------------------------------------------------------------- --- | A wrapper around 'Type' which supports equality and ordering. -newtype CType = CType { unCType :: Type } - -instance Eq CType where - (==) = eqType `on` unCType - -instance Ord CType where - compare = nonDetCmpType `on` unCType - substCTy :: TCvSubst -> CType -> CType substCTy subst = CType . substTy subst . unCType @@ -96,16 +75,6 @@ buildHypothesis where occ = occName n - ------------------------------------------------------------------------------- --- | The current bindings and goal for a hole to be filled by refinery. -data Judgement' a = Judgement - { _jHypothesis :: Map OccName a - , _jDestructed :: Set OccName - , _jGoal :: a - } - deriving stock (Eq, Ord, Generic, Functor) - hasDestructed :: Judgement -> OccName -> Bool hasDestructed j n = S.member n $ _jDestructed j @@ -130,64 +99,16 @@ jHypothesis = _jHypothesis jGoal :: Judgement' a -> a jGoal = _jGoal -type Judgement = Judgement' CType - substJdg :: TCvSubst -> Judgement -> Judgement substJdg = fmap . substCTy ------------------------------------------------------------------------------- --- | Reasons a tactic might fail. -data TacticError - = UndefinedHypothesis OccName - | GoalMismatch String CType - | UnsolvedSubgoals [Judgement] - | UnificationError CType CType - | NoProgress - | NoApplicableTactic - | AlreadyDestructed OccName - -instance Show TacticError where - show (UndefinedHypothesis name) = - occNameString name <> " is not available in the hypothesis." - show (GoalMismatch tac (CType typ)) = - mconcat - [ "The tactic " - , tac - , " doesn't apply to goal type " - , unsafeRender typ - ] - show (UnsolvedSubgoals _) = - "There were unsolved subgoals" - show (UnificationError (CType t1) (CType t2)) = - mconcat - [ "Could not unify " - , unsafeRender t1 - , " and " - , unsafeRender t2 - ] - show NoProgress = - "Unable to make progress" - show NoApplicableTactic = - "No tactic could be applied" - show (AlreadyDestructed name) = - "Aleady destructed " <> unsafeRender name - -mkContext :: [(OccName, Type)] -> Context +mkContext :: [(OccName, CType)] -> Context mkContext = Context getCurrentDefinitions :: MonadReader Context m => m [OccName] getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs -data Context = Context - { ctxDefiningFuncs :: [(OccName, Type)] - } - -type ProvableM = ProvableT Judgement (Reader Context) -type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM -type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM -type Rule = RuleM (LHsExpr GhcPs) - ------------------------------------------------------------------------------ -- | Produce a subgoal that must be solved before we can solve the original @@ -300,7 +221,7 @@ runTactic runTactic ctx jdg t = -- FIXME [Reed] This code does not work let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg - tacticState = initialTacticState { ts_skolems = skolems } + tacticState = mempty { ts_skolems = skolems } in case partitionEithers $ flip runReader ctx $ runProvableT $ runTacticT t jdg tacticState of (errs, []) -> Left $ errs (_, solns) -> diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 5d0ae4042c..c7707aa7d8 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -1,10 +1,24 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE OverloadedStrings #-} -module Ide.Plugin.Tactic.Types - ( tacticTitle - , TacticCommand (..) - ) where +module Ide.Plugin.Tactic.Types where + +import qualified Data.Map as M +import Data.Map (Map) +import qualified Data.Set as S +import Data.Set (Set) import qualified Data.Text as T +import Type +import Data.Function +import GHC.Generics +import OccName +import Ide.Plugin.Tactic.Debug +import Development.IDE.GHC.Compat +import Refinery.Tactic (RuleT) +import Refinery.Tactic.Internal +import Control.Monad.Reader ------------------------------------------------------------------------------ -- | The list of tactics exposed to the outside world. These are attached to @@ -27,3 +41,93 @@ tacticTitle Intro _ = "Intro" tacticTitle Intros _ = "Introduce lambda" tacticTitle Destruct var = "Case split on " <> var tacticTitle Homomorphism var = "Homomorphic case split on " <> var + +------------------------------------------------------------------------------ +-- | A wrapper around 'Type' which supports equality and ordering. +newtype CType = CType { unCType :: Type } + +instance Eq CType where + (==) = eqType `on` unCType + +instance Ord CType where + compare = nonDetCmpType `on` unCType + + +------------------------------------------------------------------------------ +data TacticState = TacticState + { ts_skolems :: [TyVar] + , ts_unifier :: TCvSubst + } + +instance Semigroup TacticState where + TacticState a1 b1 <> TacticState a2 b2 + = TacticState (a1 <> a2) (unionTCvSubst b1 b2) + +instance Monoid TacticState where + mempty = TacticState mempty emptyTCvSubst + +------------------------------------------------------------------------------ +-- | The current bindings and goal for a hole to be filled by refinery. +data Judgement' a = Judgement + { _jHypothesis :: Map OccName a + , _jDestructed :: Set OccName + , _jGoal :: a + } + deriving stock (Eq, Ord, Generic, Functor) + +type Judgement = Judgement' CType + +------------------------------------------------------------------------------ +-- | Reasons a tactic might fail. +data TacticError + = UndefinedHypothesis OccName + | GoalMismatch String CType + | UnsolvedSubgoals [Judgement] + | UnificationError CType CType + | NoProgress + | NoApplicableTactic + | AlreadyDestructed OccName + deriving stock (Eq, Ord) + +instance Show TacticError where + show (UndefinedHypothesis name) = + occNameString name <> " is not available in the hypothesis." + show (GoalMismatch tac (CType typ)) = + mconcat + [ "The tactic " + , tac + , " doesn't apply to goal type " + , unsafeRender typ + ] + show (UnsolvedSubgoals _) = + "There were unsolved subgoals" + show (UnificationError (CType t1) (CType t2)) = + mconcat + [ "Could not unify " + , unsafeRender t1 + , " and " + , unsafeRender t2 + ] + show NoProgress = + "Unable to make progress" + show NoApplicableTactic = + "No tactic could be applied" + show (AlreadyDestructed name) = + "Aleady destructed " <> unsafeRender name + + +------------------------------------------------------------------------------ +type ProvableM = ProvableT Judgement (Reader Context) +type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM +type Rule = RuleM (LHsExpr GhcPs) + + +------------------------------------------------------------------------------ +-- | The Reader context of tactics and rules +data Context = Context + { ctxDefiningFuncs :: [(OccName, CType)] + -- ^ The functions currently being defined + } + deriving stock (Eq, Ord) + From d2f093f841a9455cd3641cfba97c05c4cee2a767 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:08:51 -0700 Subject: [PATCH 24/64] Cleanup warnings --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 1 - .../src/Ide/Plugin/Tactic/Machinery.hs | 4 ++-- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 21 ++++++++----------- 3 files changed, 11 insertions(+), 15 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 5a52cc981a..a19c35890b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -39,7 +39,6 @@ import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.BindSites import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Tactics -import Ide.Plugin.Tactic.Types import Ide.TreeTransform (transform, graft, useAnnotatedSource) import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index a900cba451..f92d05bc1c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -10,6 +10,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery @@ -26,7 +27,6 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import Data.Set (Set) import qualified Data.Set as S import Data.Traversable import DataCon @@ -37,7 +37,6 @@ import Ide.Plugin.Tactic.Debug import Ide.Plugin.Tactic.Types import qualified FastString as FS -import GHC.Generics import GHC.SourceGen.Overloaded import Name import Refinery.Tactic @@ -47,6 +46,7 @@ import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unify + ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. instance MonadExtract (LHsExpr GhcPs) ProvableM where diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index c7707aa7d8..51ec4a2919 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -5,20 +5,17 @@ module Ide.Plugin.Tactic.Types where -import qualified Data.Map as M -import Data.Map (Map) -import qualified Data.Set as S -import Data.Set (Set) +import Control.Monad.Reader +import Data.Function +import Data.Map (Map) +import Data.Set (Set) import qualified Data.Text as T +import Development.IDE.GHC.Compat +import GHC.Generics +import Ide.Plugin.Tactic.Debug +import OccName +import Refinery.Tactic.Internal import Type -import Data.Function -import GHC.Generics -import OccName -import Ide.Plugin.Tactic.Debug -import Development.IDE.GHC.Compat -import Refinery.Tactic (RuleT) -import Refinery.Tactic.Internal -import Control.Monad.Reader ------------------------------------------------------------------------------ -- | The list of tactics exposed to the outside world. These are attached to From 9f951243b16bc81f3d1df6a1840b496a587d97ce Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:19:09 -0700 Subject: [PATCH 25/64] Continue splitting Machinery --- haskell-language-server.cabal | 3 + .../tactics/src/Ide/Plugin/Tactic/Context.hs | 13 ++++ .../src/Ide/Plugin/Tactic/Judgements.hs | 40 ++++++++++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 65 +++---------------- .../tactics/src/Ide/Plugin/Tactic/Range.hs | 18 +++++ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 11 +++- 6 files changed, 94 insertions(+), 56 deletions(-) create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Context.hs create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Range.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 0a6ce0be77..31de68ad7a 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -98,6 +98,9 @@ executable haskell-language-server Ide.Plugin.Tactic.Machinery Ide.Plugin.Tactic.Tactics Ide.Plugin.Tactic.BindSites + Ide.Plugin.Tactic.Judgements + Ide.Plugin.Tactic.Context + Ide.Plugin.Tactic.Range Ide.Plugin.Tactic.GHC Ide.TreeTransform diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs new file mode 100644 index 0000000000..caebc8bc5e --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE FlexibleContexts #-} + +module Ide.Plugin.Tactic.Context where + +import Ide.Plugin.Tactic.Types +import Control.Monad.Reader + +mkContext :: [(OccName, CType)] -> Context +mkContext = Context + +getCurrentDefinitions :: MonadReader Context m => m [OccName] +getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs new file mode 100644 index 0000000000..bd83b71e1d --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE RecordWildCards #-} + +module Ide.Plugin.Tactic.Judgements where + +import Data.Coerce +import Data.Map (Map) +import qualified Data.Map as M +import qualified Data.Set as S +import Ide.Plugin.Tactic.Types +import Type + + +hasDestructed :: Judgement -> OccName -> Bool +hasDestructed j n = S.member n $ _jDestructed j + +destructing :: OccName -> Judgement -> Judgement +destructing n jdg@Judgement{..} = jdg + { _jDestructed = _jDestructed <> S.singleton n + } + +withNewGoal :: a -> Judgement' a -> Judgement' a +withNewGoal t jdg = jdg + { _jGoal = t + } + +introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a +introducing ns jdg@Judgement{..} = jdg + { _jHypothesis = M.fromList ns <> _jHypothesis + } + +jHypothesis :: Judgement' a -> Map OccName a +jHypothesis = _jHypothesis + +jGoal :: Judgement' a -> a +jGoal = _jGoal + + +substJdg :: TCvSubst -> Judgement -> Judgement +substJdg subst = fmap $ coerce . substTy subst . coerce + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index f92d05bc1c..34c1d93ac5 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -16,31 +16,35 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery , module Ide.Plugin.Tactic.Debug , module Ide.Plugin.Tactic.Types + , module Ide.Plugin.Tactic.Judgements + , module Ide.Plugin.Tactic.Context + , module Ide.Plugin.Tactic.Range ) where import Control.Monad.Except (throwError) import Control.Monad.Reader import Control.Monad.State (gets, get, modify, evalStateT) import Data.Char +import Data.Coerce import Data.Either import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings import Development.IDE.Types.Location +import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.Debug +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Types -import qualified FastString as FS import GHC.SourceGen.Overloaded import Name import Refinery.Tactic -import SrcLoc import TcType import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) @@ -53,12 +57,12 @@ instance MonadExtract (LHsExpr GhcPs) ProvableM where hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" substCTy :: TCvSubst -> CType -> CType -substCTy subst = CType . substTy subst . unCType +substCTy subst = coerce . substTy subst . coerce ------------------------------------------------------------------------------ -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType -hypothesisFromBindings span bs = buildHypothesis (getLocalScope bs span) +hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span ------------------------------------------------------------------------------ @@ -68,46 +72,10 @@ buildHypothesis = M.fromList . mapMaybe go where - go (n, t) + go (occName -> occ, t) | Just ty <- t , isAlpha . head . occNameString $ occ = Just (occ, CType ty) | otherwise = Nothing - where - occ = occName n - -hasDestructed :: Judgement -> OccName -> Bool -hasDestructed j n = S.member n $ _jDestructed j - -destructing :: OccName -> Judgement -> Judgement -destructing n jdg@Judgement{..} = jdg - { _jDestructed = _jDestructed <> S.singleton n - } - -withNewGoal :: a -> Judgement' a -> Judgement' a -withNewGoal t jdg = jdg - { _jGoal = t - } - -introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducing ns jdg@Judgement{..} = jdg - { _jHypothesis = M.fromList ns <> _jHypothesis - } - -jHypothesis :: Judgement' a -> Map OccName a -jHypothesis = _jHypothesis - -jGoal :: Judgement' a -> a -jGoal = _jGoal - - -substJdg :: TCvSubst -> Judgement -> Judgement -substJdg = fmap . substCTy - -mkContext :: [(OccName, CType)] -> Context -mkContext = Context - -getCurrentDefinitions :: MonadReader Context m => m [OccName] -getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs ------------------------------------------------------------------------------ @@ -280,16 +248,3 @@ unify goal inst = modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) }) Nothing -> throwError (UnificationError inst goal) - ------------------------------------------------------------------------------- --- | Convert a DAML compiler Range to a GHC SrcSpan --- TODO(sandy): this doesn't belong here -rangeToSrcSpan :: String -> Range -> SrcSpan -rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range - -rangeToRealSrcSpan :: String -> Range -> RealSrcSpan -rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = - mkRealSrcSpan - (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) - (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) - diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Range.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Range.hs new file mode 100644 index 0000000000..9bf5c17d54 --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Range.hs @@ -0,0 +1,18 @@ +module Ide.Plugin.Tactic.Range where + +import qualified FastString as FS +import Development.IDE.Types.Location +import SrcLoc + +------------------------------------------------------------------------------ +-- | Convert a DAML compiler Range to a GHC SrcSpan +-- TODO(sandy): this doesn't belong here +rangeToSrcSpan :: String -> Range -> SrcSpan +rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range + +rangeToRealSrcSpan :: String -> Range -> RealSrcSpan +rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = + mkRealSrcSpan + (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) + (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 51ec4a2919..64d7d62e50 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -3,7 +3,14 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE OverloadedStrings #-} -module Ide.Plugin.Tactic.Types where +module Ide.Plugin.Tactic.Types + ( module Ide.Plugin.Tactic.Types + , OccName + , Type + , TyVar + , Span + , Range + ) where import Control.Monad.Reader import Data.Function @@ -16,6 +23,8 @@ import Ide.Plugin.Tactic.Debug import OccName import Refinery.Tactic.Internal import Type +import Development.IDE.Types.Location + ------------------------------------------------------------------------------ -- | The list of tactics exposed to the outside world. These are attached to From 03256b362755850821b8737b8d3525ea9bf3c004 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:27:31 -0700 Subject: [PATCH 26/64] Rip out GHC and Naming --- haskell-language-server.cabal | 1 + plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 24 +++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 91 +------------------ .../tactics/src/Ide/Plugin/Tactic/Naming.hs | 79 ++++++++++++++++ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 21 ++++- 5 files changed, 123 insertions(+), 93 deletions(-) create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 31de68ad7a..eddfd07302 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -101,6 +101,7 @@ executable haskell-language-server Ide.Plugin.Tactic.Judgements Ide.Plugin.Tactic.Context Ide.Plugin.Tactic.Range + Ide.Plugin.Tactic.Naming Ide.Plugin.Tactic.GHC Ide.TreeTransform diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index 337c3b6ab9..b9002aa5c5 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -1,9 +1,14 @@ +{-# LANGUAGE ViewPatterns #-} + module Ide.Plugin.Tactic.GHC where import TcType import TyCoRep import Var import Unique +import TyCon +import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) +import Type tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' @@ -46,3 +51,22 @@ cloneTyVar t = some_magic_number = 49 in setVarUnique t $ deriveUnique uniq some_magic_number + +------------------------------------------------------------------------------ +-- | Is this a function type? +isFunction :: Type -> Bool +isFunction (tcSplitFunTys -> ((_:_), _)) = True +isFunction _ = False + +------------------------------------------------------------------------------ +-- | Is this an algebraic type? +algebraicTyCon :: Type -> Maybe TyCon +algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) + | tycon == intTyCon = Nothing + | tycon == floatTyCon = Nothing + | tycon == doubleTyCon = Nothing + | tycon == charTyCon = Nothing + | tycon == funTyCon = Nothing + | otherwise = Just tycon +algebraicTyCon _ = Nothing + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 34c1d93ac5..e30b8e4551 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -19,11 +19,12 @@ module Ide.Plugin.Tactic.Machinery , module Ide.Plugin.Tactic.Judgements , module Ide.Plugin.Tactic.Context , module Ide.Plugin.Tactic.Range + , module Ide.Plugin.Tactic.Naming ) where import Control.Monad.Except (throwError) import Control.Monad.Reader -import Control.Monad.State (gets, get, modify, evalStateT) +import Control.Monad.State (gets, modify) import Data.Char import Data.Coerce import Data.Either @@ -31,7 +32,6 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import Data.Traversable import DataCon import Development.IDE.GHC.Compat import Development.IDE.Spans.LocalBindings @@ -41,21 +41,16 @@ import Ide.Plugin.Tactic.Debug import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Types +import Ide.Plugin.Tactic.Naming import GHC.SourceGen.Overloaded import Name import Refinery.Tactic import TcType import Type -import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unify ------------------------------------------------------------------------------- --- | Orphan instance for producing holes when attempting to solve tactics. -instance MonadExtract (LHsExpr GhcPs) ProvableM where - hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" - substCTy :: TCvSubst -> CType -> CType substCTy subst = coerce . substTy subst . coerce @@ -101,81 +96,6 @@ newJudgement hy g = do pure $ Judgement hy mempty g ------------------------------------------------------------------------------- --- | Produce a unique, good name for a type. -mkGoodName - :: [OccName] -- ^ Bindings in scope; used to ensure we don't shadow anything - -> Type -- ^ The type to produce a name for - -> OccName -mkGoodName in_scope t = - let tn = mkTyName t - in mkVarOcc $ case elem (mkVarOcc tn) in_scope of - True -> tn ++ show (length in_scope) - False -> tn - - ------------------------------------------------------------------------------- --- | Like 'mkGoodName' but creates several apart names. -mkManyGoodNames - :: (Traversable t, Monad m) - => M.Map OccName a - -> t Type - -> m (t OccName) -mkManyGoodNames hy args = - flip evalStateT (getInScope hy) $ for args $ \at -> do - in_scope <- Control.Monad.State.get - let n = mkGoodName in_scope at - modify (n :) - pure n - - ------------------------------------------------------------------------------- --- | Use type information to create a reasonable name. -mkTyName :: Type -> String --- eg. mkTyName (a -> B) = "fab" -mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) - = "f" ++ mkTyName a ++ mkTyName b --- eg. mkTyName (a -> b -> C) = "f_C" -mkTyName (tcSplitFunTys -> ((_:_), b)) - = "f_" ++ mkTyName b --- eg. mkTyName (Either A B) = "eab" -mkTyName (splitTyConApp_maybe -> Just (c, args)) - = mkTyConName c ++ foldMap mkTyName args --- eg. mkTyName a = "a" -mkTyName (getTyVar_maybe-> Just tv) - = occNameString $ occName tv --- eg. mkTyName (forall x. y) = "y" -mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) - = mkTyName t -mkTyName _ = "x" - - ------------------------------------------------------------------------------- --- | Is this a function type? -isFunction :: Type -> Bool -isFunction (tcSplitFunTys -> ((_:_), _)) = True -isFunction _ = False - ------------------------------------------------------------------------------- --- | Is this an algebraic type? -algebraicTyCon :: Type -> Maybe TyCon -algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) - | tycon == intTyCon = Nothing - | tycon == floatTyCon = Nothing - | tycon == doubleTyCon = Nothing - | tycon == charTyCon = Nothing - | tycon == funTyCon = Nothing - | otherwise = Just tycon -algebraicTyCon _ = Nothing - - ------------------------------------------------------------------------------- --- | Get a good name for a type constructor. -mkTyConName :: TyCon -> String -mkTyConName tc - | tc == listTyCon = "l_" - | tc == pairTyCon = "p_" - | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc ------------------------------------------------------------------------------ @@ -197,11 +117,6 @@ runTactic ctx jdg t = in Right $ fst $ fromMaybe (head solns) soln ------------------------------------------------------------------------------- --- | Which names are in scope? -getInScope :: Map OccName a -> [OccName] -getInScope = M.keys - ------------------------------------------------------------------------------ -- | Construct a data con with subgoals for each field. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs new file mode 100644 index 0000000000..e224fce6a8 --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Naming where + +import Control.Monad.State.Strict +import Data.Char +import Data.Map (Map) +import qualified Data.Map as M +import Data.Traversable +import Name +import TcType +import TyCon +import Type +import TysWiredIn (listTyCon, pairTyCon) + + +------------------------------------------------------------------------------ +-- | Use type information to create a reasonable name. +mkTyName :: Type -> String +-- eg. mkTyName (a -> B) = "fab" +mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) + = "f" ++ mkTyName a ++ mkTyName b +-- eg. mkTyName (a -> b -> C) = "f_C" +mkTyName (tcSplitFunTys -> ((_:_), b)) + = "f_" ++ mkTyName b +-- eg. mkTyName (Either A B) = "eab" +mkTyName (splitTyConApp_maybe -> Just (c, args)) + = mkTyConName c ++ foldMap mkTyName args +-- eg. mkTyName a = "a" +mkTyName (getTyVar_maybe-> Just tv) + = occNameString $ occName tv +-- eg. mkTyName (forall x. y) = "y" +mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) + = mkTyName t +mkTyName _ = "x" + + +------------------------------------------------------------------------------ +-- | Get a good name for a type constructor. +mkTyConName :: TyCon -> String +mkTyConName tc + | tc == listTyCon = "l_" + | tc == pairTyCon = "p_" + | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc + + +------------------------------------------------------------------------------ +-- | Produce a unique, good name for a type. +mkGoodName + :: [OccName] -- ^ Bindings in scope; used to ensure we don't shadow anything + -> Type -- ^ The type to produce a name for + -> OccName +mkGoodName in_scope t = + let tn = mkTyName t + in mkVarOcc $ case elem (mkVarOcc tn) in_scope of + True -> tn ++ show (length in_scope) + False -> tn + + +------------------------------------------------------------------------------ +-- | Like 'mkGoodName' but creates several apart names. +mkManyGoodNames + :: (Traversable t, Monad m) + => M.Map OccName a + -> t Type + -> m (t OccName) +mkManyGoodNames hy args = + flip evalStateT (getInScope hy) $ for args $ \at -> do + in_scope <- get + let n = mkGoodName in_scope at + modify (n :) + pure n + + +------------------------------------------------------------------------------ +-- | Which names are in scope? +getInScope :: Map OccName a -> [OccName] +getInScope = M.keys + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 64d7d62e50..6dfee7091b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -1,7 +1,10 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeSynonymInstances #-} module Ide.Plugin.Tactic.Types ( module Ide.Plugin.Tactic.Types @@ -18,12 +21,13 @@ import Data.Map (Map) import Data.Set (Set) import qualified Data.Text as T import Development.IDE.GHC.Compat +import Development.IDE.Types.Location import GHC.Generics import Ide.Plugin.Tactic.Debug import OccName +import Refinery.Tactic import Refinery.Tactic.Internal import Type -import Development.IDE.Types.Location ------------------------------------------------------------------------------ @@ -83,6 +87,13 @@ data Judgement' a = Judgement type Judgement = Judgement' CType + +------------------------------------------------------------------------------ +-- | Orphan instance for producing holes when attempting to solve tactics. +instance MonadExtract (LHsExpr GhcPs) ProvableM where + hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" + + ------------------------------------------------------------------------------ -- | Reasons a tactic might fail. data TacticError From 661858870ea429a6b78ec33b92909872c14bce38 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:29:41 -0700 Subject: [PATCH 27/64] Get it all compiling --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 3 ++- plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 24 ++++--------------- .../src/Ide/Plugin/Tactic/Machinery.hs | 2 +- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 8 +------ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 1 - 5 files changed, 8 insertions(+), 30 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index a19c35890b..b0c7ef11e7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -13,7 +13,7 @@ module Ide.Plugin.Tactic , TacticCommand (..) ) where -import Control.Arrow +import Control.Arrow import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe @@ -37,6 +37,7 @@ import GHC.Generics (Generic) import HscTypes (hsc_dflags) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.BindSites +import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Tactics import Ide.TreeTransform (transform, graft, useAnnotatedSource) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index b9002aa5c5..7ceec5801d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -4,11 +4,12 @@ module Ide.Plugin.Tactic.GHC where import TcType import TyCoRep -import Var -import Unique import TyCon -import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) import Type +import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon) +import Unique +import Var + tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' @@ -19,23 +20,6 @@ tcTyVar_maybe (TyVarTy v) = Just v tcTyVar_maybe _ = Nothing -oneWayUnify - :: [TyVar] -- ^ binders - -> Type -- ^ type to instiate - -> Type -- ^ at this type - -> Maybe TCvSubst -oneWayUnify binders toinst res = - case tcTyVar_maybe toinst of - Just var -> - case elem var binders of - True -> pure $ mkTvSubstPrs $ pure (var, res) - False -> Nothing - Nothing -> - case eqType toinst res of - True -> pure emptyTCvSubst - False -> Nothing - - instantiateType :: Type -> ([TyVar], Type) instantiateType t = do let vs = tyCoVarsOfTypeList t diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index e30b8e4551..3483585caf 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -39,9 +39,9 @@ import Development.IDE.Types.Location import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.Debug import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Types -import Ide.Plugin.Tactic.Naming import GHC.SourceGen.Overloaded import Name diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 89511fd6e0..3565a7476d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -27,6 +27,7 @@ import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.GHC import Name import Refinery.Tactic @@ -169,13 +170,6 @@ instantiate func (CType ty) = rule $ \jdg@(Judgement _ _ (CType g)) -> do let (_binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty unify (CType res) (CType g) applySpecific func (CType ty) jdg - -- case oneWayUnify binders res g of - -- Just subst -> - -- -- TODO(sandy): How does this affect the judgment wrt our new ununified - -- -- tyvars? - -- let (_fresh_vars, ty') = instantiateType $ substTy subst ty - -- in applySpecific func (CType ty') jdg - -- Nothing -> throwError $ GoalMismatch "instantiate" $ CType g ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 6dfee7091b..588a3f7768 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -26,7 +26,6 @@ import GHC.Generics import Ide.Plugin.Tactic.Debug import OccName import Refinery.Tactic -import Refinery.Tactic.Internal import Type From 289f04957ee4703f47115ecce61490a86400772c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:35:26 -0700 Subject: [PATCH 28/64] Stop re-exporting from Machinery --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 5 ++- .../src/Ide/Plugin/Tactic/Judgements.hs | 24 ++++++++++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 37 +------------------ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 5 ++- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 2 + 5 files changed, 36 insertions(+), 37 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index b0c7ef11e7..5a3f6969c3 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -37,9 +37,12 @@ import GHC.Generics (Generic) import HscTypes (hsc_dflags) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.BindSites +import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.GHC -import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types import Ide.TreeTransform (transform, graft, useAnnotatedSource) import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index bd83b71e1d..944a907c45 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -1,15 +1,39 @@ {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ViewPatterns #-} module Ide.Plugin.Tactic.Judgements where +import Data.Char import Data.Coerce import Data.Map (Map) import qualified Data.Map as M +import Data.Maybe import qualified Data.Set as S +import Development.IDE.Spans.LocalBindings import Ide.Plugin.Tactic.Types +import OccName +import SrcLoc import Type +------------------------------------------------------------------------------ +-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. +hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType +hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span + +------------------------------------------------------------------------------ +-- | Convert a @Set Id@ into a hypothesis. +buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType +buildHypothesis + = M.fromList + . mapMaybe go + where + go (occName -> occ, t) + | Just ty <- t + , isAlpha . head . occNameString $ occ = Just (occ, CType ty) + | otherwise = Nothing + + hasDestructed :: Judgement -> OccName -> Bool hasDestructed j n = S.member n $ _jDestructed j diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 3483585caf..3445aa6886 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -14,33 +14,19 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery - , module Ide.Plugin.Tactic.Debug - , module Ide.Plugin.Tactic.Types - , module Ide.Plugin.Tactic.Judgements - , module Ide.Plugin.Tactic.Context - , module Ide.Plugin.Tactic.Range - , module Ide.Plugin.Tactic.Naming ) where import Control.Monad.Except (throwError) import Control.Monad.Reader import Control.Monad.State (gets, modify) -import Data.Char import Data.Coerce import Data.Either import Data.List import Data.Map (Map) -import qualified Data.Map as M import Data.Maybe import DataCon import Development.IDE.GHC.Compat -import Development.IDE.Spans.LocalBindings -import Development.IDE.Types.Location -import Ide.Plugin.Tactic.Context -import Ide.Plugin.Tactic.Debug import Ide.Plugin.Tactic.Judgements -import Ide.Plugin.Tactic.Naming -import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Types import GHC.SourceGen.Overloaded @@ -54,24 +40,6 @@ import Unify substCTy :: TCvSubst -> CType -> CType substCTy subst = coerce . substTy subst . coerce ------------------------------------------------------------------------------- --- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. -hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType -hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span - - ------------------------------------------------------------------------------- --- | Convert a @Set Id@ into a hypothesis. -buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType -buildHypothesis - = M.fromList - . mapMaybe go - where - go (occName -> occ, t) - | Just ty <- t - , isAlpha . head . occNameString $ occ = Just (occ, CType ty) - | otherwise = Nothing - ------------------------------------------------------------------------------ -- | Produce a subgoal that must be solved before we can solve the original @@ -96,8 +64,6 @@ newJudgement hy g = do pure $ Judgement hy mempty g - - ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. @@ -117,7 +83,6 @@ runTactic ctx jdg t = in Right $ fst $ fromMaybe (head solns) soln - ------------------------------------------------------------------------------ -- | Construct a data con with subgoals for each field. buildDataCon @@ -135,6 +100,7 @@ buildDataCon hy dc apps = do $ fmap unLoc sgs +------------------------------------------------------------------------------ -- | We need to make sure that we don't try to unify any skolems. -- To see why, consider the case: -- @@ -151,6 +117,7 @@ checkSkolemUnification t1 t2 subst = do unless (all (flip notElemTCvSubst subst) skolems) $ throwError (UnificationError t1 t2) + ------------------------------------------------------------------------------ -- | Attempt to unify two types. unify :: CType -- ^ The goal type diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 3565a7476d..facf15930c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -26,8 +26,11 @@ import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat -import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.GHC +import Ide.Plugin.Tactic.Types +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Naming +import Ide.Plugin.Tactic.Machinery import Name import Refinery.Tactic diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 588a3f7768..f838b7d674 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -8,7 +8,9 @@ module Ide.Plugin.Tactic.Types ( module Ide.Plugin.Tactic.Types + , module Ide.Plugin.Tactic.Debug , OccName + , Name , Type , TyVar , Span From fce02e264a42865db72d2b22b007b54ba3fa5bd5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:45:09 -0700 Subject: [PATCH 29/64] Split out codegen/rules --- haskell-language-server.cabal | 15 ++-- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 78 +++++++++++++++++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 50 ++++-------- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 68 ++++------------ 4 files changed, 116 insertions(+), 95 deletions(-) create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index eddfd07302..39c67e3bdd 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -93,16 +93,17 @@ executable haskell-language-server Ide.Plugin.Retrie Ide.Plugin.StylishHaskell Ide.Plugin.Tactic - Ide.Plugin.Tactic.Debug - Ide.Plugin.Tactic.Types - Ide.Plugin.Tactic.Machinery - Ide.Plugin.Tactic.Tactics Ide.Plugin.Tactic.BindSites - Ide.Plugin.Tactic.Judgements + Ide.Plugin.Tactic.CodeGen Ide.Plugin.Tactic.Context - Ide.Plugin.Tactic.Range - Ide.Plugin.Tactic.Naming + Ide.Plugin.Tactic.Debug Ide.Plugin.Tactic.GHC + Ide.Plugin.Tactic.Judgements + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Naming + Ide.Plugin.Tactic.Range + Ide.Plugin.Tactic.Tactics + Ide.Plugin.Tactic.Types Ide.TreeTransform ghc-options: diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs new file mode 100644 index 0000000000..4923123546 --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -0,0 +1,78 @@ +module Ide.Plugin.Tactic.CodeGen where + +import Data.Map (Map) +import GHC.Exts +import GHC.SourceGen.Binds +import GHC.SourceGen.Expr +import GHC.SourceGen.Overloaded +import GHC.SourceGen.Pat +import OccName +import DataCon +import Development.IDE.GHC.Compat +import Ide.Plugin.Tactic.Types +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Machinery +import Name +import Ide.Plugin.Tactic.Naming +import Data.Traversable +import Type hiding (Var) +import Data.List +import Control.Monad.Except + + +------------------------------------------------------------------------------ +-- | Combinator for performign case splitting, and running sub-rules on the +-- resulting matches. +destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule +destruct' f term jdg@(Judgement hy _ g) = do + case find ((== term) . fst) $ toList hy of + Nothing -> throwError $ UndefinedHypothesis term + Just (_, t) -> + case splitTyConApp_maybe $ unCType t of + Nothing -> throwError $ GoalMismatch "destruct" g + Just (tc, apps) -> do + fmap noLoc + $ case' (var' term) + <$> do + for (tyConDataCons tc) $ \dc -> do + let args = dataConInstArgTys dc apps + names <- mkManyGoodNames hy args + + let pat :: Pat GhcPs + pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) + $ fmap bvar' names + + let j = destructing term + $ introducing (zip names $ coerce args) + $ withNewGoal g jdg + sg <- f dc j + pure $ match [pat] $ unLoc sg + + +------------------------------------------------------------------------------ +-- | Construct a data con with subgoals for each field. +buildDataCon + :: Map OccName CType -- ^ In-scope bindings + -> DataCon -- ^ The data con to build + -> [Type] -- ^ Type arguments for the data con + -> RuleM (LHsExpr GhcPs) +buildDataCon hy dc apps = do + let args = dataConInstArgTys dc apps + sgs <- traverse (newSubgoal hy . CType) args + pure + . noLoc + . foldl' (@@) + (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) + $ fmap unLoc sgs + + +------------------------------------------------------------------------------ +-- | Like 'var', but works over standard GHC 'OccName's. +var' :: Var a => OccName -> a +var' = var . fromString . occNameString + +------------------------------------------------------------------------------ +-- | Like 'bvar', but works over standard GHC 'OccName's. +bvar' :: BVar a => OccName -> a +bvar' = bvar . fromString . occNameString + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 3445aa6886..f802bb754e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -16,25 +16,20 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery ) where -import Control.Monad.Except (throwError) -import Control.Monad.Reader -import Control.Monad.State (gets, modify) -import Data.Coerce -import Data.Either -import Data.List -import Data.Map (Map) -import Data.Maybe -import DataCon -import Development.IDE.GHC.Compat -import Ide.Plugin.Tactic.Judgements -import Ide.Plugin.Tactic.Types - -import GHC.SourceGen.Overloaded -import Name -import Refinery.Tactic -import TcType -import Type -import Unify +import Control.Monad.Except (throwError) +import Control.Monad.Reader +import Control.Monad.State (gets, modify) +import Data.Coerce +import Data.Either +import Data.Map (Map) +import Data.Maybe +import Development.IDE.GHC.Compat +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Types +import Refinery.Tactic +import TcType +import Type +import Unify substCTy :: TCvSubst -> CType -> CType @@ -53,6 +48,7 @@ newSubgoal hy g = do unifier <- gets ts_unifier subgoal $ substJdg unifier j + ------------------------------------------------------------------------------ -- | Create a new judgment newJudgement @@ -83,22 +79,6 @@ runTactic ctx jdg t = in Right $ fst $ fromMaybe (head solns) soln ------------------------------------------------------------------------------- --- | Construct a data con with subgoals for each field. -buildDataCon - :: Map OccName CType -- ^ In-scope bindings - -> DataCon -- ^ The data con to build - -> [Type] -- ^ Type arguments for the data con - -> RuleM (LHsExpr GhcPs) -buildDataCon hy dc apps = do - let args = dataConInstArgTys dc apps - sgs <- traverse (newSubgoal hy . CType) args - pure - . noLoc - . foldl' (@@) - (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) - $ fmap unLoc sgs - ------------------------------------------------------------------------------ -- | We need to make sure that we don't try to unify any skolems. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index facf15930c..98f346ae71 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -11,45 +11,29 @@ module Ide.Plugin.Tactic.Tactics import Control.Applicative -import Control.Monad.State.Strict (StateT(..), runStateT) import Control.Monad.Except (throwError) -import Data.Coerce +import Control.Monad.State.Strict (StateT(..), runStateT) import Data.Function import Data.List -import Data.Maybe import qualified Data.Map as M -import Data.Traversable -import DataCon +import Data.Maybe import Development.IDE.GHC.Compat import GHC.Exts -import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded -import GHC.SourceGen.Pat +import Ide.Plugin.Tactic.CodeGen import Ide.Plugin.Tactic.GHC -import Ide.Plugin.Tactic.Types import Ide.Plugin.Tactic.Judgements -import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Naming +import Ide.Plugin.Tactic.Types -import Name import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) ------------------------------------------------------------------------------- --- | Like 'var', but works over standard GHC 'OccName's. -var' :: Var a => OccName -> a -var' = var . fromString . occNameString - ------------------------------------------------------------------------------- --- | Like 'bvar', but works over standard GHC 'OccName's. -bvar' :: BVar a => OccName -> a -bvar' = bvar . fromString . occNameString - - ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () @@ -85,35 +69,6 @@ intros = rule $ \(Judgement hy _ g) -> $ unLoc sg ------------------------------------------------------------------------------- --- | Combinator for performign case splitting, and running sub-rules on the --- resulting matches. -destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM () -destruct' f term = rule $ \jdg@(Judgement hy _ g) -> do - case find ((== term) . fst) $ toList hy of - Nothing -> throwError $ UndefinedHypothesis term - Just (_, t) -> - case splitTyConApp_maybe $ unCType t of - Nothing -> throwError $ GoalMismatch "destruct" g - Just (tc, apps) -> do - fmap noLoc - $ case' (var' term) - <$> do - for (tyConDataCons tc) $ \dc -> do - let args = dataConInstArgTys dc apps - names <- mkManyGoodNames hy args - - let pat :: Pat GhcPs - pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) - $ fmap bvar' names - - let j = destructing term - $ introducing (zip names $ coerce args) - $ withNewGoal g jdg - sg <- f dc j - pure $ match [pat] $ unLoc sg - - ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. destruct :: OccName -> TacticsM () @@ -121,14 +76,15 @@ destruct name = do jdg <- goal case hasDestructed jdg name of True -> throwError $ AlreadyDestructed name - False -> destruct' (const subgoal) name + False -> rule $ \jdg -> destruct' (const subgoal) name jdg ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () -homo = destruct' $ \dc (Judgement hy _ (CType g)) -> - buildDataCon hy dc (snd $ splitAppTys g) +homo = rule . destruct' + (\dc (Judgement hy _ (CType g)) -> + buildDataCon hy dc (snd $ splitAppTys g)) ------------------------------------------------------------------------------ @@ -137,6 +93,7 @@ homo = destruct' $ \dc (Judgement hy _ (CType g)) -> solve :: TacticsM () -> TacticsM () solve t = t >> throwError NoProgress + ------------------------------------------------------------------------------ -- | Apply a function from the hypothesis. apply :: TacticsM () @@ -157,6 +114,7 @@ apply' func = rule $ \(Judgement hys _ g) -> $ fmap unLoc sgs Nothing -> throwError $ GoalMismatch "apply" g + applySpecific :: OccName -> CType -> Judgement -> RuleM (LHsExpr GhcPs) applySpecific func (CType ty) (Judgement hy _ _) = do let (args, _) = splitFunTys ty @@ -196,15 +154,18 @@ deepen depth = do one deepen $ depth - 1 + ------------------------------------------------------------------------------ -- | @matching f@ takes a function from a judgement to a @Tactic@, and -- then applies the resulting @Tactic@. matching :: (Judgement -> TacticsM ()) -> TacticsM () matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f $ s) s + attemptOn :: (a -> TacticsM ()) -> (Judgement -> [a]) -> TacticsM () attemptOn tac getNames = matching (choice . fmap (\s -> tac s) . getNames) + ------------------------------------------------------------------------------ -- | Automatically solve a goal. auto :: TacticsM () @@ -227,6 +188,7 @@ auto' n = do algebraicNames :: Judgement -> [OccName] algebraicNames (Judgement hys _ _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys + ------------------------------------------------------------------------------ -- | Run a tactic, and subsequently apply auto if it completes. If not, just -- run the first tactic, leaving its subgoals as holes. From b01f77f24c099c884c2b1bfb9570fe131c6b9896 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 15:49:29 -0700 Subject: [PATCH 30/64] Remove gross/unused tactics --- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 33 ------------------- 1 file changed, 33 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 98f346ae71..0936e2e9b2 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -87,20 +87,6 @@ homo = rule . destruct' buildDataCon hy dc (snd $ splitAppTys g)) ------------------------------------------------------------------------------- --- | Ensure a tactic produces no subgoals. Useful when working with --- backtracking. -solve :: TacticsM () -> TacticsM () -solve t = t >> throwError NoProgress - - ------------------------------------------------------------------------------- --- | Apply a function from the hypothesis. -apply :: TacticsM () -apply = rule $ \jdg@(Judgement hy _ g) -> do - case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of - Just (func, ty) -> applySpecific func ty jdg - Nothing -> throwError $ GoalMismatch "apply" g apply' :: OccName -> TacticsM () apply' func = rule $ \(Judgement hys _ g) -> @@ -146,14 +132,6 @@ split = rule $ \(Judgement hy _ g) -> Nothing -> throwError $ GoalMismatch "split" g ------------------------------------------------------------------------------- --- | Run 'one' many times. -deepen :: Int -> TacticsM () -deepen 0 = pure () -deepen depth = do - one - deepen $ depth - 1 - ------------------------------------------------------------------------------ -- | @matching f@ takes a function from a judgement to a @Tactic@, and @@ -189,15 +167,4 @@ auto' n = do algebraicNames (Judgement hys _ _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys ------------------------------------------------------------------------------- --- | Run a tactic, and subsequently apply auto if it completes. If not, just --- run the first tactic, leaving its subgoals as holes. -autoIfPossible :: TacticsM () -> TacticsM () -autoIfPossible t = (t >> solve auto) <|> t - - ------------------------------------------------------------------------------- --- | Do one obvious thing. -one :: TacticsM () -one = intro <|> assumption <|> split <|> apply <|> pure () From f2e9f8b97e8ab3175b82f7a79d8ac8c36d011a41 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 16:02:42 -0700 Subject: [PATCH 31/64] Make newSubgoal derive from an existing judgement --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 26 ++++++------ .../src/Ide/Plugin/Tactic/Machinery.hs | 6 +-- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 42 ++++++------------- 3 files changed, 27 insertions(+), 47 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 4923123546..c79d470062 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -1,23 +1,21 @@ module Ide.Plugin.Tactic.CodeGen where -import Data.Map (Map) +import Control.Monad.Except +import Data.List +import Data.Traversable +import DataCon +import Development.IDE.GHC.Compat import GHC.Exts import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat -import OccName -import DataCon -import Development.IDE.GHC.Compat -import Ide.Plugin.Tactic.Types -import Ide.Plugin.Tactic.Judgements -import Ide.Plugin.Tactic.Machinery -import Name +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming -import Data.Traversable +import Ide.Plugin.Tactic.Types +import Name import Type hiding (Var) -import Data.List -import Control.Monad.Except ------------------------------------------------------------------------------ @@ -52,13 +50,13 @@ destruct' f term jdg@(Judgement hy _ g) = do ------------------------------------------------------------------------------ -- | Construct a data con with subgoals for each field. buildDataCon - :: Map OccName CType -- ^ In-scope bindings + :: Judgement -> DataCon -- ^ The data con to build -> [Type] -- ^ Type arguments for the data con -> RuleM (LHsExpr GhcPs) -buildDataCon hy dc apps = do +buildDataCon jdg dc apps = do let args = dataConInstArgTys dc apps - sgs <- traverse (newSubgoal hy . CType) args + sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args pure . noLoc . foldl' (@@) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index f802bb754e..13791b1793 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -40,11 +40,9 @@ substCTy subst = coerce . substTy subst . coerce -- | Produce a subgoal that must be solved before we can solve the original -- goal. newSubgoal - :: Map OccName CType -- ^ Available bindings - -> CType -- ^ Sub-goal type + :: Judgement -> RuleM (LHsExpr GhcPs) -newSubgoal hy g = do - j <- newJudgement hy g +newSubgoal j = do unifier <- gets ts_unifier subgoal $ substJdg unifier j diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 0936e2e9b2..2248abb0e9 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -27,7 +27,6 @@ import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Types - import Refinery.Tactic import Refinery.Tactic.Internal import TcType @@ -46,23 +45,26 @@ assumption = rule $ \(Judgement hy _ g) -> ------------------------------------------------------------------------------ -- | Introduce a lambda. intro :: TacticsM () -intro = rule $ \(Judgement hy _ g) -> +intro = rule $ \jdg@(Judgement hy _ g) -> case splitFunTy_maybe $ unCType g of Just (a, b) -> do v <- pure $ mkGoodName (getInScope hy) a - sg <- newSubgoal (M.singleton v (CType a) <> hy) $ CType b + let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg + sg <- newSubgoal jdg' pure $ noLoc $ lambda [bvar' v] $ unLoc sg _ -> throwError $ GoalMismatch "intro" g + ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros :: TacticsM () -intros = rule $ \(Judgement hy _ g) -> +intros = rule $ \jdg@(Judgement hy _ g) -> case tcSplitFunTys $ unCType g of ([], _) -> throwError $ GoalMismatch "intro" g (as, b) -> do vs <- mkManyGoodNames hy as - sg <- newSubgoal (M.fromList (zip vs $ fmap CType as) <> hy) $ CType b + let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg + sg <- newSubgoal jdg' pure . noLoc . lambda (fmap bvar' vs) @@ -83,51 +85,33 @@ destruct name = do -- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () homo = rule . destruct' - (\dc (Judgement hy _ (CType g)) -> - buildDataCon hy dc (snd $ splitAppTys g)) + (\dc jdg@(Judgement _ _ (CType g)) -> + buildDataCon jdg dc (snd $ splitAppTys g)) apply' :: OccName -> TacticsM () -apply' func = rule $ \(Judgement hys _ g) -> +apply' func = rule $ \jdg@(Judgement hys _ g) -> case M.lookup func hys of Just (CType ty) -> do let (args, ret) = splitFunTys ty unify g (CType ret) - sgs <- traverse (newSubgoal hys . CType) args + sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args pure . noLoc . foldl' (@@) (var' func) $ fmap unLoc sgs Nothing -> throwError $ GoalMismatch "apply" g -applySpecific :: OccName -> CType -> Judgement -> RuleM (LHsExpr GhcPs) -applySpecific func (CType ty) (Judgement hy _ _) = do - let (args, _) = splitFunTys ty - sgs <- traverse (newSubgoal hy . CType) args - pure . noLoc - . foldl' (@@) (var' func) - $ fmap unLoc sgs - - -instantiate :: OccName -> CType -> TacticsM () -instantiate func (CType ty) = rule $ \jdg@(Judgement _ _ (CType g)) -> do - -- TODO(sandy): We need to get available from the type sig and compare - -- against _ctx - let (_binders, _ctx, tcSplitFunTys -> (_, res)) = tcSplitSigmaTy ty - unify (CType res) (CType g) - applySpecific func (CType ty) jdg - - ------------------------------------------------------------------------------ -- | Introduce a data constructor, splitting a goal into the datacon's -- constituent sub-goals. split :: TacticsM () -split = rule $ \(Judgement hy _ g) -> +split = rule $ \jdg@(Judgement _ _ g) -> case splitTyConApp_maybe $ unCType g of Just (tc, apps) -> case tyConDataCons tc of - [dc] -> buildDataCon hy dc apps + [dc] -> buildDataCon jdg dc apps _ -> throwError $ GoalMismatch "split" g Nothing -> throwError $ GoalMismatch "split" g From 90c0435bac6052ee507d01c17788c0967cc854cd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 16:06:01 -0700 Subject: [PATCH 32/64] remove newJudgement --- plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 12 ------------ plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 3 --- 2 files changed, 15 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 13791b1793..3d9928889b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -21,7 +21,6 @@ import Control.Monad.Reader import Control.Monad.State (gets, modify) import Data.Coerce import Data.Either -import Data.Map (Map) import Data.Maybe import Development.IDE.GHC.Compat import Ide.Plugin.Tactic.Judgements @@ -47,17 +46,6 @@ newSubgoal j = do subgoal $ substJdg unifier j ------------------------------------------------------------------------------- --- | Create a new judgment -newJudgement - :: Monad m - => Map OccName CType -- ^ Available bindings - -> CType -- ^ Sub-goal type - -> m Judgement -newJudgement hy g = do - pure $ Judgement hy mempty g - - ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 2248abb0e9..106897f5da 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -9,7 +9,6 @@ module Ide.Plugin.Tactic.Tactics , runTactic ) where - import Control.Applicative import Control.Monad.Except (throwError) import Control.Monad.State.Strict (StateT(..), runStateT) @@ -150,5 +149,3 @@ auto' n = do algebraicNames :: Judgement -> [OccName] algebraicNames (Judgement hys _ _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys - - From ec12dcd7b1464aff1a076811aa02632431fe8ff5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 16:13:15 -0700 Subject: [PATCH 33/64] Disallow current function from auto --- .../src/Ide/Plugin/Tactic/Judgements.hs | 5 +++++ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 18 ++++++++++++------ 2 files changed, 17 insertions(+), 6 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 944a907c45..20587ff4ec 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -52,6 +52,11 @@ introducing ns jdg@Judgement{..} = jdg { _jHypothesis = M.fromList ns <> _jHypothesis } +disallowing :: [OccName] -> Judgement' a -> Judgement' a +disallowing ns jdg@Judgement{..} = jdg + { _jHypothesis = M.withoutKeys _jHypothesis $ S.fromList ns + } + jHypothesis :: Judgement' a -> Map OccName a jHypothesis = _jHypothesis diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 106897f5da..b603bc31c3 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -21,6 +21,7 @@ import GHC.Exts import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import Ide.Plugin.Tactic.CodeGen +import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery @@ -30,6 +31,7 @@ import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) +import Control.Monad.Trans ------------------------------------------------------------------------------ @@ -130,18 +132,22 @@ attemptOn tac getNames = matching (choice . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------ -- | Automatically solve a goal. auto :: TacticsM () -auto = TacticT $ StateT $ \(Judgement _ _ goal) -> runStateT (unTacticT $ auto' 5) (Judgement mempty mempty goal) +auto = do + -- TODO(reed): there is no MonadReader instance for ProvableT + current <- TacticT $ lift $ lift $ lift getCurrentDefinitions + TacticT $ StateT $ \jdg -> + runStateT (unTacticT $ auto' 5) $ disallowing current jdg auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress auto' n = do intros <|> many_ intro choice - [ attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames - , attemptOn (\aname -> progress ((==) `on` jGoal) NoProgress (destruct aname) >> (auto' $ n - 1)) algebraicNames - , split >> (auto' $ n - 1) - , assumption >> (auto' $ n - 1) - ] + [ attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames + , attemptOn (\aname -> progress ((==) `on` jGoal) NoProgress (destruct aname) >> (auto' $ n - 1)) algebraicNames + , split >> (auto' $ n - 1) + , assumption >> (auto' $ n - 1) + ] where functionNames :: Judgement -> [OccName] functionNames (Judgement hys _ _) = M.keys $ M.filter (isFunction . unCType) hys From 8fdf25bbf16969c4e1139b7e6d17e78123c6d737 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 16:19:05 -0700 Subject: [PATCH 34/64] Cleanup auto --- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 39 +++++++++++-------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index b603bc31c3..00209e0a38 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -122,11 +122,11 @@ split = rule $ \jdg@(Judgement _ _ g) -> -- | @matching f@ takes a function from a judgement to a @Tactic@, and -- then applies the resulting @Tactic@. matching :: (Judgement -> TacticsM ()) -> TacticsM () -matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f $ s) s +matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f s) s -attemptOn :: (a -> TacticsM ()) -> (Judgement -> [a]) -> TacticsM () -attemptOn tac getNames = matching (choice . fmap (\s -> tac s) . getNames) +attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM () +attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------ @@ -141,17 +141,24 @@ auto = do auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress auto' n = do - intros <|> many_ intro - choice - [ attemptOn (\fname -> apply' fname >> (auto' $ n - 1)) functionNames - , attemptOn (\aname -> progress ((==) `on` jGoal) NoProgress (destruct aname) >> (auto' $ n - 1)) algebraicNames - , split >> (auto' $ n - 1) - , assumption >> (auto' $ n - 1) - ] - where - functionNames :: Judgement -> [OccName] - functionNames (Judgement hys _ _) = M.keys $ M.filter (isFunction . unCType) hys - - algebraicNames :: Judgement -> [OccName] - algebraicNames (Judgement hys _ _) = M.keys $ M.filter (isJust . algebraicTyCon . unCType) hys + let loop = auto' (n - 1) + intros <|> many_ intro + choice + [ attemptOn functionNames $ \fname -> do + apply' fname + loop + , attemptOn algebraicNames $ \aname -> do + progress ((==) `on` jGoal) NoProgress (destruct aname) + loop + , split >> loop + , assumption >> loop + ] + +functionNames :: Judgement -> [OccName] +functionNames = + M.keys . M.filter (isFunction . unCType) . jHypothesis + +algebraicNames :: Judgement -> [OccName] +algebraicNames = + M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis From f08bd0da7fdb94987651b56ecd314d1bfea35f81 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 21:54:32 -0700 Subject: [PATCH 35/64] Stop using the Judgement ctor --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 18 ++++---- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 4 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 3 ++ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 43 +++++++++++-------- 4 files changed, 41 insertions(+), 27 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 5a3f6969c3..6eebbf10a1 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -177,8 +177,8 @@ provide tc name plId uri range _ = do -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider -filterGoalType p tp plId uri range jdg@(Judgement _ _ (CType g)) = - case p g of +filterGoalType p tp plId uri range jdg = + case p $ unCType $ jGoal jdg of True -> tp plId uri range jdg False -> pure [] @@ -190,11 +190,13 @@ filterBindingType :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider -filterBindingType p tp plId uri range jdg@(Judgement hys _ (CType g)) = - fmap join $ for (M.toList hys) $ \(occ, CType ty) -> - case p g ty of - True -> tp occ ty plId uri range jdg - False -> pure [] +filterBindingType p tp plId uri range jdg = + let hy = jHypothesis jdg + g = jGoal jdg + in fmap join $ for (M.toList hy) $ \(occ, CType ty) -> + case p (unCType g) ty of + True -> tp occ ty plId uri range jdg + False -> pure [] data TacticParams = TacticParams @@ -233,7 +235,7 @@ judgementForHole state nfp range = runMaybeT $ do resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (amapping, b2, resulting_range, Judgement hyps mempty $ CType goal) + pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index c79d470062..1df7d3643d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -22,7 +22,9 @@ import Type hiding (Var) -- | Combinator for performign case splitting, and running sub-rules on the -- resulting matches. destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule -destruct' f term jdg@(Judgement hy _ g) = do +destruct' f term jdg = do + let hy = jHypothesis jdg + g = jGoal jdg case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term Just (_, t) -> diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 20587ff4ec..e8ab92574d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -67,3 +67,6 @@ jGoal = _jGoal substJdg :: TCvSubst -> Judgement -> Judgement substJdg subst = fmap $ coerce . substTy subst . coerce +mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType +mkFirstJudgement hy = Judgement hy mempty . CType + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 00209e0a38..fedaf26e4c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -37,7 +37,9 @@ import Control.Monad.Trans ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () -assumption = rule $ \(Judgement hy _ g) -> +assumption = rule $ \jdg -> do + let hy = jHypothesis jdg + g = jGoal jdg case find ((== g) . snd) $ toList hy of Just (v, _) -> pure $ noLoc $ var' v Nothing -> throwError $ GoalMismatch "assumption" g @@ -46,7 +48,9 @@ assumption = rule $ \(Judgement hy _ g) -> ------------------------------------------------------------------------------ -- | Introduce a lambda. intro :: TacticsM () -intro = rule $ \jdg@(Judgement hy _ g) -> +intro = rule $ \jdg -> do + let hy = jHypothesis jdg + g = jGoal jdg case splitFunTy_maybe $ unCType g of Just (a, b) -> do v <- pure $ mkGoodName (getInScope hy) a @@ -59,7 +63,9 @@ intro = rule $ \jdg@(Judgement hy _ g) -> ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros :: TacticsM () -intros = rule $ \jdg@(Judgement hy _ g) -> +intros = rule $ \jdg -> do + let hy = jHypothesis jdg + g = jGoal jdg case tcSplitFunTys $ unCType g of ([], _) -> throwError $ GoalMismatch "intro" g (as, b) -> do @@ -85,30 +91,31 @@ destruct name = do ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () -homo = rule . destruct' - (\dc jdg@(Judgement _ _ (CType g)) -> - buildDataCon jdg dc (snd $ splitAppTys g)) - +homo = rule . destruct' (\dc jdg -> + buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) apply' :: OccName -> TacticsM () -apply' func = rule $ \jdg@(Judgement hys _ g) -> - case M.lookup func hys of - Just (CType ty) -> do - let (args, ret) = splitFunTys ty - unify g (CType ret) - sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args - pure . noLoc - . foldl' (@@) (var' func) - $ fmap unLoc sgs - Nothing -> throwError $ GoalMismatch "apply" g +apply' func = rule $ \jdg -> do + let hy = jHypothesis jdg + g = jGoal jdg + case M.lookup func hy of + Just (CType ty) -> do + let (args, ret) = splitFunTys ty + unify g (CType ret) + sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args + pure . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs + Nothing -> throwError $ GoalMismatch "apply" g ------------------------------------------------------------------------------ -- | Introduce a data constructor, splitting a goal into the datacon's -- constituent sub-goals. split :: TacticsM () -split = rule $ \jdg@(Judgement _ _ g) -> +split = rule $ \jdg -> do + let g = jGoal jdg case splitTyConApp_maybe $ unCType g of Just (tc, apps) -> case tyConDataCons tc of From 92c697c9ed72efe0b1b387372a143bd0d7a2ab41 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 28 Sep 2020 22:02:56 -0700 Subject: [PATCH 36/64] Track pattern value --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 19 ++++++++++++++++++- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 2 +- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 3 +++ 4 files changed, 23 insertions(+), 3 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 1df7d3643d..7abd7bf2c9 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -43,7 +43,7 @@ destruct' f term jdg = do $ fmap bvar' names let j = destructing term - $ introducing (zip names $ coerce args) + $ introducingPat (zip names $ coerce args) $ withNewGoal g jdg sg <- f dc j pure $ match [pat] $ unLoc sg diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index e8ab92574d..51c1cef988 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -52,6 +52,15 @@ introducing ns jdg@Judgement{..} = jdg { _jHypothesis = M.fromList ns <> _jHypothesis } +------------------------------------------------------------------------------ +-- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals. +introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a +introducingPat ns jdg@Judgement{..} = jdg + { _jHypothesis = M.fromList ns <> _jHypothesis + , _jPatternVals = S.fromList (fmap fst ns) <> _jPatternVals + } + + disallowing :: [OccName] -> Judgement' a -> Judgement' a disallowing ns jdg@Judgement{..} = jdg { _jHypothesis = M.withoutKeys _jHypothesis $ S.fromList ns @@ -60,6 +69,14 @@ disallowing ns jdg@Judgement{..} = jdg jHypothesis :: Judgement' a -> Map OccName a jHypothesis = _jHypothesis + +------------------------------------------------------------------------------ +-- | Only the hypothesis members which are pattern vals +jPatHypothesis :: Judgement' a -> Map OccName a +jPatHypothesis jdg + = M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg + + jGoal :: Judgement' a -> a jGoal = _jGoal @@ -68,5 +85,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement substJdg subst = fmap $ coerce . substTy subst . coerce mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType -mkFirstJudgement hy = Judgement hy mempty . CType +mkFirstJudgement hy = Judgement hy mempty mempty . CType diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index fedaf26e4c..0180093ba2 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -12,6 +12,7 @@ module Ide.Plugin.Tactic.Tactics import Control.Applicative import Control.Monad.Except (throwError) import Control.Monad.State.Strict (StateT(..), runStateT) +import Control.Monad.Trans import Data.Function import Data.List import qualified Data.Map as M @@ -31,7 +32,6 @@ import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) -import Control.Monad.Trans ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index f838b7d674..2d2c583f21 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -82,6 +82,9 @@ instance Monoid TacticState where data Judgement' a = Judgement { _jHypothesis :: Map OccName a , _jDestructed :: Set OccName + -- ^ These should align with keys of _jHypothesis + , _jPatternVals :: Set OccName + -- ^ These should align with keys of _jHypothesis , _jGoal :: a } deriving stock (Eq, Ord, Generic, Functor) From a175ff20eb656a21f0b0ba72a911fb0046eea9ae Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 29 Sep 2020 02:26:03 -0700 Subject: [PATCH 37/64] Better showAstData --- .../tactics/src/Ide/Plugin/Tactic/Debug.hs | 164 +++++++++++++++++- 1 file changed, 162 insertions(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs index 87b4a1c17c..0b20ec1548 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs @@ -1,13 +1,35 @@ +{-# LANGUAGE ScopedTypeVariables #-} + module Ide.Plugin.Tactic.Debug - ( module Ide.Plugin.Tactic.Debug + ( unsafeRender + , unsafeRender' + , showAstData + , BlankSrcSpan (..) , traceM , traceShowId , trace ) where +import Prelude hiding ((<>)) import Debug.Trace import DynFlags (unsafeGlobalDynFlags) -import Outputable hiding ((<>)) + +import Data.Data hiding (Fixity) +import Bag +import BasicTypes +import FastString +import NameSet +import Name +import DataCon +import SrcLoc +import HsSyn +import OccName hiding (occName) +import Var +import Module +import Outputable +import qualified Data.ByteString as B +import Generics.SYB hiding (Fixity, empty) +import Id ------------------------------------------------------------------------------ -- | Print something @@ -17,3 +39,141 @@ unsafeRender = unsafeRender' . ppr unsafeRender' :: SDoc -> String unsafeRender' = showSDoc unsafeGlobalDynFlags + + + +data BlankSrcSpan = BlankSrcSpan | NoBlankSrcSpan + deriving (Eq,Show) + +-- | Show a GHC syntax tree. This parameterised because it is also used for +-- comparing ASTs in ppr roundtripping tests, where the SrcSpan's are blanked +-- out, to avoid comparing locations, only structure +-- +-- ripped out of GHC so that I could make it print the types of ids +showAstData :: Data a => BlankSrcSpan -> a -> SDoc +showAstData b a0 = blankLine $$ showAstData' a0 + where + showAstData' :: Data a => a -> SDoc + showAstData' = + generic + `ext1Q` list + `extQ` string `extQ` fastString `extQ` srcSpan + `extQ` lit `extQ` litr `extQ` litt + `extQ` bytestring + `extQ` name `extQ` occName `extQ` moduleName `extQ` var + `extQ` dataCon + `extQ` bagName `extQ` bagRdrName `extQ` bagVar `extQ` nameSet + `extQ` fixity + `ext2Q` located + + where generic :: Data a => a -> SDoc + generic t = parens $ text (showConstr (toConstr t)) + $$ vcat (gmapQ showAstData' t) + + string :: String -> SDoc + string = text . normalize_newlines . show + + fastString :: FastString -> SDoc + fastString s = braces $ + text "FastString: " + <> text (normalize_newlines . show $ s) + + bytestring :: B.ByteString -> SDoc + bytestring = text . normalize_newlines . show + + list [] = brackets empty + list [x] = brackets (showAstData' x) + list (x1 : x2 : xs) = (text "[" <> showAstData' x1) + $$ go x2 xs + where + go y [] = text "," <> showAstData' y <> text "]" + go y1 (y2 : ys) = (text "," <> showAstData' y1) $$ go y2 ys + + -- Eliminate word-size dependence + lit :: HsLit GhcPs -> SDoc + lit (HsWordPrim s x) = numericLit "HsWord{64}Prim" x s + lit (HsWord64Prim s x) = numericLit "HsWord{64}Prim" x s + lit (HsIntPrim s x) = numericLit "HsInt{64}Prim" x s + lit (HsInt64Prim s x) = numericLit "HsInt{64}Prim" x s + lit l = generic l + + litr :: HsLit GhcRn -> SDoc + litr (HsWordPrim s x) = numericLit "HsWord{64}Prim" x s + litr (HsWord64Prim s x) = numericLit "HsWord{64}Prim" x s + litr (HsIntPrim s x) = numericLit "HsInt{64}Prim" x s + litr (HsInt64Prim s x) = numericLit "HsInt{64}Prim" x s + litr l = generic l + + litt :: HsLit GhcTc -> SDoc + litt (HsWordPrim s x) = numericLit "HsWord{64}Prim" x s + litt (HsWord64Prim s x) = numericLit "HsWord{64}Prim" x s + litt (HsIntPrim s x) = numericLit "HsInt{64}Prim" x s + litt (HsInt64Prim s x) = numericLit "HsInt{64}Prim" x s + litt l = generic l + + numericLit :: String -> Integer -> SourceText -> SDoc + numericLit tag x s = braces $ hsep [ text tag + , generic x + , generic s ] + + name :: Name -> SDoc + name nm = braces $ text "Name: " <> ppr nm + + occName n = braces $ + text "OccName: " + <> text (OccName.occNameString n) + + moduleName :: ModuleName -> SDoc + moduleName m = braces $ text "ModuleName: " <> ppr m + + srcSpan :: SrcSpan -> SDoc + srcSpan ss = case b of + BlankSrcSpan -> text "{ ss }" + NoBlankSrcSpan -> braces $ char ' ' <> + (hang (ppr ss) 1 + -- TODO: show annotations here + (text "")) + + var :: Var -> SDoc + var v = braces $ text "Var: " <> ppr v <> text " (" <> ppr (idType v) <> text ")" + + dataCon :: DataCon -> SDoc + dataCon c = braces $ text "DataCon: " <> ppr c + + bagRdrName:: Bag (Located (HsBind GhcPs)) -> SDoc + bagRdrName bg = braces $ + text "Bag(Located (HsBind GhcPs)):" + $$ (list . bagToList $ bg) + + bagName :: Bag (Located (HsBind GhcRn)) -> SDoc + bagName bg = braces $ + text "Bag(Located (HsBind Name)):" + $$ (list . bagToList $ bg) + + bagVar :: Bag (Located (HsBind GhcTc)) -> SDoc + bagVar bg = braces $ + text "Bag(Located (HsBind Var)):" + $$ (list . bagToList $ bg) + + nameSet ns = braces $ + text "NameSet:" + $$ (list . nameSetElemsStable $ ns) + + fixity :: Fixity -> SDoc + fixity fx = braces $ + text "Fixity: " + <> ppr fx + + located :: (Data b,Data loc) => GenLocated loc b -> SDoc + located (L ss a) = parens $ + case cast ss of + Just (s :: SrcSpan) -> + srcSpan s + Nothing -> text "nnnnnnnn" + $$ showAstData' a + +normalize_newlines :: String -> String +normalize_newlines ('\\':'r':'\\':'n':xs) = '\\':'n':normalize_newlines xs +normalize_newlines (x:xs) = x:normalize_newlines xs +normalize_newlines [] = [] + From e7061f118c3b1955ac23383246d24b7c46d6321b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 29 Sep 2020 02:37:49 -0700 Subject: [PATCH 38/64] Get module-scoped funcs --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 25 +++++++------ .../tactics/src/Ide/Plugin/Tactic/Context.hs | 35 +++++++++++++++++-- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 2 ++ 3 files changed, 49 insertions(+), 13 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 6eebbf10a1..79b2f80472 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -1,10 +1,11 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} -- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic @@ -220,8 +221,7 @@ judgementForHole state nfp range = runMaybeT $ do range' <- liftMaybe $ fromCurrentRange amapping range (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp - (har, _) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp - let b2 = bindSites $ refMap har + let b2 = bindSites $ refMap asts (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of @@ -238,6 +238,7 @@ judgementForHole state nfp range = runMaybeT $ do pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal) + tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = @@ -247,11 +248,15 @@ tacticCmd tac lf state (TacticParams uri range var_name) -- which don't change very often. (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp range' <- liftMaybe $ toCurrentRange pos range + (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' -- TODO(sandy): unclear if this span is correct; might be -- pointing to the wrong version of the file dflags = hsc_dflags $ hscEnv hscenv - ctx = mkContext $ mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings b2 span + tcg = fst $ tm_internals_ $ tmrModule tcmod + ctx = mkContext + (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings b2 span) + tcg pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic ctx jdg $ tac diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs index caebc8bc5e..f1cccae928 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs @@ -1,13 +1,42 @@ {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} module Ide.Plugin.Tactic.Context where +import Bag +import Control.Arrow +import Control.Monad.Reader +import Development.IDE.GHC.Compat import Ide.Plugin.Tactic.Types -import Control.Monad.Reader +import OccName +import TcRnTypes + + +mkContext :: [(OccName, CType)] -> TcGblEnv -> Context +mkContext locals + = Context locals + . fmap splitId + . (getFunBindId =<<) + . fmap unLoc + . bagToList + . tcg_binds + + +splitId :: Id -> (OccName, CType) +splitId = occName &&& CType . idType + + +getFunBindId :: HsBindLR GhcTc GhcTc -> [Id] +getFunBindId (AbsBinds _ _ _ abes _ _ _) + = abes >>= \case + ABE _ poly _ _ _ -> pure poly + _ -> [] +getFunBindId _ = [] -mkContext :: [(OccName, CType)] -> Context -mkContext = Context getCurrentDefinitions :: MonadReader Context m => m [OccName] getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs +getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)] +getModuleHypothesis = asks ctxModuleFuncs + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 2d2c583f21..ec400428d5 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -149,6 +149,8 @@ type Rule = RuleM (LHsExpr GhcPs) data Context = Context { ctxDefiningFuncs :: [(OccName, CType)] -- ^ The functions currently being defined + , ctxModuleFuncs :: [(OccName, CType)] + -- ^ Everything defined in the current module } deriving stock (Eq, Ord) From 44e6bfcbd5f9ec15bcb963507aea2432fe91ee91 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 29 Sep 2020 20:20:32 -0700 Subject: [PATCH 39/64] Split all data constructors --- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 27 +++++++++++++------ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 7 +++-- 2 files changed, 24 insertions(+), 10 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 0180093ba2..eea6bf2373 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -111,18 +111,29 @@ apply' func = rule $ \jdg -> do ------------------------------------------------------------------------------ --- | Introduce a data constructor, splitting a goal into the datacon's --- constituent sub-goals. +-- | Choose between each of the goal's data constructors. split :: TacticsM () -split = rule $ \jdg -> do +split = do + jdg <- goal let g = jGoal jdg case splitTyConApp_maybe $ unCType g of - Just (tc, apps) -> - case tyConDataCons tc of - [dc] -> buildDataCon jdg dc apps - _ -> throwError $ GoalMismatch "split" g - Nothing -> throwError $ GoalMismatch "split" g + Nothing -> throwError $ GoalMismatch "getGoalTyCon" g + Just (tc, _) -> do + let dcs = tyConDataCons tc + choice $ fmap splitDataCon dcs + +------------------------------------------------------------------------------ +-- | Attempt to instantiate the given data constructor to solve the goal. +splitDataCon :: DataCon -> TacticsM () +splitDataCon dc = rule $ \jdg -> do + let g = jGoal jdg + case splitTyConApp_maybe $ unCType g of + Just (tc, apps) -> do + case elem dc $ tyConDataCons tc of + True -> buildDataCon jdg dc apps + False -> throwError $ IncorrectDataCon dc + Nothing -> throwError $ GoalMismatch "splitDataCon" g ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index ec400428d5..6fb9ccb5f2 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -108,7 +108,8 @@ data TacticError | NoProgress | NoApplicableTactic | AlreadyDestructed OccName - deriving stock (Eq, Ord) + | IncorrectDataCon DataCon + deriving stock (Eq) instance Show TacticError where show (UndefinedHypothesis name) = @@ -134,7 +135,9 @@ instance Show TacticError where show NoApplicableTactic = "No tactic could be applied" show (AlreadyDestructed name) = - "Aleady destructed " <> unsafeRender name + "Already destructed " <> unsafeRender name + show (IncorrectDataCon dcon) = + "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")" ------------------------------------------------------------------------------ From fdbb9f41fb41ef4cd74974d2622aa91b3aaccedb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 29 Sep 2020 20:35:22 -0700 Subject: [PATCH 40/64] assumption -> assume --- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 25 ++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index eea6bf2373..50a2db5b46 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -34,8 +34,10 @@ import TcType import Type hiding (Var) + ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. +-- TODO(sandy): deprecate this assumption :: TacticsM () assumption = rule $ \jdg -> do let hy = jHypothesis jdg @@ -45,6 +47,19 @@ assumption = rule $ \jdg -> do Nothing -> throwError $ GoalMismatch "assumption" g +------------------------------------------------------------------------------ +-- | Use something named in the hypothesis to fill the hole. +assume :: OccName -> TacticsM () +assume name = rule $ \jdg -> do + let g = jGoal jdg + case M.lookup name $ jHypothesis jdg of + Just ty -> + case ty == jGoal jdg of + True -> pure $ noLoc $ var' name + False -> throwError $ GoalMismatch "assume" g + Nothing -> throwError $ UndefinedHypothesis name + + ------------------------------------------------------------------------------ -- | Introduce a lambda. intro :: TacticsM () @@ -169,14 +184,22 @@ auto' n = do progress ((==) `on` jGoal) NoProgress (destruct aname) loop , split >> loop - , assumption >> loop + , attemptOn allNames $ \name -> do + assume name + loop ] + functionNames :: Judgement -> [OccName] functionNames = M.keys . M.filter (isFunction . unCType) . jHypothesis + algebraicNames :: Judgement -> [OccName] algebraicNames = M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis + +allNames :: Judgement -> [OccName] +allNames = M.keys . jHypothesis + From cc5fcbd39b5e4732f4d521a8e53d77e69f99083a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 29 Sep 2020 20:49:28 -0700 Subject: [PATCH 41/64] Don't destruct if there are zero datacons --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 7abd7bf2c9..58c2b17211 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -30,23 +30,23 @@ destruct' f term jdg = do Just (_, t) -> case splitTyConApp_maybe $ unCType t of Nothing -> throwError $ GoalMismatch "destruct" g - Just (tc, apps) -> do - fmap noLoc - $ case' (var' term) - <$> do - for (tyConDataCons tc) $ \dc -> do - let args = dataConInstArgTys dc apps - names <- mkManyGoodNames hy args + Just (tc, apps) -> + fmap noLoc $ case' (var' term) <$> do + let dcs = tyConDataCons tc + case dcs of + [] -> throwError $ GoalMismatch "destruct" g + _ -> for dcs $ \dc -> do + let args = dataConInstArgTys dc apps + names <- mkManyGoodNames hy args - let pat :: Pat GhcPs - pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) - $ fmap bvar' names - - let j = destructing term - $ introducingPat (zip names $ coerce args) - $ withNewGoal g jdg - sg <- f dc j - pure $ match [pat] $ unLoc sg + let pat :: Pat GhcPs + pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) + $ fmap bvar' names + j = destructing term + $ introducingPat (zip names $ coerce args) + $ withNewGoal g jdg + sg <- f dc j + pure $ match [pat] $ unLoc sg ------------------------------------------------------------------------------ From 84d47cda8c31e66c461348397390505e6526cbdd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 07:09:41 -0700 Subject: [PATCH 42/64] Lambda case destruct tactics --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 69 +++++++++++-------- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 66 +++++++++++++----- plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 13 ++++ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 13 ++++ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 8 +-- 5 files changed, 117 insertions(+), 52 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 79b2f80472..f214404f2b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -31,11 +31,11 @@ import Development.IDE.Core.Service (runAction) import Development.IDE.Core.Shake (useWithStale, IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (realSrcSpanToRange) -import Development.IDE.GHC.Util (hscEnv) import Development.Shake (Action) +import DynFlags (xopt) import qualified FastString import GHC.Generics (Generic) -import HscTypes (hsc_dflags) +import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.BindSites import Ide.Plugin.Tactic.Context @@ -59,22 +59,17 @@ descriptor plId = (defaultPluginDescriptor plId) (tcCommandId tc) (tacticDesc $ tcCommandName tc) (tacticCmd $ commandTactic tc)) - enabledTactics + [minBound .. maxBound] , pluginCodeActionProvider = Just codeActionProvider } tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" ------------------------------------------------------------------------------- - -enabledTactics :: [TacticCommand] -enabledTactics = [Intros, Destruct, Homomorphism, Auto] - ------------------------------------------------------------------------------ -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS -- UI. -type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] ------------------------------------------------------------------------------ @@ -93,10 +88,6 @@ tcCommandName = T.pack . show -- 'filterGoalType' and 'filterBindingType' for the nitty gritty. commandProvider :: TacticCommand -> TacticProvider commandProvider Auto = provide Auto "" -commandProvider Split = provide Split "" -commandProvider Intro = - filterGoalType isFunction $ - provide Intro "" commandProvider Intros = filterGoalType isFunction $ provide Intros "" @@ -106,17 +97,25 @@ commandProvider Destruct = commandProvider Homomorphism = filterBindingType homoFilter $ \occ _ -> provide Homomorphism $ T.pack $ occNameString occ +commandProvider DestructLambdaCase = + requireExtension LambdaCase $ + filterGoalType (isJust . lambdaCaseable) $ + provide DestructLambdaCase "" +commandProvider HomomorphismLambdaCase = + requireExtension LambdaCase $ + filterGoalType ((== Just True) . lambdaCaseable) $ + provide HomomorphismLambdaCase "" ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto -commandTactic Split = const split -commandTactic Intro = const intro commandTactic Intros = const intros commandTactic Destruct = destruct commandTactic Homomorphism = homo +commandTactic DestructLambdaCase = const destructLambdaCase +commandTactic HomomorphismLambdaCase = const homoLambdaCase ------------------------------------------------------------------------------ @@ -143,10 +142,11 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right $ List []) $ do - (_, _, span, jdg) <- MaybeT $ judgementForHole state nfp range + (_, _, span, jdg, dflags) <- MaybeT $ judgementForHole state nfp range actions <- lift $ -- This foldMap is over the function monoid. - foldMap commandProvider enabledTactics + foldMap commandProvider [minBound .. maxBound] + dflags plId uri span @@ -163,7 +163,7 @@ codeActions = List . fmap CACodeAction -- | Terminal constructor for providing context-sensitive tactics. Tactics -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider -provide tc name plId uri range _ = do +provide tc name _ plId uri range _ = do let title = tacticTitle tc name params = TacticParams { file = uri , range = range , var_name = name } cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params]) @@ -174,13 +174,23 @@ provide tc name plId uri range _ = do $ Just cmd +------------------------------------------------------------------------------ +-- | Restrict a 'TacticProvider', making sure it appears only when the given +-- predicate holds for the goal. +requireExtension :: Extension -> TacticProvider -> TacticProvider +requireExtension ext tp dflags plId uri range jdg = + case xopt ext dflags of + True -> tp dflags plId uri range jdg + False -> pure [] + + ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider -filterGoalType p tp plId uri range jdg = +filterGoalType p tp dflags plId uri range jdg = case p $ unCType $ jGoal jdg of - True -> tp plId uri range jdg + True -> tp dflags plId uri range jdg False -> pure [] @@ -191,12 +201,12 @@ filterBindingType :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider -filterBindingType p tp plId uri range jdg = +filterBindingType p tp dflags plId uri range jdg = let hy = jHypothesis jdg g = jGoal jdg in fmap join $ for (M.toList hy) $ \(occ, CType ty) -> case p (unCType g) ty of - True -> tp occ ty plId uri range jdg + True -> tp occ ty dflags plId uri range jdg False -> pure [] @@ -215,7 +225,7 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (Maybe (PositionMapping, BindSites, Range, Judgement)) + -> IO (Maybe (PositionMapping, BindSites, Range, Judgement, DynFlags)) judgementForHole state nfp range = runMaybeT $ do (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp range' <- liftMaybe $ fromCurrentRange amapping range @@ -223,6 +233,11 @@ judgementForHole state nfp range = runMaybeT $ do (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp let b2 = bindSites $ refMap asts + -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' + -- which don't change very often. + (modsum, _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp + let dflags = ms_hspp_opts modsum + (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of Nothing -> Nothing @@ -235,7 +250,7 @@ judgementForHole state nfp range = runMaybeT $ do resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal) + pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal, dflags) @@ -243,16 +258,12 @@ tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do - (pos, b2, _, jdg) <- MaybeT $ judgementForHole state nfp range - -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' - -- which don't change very often. - (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp + (pos, b2, _, jdg, dflags) <- MaybeT $ judgementForHole state nfp range range' <- liftMaybe $ toCurrentRange pos range (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' -- TODO(sandy): unclear if this span is correct; might be -- pointing to the wrong version of the file - dflags = hsc_dflags $ hscEnv hscenv tcg = fst $ tm_internals_ $ tmrModule tcmod ctx = mkContext (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings b2 span) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 58c2b17211..8e4b40b15e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE FlexibleContexts #-} module Ide.Plugin.Tactic.CodeGen where import Control.Monad.Except @@ -18,35 +19,62 @@ import Name import Type hiding (Var) +destructMatches + :: (DataCon -> Judgement -> Rule) + -- ^ How to construct each match + -> (Judgement -> Judgement) + -- ^ How to derive each match judgement + -> CType + -- ^ Type being destructed + -> Judgement + -> RuleM [RawMatch] +destructMatches f f2 t jdg = do + let hy = jHypothesis jdg + g = jGoal jdg + case splitTyConApp_maybe $ unCType t of + Nothing -> throwError $ GoalMismatch "destruct" g + Just (tc, apps) -> do + let dcs = tyConDataCons tc + case dcs of + [] -> throwError $ GoalMismatch "destruct" g + _ -> for dcs $ \dc -> do + let args = dataConInstArgTys dc apps + names <- mkManyGoodNames hy args + + let pat :: Pat GhcPs + pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) + $ fmap bvar' names + j = f2 + $ introducingPat (zip names $ coerce args) + $ withNewGoal g jdg + sg <- f dc j + pure $ match [pat] $ unLoc sg + + ------------------------------------------------------------------------------ -- | Combinator for performign case splitting, and running sub-rules on the -- resulting matches. destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule destruct' f term jdg = do let hy = jHypothesis jdg - g = jGoal jdg case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term Just (_, t) -> - case splitTyConApp_maybe $ unCType t of - Nothing -> throwError $ GoalMismatch "destruct" g - Just (tc, apps) -> - fmap noLoc $ case' (var' term) <$> do - let dcs = tyConDataCons tc - case dcs of - [] -> throwError $ GoalMismatch "destruct" g - _ -> for dcs $ \dc -> do - let args = dataConInstArgTys dc apps - names <- mkManyGoodNames hy args + fmap noLoc $ case' (var' term) <$> + destructMatches f (destructing term) t jdg + - let pat :: Pat GhcPs - pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) - $ fmap bvar' names - j = destructing term - $ introducingPat (zip names $ coerce args) - $ withNewGoal g jdg - sg <- f dc j - pure $ match [pat] $ unLoc sg +------------------------------------------------------------------------------ +-- | Combinator for performign case splitting, and running sub-rules on the +-- resulting matches. +destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule +destructLambdaCase' f jdg = do + let g = jGoal jdg + case splitFunTy_maybe (unCType g) of + Just (arg, _) | isAlgType arg -> + fmap noLoc $ lambdaCase <$> + destructMatches f id (CType arg) jdg + _ -> throwError $ GoalMismatch "destructLambdaCase'" g ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index 7ceec5801d..9d1c34851b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -2,6 +2,7 @@ module Ide.Plugin.Tactic.GHC where +import Data.Maybe (isJust) import TcType import TyCoRep import TyCon @@ -54,3 +55,15 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) | otherwise = Just tycon algebraicTyCon _ = Nothing +------------------------------------------------------------------------------ +-- | Can ths type be lambda-cased? +-- +-- Return: 'Nothing' if no +-- @Just False@ if it can't be homomorphic +-- @Just True@ if it can +lambdaCaseable :: Type -> Maybe Bool +lambdaCaseable (splitFunTy_maybe -> Just (arg, res)) + | isJust (algebraicTyCon arg) + = Just $ isJust $ algebraicTyCon res +lambdaCaseable _ = Nothing + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 50a2db5b46..59ff84f724 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -110,6 +110,19 @@ homo = rule . destruct' (\dc jdg -> buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) +------------------------------------------------------------------------------ +-- | LambdaCase split, and leave holes in the matches. +destructLambdaCase :: TacticsM () +destructLambdaCase = rule $ destructLambdaCase' (const subgoal) + + +------------------------------------------------------------------------------ +-- | LambdaCase split, using the same data constructor in the matches. +homoLambdaCase :: TacticsM () +homoLambdaCase = rule $ destructLambdaCase' (\dc jdg -> + buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) + + apply' :: OccName -> TacticsM () apply' func = rule $ \jdg -> do let hy = jHypothesis jdg diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 6fb9ccb5f2..b5d56b69bd 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -37,21 +37,21 @@ import Type -- editor via 'commandProvider'. data TacticCommand = Auto - | Split - | Intro | Intros | Destruct | Homomorphism + | DestructLambdaCase + | HomomorphismLambdaCase deriving (Eq, Ord, Show, Enum, Bounded) -- | Generate a title for the command. tacticTitle :: TacticCommand -> T.Text -> T.Text tacticTitle Auto _ = "Auto" -tacticTitle Split _ = "Auto" -tacticTitle Intro _ = "Intro" tacticTitle Intros _ = "Introduce lambda" tacticTitle Destruct var = "Case split on " <> var tacticTitle Homomorphism var = "Homomorphic case split on " <> var +tacticTitle DestructLambdaCase _ = "Lambda case split" +tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split" ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. From 7a023b282344c46dab724eaf72d434e3057c3da4 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 07:28:12 -0700 Subject: [PATCH 43/64] Fix the tests --- haskell-language-server.cabal | 6 ++- plugins/tactics/src/Ide/Plugin/Tactic.hs | 1 + .../src/Ide/Plugin/Tactic/TestTypes.hs | 27 +++++++++++ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 46 +++++-------------- test/functional/Tactic.hs | 2 +- 5 files changed, 44 insertions(+), 38 deletions(-) create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 39c67e3bdd..f4a3bd3507 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -104,6 +104,7 @@ executable haskell-language-server Ide.Plugin.Tactic.Range Ide.Plugin.Tactic.Tactics Ide.Plugin.Tactic.Types + Ide.Plugin.Tactic.TestTypes Ide.TreeTransform ghc-options: @@ -246,7 +247,8 @@ test-suite func-test , tasty-golden , tasty-rerun - hs-source-dirs: test/functional + hs-source-dirs: test/functional plugins/tactics/src + main-is: Main.hs other-modules: Command @@ -267,7 +269,7 @@ test-suite func-test Symbol TypeDefinition Tactic - Ide.Plugin.Tactic.Types + Ide.Plugin.Tactic.TestTypes ghc-options: -Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index f214404f2b..062ff74663 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -44,6 +44,7 @@ import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Tactics import Ide.Plugin.Tactic.Types +import Ide.Plugin.Tactic.TestTypes import Ide.TreeTransform (transform, graft, useAnnotatedSource) import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs new file mode 100644 index 0000000000..a5bbde06dd --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Ide.Plugin.Tactic.TestTypes where + +import qualified Data.Text as T + +------------------------------------------------------------------------------ +-- | The list of tactics exposed to the outside world. These are attached to +-- actual tactics via 'commandTactic' and are contextually provided to the +-- editor via 'commandProvider'. +data TacticCommand + = Auto + | Intros + | Destruct + | Homomorphism + | DestructLambdaCase + | HomomorphismLambdaCase + deriving (Eq, Ord, Show, Enum, Bounded) + +-- | Generate a title for the command. +tacticTitle :: TacticCommand -> T.Text -> T.Text +tacticTitle Auto _ = "Auto" +tacticTitle Intros _ = "Introduce lambda" +tacticTitle Destruct var = "Case split on " <> var +tacticTitle Homomorphism var = "Homomorphic case split on " <> var +tacticTitle DestructLambdaCase _ = "Lambda case split" +tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split" diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index b5d56b69bd..2e3678d373 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -3,7 +3,6 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeSynonymInstances #-} module Ide.Plugin.Tactic.Types @@ -17,42 +16,19 @@ module Ide.Plugin.Tactic.Types , Range ) where -import Control.Monad.Reader -import Data.Function -import Data.Map (Map) -import Data.Set (Set) -import qualified Data.Text as T -import Development.IDE.GHC.Compat -import Development.IDE.Types.Location -import GHC.Generics -import Ide.Plugin.Tactic.Debug -import OccName -import Refinery.Tactic -import Type +import Control.Monad.Reader +import Data.Function +import Data.Map (Map) +import Data.Set (Set) +import Development.IDE.GHC.Compat +import Development.IDE.Types.Location +import GHC.Generics +import Ide.Plugin.Tactic.Debug +import OccName +import Refinery.Tactic +import Type ------------------------------------------------------------------------------- --- | The list of tactics exposed to the outside world. These are attached to --- actual tactics via 'commandTactic' and are contextually provided to the --- editor via 'commandProvider'. -data TacticCommand - = Auto - | Intros - | Destruct - | Homomorphism - | DestructLambdaCase - | HomomorphismLambdaCase - deriving (Eq, Ord, Show, Enum, Bounded) - --- | Generate a title for the command. -tacticTitle :: TacticCommand -> T.Text -> T.Text -tacticTitle Auto _ = "Auto" -tacticTitle Intros _ = "Introduce lambda" -tacticTitle Destruct var = "Case split on " <> var -tacticTitle Homomorphism var = "Homomorphic case split on " <> var -tacticTitle DestructLambdaCase _ = "Lambda case split" -tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split" - ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type } diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 17ca8e3843..87b34d6938 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -22,7 +22,7 @@ import Test.Hls.Util import Test.Tasty import Test.Tasty.HUnit import Data.Maybe (mapMaybe) -import Ide.Plugin.Tactic.Types (tacticTitle, TacticCommand (..)) +import Ide.Plugin.Tactic.TestTypes (tacticTitle, TacticCommand (..)) ------------------------------------------------------------------------------ From 53ac0d563b23a7c37425ff1e12bccfe858e5c570 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 07:35:25 -0700 Subject: [PATCH 44/64] Rip out debug stuff since it fails CI --- .../tactics/src/Ide/Plugin/Tactic/Debug.hs | 159 ------------------ 1 file changed, 159 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs index 0b20ec1548..6d1053c2c6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs @@ -1,35 +1,14 @@ -{-# LANGUAGE ScopedTypeVariables #-} - module Ide.Plugin.Tactic.Debug ( unsafeRender , unsafeRender' - , showAstData - , BlankSrcSpan (..) , traceM , traceShowId , trace ) where -import Prelude hiding ((<>)) import Debug.Trace import DynFlags (unsafeGlobalDynFlags) - -import Data.Data hiding (Fixity) -import Bag -import BasicTypes -import FastString -import NameSet -import Name -import DataCon -import SrcLoc -import HsSyn -import OccName hiding (occName) -import Var -import Module import Outputable -import qualified Data.ByteString as B -import Generics.SYB hiding (Fixity, empty) -import Id ------------------------------------------------------------------------------ -- | Print something @@ -39,141 +18,3 @@ unsafeRender = unsafeRender' . ppr unsafeRender' :: SDoc -> String unsafeRender' = showSDoc unsafeGlobalDynFlags - - - -data BlankSrcSpan = BlankSrcSpan | NoBlankSrcSpan - deriving (Eq,Show) - --- | Show a GHC syntax tree. This parameterised because it is also used for --- comparing ASTs in ppr roundtripping tests, where the SrcSpan's are blanked --- out, to avoid comparing locations, only structure --- --- ripped out of GHC so that I could make it print the types of ids -showAstData :: Data a => BlankSrcSpan -> a -> SDoc -showAstData b a0 = blankLine $$ showAstData' a0 - where - showAstData' :: Data a => a -> SDoc - showAstData' = - generic - `ext1Q` list - `extQ` string `extQ` fastString `extQ` srcSpan - `extQ` lit `extQ` litr `extQ` litt - `extQ` bytestring - `extQ` name `extQ` occName `extQ` moduleName `extQ` var - `extQ` dataCon - `extQ` bagName `extQ` bagRdrName `extQ` bagVar `extQ` nameSet - `extQ` fixity - `ext2Q` located - - where generic :: Data a => a -> SDoc - generic t = parens $ text (showConstr (toConstr t)) - $$ vcat (gmapQ showAstData' t) - - string :: String -> SDoc - string = text . normalize_newlines . show - - fastString :: FastString -> SDoc - fastString s = braces $ - text "FastString: " - <> text (normalize_newlines . show $ s) - - bytestring :: B.ByteString -> SDoc - bytestring = text . normalize_newlines . show - - list [] = brackets empty - list [x] = brackets (showAstData' x) - list (x1 : x2 : xs) = (text "[" <> showAstData' x1) - $$ go x2 xs - where - go y [] = text "," <> showAstData' y <> text "]" - go y1 (y2 : ys) = (text "," <> showAstData' y1) $$ go y2 ys - - -- Eliminate word-size dependence - lit :: HsLit GhcPs -> SDoc - lit (HsWordPrim s x) = numericLit "HsWord{64}Prim" x s - lit (HsWord64Prim s x) = numericLit "HsWord{64}Prim" x s - lit (HsIntPrim s x) = numericLit "HsInt{64}Prim" x s - lit (HsInt64Prim s x) = numericLit "HsInt{64}Prim" x s - lit l = generic l - - litr :: HsLit GhcRn -> SDoc - litr (HsWordPrim s x) = numericLit "HsWord{64}Prim" x s - litr (HsWord64Prim s x) = numericLit "HsWord{64}Prim" x s - litr (HsIntPrim s x) = numericLit "HsInt{64}Prim" x s - litr (HsInt64Prim s x) = numericLit "HsInt{64}Prim" x s - litr l = generic l - - litt :: HsLit GhcTc -> SDoc - litt (HsWordPrim s x) = numericLit "HsWord{64}Prim" x s - litt (HsWord64Prim s x) = numericLit "HsWord{64}Prim" x s - litt (HsIntPrim s x) = numericLit "HsInt{64}Prim" x s - litt (HsInt64Prim s x) = numericLit "HsInt{64}Prim" x s - litt l = generic l - - numericLit :: String -> Integer -> SourceText -> SDoc - numericLit tag x s = braces $ hsep [ text tag - , generic x - , generic s ] - - name :: Name -> SDoc - name nm = braces $ text "Name: " <> ppr nm - - occName n = braces $ - text "OccName: " - <> text (OccName.occNameString n) - - moduleName :: ModuleName -> SDoc - moduleName m = braces $ text "ModuleName: " <> ppr m - - srcSpan :: SrcSpan -> SDoc - srcSpan ss = case b of - BlankSrcSpan -> text "{ ss }" - NoBlankSrcSpan -> braces $ char ' ' <> - (hang (ppr ss) 1 - -- TODO: show annotations here - (text "")) - - var :: Var -> SDoc - var v = braces $ text "Var: " <> ppr v <> text " (" <> ppr (idType v) <> text ")" - - dataCon :: DataCon -> SDoc - dataCon c = braces $ text "DataCon: " <> ppr c - - bagRdrName:: Bag (Located (HsBind GhcPs)) -> SDoc - bagRdrName bg = braces $ - text "Bag(Located (HsBind GhcPs)):" - $$ (list . bagToList $ bg) - - bagName :: Bag (Located (HsBind GhcRn)) -> SDoc - bagName bg = braces $ - text "Bag(Located (HsBind Name)):" - $$ (list . bagToList $ bg) - - bagVar :: Bag (Located (HsBind GhcTc)) -> SDoc - bagVar bg = braces $ - text "Bag(Located (HsBind Var)):" - $$ (list . bagToList $ bg) - - nameSet ns = braces $ - text "NameSet:" - $$ (list . nameSetElemsStable $ ns) - - fixity :: Fixity -> SDoc - fixity fx = braces $ - text "Fixity: " - <> ppr fx - - located :: (Data b,Data loc) => GenLocated loc b -> SDoc - located (L ss a) = parens $ - case cast ss of - Just (s :: SrcSpan) -> - srcSpan s - Nothing -> text "nnnnnnnn" - $$ showAstData' a - -normalize_newlines :: String -> String -normalize_newlines ('\\':'r':'\\':'n':xs) = '\\':'n':normalize_newlines xs -normalize_newlines (x:xs) = x:normalize_newlines xs -normalize_newlines [] = [] - From 1f30cfe783fbfca41d49ec9574d86fe05b68a6fb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 07:49:14 -0700 Subject: [PATCH 45/64] Tests for lambda case actions --- test/functional/Tactic.hs | 16 ++++++++++++++++ test/testdata/tactic/T2.hs | 3 +++ test/testdata/tactic/T3.hs | 8 ++++++++ test/testdata/tactic/hie.yaml | 2 +- 4 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 test/testdata/tactic/T3.hs diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 87b34d6938..d8fe1d84da 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -73,6 +73,22 @@ tests = testGroup "T2.hs" 8 8 [ (not, Intros, "") ] + , mkTest + "Produces (homomorphic) lambdacase code actions" + "T3.hs" 4 24 + [ (id, HomomorphismLambdaCase, "") + , (id, DestructLambdaCase, "") + ] + , mkTest + "Produces lambdacase code actions" + "T3.hs" 7 13 + [ (id, DestructLambdaCase, "") + ] + , mkTest + "Doesn't suggest lambdacase without -XLambdaCase" + "T2.hs" 11 25 + [ (not, DestructLambdaCase, "") + ] ] diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs index a81756abbb..20b1644a8f 100644 --- a/test/testdata/tactic/T2.hs +++ b/test/testdata/tactic/T2.hs @@ -7,3 +7,6 @@ global = True foo :: Int foo = _ +dontSuggestLambdaCase :: Either a b -> Int +dontSuggestLambdaCase = _ + diff --git a/test/testdata/tactic/T3.hs b/test/testdata/tactic/T3.hs new file mode 100644 index 0000000000..1bb42a9b02 --- /dev/null +++ b/test/testdata/tactic/T3.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE LambdaCase #-} + +suggestHomomorphicLC :: Either a b -> Either a b +suggestHomomorphicLC = _ + +suggestLC :: Either a b -> Int +suggestLC = _ + diff --git a/test/testdata/tactic/hie.yaml b/test/testdata/tactic/hie.yaml index c95f6c9a09..7aa4f9e0ad 100644 --- a/test/testdata/tactic/hie.yaml +++ b/test/testdata/tactic/hie.yaml @@ -1 +1 @@ -cradle: {direct: {arguments: ["T1", "T2"]}} +cradle: {direct: {arguments: ["T1", "T2", "T3"]}} From 9a50f47b10d0937d45a1d3231e6d02876a9ea7ff Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 08:23:02 -0700 Subject: [PATCH 46/64] Golden testing machinery --- test/functional/Tactic.hs | 47 +++++++++++++++---- test/testdata/tactic/GoldenEitherAuto.hs | 2 + .../tactic/GoldenEitherAuto.hs.expected | 5 ++ .../tactic/GoldenEitherHomomorphic.hs | 2 + .../GoldenEitherHomomorphic.hs.expected | 5 ++ test/testdata/tactic/GoldenIdTypeFam.hs | 7 +++ .../tactic/GoldenIdTypeFam.hs.expected | 7 +++ test/testdata/tactic/GoldenIdentityFunctor.hs | 3 ++ .../tactic/GoldenIdentityFunctor.hs.expected | 3 ++ test/testdata/tactic/GoldenIntros.hs | 2 + test/testdata/tactic/GoldenIntros.hs.expected | 2 + test/testdata/tactic/GoldenJoinCont.hs | 4 ++ .../tactic/GoldenJoinCont.hs.expected | 7 +++ 13 files changed, 86 insertions(+), 10 deletions(-) create mode 100644 test/testdata/tactic/GoldenEitherAuto.hs create mode 100644 test/testdata/tactic/GoldenEitherAuto.hs.expected create mode 100644 test/testdata/tactic/GoldenEitherHomomorphic.hs create mode 100644 test/testdata/tactic/GoldenEitherHomomorphic.hs.expected create mode 100644 test/testdata/tactic/GoldenIdTypeFam.hs create mode 100644 test/testdata/tactic/GoldenIdTypeFam.hs.expected create mode 100644 test/testdata/tactic/GoldenIdentityFunctor.hs create mode 100644 test/testdata/tactic/GoldenIdentityFunctor.hs.expected create mode 100644 test/testdata/tactic/GoldenIntros.hs create mode 100644 test/testdata/tactic/GoldenIntros.hs.expected create mode 100644 test/testdata/tactic/GoldenJoinCont.hs create mode 100644 test/testdata/tactic/GoldenJoinCont.hs.expected diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index d8fe1d84da..f688cb0138 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -8,21 +8,22 @@ module Tactic ) where -import Data.Foldable -import Data.Text (Text) +import Control.Applicative.Combinators ( skipManyTill ) +import Control.Monad.IO.Class +import Data.Foldable +import Data.Maybe +import Data.Text (Text) import qualified Data.Text as T -import Control.Monad.IO.Class ( MonadIO(liftIO) ) +import qualified Data.Text.IO as T +import Ide.Plugin.Tactic.TestTypes import Language.Haskell.LSP.Test -import Language.Haskell.LSP.Types ( Position(..) - , Range(..) - , CAResult(..) - , CodeAction(..) - ) +import Language.Haskell.LSP.Types (ApplyWorkspaceEditRequest, Position(..) , Range(..) , CAResult(..) , CodeAction(..)) import Test.Hls.Util import Test.Tasty import Test.Tasty.HUnit -import Data.Maybe (mapMaybe) -import Ide.Plugin.Tactic.TestTypes (tacticTitle, TacticCommand (..)) +import System.FilePath +import System.Directory (doesFileExist) +import Control.Monad (unless) ------------------------------------------------------------------------------ @@ -89,6 +90,12 @@ tests = testGroup "T2.hs" 11 25 [ (not, DestructLambdaCase, "") ] + , goldenTest "GoldenIntros.hs" 2 8 Intros "" + , goldenTest "GoldenEitherAuto.hs" 2 11 Auto "" + , goldenTest "GoldenJoinCont.hs" 4 12 Auto "" + , goldenTest "GoldenIdentityFunctor.hs" 3 11 Auto "" + , goldenTest "GoldenIdTypeFam.hs" 7 11 Auto "" + , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto "" ] @@ -117,6 +124,26 @@ mkTest name fp line col ts = f (elem title titles) @? ("Expected a code action with title " <> T.unpack title) + +goldenTest :: FilePath -> Int -> Int -> TacticCommand -> Text -> TestTree +goldenTest input line col tc occ = + testCase (input <> " (golden)") $ do + runSession hieCommand fullCaps tacticPath $ do + doc <- openDoc input "haskell" + actions <- getCodeActions doc $ pointRange line col + Just (CACodeAction (CodeAction {_command = Just c})) + <- pure $ find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions + executeCommand c + _resp :: ApplyWorkspaceEditRequest <- skipManyTill anyMessage message + edited <- documentContents doc + let expected_name = tacticPath input <.> "expected" + -- 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 @?= expected + + tacticPath :: FilePath tacticPath = "test/testdata/tactic" diff --git a/test/testdata/tactic/GoldenEitherAuto.hs b/test/testdata/tactic/GoldenEitherAuto.hs new file mode 100644 index 0000000000..eb34cd8209 --- /dev/null +++ b/test/testdata/tactic/GoldenEitherAuto.hs @@ -0,0 +1,2 @@ +either' :: (a -> c) -> (b -> c) -> Either a b -> c +either' = _ diff --git a/test/testdata/tactic/GoldenEitherAuto.hs.expected b/test/testdata/tactic/GoldenEitherAuto.hs.expected new file mode 100644 index 0000000000..10d633470c --- /dev/null +++ b/test/testdata/tactic/GoldenEitherAuto.hs.expected @@ -0,0 +1,5 @@ +either' :: (a -> c) -> (b -> c) -> Either a b -> c +either' = (\ fac fbc eab + -> case eab of + (Left a) -> fac a + (Right b) -> fbc b) diff --git a/test/testdata/tactic/GoldenEitherHomomorphic.hs b/test/testdata/tactic/GoldenEitherHomomorphic.hs new file mode 100644 index 0000000000..dee865d1a2 --- /dev/null +++ b/test/testdata/tactic/GoldenEitherHomomorphic.hs @@ -0,0 +1,2 @@ +eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c +eitherSplit = _ diff --git a/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected new file mode 100644 index 0000000000..8276908d71 --- /dev/null +++ b/test/testdata/tactic/GoldenEitherHomomorphic.hs.expected @@ -0,0 +1,5 @@ +eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c +eitherSplit = (\ a efabfac + -> case efabfac of + (Left fab) -> Left (fab a) + (Right fac) -> Right (fac a)) diff --git a/test/testdata/tactic/GoldenIdTypeFam.hs b/test/testdata/tactic/GoldenIdTypeFam.hs new file mode 100644 index 0000000000..be8903fec0 --- /dev/null +++ b/test/testdata/tactic/GoldenIdTypeFam.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE TypeFamilies #-} + +type family TyFam +type instance TyFam = Int + +tyblah' :: TyFam -> Int +tyblah' = _ diff --git a/test/testdata/tactic/GoldenIdTypeFam.hs.expected b/test/testdata/tactic/GoldenIdTypeFam.hs.expected new file mode 100644 index 0000000000..ad5697334e --- /dev/null +++ b/test/testdata/tactic/GoldenIdTypeFam.hs.expected @@ -0,0 +1,7 @@ +{-# LANGUAGE TypeFamilies #-} + +type family TyFam +type instance TyFam = Int + +tyblah' :: TyFam -> Int +tyblah' = (\ i -> i) diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs b/test/testdata/tactic/GoldenIdentityFunctor.hs new file mode 100644 index 0000000000..6d1de50992 --- /dev/null +++ b/test/testdata/tactic/GoldenIdentityFunctor.hs @@ -0,0 +1,3 @@ +data Ident a = Ident a +instance Functor Ident where + fmap = _ diff --git a/test/testdata/tactic/GoldenIdentityFunctor.hs.expected b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected new file mode 100644 index 0000000000..fa0a8b629b --- /dev/null +++ b/test/testdata/tactic/GoldenIdentityFunctor.hs.expected @@ -0,0 +1,3 @@ +data Ident a = Ident a +instance Functor Ident where + fmap = (\ fab ia -> case ia of { (Ident a) -> Ident (fab a) }) diff --git a/test/testdata/tactic/GoldenIntros.hs b/test/testdata/tactic/GoldenIntros.hs new file mode 100644 index 0000000000..5b4e6e241f --- /dev/null +++ b/test/testdata/tactic/GoldenIntros.hs @@ -0,0 +1,2 @@ +blah :: Int -> Bool -> (a -> b) -> String -> Int +blah = _ diff --git a/test/testdata/tactic/GoldenIntros.hs.expected b/test/testdata/tactic/GoldenIntros.hs.expected new file mode 100644 index 0000000000..26d8599e4e --- /dev/null +++ b/test/testdata/tactic/GoldenIntros.hs.expected @@ -0,0 +1,2 @@ +blah :: Int -> Bool -> (a -> b) -> String -> Int +blah = (\ i b fab l_c -> _) diff --git a/test/testdata/tactic/GoldenJoinCont.hs b/test/testdata/tactic/GoldenJoinCont.hs new file mode 100644 index 0000000000..a0cdb05da6 --- /dev/null +++ b/test/testdata/tactic/GoldenJoinCont.hs @@ -0,0 +1,4 @@ +type Cont r a = ((a -> r) -> r) + +joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d +joinCont = _ diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected new file mode 100644 index 0000000000..306591b32c --- /dev/null +++ b/test/testdata/tactic/GoldenJoinCont.hs.expected @@ -0,0 +1,7 @@ +type Cont r a = ((a -> r) -> r) + +joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d +joinCont = (\ fac fbc eab fcd + -> case eab of + (Left a) -> fcd (fac a) + (Right b) -> fcd (fbc b)) From 6d4eba37209bbee4d8ba0d20bd59af93d2248fd5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 08:47:41 -0700 Subject: [PATCH 47/64] Attempt to fill hole --- plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs index a5bbde06dd..2ea4b8d06c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs @@ -19,7 +19,7 @@ data TacticCommand -- | Generate a title for the command. tacticTitle :: TacticCommand -> T.Text -> T.Text -tacticTitle Auto _ = "Auto" +tacticTitle Auto _ = "Attempt to fill hole" tacticTitle Intros _ = "Introduce lambda" tacticTitle Destruct var = "Case split on " <> var tacticTitle Homomorphism var = "Homomorphic case split on " <> var From f56a923237c287ee8a0de8876f9b5c821ec32453 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 30 Sep 2020 09:32:51 -0700 Subject: [PATCH 48/64] [WIP] Use 'refinery-0.2.0.0' --- .../src/Ide/Plugin/Tactic/Machinery.hs | 3 +-- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 4 +--- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 23 +++++++++++-------- stack.yaml | 4 +--- 4 files changed, 16 insertions(+), 18 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 3d9928889b..c386f0ad1c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -55,10 +55,9 @@ runTactic -> TacticsM () -- ^ Tactic to use -> Either [TacticError] (LHsExpr GhcPs) runTactic ctx jdg t = - -- FIXME [Reed] This code does not work let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg tacticState = mempty { ts_skolems = skolems } - in case partitionEithers $ flip runReader ctx $ runProvableT $ runTacticT t jdg tacticState of + in case partitionEithers $ flip runReader ctx $ unExtractM $ runTacticT t jdg tacticState of (errs, []) -> Left $ errs (_, solns) -> let soln = listToMaybe $ filter (null . snd) solns diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 59ff84f724..8e2d551b4c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -12,7 +12,6 @@ module Ide.Plugin.Tactic.Tactics import Control.Applicative import Control.Monad.Except (throwError) import Control.Monad.State.Strict (StateT(..), runStateT) -import Control.Monad.Trans import Data.Function import Data.List import qualified Data.Map as M @@ -179,8 +178,7 @@ attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames) -- | Automatically solve a goal. auto :: TacticsM () auto = do - -- TODO(reed): there is no MonadReader instance for ProvableT - current <- TacticT $ lift $ lift $ lift getCurrentDefinitions + current <- getCurrentDefinitions TacticT $ StateT $ \jdg -> runStateT (unTacticT $ auto' 5) $ disallowing current jdg diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 2e3678d373..c561cffe8f 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -1,9 +1,10 @@ -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} module Ide.Plugin.Tactic.Types ( module Ide.Plugin.Tactic.Types @@ -68,9 +69,12 @@ data Judgement' a = Judgement type Judgement = Judgement' CType +newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } + deriving (Functor, Applicative, Monad, MonadReader Context) + ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. -instance MonadExtract (LHsExpr GhcPs) ProvableM where +instance MonadExtract (LHsExpr GhcPs) ExtractM where hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" @@ -117,9 +121,8 @@ instance Show TacticError where ------------------------------------------------------------------------------ -type ProvableM = ProvableT Judgement (Reader Context) -type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM -type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ProvableM +type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM +type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM type Rule = RuleM (LHsExpr GhcPs) diff --git a/stack.yaml b/stack.yaml index ee66c65fdf..65e1e14ee4 100644 --- a/stack.yaml +++ b/stack.yaml @@ -45,9 +45,7 @@ extra-deps: - ormolu-0.1.2.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- github: totbwf/refinery - commit: 5709a3f10645dd49af20912aec5eb06e72990849 - +- refinery-0.2.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 From fa7234c7e15d0dc54b1c0237614891417c81bd63 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 30 Sep 2020 09:41:23 -0700 Subject: [PATCH 49/64] [WIP] Update refinery in all stack.yaml files --- stack-8.10.1.yaml | 2 +- stack-8.10.2.yaml | 2 +- stack-8.6.4.yaml | 2 +- stack-8.6.5.yaml | 2 +- stack-8.8.2.yaml | 2 +- stack-8.8.3.yaml | 2 +- stack-8.8.4.yaml | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml index 1fe0cba806..d198452493 100644 --- a/stack-8.10.1.yaml +++ b/stack-8.10.1.yaml @@ -20,7 +20,7 @@ extra-deps: - HsYAML-aeson-0.2.0.0@rev:2 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - retrie-0.1.1.1 - stylish-haskell-0.11.0.3 - semigroups-0.18.5 diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index ea835fd350..a917a40fe9 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -21,7 +21,7 @@ extra-deps: - HsYAML-aeson-0.2.0.0@rev:2 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - retrie-0.1.1.1 - stylish-haskell-0.11.0.3 - semigroups-0.18.5 diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml index edd214620a..116d7619c0 100644 --- a/stack-8.6.4.yaml +++ b/stack-8.6.4.yaml @@ -46,7 +46,7 @@ extra-deps: - ormolu-0.1.2.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index 1092a77489..65e1e14ee4 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -45,7 +45,7 @@ extra-deps: - ormolu-0.1.2.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml index 6c71cdfd59..2b2308268d 100644 --- a/stack-8.8.2.yaml +++ b/stack-8.8.2.yaml @@ -38,7 +38,7 @@ extra-deps: - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 - ormolu-0.1.2.0 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml index c63e172e69..30a7c72bb3 100644 --- a/stack-8.8.3.yaml +++ b/stack-8.8.3.yaml @@ -29,7 +29,7 @@ extra-deps: - ilist-0.3.1.0 - lsp-test-0.11.0.5 - monad-dijkstra-0.1.1.2 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml index 63fde601f3..10bc12c58d 100644 --- a/stack-8.8.4.yaml +++ b/stack-8.8.4.yaml @@ -32,7 +32,7 @@ extra-deps: - ilist-0.3.1.0 - lsp-test-0.11.0.5 - monad-dijkstra-0.1.1.2 -- refinery-0.1.0.0 +- refinery-0.2.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 - stylish-haskell-0.11.0.3 From ccf92b7223f0527928c89a3eddbb39ede00a0bf5 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Wed, 30 Sep 2020 10:36:17 -0700 Subject: [PATCH 50/64] Bump version in cabal file --- haskell-language-server.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index f4a3bd3507..379a9a3f53 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -156,7 +156,7 @@ executable haskell-language-server , transformers , unordered-containers , ghc-source-gen - , refinery + , refinery >=0.2.0.0 , ghc-exactprint , fingertree From ae2afcfd72eb36cd7520ce5cfb02fef5bdc359ae Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 13:52:53 -0700 Subject: [PATCH 51/64] Bump cabal index state --- cabal.project | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index 45ef601d1f..a7b601076d 100644 --- a/cabal.project +++ b/cabal.project @@ -20,6 +20,6 @@ package ghcide write-ghc-environment-files: never -index-state: 2020-09-23T17:24:43Z +index-state: 2020-09-30T21:52:43Z allow-newer: data-tree-print:base From 002339d6bb47c2e67096718c7354e704bbbcfa17 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 22:35:56 -0700 Subject: [PATCH 52/64] Sort goals by heuristic --- .../src/Ide/Plugin/Tactic/Machinery.hs | 47 +++++++++++++++++-- 1 file changed, 43 insertions(+), 4 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index c386f0ad1c..fb4a805fa7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -16,16 +16,20 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery ) where +import Control.Applicative import Control.Monad.Except (throwError) import Control.Monad.Reader import Control.Monad.State (gets, modify) import Data.Coerce import Data.Either -import Data.Maybe +import Data.List (sortBy) +import Data.Ord (comparing) import Development.IDE.GHC.Compat import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Types +import Refinery.ProofState import Refinery.Tactic +import Refinery.Tactic.Internal import TcType import Type import Unify @@ -57,13 +61,48 @@ runTactic runTactic ctx jdg t = let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg tacticState = mempty { ts_skolems = skolems } - in case partitionEithers $ flip runReader ctx $ unExtractM $ runTacticT t jdg tacticState of + in case partitionEithers $ flip runReader ctx $ unExtractM $ runTacticTWithState t jdg tacticState of (errs, []) -> Left $ errs (_, solns) -> - let soln = listToMaybe $ filter (null . snd) solns - in Right $ fst $ fromMaybe (head solns) soln + case sortBy (comparing $ uncurry scoreSolution . snd) solns of + (res : _) -> Right $ fst res + -- guaranteed to not be empty + _ -> Left [] +scoreSolution :: TacticState -> [Judgement] -> Int +scoreSolution _ _ = 0 + + +runTacticTWithState + :: (MonadExtract ext m) + => TacticT jdg ext err s m () + -> jdg + -> s + -> m [Either err (ext, (s, [jdg]))] +runTacticTWithState t j s = proofs' s $ fmap snd $ proofState t j + + +proofs' + :: (MonadExtract ext m) + => s + -> ProofStateT ext ext err s m goal + -> m [(Either err (ext, (s, [goal])))] +proofs' s p = go s [] p + where + go s goals (Subgoal goal k) = do + h <- hole + (go s (goals ++ [goal]) $ k h) + go s goals (Effect m) = go s goals =<< m + go s goals (Stateful f) = + let (s', p) = f s + in go s' goals p + go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2) + go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2) + go _ _ Empty = pure [] + go _ _ (Failure err) = pure [throwError err] + go s goals (Axiom ext) = pure [Right (ext, (s, goals))] + ------------------------------------------------------------------------------ -- | We need to make sure that we don't try to unify any skolems. From cf943c81a2b92f0ac586ee99bbde4e67757edf2b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:01:37 -0700 Subject: [PATCH 53/64] Naming for unit types --- plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs index e224fce6a8..5366d6782d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs @@ -11,7 +11,7 @@ import Name import TcType import TyCon import Type -import TysWiredIn (listTyCon, pairTyCon) +import TysWiredIn (listTyCon, pairTyCon, unitTyCon) ------------------------------------------------------------------------------ @@ -41,6 +41,7 @@ mkTyConName :: TyCon -> String mkTyConName tc | tc == listTyCon = "l_" | tc == pairTyCon = "p_" + | tc == unitTyCon = "u_" | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc From b65ccfa9018a485cc7f838bbf0e3d181ef466849 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:04:15 -0700 Subject: [PATCH 54/64] Heuristic for auto --- .../src/Ide/Plugin/Tactic/Machinery.hs | 45 ++++++++++--------- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 14 +++++- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 21 ++++++--- test/functional/Tactic.hs | 4 +- test/testdata/tactic/GoldenNote.hs | 2 + test/testdata/tactic/GoldenNote.hs.expected | 5 +++ test/testdata/tactic/GoldenPureList.hs | 2 + .../tactic/GoldenPureList.hs.expected | 2 + 8 files changed, 68 insertions(+), 27 deletions(-) create mode 100644 test/testdata/tactic/GoldenNote.hs create mode 100644 test/testdata/tactic/GoldenNote.hs.expected create mode 100644 test/testdata/tactic/GoldenPureList.hs create mode 100644 test/testdata/tactic/GoldenPureList.hs.expected diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index fb4a805fa7..ed19ed2ba1 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -16,23 +16,24 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery ) where -import Control.Applicative -import Control.Monad.Except (throwError) -import Control.Monad.Reader -import Control.Monad.State (gets, modify) -import Data.Coerce -import Data.Either -import Data.List (sortBy) -import Data.Ord (comparing) -import Development.IDE.GHC.Compat -import Ide.Plugin.Tactic.Judgements -import Ide.Plugin.Tactic.Types -import Refinery.ProofState -import Refinery.Tactic -import Refinery.Tactic.Internal -import TcType -import Type -import Unify +import Control.Applicative +import Control.Monad.Except (throwError) +import Control.Monad.Reader +import Control.Monad.State (gets, modify) +import Data.Coerce +import Data.Either +import Data.List (intercalate, sortBy) +import Data.Ord (comparing, Down(..)) +import qualified Data.Set as S +import Development.IDE.GHC.Compat +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Types +import Refinery.ProofState +import Refinery.Tactic +import Refinery.Tactic.Internal +import TcType +import Type +import Unify substCTy :: TCvSubst -> CType -> CType @@ -63,15 +64,19 @@ runTactic ctx jdg t = tacticState = mempty { ts_skolems = skolems } in case partitionEithers $ flip runReader ctx $ unExtractM $ runTacticTWithState t jdg tacticState of (errs, []) -> Left $ errs - (_, solns) -> - case sortBy (comparing $ uncurry scoreSolution . snd) solns of + (_, solns) -> do + -- TODO(sandy): remove this trace sometime + traceM $ intercalate "\n" $ fmap (unsafeRender . fst) $ solns + case sortBy (comparing $ Down . uncurry scoreSolution . snd) solns of (res : _) -> Right $ fst res -- guaranteed to not be empty _ -> Left [] scoreSolution :: TacticState -> [Judgement] -> Int -scoreSolution _ _ = 0 +scoreSolution TacticState{..} holes + -- TODO(sandy): should this be linear? + = S.size ts_used_vals - length holes runTacticTWithState diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 8e2d551b4c..89cb181275 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} @@ -11,11 +12,13 @@ module Ide.Plugin.Tactic.Tactics import Control.Applicative import Control.Monad.Except (throwError) +import Control.Monad.State.Class import Control.Monad.State.Strict (StateT(..), runStateT) import Data.Function import Data.List import qualified Data.Map as M import Data.Maybe +import qualified Data.Set as S import Development.IDE.GHC.Compat import GHC.Exts import GHC.SourceGen.Expr @@ -54,11 +57,20 @@ assume name = rule $ \jdg -> do case M.lookup name $ jHypothesis jdg of Just ty -> case ty == jGoal jdg of - True -> pure $ noLoc $ var' name + True -> do + useOccName jdg name + pure $ noLoc $ var' name False -> throwError $ GoalMismatch "assume" g Nothing -> throwError $ UndefinedHypothesis name +useOccName :: MonadState TacticState m => Judgement -> OccName -> m () +useOccName jdg name = + case M.lookup name $ jHypothesis jdg of + Just{} -> modify $ withUsedVals $ S.insert name + Nothing -> pure () + + ------------------------------------------------------------------------------ -- | Introduce a lambda. intro :: TacticsM () diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index c561cffe8f..2f29719944 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -43,16 +43,27 @@ instance Ord CType where ------------------------------------------------------------------------------ data TacticState = TacticState - { ts_skolems :: [TyVar] - , ts_unifier :: TCvSubst + { ts_skolems :: [TyVar] + , ts_unifier :: TCvSubst + , ts_used_vals :: Set OccName } instance Semigroup TacticState where - TacticState a1 b1 <> TacticState a2 b2 - = TacticState (a1 <> a2) (unionTCvSubst b1 b2) + TacticState a1 b1 c1 <> TacticState a2 b2 c2 + = TacticState + (a1 <> a2) + (unionTCvSubst b1 b2) + (c1 <> c2) instance Monoid TacticState where - mempty = TacticState mempty emptyTCvSubst + mempty = TacticState mempty emptyTCvSubst mempty + + +withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState +withUsedVals f ts = ts + { ts_used_vals = f $ ts_used_vals ts + } + ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 50046e19f0..e770ad8a41 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -90,7 +90,9 @@ tests = testGroup , goldenTest "GoldenJoinCont.hs" 4 12 Auto "" , goldenTest "GoldenIdentityFunctor.hs" 3 11 Auto "" , goldenTest "GoldenIdTypeFam.hs" 7 11 Auto "" - , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto "" + , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto "" + , goldenTest "GoldenNote.hs" 2 8 Auto "" + , goldenTest "GoldenPureList.hs" 2 12 Auto "" ] diff --git a/test/testdata/tactic/GoldenNote.hs b/test/testdata/tactic/GoldenNote.hs new file mode 100644 index 0000000000..c9e0c820e4 --- /dev/null +++ b/test/testdata/tactic/GoldenNote.hs @@ -0,0 +1,2 @@ +note :: e -> Maybe a -> Either e a +note = _ diff --git a/test/testdata/tactic/GoldenNote.hs.expected b/test/testdata/tactic/GoldenNote.hs.expected new file mode 100644 index 0000000000..47a9bd6d92 --- /dev/null +++ b/test/testdata/tactic/GoldenNote.hs.expected @@ -0,0 +1,5 @@ +note :: e -> Maybe a -> Either e a +note = (\ e ma + -> case ma of + Nothing -> Left e + (Just a) -> Right a) diff --git a/test/testdata/tactic/GoldenPureList.hs b/test/testdata/tactic/GoldenPureList.hs new file mode 100644 index 0000000000..3a3293b4ec --- /dev/null +++ b/test/testdata/tactic/GoldenPureList.hs @@ -0,0 +1,2 @@ +pureList :: a -> [a] +pureList = _ diff --git a/test/testdata/tactic/GoldenPureList.hs.expected b/test/testdata/tactic/GoldenPureList.hs.expected new file mode 100644 index 0000000000..9410eea557 --- /dev/null +++ b/test/testdata/tactic/GoldenPureList.hs.expected @@ -0,0 +1,2 @@ +pureList :: a -> [a] +pureList = (\ a -> (:) a []) From 419224babcf9d65ea10ab45e421c0bde83732d87 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:09:26 -0700 Subject: [PATCH 55/64] Penalize holes more --- plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index ed19ed2ba1..65885324c0 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -62,7 +62,10 @@ runTactic runTactic ctx jdg t = let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg tacticState = mempty { ts_skolems = skolems } - in case partitionEithers $ flip runReader ctx $ unExtractM $ runTacticTWithState t jdg tacticState of + in case partitionEithers + . flip runReader ctx + . unExtractM + $ runTacticTWithState t jdg tacticState of (errs, []) -> Left $ errs (_, solns) -> do -- TODO(sandy): remove this trace sometime @@ -76,7 +79,7 @@ runTactic ctx jdg t = scoreSolution :: TacticState -> [Judgement] -> Int scoreSolution TacticState{..} holes -- TODO(sandy): should this be linear? - = S.size ts_used_vals - length holes + = S.size ts_used_vals - length holes * 5 runTacticTWithState From cfd3b063e81a295debe8d80db200f7d5a20250f4 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:01:37 -0700 Subject: [PATCH 56/64] Naming for unit types --- plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs index e224fce6a8..5366d6782d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs @@ -11,7 +11,7 @@ import Name import TcType import TyCon import Type -import TysWiredIn (listTyCon, pairTyCon) +import TysWiredIn (listTyCon, pairTyCon, unitTyCon) ------------------------------------------------------------------------------ @@ -41,6 +41,7 @@ mkTyConName :: TyCon -> String mkTyConName tc | tc == listTyCon = "l_" | tc == pairTyCon = "p_" + | tc == unitTyCon = "u_" | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc From 141c3635940919f50d90b22aacbf3226306a165a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:13:47 -0700 Subject: [PATCH 57/64] Give the name "unit" to units --- plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs index 5366d6782d..1f05e6bcf6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs @@ -41,7 +41,7 @@ mkTyConName :: TyCon -> String mkTyConName tc | tc == listTyCon = "l_" | tc == pairTyCon = "p_" - | tc == unitTyCon = "u_" + | tc == unitTyCon = "unit" | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc From 54b335ab7ba478d5926b190ca51883e7d9b83403 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:24:53 -0700 Subject: [PATCH 58/64] Fallback names for symbols and punctuation --- plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs index 1f05e6bcf6..1076057b0c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs @@ -3,6 +3,7 @@ module Ide.Plugin.Tactic.Naming where import Control.Monad.State.Strict +import Data.Bool (bool) import Data.Char import Data.Map (Map) import qualified Data.Map as M @@ -42,7 +43,19 @@ mkTyConName tc | tc == listTyCon = "l_" | tc == pairTyCon = "p_" | tc == unitTyCon = "unit" - | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc + | otherwise + = filterReplace isSymbol 's' + . filterReplace isSymbol 'p' + . fmap toLower + . take 1 + . occNameString + $ getOccName tc + + +------------------------------------------------------------------------------ +-- | Maybe replace an element in the list if the predicate matches +filterReplace :: (a -> Bool) -> a -> [a] -> [a] +filterReplace f r = fmap (\a -> bool a r $ f a) ------------------------------------------------------------------------------ From 35040d69b0a9863efb09d7491303e3fd7832e786 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 30 Sep 2020 23:33:44 -0700 Subject: [PATCH 59/64] Get "good" name for symbolic names --- plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs index 1076057b0c..5426701106 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Naming.hs @@ -28,10 +28,10 @@ mkTyName (tcSplitFunTys -> ((_:_), b)) mkTyName (splitTyConApp_maybe -> Just (c, args)) = mkTyConName c ++ foldMap mkTyName args -- eg. mkTyName a = "a" -mkTyName (getTyVar_maybe-> Just tv) +mkTyName (getTyVar_maybe -> Just tv) = occNameString $ occName tv -- eg. mkTyName (forall x. y) = "y" -mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) +mkTyName (tcSplitSigmaTy -> ((_:_), _, t)) = mkTyName t mkTyName _ = "x" @@ -44,10 +44,10 @@ mkTyConName tc | tc == pairTyCon = "p_" | tc == unitTyCon = "unit" | otherwise - = filterReplace isSymbol 's' - . filterReplace isSymbol 'p' + = take 1 . fmap toLower - . take 1 + . filterReplace isSymbol 's' + . filterReplace isPunctuation 'p' . occNameString $ getOccName tc From e2005c9c57e022c153c3d434a0b63ec57f74de43 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 2 Oct 2020 21:56:41 -0700 Subject: [PATCH 60/64] Update plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs Co-authored-by: wz1000 --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 8e4b40b15e..1f1f3ea449 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -52,7 +52,7 @@ destructMatches f f2 t jdg = do ------------------------------------------------------------------------------ --- | Combinator for performign case splitting, and running sub-rules on the +-- | Combinator for performing case splitting, and running sub-rules on the -- resulting matches. destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule destruct' f term jdg = do @@ -103,4 +103,3 @@ var' = var . fromString . occNameString -- | Like 'bvar', but works over standard GHC 'OccName's. bvar' :: BVar a => OccName -> a bvar' = bvar . fromString . occNameString - From 061a65dd072fb353fd908db1df89f3674988d0b3 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 2 Oct 2020 21:59:13 -0700 Subject: [PATCH 61/64] Make the TacticState strict --- plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 2f29719944..296e1f7893 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -43,9 +43,9 @@ instance Ord CType where ------------------------------------------------------------------------------ data TacticState = TacticState - { ts_skolems :: [TyVar] - , ts_unifier :: TCvSubst - , ts_used_vals :: Set OccName + { ts_skolems :: !([TyVar]) + , ts_unifier :: !(TCvSubst) + , ts_used_vals :: !(Set OccName) } instance Semigroup TacticState where From 14c58cc234baf1e1e7ca1a0f2b4fd198599513ee Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 2 Oct 2020 21:59:42 -0700 Subject: [PATCH 62/64] Make the judgement strict --- plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 296e1f7893..291d732fad 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -68,12 +68,12 @@ withUsedVals f ts = ts ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement - { _jHypothesis :: Map OccName a - , _jDestructed :: Set OccName + { _jHypothesis :: !(Map OccName a) + , _jDestructed :: !(Set OccName) -- ^ These should align with keys of _jHypothesis - , _jPatternVals :: Set OccName + , _jPatternVals :: !(Set OccName) -- ^ These should align with keys of _jHypothesis - , _jGoal :: a + , _jGoal :: !(a) } deriving stock (Eq, Ord, Generic, Functor) From 8fa9102eb752d2a280999906b174c98ccdbb6763 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 2 Oct 2020 22:28:19 -0700 Subject: [PATCH 63/64] Simplify when we use position mapping --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 062ff74663..3586761711 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -143,14 +143,14 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right $ List []) $ do - (_, _, span, jdg, dflags) <- MaybeT $ judgementForHole state nfp range + (_, _, jdg, dflags) <- judgementForHole state nfp range actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider [minBound .. maxBound] dflags plId uri - span + range jdg pure $ Right $ List actions codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -226,8 +226,8 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (Maybe (PositionMapping, BindSites, Range, Judgement, DynFlags)) -judgementForHole state nfp range = runMaybeT $ do + -> MaybeT IO (BindSites, Range, Judgement, DynFlags) +judgementForHole state nfp range = do (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp range' <- liftMaybe $ fromCurrentRange amapping range @@ -251,7 +251,7 @@ judgementForHole state nfp range = runMaybeT $ do resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal, dflags) + pure (b2, resulting_range, mkFirstJudgement hyps goal, dflags) @@ -259,15 +259,13 @@ tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do - (pos, b2, _, jdg, dflags) <- MaybeT $ judgementForHole state nfp range - range' <- liftMaybe $ toCurrentRange pos range + (b2, range', jdg, dflags) <- judgementForHole state nfp range (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' - -- TODO(sandy): unclear if this span is correct; might be - -- pointing to the wrong version of the file tcg = fst $ tm_internals_ $ tmrModule tcmod ctx = mkContext - (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings b2 span) + (mapMaybe (sequenceA . (occName *** coerce)) + $ getDefiningBindings b2 span) tcg pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic ctx jdg From 67bff917aaf03b3a7da307369c6fc0d01681a52e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 2 Oct 2020 22:49:44 -0700 Subject: [PATCH 64/64] Move bindsites to ghcide --- ghcide | 2 +- haskell-language-server.cabal | 1 - plugins/tactics/src/Ide/Plugin/Tactic.hs | 28 +++++----- .../src/Ide/Plugin/Tactic/BindSites.hs | 55 ------------------- 4 files changed, 14 insertions(+), 72 deletions(-) delete mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/BindSites.hs diff --git a/ghcide b/ghcide index b279afbce7..0bfce3114c 160000 --- a/ghcide +++ b/ghcide @@ -1 +1 @@ -Subproject commit b279afbce74ef691a47159314e0b7023b2f7074a +Subproject commit 0bfce3114c28bd00f7bf5729c32ec0f23a8d8854 diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 379a9a3f53..e49e1a5451 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -93,7 +93,6 @@ executable haskell-language-server Ide.Plugin.Retrie Ide.Plugin.StylishHaskell Ide.Plugin.Tactic - Ide.Plugin.Tactic.BindSites Ide.Plugin.Tactic.CodeGen Ide.Plugin.Tactic.Context Ide.Plugin.Tactic.Debug diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 3586761711..199cc1a609 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -31,20 +31,20 @@ import Development.IDE.Core.Service (runAction) import Development.IDE.Core.Shake (useWithStale, IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (realSrcSpanToRange) +import Development.IDE.Spans.LocalBindings (getDefiningBindings) import Development.Shake (Action) import DynFlags (xopt) import qualified FastString import GHC.Generics (Generic) import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Plugin (mkLspCommand) -import Ide.Plugin.Tactic.BindSites import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Tactics -import Ide.Plugin.Tactic.Types import Ide.Plugin.Tactic.TestTypes +import Ide.Plugin.Tactic.Types import Ide.TreeTransform (transform, graft, useAnnotatedSource) import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) @@ -143,7 +143,7 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right $ List []) $ do - (_, _, jdg, dflags) <- judgementForHole state nfp range + (_, jdg, _, dflags) <- judgementForHole state nfp range actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider [minBound .. maxBound] @@ -226,13 +226,12 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> MaybeT IO (BindSites, Range, Judgement, DynFlags) + -> MaybeT IO (Range, Judgement, Context, DynFlags) judgementForHole state nfp range = do (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp range' <- liftMaybe $ fromCurrentRange amapping range (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp - let b2 = bindSites $ refMap asts -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. @@ -249,9 +248,14 @@ judgementForHole state nfp range = do pure (nodeSpan ast', ty) resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss - - let hyps = hypothesisFromBindings rss binds - pure (b2, resulting_range, mkFirstJudgement hyps goal, dflags) + (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp + let tcg = fst $ tm_internals_ $ tmrModule tcmod + ctx = mkContext + (mapMaybe (sequenceA . (occName *** coerce)) + $ getDefiningBindings binds rss) + tcg + hyps = hypothesisFromBindings rss binds + pure (resulting_range, mkFirstJudgement hyps goal, ctx, dflags) @@ -259,14 +263,8 @@ tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do - (b2, range', jdg, dflags) <- judgementForHole state nfp range - (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp + (range', jdg, ctx, dflags) <- judgementForHole state nfp range let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' - tcg = fst $ tm_internals_ $ tmrModule tcmod - ctx = mkContext - (mapMaybe (sequenceA . (occName *** coerce)) - $ getDefiningBindings b2 span) - tcg pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic ctx jdg $ tac diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/BindSites.hs b/plugins/tactics/src/Ide/Plugin/Tactic/BindSites.hs deleted file mode 100644 index 568f1c2ede..0000000000 --- a/plugins/tactics/src/Ide/Plugin/Tactic/BindSites.hs +++ /dev/null @@ -1,55 +0,0 @@ -module Ide.Plugin.Tactic.BindSites - ( BindSites () - , bindSites - , getDefiningBindings - ) where - -import Data.IntervalMap.FingerTree (IntervalMap, Interval (..)) -import qualified Data.IntervalMap.FingerTree as IM -import qualified Data.Map as M -import qualified Data.Set as S -import Development.IDE.GHC.Compat -import Development.IDE.GHC.Error -import Development.IDE.Types.Location -import NameEnv -import SrcLoc - - --- TODO(sandy): Consolidate this with LocalBindings -data BindSites = BindSites - { unBindSites :: IntervalMap Position (NameEnv (Name, Maybe Type)) - } - ------------------------------------------------------------------------------- --- | Turn a 'RealSrcSpan' into an 'Interval'. -realSrcSpanToInterval :: RealSrcSpan -> Interval Position -realSrcSpanToInterval rss = - Interval - (realSrcLocToPosition $ realSrcSpanStart rss) - (realSrcLocToPosition $ realSrcSpanEnd rss) - ------------------------------------------------------------------------------- --- | Compute which identifiers are in scope at every point in the AST. Use --- 'getDefiningBindings' to find the results. -bindSites :: RefMap -> BindSites -bindSites refmap = BindSites $ foldr (uncurry IM.insert) mempty $ do - (ident, refs) <- M.toList refmap - Right name <- pure ident - (_, ident_details) <- refs - let ty = identType ident_details - info <- S.toList $ identInfo ident_details - Just scope <- pure $ getBindSiteFromContext info - pure ( realSrcSpanToInterval scope - , unitNameEnv name (name,ty) - ) - ------------------------------------------------------------------------------- --- | Given a 'BindSites', get every binding currently active at a given --- 'RealSrcSpan', -getDefiningBindings :: BindSites -> RealSrcSpan -> [(Name, Maybe Type)] -getDefiningBindings bs rss - = nameEnvElts - $ foldMap snd - $ IM.dominators (realSrcSpanToInterval rss) - $ unBindSites bs -