From a9da2145ad3050c3c98985841eaf437bc0a3fd26 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 08:54:13 -0800 Subject: [PATCH 01/10] Add new variables to the extract when doing intros --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index da8f9f86e2..f75fb07054 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -12,7 +12,7 @@ module Ide.Plugin.Tactic.Tactics ) where import Control.Applicative (Alternative(empty)) -import Control.Lens ((&), (%~)) +import Control.Lens ((&), (%~), (<>~)) import Control.Monad (unless) import Control.Monad.Except (throwError) import Control.Monad.Reader.Class (MonadReader (ask)) @@ -104,6 +104,7 @@ intros = rule $ \jdg -> do ext & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") . pure + & #syn_scoped <>~ hy' & #syn_val %~ noLoc . lambda (fmap bvar' vs) . unLoc From 10dbfc03ef2a8f9f643cee155b91babbde557512 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 08:37:05 -0800 Subject: [PATCH 02/10] Implement the correct top-level hypothesis --- .../src/Ide/Plugin/Tactic/Judgements.hs | 9 + .../src/Ide/Plugin/Tactic/LanguageServer.hs | 195 ++++++++++++++---- .../src/Ide/Plugin/Tactic/Naming.hs | 2 + 3 files changed, 163 insertions(+), 43 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs index a691441d86..882cd4b5f8 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs @@ -210,6 +210,15 @@ jAncestryMap jdg = flip M.map (jPatHypothesis jdg) pv_ancestry +provAncestryOf :: Provenance -> Set OccName +provAncestryOf (TopLevelArgPrv o i i3) = S.singleton o +provAncestryOf (PatternMatchPrv (PatVal mo so ud i)) = maybe mempty S.singleton mo <> so +provAncestryOf (ClassMethodPrv uc) = mempty +provAncestryOf UserPrv = mempty +provAncestryOf RecursivePrv = mempty +provAncestryOf (DisallowedPrv d p2) = provAncestryOf p2 + + ------------------------------------------------------------------------------ -- TODO(sandy): THIS THING IS A BIG BIG HACK -- diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index bd8c5e8038..2ad1c28875 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -1,57 +1,58 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wall #-} module Ide.Plugin.Tactic.LanguageServer where +import ConLike import Control.Arrow import Control.Monad +import Control.Monad.State (State, get, put, evalState) import Control.Monad.Trans.Maybe -import Data.Aeson (Value (Object), fromJSON) -import Data.Aeson.Types (Result (Error, Success)) +import Data.Aeson (Value (Object), fromJSON) +import Data.Aeson.Types (Result (Error, Success)) import Data.Coerce -import Data.Functor ((<&>)) -import Data.Generics.Aliases (mkQ) -import Data.Generics.Schemes (everything) -import Data.Map (Map) -import qualified Data.Map as M +import Data.Functor ((<&>)) +import Data.Generics.Aliases (mkQ) +import Data.Generics.Schemes (everything) +import qualified Data.Map as M import Data.Maybe import Data.Monoid -import qualified Data.Set as S -import qualified Data.Text as T +import qualified Data.Set as S +import qualified Data.Text as T import Data.Traversable -import Development.IDE (ShakeExtras, - getPluginConfig) +import Development.IDE (ShakeExtras, getPluginConfig) import Development.IDE.Core.PositionMapping import Development.IDE.Core.RuleTypes -import Development.IDE.Core.Service (runAction) -import Development.IDE.Core.Shake (IdeState (..), - useWithStale) +import Development.IDE.Core.Service (runAction) +import Development.IDE.Core.Shake (IdeState (..), useWithStale) import Development.IDE.GHC.Compat -import Development.IDE.GHC.Error (realSrcSpanToRange) -import Development.IDE.Spans.LocalBindings (Bindings, - getDefiningBindings) -import Development.Shake (Action, RuleResult) -import Development.Shake.Classes +import Development.IDE.GHC.Error (realSrcSpanToRange) +import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings) +import Development.Shake (Action, RuleResult) +import Development.Shake.Classes (Typeable, Binary, Hashable, NFData) import qualified FastString -import Ide.Plugin.Config (PluginConfig (plcConfig)) -import qualified Ide.Plugin.Config as Plugin +import GhcPlugins (mkAppTys) +import Ide.Plugin.Config (PluginConfig (plcConfig)) +import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.FeatureSet import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Range -import Ide.Plugin.Tactic.TestTypes (TacticCommand, - cfg_feature_set, emptyConfig, Config) +import Ide.Plugin.Tactic.TestTypes (TacticCommand, cfg_feature_set, emptyConfig, Config) import Ide.Plugin.Tactic.Types -import Language.LSP.Server (MonadLsp) +import Language.LSP.Server (MonadLsp) import Language.LSP.Types import OccName -import Prelude hiding (span) -import SrcLoc (containsSpan) -import TcRnTypes (tcg_binds) +import Prelude hiding (span) +import SrcLoc (containsSpan) +import TcRnTypes (tcg_binds) tacticDesc :: T.Text -> T.Text @@ -145,7 +146,7 @@ mkJudgementAndContext features g binds rss tcmod = do (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings binds rss) tcg - top_provs = getRhsPosVals rss tcs + top_provs = traceIdX "top_provs" $ getRhsPosVals rss tcs local_hy = spliceProvenance top_provs $ hypothesisFromBindings rss binds cls_hy = contextMethodHypothesis ctx @@ -178,37 +179,145 @@ liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a +------------------------------------------------------------------------------ +-- | Combine two (possibly-overlapping) hypotheses; using the provenance from +-- the first hypothesis if the bindings overlap. spliceProvenance - :: Map OccName Provenance - -> Hypothesis a + :: Hypothesis a -- ^ Bindings to keep + -> Hypothesis a -- ^ Bindings to keep if they don't overlap with the first set -> Hypothesis a -spliceProvenance provs x = - Hypothesis $ flip fmap (unHypothesis x) $ \hi -> - overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi +spliceProvenance top x = + let bound = S.fromList $ fmap hi_name $ unHypothesis top + in mappend top $ Hypothesis . filter (flip S.notMember bound . hi_name) $ unHypothesis x ------------------------------------------------------------------------------ -- | Compute top-level position vals of a function -getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance +getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Hypothesis CType getRhsPosVals rss tcs - = M.fromList - $ join - $ maybeToList - $ getFirst - $ everything (<>) (mkQ mempty $ \case + = everything (<>) (mkQ mempty $ \case TopLevelRHS name ps (L (RealSrcSpan span) -- body with no guards and a single defn (HsVar _ (L _ hole))) | containsSpan rss span -- which contains our span , isHole $ occName hole -- and the span is a hole - -> First $ do - patnames <- traverse getPatName ps - pure $ zip patnames $ [0..] <&> \n -> - TopLevelArgPrv name n (length patnames) + -> flip evalState 0 $ buildTopLevelHypothesis name ps _ -> mempty ) tcs +------------------------------------------------------------------------------ +-- | Construct a hypothesis given the patterns from the left side of a HsMatch. +-- These correspond to things that the user put in scope before running +-- tactics. +buildTopLevelHypothesis + :: OccName -- ^ Function name + -> [PatCompat GhcTc] + -> State Int (Hypothesis CType) +buildTopLevelHypothesis name (fmap fromPatCompatTc -> ps) = do + fmap mconcat $ + for (zip [0..] ps) $ \(ix, p) -> + buildPatHy (TopLevelArgPrv name ix $ length ps) p + + +------------------------------------------------------------------------------ +-- | Construct a hypothesis for a single pattern, including building +-- sub-hypotheses for constructor pattern matches. +buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType) +buildPatHy prov (fromPatCompatTc -> p0) = + case p0 of + VarPat _ x -> pure $ mkIdHypothesis (unLoc x) prov + LazyPat _ p -> buildPatHy prov p + AsPat _ x p -> do + hy' <- buildPatHy prov p + pure $ mkIdHypothesis (unLoc x) prov <> hy' + ParPat _ p -> buildPatHy prov p + BangPat _ p -> buildPatHy prov p + ViewPat _ _ p -> buildPatHy prov p + ConPatOut (L _ (RealDataCon dc)) args _ _ _ f _ -> + case f of + PrefixCon l_pgt -> mkDerivedConHypothesis prov dc args $ zip [0..] l_pgt + InfixCon pgt pgt5 -> mkDerivedConHypothesis prov dc args $ zip [0..] [pgt, pgt5] + RecCon r -> mkDerivedRecordHypothesis prov dc args r +#if __GLASGOW_HASKELL__ >= 808 + SigPat _ p _ -> buildPatHy prov p +#endif +#if __GLASGOW_HASKELL__ == 808 + XPat p -> buildPatHy prov $ unLoc p +#endif + _ -> pure mempty + + +------------------------------------------------------------------------------ +-- | Like 'mkDerivedConHypothesis', but for record patterns. +mkDerivedRecordHypothesis + :: Provenance + -> DataCon -- ^ Destructing constructor + -> [Type] -- ^ Applied type variables + -> HsRecFields GhcTc (PatCompat GhcTc) + -> State Int (Hypothesis CType) +mkDerivedRecordHypothesis prov dc args (HsRecFields (fmap unLoc -> fs) _) + | Just rec_fields <- getRecordFields dc + = do + let field_lookup = M.fromList $ zip (fmap (occNameFS . fst) rec_fields) [0..] + mkDerivedConHypothesis prov dc args $ fs <&> \(HsRecField (L _ rec_occ) p _) -> + ( field_lookup M.! (occNameFS $ occName $ unLoc $ rdrNameFieldOcc rec_occ) + , p + ) +mkDerivedRecordHypothesis _ _ _ _ = + error "impossible! using record pattern on something that isn't a record" + + +------------------------------------------------------------------------------ +-- | Construct a fake variable name. Used to track the provenance of top-level +-- pattern matches which otherwise wouldn't have anything to attach their +-- 'TopLevelArgPrv' to. +mkFakeVar :: State Int OccName +mkFakeVar = do + i <- get + put $ i + 1 + pure $ mkVarOcc $ "_" <> show i + + +------------------------------------------------------------------------------ +-- | Construct a fake varible to attach the current 'Provenance' to, and then +-- build a sub-hypothesis for the pattern match. +mkDerivedConHypothesis + :: Provenance + -> DataCon -- ^ Destructing constructor + -> [Type] -- ^ Applied type variables + -> [(Int, PatCompat GhcTc)] -- ^ Patterns, and their order in the data con + -> State Int (Hypothesis CType) +mkDerivedConHypothesis prov dc args (fmap (second fromPatCompatTc) -> ps) = do + var <- mkFakeVar + hy' <- fmap mconcat $ + for ps $ \(ix, p) -> do + let prov' = PatternMatchPrv + $ PatVal (Just var) + (S.singleton var <> provAncestryOf prov) + (Uniquely dc) + ix + buildPatHy prov' p + pure + $ mappend hy' + $ Hypothesis + $ pure + $ HyInfo var (DisallowedPrv AlreadyDestructed prov) + $ CType + -- TODO(sandy): This is the completely wrong type, but we don't have a good + -- way to get the real one. It's probably OK though, since we're generating + -- this term with a disallowed provenance, and it doesn't actually exist + -- anyway. + $ mkAppTys (dataConUserType dc) args + + +------------------------------------------------------------------------------ +-- | Build a 'Hypothesis' given an 'Id'. +mkIdHypothesis :: Id -> Provenance -> Hypothesis CType +mkIdHypothesis (splitId -> (name, ty)) prov = + Hypothesis $ pure $ HyInfo name prov ty + + ------------------------------------------------------------------------------ -- | Is this hole immediately to the right of an equals sign? isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs index 31944ad1dd..03c91972a4 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs @@ -15,6 +15,7 @@ import TcType import TyCon import Type import TysWiredIn (listTyCon, pairTyCon, unitTyCon) +import Ide.Plugin.Tactic.Types ------------------------------------------------------------------------------ @@ -95,3 +96,4 @@ mkManyGoodNames in_scope args = -- | Which names are in scope? getInScope :: Map OccName a -> [OccName] getInScope = M.keys + From dab2278f4407ac1f9455feeae78781d8e9ddce96 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 09:55:28 -0800 Subject: [PATCH 03/10] Implement top-level list and tuple hypotheses --- .../src/Ide/Plugin/Tactic/GHC.hs | 3 +++ .../src/Ide/Plugin/Tactic/LanguageServer.hs | 25 ++++++++++++++++--- 2 files changed, 24 insertions(+), 4 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs index 549dd5f4b1..698cde4c1d 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs @@ -250,15 +250,18 @@ lambdaCaseable _ = Nothing -- It's hard to generalize over these since weird type families are involved. fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc +toPatCompatTc :: Pat GhcTc -> PatCompat GhcTc fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs #if __GLASGOW_HASKELL__ == 808 type PatCompat pass = Pat pass fromPatCompatTc = id fromPatCompatPs = id +toPatCompatTc = id #else type PatCompat pass = LPat pass fromPatCompatTc = unLoc fromPatCompatPs = unLoc +toPatCompatTc = noLoc #endif ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 2ad1c28875..63efd63f34 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -37,7 +37,7 @@ import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi import Development.Shake (Action, RuleResult) import Development.Shake.Classes (Typeable, Binary, Hashable, NFData) import qualified FastString -import GhcPlugins (mkAppTys) +import GhcPlugins (mkAppTys, tupleDataCon, consDataCon) import Ide.Plugin.Config (PluginConfig (plcConfig)) import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Tactic.Context @@ -234,11 +234,28 @@ buildPatHy prov (fromPatCompatTc -> p0) = ParPat _ p -> buildPatHy prov p BangPat _ p -> buildPatHy prov p ViewPat _ _ p -> buildPatHy prov p + -- Desugar lists into cons + ListPat _ [] -> pure mempty + ListPat x@(ListPatTc ty _) (fmap fromPatCompatTc -> (p : ps)) -> + mkDerivedConHypothesis prov consDataCon [ty] + [ (0, toPatCompatTc p) + , (1, ListPat x $ fmap toPatCompatTc ps) + ] + -- Desugar tuples into an explicit constructor + TuplePat tys pats boxity -> + mkDerivedConHypothesis + prov + (tupleDataCon boxity $ length pats) + tys + $ zip [0.. ] pats ConPatOut (L _ (RealDataCon dc)) args _ _ _ f _ -> case f of - PrefixCon l_pgt -> mkDerivedConHypothesis prov dc args $ zip [0..] l_pgt - InfixCon pgt pgt5 -> mkDerivedConHypothesis prov dc args $ zip [0..] [pgt, pgt5] - RecCon r -> mkDerivedRecordHypothesis prov dc args r + PrefixCon l_pgt -> + mkDerivedConHypothesis prov dc args $ zip [0..] l_pgt + InfixCon pgt pgt5 -> + mkDerivedConHypothesis prov dc args $ zip [0..] [pgt, pgt5] + RecCon r -> + mkDerivedRecordHypothesis prov dc args r #if __GLASGOW_HASKELL__ >= 808 SigPat _ p _ -> buildPatHy prov p #endif From b9e8b5a85799ef298297c5ced3f3547f9fc3b8e8 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 10:07:13 -0800 Subject: [PATCH 04/10] Add tests to prove top level matches work now --- plugins/hls-tactics-plugin/test/GoldenSpec.hs | 1 + .../test/golden/DestructAllNonVarTopMatch.hs | 3 +++ .../test/golden/DestructAllNonVarTopMatch.hs.expected | 6 ++++++ 3 files changed, 10 insertions(+) create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs.expected diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs index add283d012..c364b75a66 100644 --- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs +++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs @@ -99,6 +99,7 @@ spec = do describe "golden" $ do destructAllTest "DestructAllAnd.hs" 2 11 destructAllTest "DestructAllMany.hs" 4 23 + destructAllTest "DestructAllNonVarTopMatch.hs" 2 18 -- test via: diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs b/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs new file mode 100644 index 0000000000..358223ae67 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs @@ -0,0 +1,3 @@ +and :: (a, b) -> Bool -> Bool -> Bool +and (a, b) x y = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs.expected b/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs.expected new file mode 100644 index 0000000000..c63a963932 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs.expected @@ -0,0 +1,6 @@ +and :: (a, b) -> Bool -> Bool -> Bool +and (a, b) False False = _ +and (a, b) True False = _ +and (a, b) False True = _ +and (a, b) True True = _ + From 65f76d5317b42531bbbfb24dd7770dafe18f6e92 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 10:08:27 -0800 Subject: [PATCH 05/10] Remove getPatName --- .../src/Ide/Plugin/Tactic/GHC.hs | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs index 698cde4c1d..c4d9de9728 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs @@ -274,22 +274,6 @@ pattern TopLevelRHS name ps body <- (GRHSs _ [L _ (GRHS _ [] body)] _) -getPatName :: PatCompat GhcTc -> Maybe OccName -getPatName (fromPatCompatTc -> p0) = - case p0 of - VarPat _ x -> Just $ occName $ unLoc x - LazyPat _ p -> getPatName p - AsPat _ x _ -> Just $ occName $ unLoc x - ParPat _ p -> getPatName p - BangPat _ p -> getPatName p - ViewPat _ _ p -> getPatName p -#if __GLASGOW_HASKELL__ >= 808 - SigPat _ p _ -> getPatName p -#endif -#if __GLASGOW_HASKELL__ == 808 - XPat p -> getPatName $ unLoc p -#endif - _ -> Nothing dataConExTys :: DataCon -> [TyCoVar] #if __GLASGOW_HASKELL__ >= 808 From a643bdc6073fd77bd0b05208ede1877887d1af84 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 10:09:51 -0800 Subject: [PATCH 06/10] Remove debug trace --- .../hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 63efd63f34..c3bf2e81ca 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -146,7 +146,7 @@ mkJudgementAndContext features g binds rss tcmod = do (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings binds rss) tcg - top_provs = traceIdX "top_provs" $ getRhsPosVals rss tcs + top_provs = getRhsPosVals rss tcs local_hy = spliceProvenance top_provs $ hypothesisFromBindings rss binds cls_hy = contextMethodHypothesis ctx From ed43eb7dac72777df69d3f06ece92db9a8380300 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 3 Mar 2021 21:14:22 -0800 Subject: [PATCH 07/10] PatCompat issues --- .../src/Ide/Plugin/Tactic/LanguageServer.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index c3bf2e81ca..d9cee88cf3 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -214,7 +214,7 @@ buildTopLevelHypothesis :: OccName -- ^ Function name -> [PatCompat GhcTc] -> State Int (Hypothesis CType) -buildTopLevelHypothesis name (fmap fromPatCompatTc -> ps) = do +buildTopLevelHypothesis name ps = do fmap mconcat $ for (zip [0..] ps) $ \(ix, p) -> buildPatHy (TopLevelArgPrv name ix $ length ps) p @@ -236,10 +236,10 @@ buildPatHy prov (fromPatCompatTc -> p0) = ViewPat _ _ p -> buildPatHy prov p -- Desugar lists into cons ListPat _ [] -> pure mempty - ListPat x@(ListPatTc ty _) (fmap fromPatCompatTc -> (p : ps)) -> + ListPat x@(ListPatTc ty _) (p : ps) -> mkDerivedConHypothesis prov consDataCon [ty] - [ (0, toPatCompatTc p) - , (1, ListPat x $ fmap toPatCompatTc ps) + [ (0, p) + , (1, ListPat x ps) ] -- Desugar tuples into an explicit constructor TuplePat tys pats boxity -> @@ -257,7 +257,7 @@ buildPatHy prov (fromPatCompatTc -> p0) = RecCon r -> mkDerivedRecordHypothesis prov dc args r #if __GLASGOW_HASKELL__ >= 808 - SigPat _ p _ -> buildPatHy prov p + SigPat _ p _ -> buildPatHy prov $ toPatCompatTc p #endif #if __GLASGOW_HASKELL__ == 808 XPat p -> buildPatHy prov $ unLoc p @@ -279,7 +279,7 @@ mkDerivedRecordHypothesis prov dc args (HsRecFields (fmap unLoc -> fs) _) let field_lookup = M.fromList $ zip (fmap (occNameFS . fst) rec_fields) [0..] mkDerivedConHypothesis prov dc args $ fs <&> \(HsRecField (L _ rec_occ) p _) -> ( field_lookup M.! (occNameFS $ occName $ unLoc $ rdrNameFieldOcc rec_occ) - , p + , fromPatCompatTc p ) mkDerivedRecordHypothesis _ _ _ _ = error "impossible! using record pattern on something that isn't a record" From bfc855c77ae6cb1745f1144c38a1ee6878c76eec Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 3 Mar 2021 22:07:14 -0800 Subject: [PATCH 08/10] More PatCompat woes --- .../src/Ide/Plugin/Tactic/LanguageServer.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index d9cee88cf3..640b523f97 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -239,7 +239,7 @@ buildPatHy prov (fromPatCompatTc -> p0) = ListPat x@(ListPatTc ty _) (p : ps) -> mkDerivedConHypothesis prov consDataCon [ty] [ (0, p) - , (1, ListPat x ps) + , (1, toPatCompatTc $ ListPat x ps) ] -- Desugar tuples into an explicit constructor TuplePat tys pats boxity -> @@ -279,7 +279,7 @@ mkDerivedRecordHypothesis prov dc args (HsRecFields (fmap unLoc -> fs) _) let field_lookup = M.fromList $ zip (fmap (occNameFS . fst) rec_fields) [0..] mkDerivedConHypothesis prov dc args $ fs <&> \(HsRecField (L _ rec_occ) p _) -> ( field_lookup M.! (occNameFS $ occName $ unLoc $ rdrNameFieldOcc rec_occ) - , fromPatCompatTc p + , p ) mkDerivedRecordHypothesis _ _ _ _ = error "impossible! using record pattern on something that isn't a record" @@ -305,7 +305,7 @@ mkDerivedConHypothesis -> [Type] -- ^ Applied type variables -> [(Int, PatCompat GhcTc)] -- ^ Patterns, and their order in the data con -> State Int (Hypothesis CType) -mkDerivedConHypothesis prov dc args (fmap (second fromPatCompatTc) -> ps) = do +mkDerivedConHypothesis prov dc args ps = do var <- mkFakeVar hy' <- fmap mconcat $ for ps $ \(ix, p) -> do From ae07231e08ac45af3ca60ca481a7e02e4907c22a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 3 Mar 2021 23:10:47 -0800 Subject: [PATCH 09/10] PatCompat is the bane of my existence --- .../hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 640b523f97..0da4fc512a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -257,7 +257,7 @@ buildPatHy prov (fromPatCompatTc -> p0) = RecCon r -> mkDerivedRecordHypothesis prov dc args r #if __GLASGOW_HASKELL__ >= 808 - SigPat _ p _ -> buildPatHy prov $ toPatCompatTc p + SigPat _ p _ -> buildPatHy prov p #endif #if __GLASGOW_HASKELL__ == 808 XPat p -> buildPatHy prov $ unLoc p From cf5893a14df2cdfe48851179f824e74aabd94ed6 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 4 Mar 2021 14:24:34 -0800 Subject: [PATCH 10/10] Maybe the test was wrong all along --- plugins/hls-tactics-plugin/test/golden/SplitPattern.hs.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/test/golden/SplitPattern.hs.expected b/plugins/hls-tactics-plugin/test/golden/SplitPattern.hs.expected index 720b6fe3c4..8fe407a304 100644 --- a/plugins/hls-tactics-plugin/test/golden/SplitPattern.hs.expected +++ b/plugins/hls-tactics-plugin/test/golden/SplitPattern.hs.expected @@ -7,6 +7,6 @@ case_split Three = _ case_split (Four b One) = _ case_split (Four b (Two i)) = _ case_split (Four b Three) = _ -case_split (Four b (Four b2 a3)) = _ +case_split (Four b (Four b3 a4)) = _ case_split (Four b Five) = _ case_split Five = _