Generate a more robust top-level binding Provenance

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
 
 ------------------------------------------------------------------------------
@@ -271,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

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
 --

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, tupleDataCon, consDataCon)
+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
@@ -178,37 +179,162 @@ 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 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
+    -- Desugar lists into cons
+    ListPat _ [] -> pure mempty
+    ListPat x@(ListPatTc ty _) (p : ps) ->
+      mkDerivedConHypothesis prov consDataCon [ty]
+        [ (0, p)
+        , (1, toPatCompatTc $ ListPat x 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
+#if __GLASGOW_HASKELL__ >= 808
+    SigPat  _ p _ -> buildPatHy prov $ toPatCompatTc 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 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

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
+

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
 
 

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:

plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs

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

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 = _
+