Refactor the hypothesis type in hls-tactics-plugin (#1347)

* Add name to HyInfo

* Use a newtype for Hypotheses

* Use a set for tracking names in scope

* Remove the internal Map OccName representation of Hypothesis

* Remove most spurious uses of hyByName

* Stop looking up things by name in hyByName; use hi directly

* Cleanup imports

* Add test for invoking methods at different types

* Improve generated names for tyvar applications

* Minor formatting and haddocks

* Minor styling

* Fix test

Author: isovector

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs

@@ -17,6 +17,7 @@ module Ide.Plugin.Tactic
 
 import           Control.Arrow
 import           Control.Monad
+import           Control.Monad.Error.Class (MonadError(throwError))
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
@@ -38,6 +39,7 @@ 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.ExactPrint (graft, transform, useAnnotatedSource)
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
 import           DynFlags (xopt)
@@ -53,11 +55,11 @@ import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
 import           Ide.PluginUtils
-import Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource)
 import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
@@ -124,12 +126,24 @@ commandProvider HomomorphismLambdaCase =
 commandTactic :: TacticCommand -> OccName -> TacticsM ()
 commandTactic Auto         = const auto
 commandTactic Intros       = const intros
-commandTactic Destruct     = destruct
-commandTactic Homomorphism = homo
+commandTactic Destruct     = useNameFromHypothesis destruct
+commandTactic Homomorphism = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 
 
+------------------------------------------------------------------------------
+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
+-- look it up in the hypothesis.
+useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
+useNameFromHypothesis f name = do
+  hy <- jHypothesis <$> goal
+  case M.lookup name $ hyByName hy of
+    Just hi -> f hi
+    Nothing -> throwError $ NotInScope name
+
+
+
 ------------------------------------------------------------------------------
 -- | We should show homos only when the goal type is the same as the binding
 -- type, and that both are usual algebraic types.
@@ -216,10 +230,11 @@ filterBindingType
 filterBindingType p tp dflags plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
-   in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) ->
-        case p (unCType g) ty of
-          True  -> tp occ ty dflags plId uri range jdg
-          False -> pure []
+   in fmap join $ for (unHypothesis hy) $ \hi ->
+        let ty = unCType $ hi_type hi
+         in case p (unCType g) ty of
+              True  -> tp (hi_name hi) ty dflags plId uri range jdg
+              False -> pure []
 
 
 data TacticParams = TacticParams
@@ -287,11 +302,11 @@ judgementForHole state nfp range = do
 
 spliceProvenance
     :: Map OccName Provenance
-    -> Map OccName (HyInfo a)
-    -> Map OccName (HyInfo a)
-spliceProvenance provs =
-  M.mapWithKey $ \name hi ->
-    overProvenance (maybe id const $ M.lookup name provs) hi
+    -> Hypothesis a
+    -> Hypothesis a
+spliceProvenance provs x =
+  Hypothesis $ flip fmap (unHypothesis x) $ \hi ->
+    overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi
 
 
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs

@@ -35,7 +35,7 @@ import           Type hiding (Var)
 useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
 useOccName jdg name =
   -- Only score points if this is in the local hypothesis
-  case M.lookup name $ jLocalHypothesis jdg of
+  case M.lookup name $ hyByName $ jLocalHypothesis jdg of
     Just{}  -> modify
              $ (withUsedVals $ S.insert name)
              . (field @"ts_unused_top_vals" %~ S.delete name)
@@ -75,7 +75,7 @@ destructMatches f scrut t jdg = do
         [] -> throwError $ GoalMismatch "destruct" g
         _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let args = dataConInstOrigArgTys' dc apps
-          names <- mkManyGoodNames hy args
+          names <- mkManyGoodNames (hyNamesInScope hy) args
           let hy' = zip names $ coerce args
               j = introducingPat scrut dc hy'
                 $ withNewGoal g jdg
@@ -150,23 +150,20 @@ dataConInstOrigArgTys' con uniTys =
 -- | 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
+destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
+destruct' f hi jdg = do
   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
-  let hy = jHypothesis jdg
-  case M.lookup term hy of
-    Nothing -> throwError $ UndefinedHypothesis term
-    Just (hi_type -> t) -> do
-      useOccName jdg term
-      (tr, ms)
-          <- destructMatches
-               f
-               (Just term)
-               t
-               $ disallowing AlreadyDestructed [term] jdg
-      pure ( rose ("destruct " <> show term) $ pure tr
-           , noLoc $ case' (var' term) ms
-           )
+  let term = hi_name hi
+  useOccName jdg term
+  (tr, ms)
+      <- destructMatches
+           f
+           (Just term)
+           (hi_type hi)
+           $ disallowing AlreadyDestructed [term] jdg
+  pure ( rose ("destruct " <> show term) $ pure tr
+       , noLoc $ case' (var' term) ms
+       )
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs

@@ -35,9 +35,9 @@ mkContext locals tcg = Context
 
 ------------------------------------------------------------------------------
 -- | Find all of the class methods that exist from the givens in the context.
-contextMethodHypothesis :: Context -> Map OccName (HyInfo CType)
+contextMethodHypothesis :: Context -> Hypothesis CType
 contextMethodHypothesis ctx
-  = M.fromList
+  = Hypothesis
   . excludeForbiddenMethods
   . join
   . concatMap
@@ -54,8 +54,8 @@ contextMethodHypothesis ctx
 -- | Many operations are defined in typeclasses for performance reasons, rather
 -- than being a true part of the class. This function filters out those, in
 -- order to keep our hypothesis space small.
-excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)]
-excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)
+excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
   where
     forbiddenMethods :: Set OccName
     forbiddenMethods = S.map mkVarOcc $ S.fromList

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs

@@ -26,8 +26,11 @@ module Ide.Plugin.Tactic.Judgements
   , mkFirstJudgement
   , hypothesisFromBindings
   , isTopLevel
+  , hyNamesInScope
+  , hyByName
   ) where
 
+import           Control.Arrow
 import           Control.Lens hiding (Context)
 import           Data.Bool
 import           Data.Char
@@ -48,20 +51,20 @@ import           Type
 
 ------------------------------------------------------------------------------
 -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
-hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)
+hypothesisFromBindings :: RealSrcSpan -> Bindings -> Hypothesis CType
 hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span
 
 
 ------------------------------------------------------------------------------
 -- | Convert a @Set Id@ into a hypothesis.
-buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType)
+buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
 buildHypothesis
-  = M.fromList
+  = Hypothesis
   . mapMaybe go
   where
     go (occName -> occ, t)
       | Just ty <- t
-      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty)
+      , isAlpha . head . occNameString $ occ = Just $ HyInfo occ UserPrv $ CType ty
       | otherwise = Nothing
 
 
@@ -96,8 +99,8 @@ introducing
     -> Judgement' a
     -> Judgement' a
 introducing f ns =
-  field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>
-    \(pos, (name, ty)) -> (name, HyInfo (f pos) ty))
+  field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&>
+    \(pos, (name, ty)) -> HyInfo name (f pos) ty)
 
 
 ------------------------------------------------------------------------------
@@ -149,7 +152,7 @@ filterAncestry
     -> Judgement
     -> Judgement
 filterAncestry ancestry reason jdg =
-    disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg
+    disallowing reason (M.keys $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg
   where
     go name _
       = not
@@ -172,7 +175,7 @@ findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
 findPositionVal jdg defn pos = listToMaybe $ do
   -- It's important to inspect the entire hypothesis here, as we need to trace
   -- ancstry through potentially disallowed terms in the hypothesis.
-  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg
+  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg
   case hi_provenance hi of
     TopLevelArgPrv defn' pos'
       | defn == defn'
@@ -188,7 +191,7 @@ findPositionVal jdg defn pos = listToMaybe $ do
 -- 'filterSameTypeFromOtherPositions'.
 findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]
 findDconPositionVals jdg dcon pos = do
-  (name, hi) <- M.toList $ jHypothesis jdg
+  (name, hi) <- M.toList $ hyByName $ jHypothesis jdg
   case hi_provenance hi of
     PatternMatchPrv pv
       | pv_datacon  pv == Uniquely dcon
@@ -203,14 +206,15 @@ findDconPositionVals jdg dcon pos = do
 -- other term which might match.
 filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement
 filterSameTypeFromOtherPositions dcon pos jdg =
-  let hy = jHypothesis
+  let hy = hyByName
+         . jHypothesis
          $ filterAncestry
              (findDconPositionVals jdg dcon pos)
              (WrongBranch pos)
              jdg
       tys = S.fromList $ hi_type <$> M.elems hy
       to_remove =
-        M.filter (flip S.member tys . hi_type) (jHypothesis jdg)
+        M.filter (flip S.member tys . hi_type) (hyByName $ jHypothesis jdg)
           M.\\ hy
    in disallowing Shadowed (M.keys to_remove) jdg
 
@@ -267,8 +271,8 @@ introducingPat scrutinee dc ns jdg
 -- them from 'jHypothesis', but not from 'jEntireHypothesis'.
 disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
 disallowing reason (S.fromList -> ns) =
-  field @"_jHypothesis" %~ (M.mapWithKey $ \name hi ->
-    case S.member name ns of
+  field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->
+    case S.member (hi_name hi) ns of
       True -> overProvenance (DisallowedPrv reason) hi
       False -> hi
                            )
@@ -277,20 +281,28 @@ disallowing reason (S.fromList -> ns) =
 ------------------------------------------------------------------------------
 -- | The hypothesis, consisting of local terms and the ambient environment
 -- (impors and class methods.) Hides disallowed values.
-jHypothesis :: Judgement' a -> Map OccName (HyInfo a)
-jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis
+jHypothesis :: Judgement' a -> Hypothesis a
+jHypothesis
+  = Hypothesis
+  . filter (not . isDisallowed . hi_provenance)
+  . unHypothesis
+  . jEntireHypothesis
 
 
 ------------------------------------------------------------------------------
 -- | The whole hypothesis, including things disallowed.
-jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)
+jEntireHypothesis :: Judgement' a -> Hypothesis a
 jEntireHypothesis = _jHypothesis
 
 
 ------------------------------------------------------------------------------
 -- | Just the local hypothesis.
-jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)
-jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis
+jLocalHypothesis :: Judgement' a -> Hypothesis a
+jLocalHypothesis
+  = Hypothesis
+  . filter (isLocalHypothesis . hi_provenance)
+  . unHypothesis
+  . jHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -304,10 +316,30 @@ unsetIsTopHole :: Judgement' a -> Judgement' a
 unsetIsTopHole = field @"_jIsTopHole" .~ False
 
 
+------------------------------------------------------------------------------
+-- | What names are currently in scope in the hypothesis?
+hyNamesInScope :: Hypothesis a -> Set OccName
+hyNamesInScope = M.keysSet . hyByName
+
+
+------------------------------------------------------------------------------
+-- | Fold a hypothesis into a single mapping from name to info. This
+-- unavoidably will cause duplicate names (things like methods) to shadow one
+-- another.
+hyByName :: Hypothesis a -> Map OccName (HyInfo a)
+hyByName
+  = M.fromList
+  . fmap (hi_name &&& id)
+  . unHypothesis
+
+
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
 jPatHypothesis :: Judgement' a -> Map OccName PatVal
-jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis
+jPatHypothesis
+  = M.mapMaybe (getPatVal . hi_provenance)
+  . hyByName
+  . jHypothesis
 
 
 getPatVal :: Provenance-> Maybe PatVal
@@ -326,7 +358,7 @@ substJdg subst = fmap $ coerce . substTy subst . coerce
 
 
 mkFirstJudgement
-    :: M.Map OccName (HyInfo CType)
+    :: Hypothesis CType
     -> Bool  -- ^ are we in the top level rhs hole?
     -> Type
     -> Judgement' CType

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs

@@ -74,9 +74,11 @@ runTactic ctx jdg t =
                 $ (:) (jGoal jdg)
                 $ fmap hi_type
                 $ toList
+                $ hyByName
                 $ jHypothesis jdg
         unused_topvals = M.keysSet
                        $ M.filter (isTopLevel . hi_provenance)
+                       $ hyByName
                        $ jHypothesis jdg
         tacticState =
           defaultTacticState
@@ -218,7 +220,7 @@ unify goal inst = do
 ------------------------------------------------------------------------------
 -- | Get the class methods of a 'PredType', correctly dealing with
 -- instantiation of quantified class types.
-methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]
+methodHypothesis :: PredType -> Maybe [HyInfo CType]
 methodHypothesis ty = do
   (tc, apps) <- splitTyConApp_maybe ty
   cls <- tyConClass_maybe tc
@@ -230,8 +232,7 @@ methodHypothesis ty = do
               $ classSCTheta cls
   pure $ mappend sc_methods $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
-    in ( occName method
-       , HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
+    in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
        )