[wip] not working, but most of the pieces are here

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

@@ -167,6 +167,15 @@ destruct' f hi jdg = do
     & #syn_val       %~ noLoc . case' (var' term)
 
 
+destructExpr :: (ConLike -> Judgement -> Rule) -> HsExpr GhcPs -> Type -> Judgement -> Rule
+destructExpr f term ty jdg = do
+  ext
+      <- destructMatches f Nothing (CType ty) jdg
+  pure $ ext
+    & #syn_trace     %~ rose ("destruct " <> show term) . pure
+    & #syn_val       %~ noLoc . case' term
+
+
 ------------------------------------------------------------------------------
 -- | Combinator for performign case splitting, and running sub-rules on the
 -- resulting matches.

plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

@@ -57,6 +57,7 @@ import           Wingman.Judgements.SYB (everythingContaining, smallestQ, generi
 import           Wingman.Judgements.Theta
 import           Wingman.Range
 import           Wingman.Types
+import Control.Applicative (empty)
 
 
 tacticDesc :: T.Text -> T.Text
@@ -165,6 +166,11 @@ getIdeDynflags state nfp = do
   pure $ ms_hspp_opts $ msrModSummary msr
 
 
+data GoalOrScrutinee
+  = Goal Type
+  | Scrutinee (HsExpr GhcPs) Type
+
+
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
 -- as the judgement at the given range.
@@ -173,7 +179,7 @@ judgementForHole
     -> NormalizedFilePath
     -> Tracked 'Current Range
     -> FeatureSet
-    -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
+    -> MaybeT IO (Tracked 'Current Range, Hook (), Context, DynFlags)
 judgementForHole state nfp range features = do
   TrackedStale asts amapping  <- runStaleIde state nfp GetHieAst
   case unTrack asts of
@@ -185,24 +191,30 @@ judgementForHole state nfp range features = do
            $ runStaleIde state nfp TypeCheck
       hscenv <- runStaleIde state nfp GhcSessionDeps
 
-      rss2 <- liftMaybe $ getSpanAtCursor range' hf
-      (new_span, scrutinee) <- liftMaybe $ getFirst $
-        emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds $ untrackedStaleValue tcg
-      x <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) (untrackedStaleValue tcg) scrutinee
-
-      (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
-      new_rss <- liftMaybe $ mapAgeTo amapping rss
-
       -- KnownThings is just the instances in scope. There are no ranges
       -- involved, so it's not crucial to track ages.
-      let henv = untrackedStaleValue $ hscenv
+      let henv = untrackedStaleValue hscenv
+          untracked_tcg = untrackedStaleValue tcg
       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
-      kt <- knownThings (untrackedStaleValue tcg) henv
+      kt <- knownThings untracked_tcg henv
+
+      (rss, g_or_s) <-
+        case getSpanAndTypeAtHole range' hf of
+          Just (rss, g) -> pure (rss, Goal g)
+          Nothing -> do
+            rss2 <- liftMaybe $ getSpanAtCursor range' hf
+            (new_span, scrutinee) <- liftMaybe $ getFirst $
+              emptyCaseQ (RealSrcSpan $ unTrack rss2) $ tcg_binds untracked_tcg
+            ty <- MaybeT $ typeCheck (hscEnv henv) untracked_tcg scrutinee
+            case new_span of
+              RealSrcSpan rss -> pure (pure rss, Scrutinee scrutinee ty)
+              UnhelpfulSpan _ -> empty
 
-      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt
+      new_rss <- liftMaybe $ mapAgeTo amapping rss
+      (hook, ctx) <- liftMaybe $ mkJudgementAndContext features g_or_s binds new_rss tcg eps kt
 
       dflags <- getIdeDynflags state nfp
-      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
+      pure (fmap realSrcSpanToRange new_rss, hook, ctx, dflags)
 
 
 
@@ -219,14 +231,14 @@ emptyCaseQ span =
 
 mkJudgementAndContext
     :: FeatureSet
-    -> Type
+    -> GoalOrScrutinee
     -> TrackedStale Bindings
     -> Tracked 'Current RealSrcSpan
     -> TrackedStale TcGblEnv
     -> ExternalPackageState
     -> KnownThings
-    -> Maybe (Judgement, Context)
-mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
+    -> Maybe (Hook (), Context)
+mkJudgementAndContext features g_or_s (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
   binds_rss <- mapAgeFrom bmap rss
   tcg_rss <- mapAgeFrom tcgmap rss
 
@@ -246,14 +258,19 @@ mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg
       evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs
       cls_hy = foldMap evidenceToHypothesis evidence
       subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
+
   pure $
-    ( disallowing AlreadyDestructed already_destructed
-    $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
-          (local_hy <> cls_hy)
-          (isRhsHole tcg_rss tcs)
-          g
-    , ctx
-    )
+    case g_or_s of
+      Goal g ->
+        ( Tactic ()
+        $ disallowing AlreadyDestructed already_destructed
+        $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
+              (local_hy <> cls_hy)
+              (isRhsHole tcg_rss tcs)
+              g
+        , ctx
+        )
+      Scrutinee scrutinee ty -> (EmptyCase scrutinee ty, ctx)
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs

@@ -152,7 +152,7 @@ data TacticProviderData = TacticProviderData
   , tpd_plid   :: PluginId
   , tpd_uri    :: Uri
   , tpd_range  :: Tracked 'Current Range
-  , tpd_jdg    :: Judgement
+  , tpd_hook   :: Hook ()
   }
 
 
@@ -189,17 +189,21 @@ requireExtension ext tp tpd =
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp tpd =
-  case p $ unCType $ jGoal $ tpd_jdg tpd of
-    True  -> tp tpd
-    False -> pure []
+filterGoalType p tp =
+  withJudgement $ \jdg ->
+    case p $ unCType $ jGoal jdg of
+      True  -> tp
+      False -> mempty
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 withJudgement :: (Judgement -> TacticProvider) -> TacticProvider
-withJudgement tp tpd = tp (tpd_jdg tpd) tpd
+withJudgement tp tpd =
+  case tpd_hook tpd of
+    Tactic _ jdg -> tp jdg tpd
+    _ -> pure []
 
 
 ------------------------------------------------------------------------------
@@ -210,14 +214,16 @@ filterBindingType
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
 filterBindingType p tp tpd =
-  let jdg = tpd_jdg tpd
-      hy  = jLocalHypothesis jdg
-      g   = jGoal jdg
-   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 tpd
-              False -> pure []
+  case tpd_hook tpd of
+    Tactic _ jdg ->
+      let hy  = jLocalHypothesis jdg
+          g   = jGoal jdg
+      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 tpd
+                  False -> pure []
+    _ -> mempty
 
 
 ------------------------------------------------------------------------------
@@ -228,9 +234,11 @@ filterTypeProjection
     -> (a -> TacticProvider)
     -> TacticProvider
 filterTypeProjection p tp tpd =
-  fmap join $ for (p $ unCType $ jGoal $ tpd_jdg tpd) $ \a ->
-      tp a tpd
-
+  case tpd_hook tpd of
+    Tactic _ jdg ->
+      fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
+          tp a tpd
+    _ -> mempty
 
 ------------------------------------------------------------------------------
 -- | Get access to the 'Config' when building a 'TacticProvider'.

plugins/hls-tactics-plugin/src/Wingman/Machinery.hs

@@ -33,6 +33,7 @@ import           Unify
 import           Wingman.Judgements
 import           Wingman.Simplify (simplify)
 import           Wingman.Types
+import GhcPlugins (unitTy)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -52,6 +53,7 @@ newSubgoal j = do
       $ unsetIsTopHole j
 
 
+
 ------------------------------------------------------------------------------
 -- | Attempt to generate a term of the right type using in-scope bindings, and
 -- a given tactic.

plugins/hls-tactics-plugin/src/Wingman/Plugin.hs

@@ -36,6 +36,8 @@ import           Wingman.Machinery (scoreSolution)
 import           Wingman.Range
 import           Wingman.Tactics
 import           Wingman.Types
+import GhcPlugins (unitTy)
+import Wingman.Judgements (mkFirstJudgement)
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -60,7 +62,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       cfg <- getTacticConfig plId
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
+        (_, hook, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound] $ TacticProviderData
@@ -69,7 +71,7 @@ codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri)
             , tpd_plid   = plId
             , tpd_uri    = uri
             , tpd_range  = range
-            , tpd_jdg    = jdg
+            , tpd_hook   = hook
             }
         pure $ Right $ List actions
 codeActionProvider _ _ _ = pure $ Right $ List []
@@ -214,3 +216,11 @@ graftDecl _ _ _ _ x = pure $ pure x
 fromMaybeT :: Functor m => a -> MaybeT m a -> m a
 fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 
+
+runHook
+    :: Context
+    -> Hook (TacticsM ())
+    -> Either [TacticError] RunTacticResults
+runHook ctx (Tactic t jdg) = runTactic ctx jdg t
+runHook ctx (EmptyCase ty) = runTactic ctx (mkFirstJudgement mempty False unitTy) _
+

plugins/hls-tactics-plugin/src/Wingman/Types.hs

@@ -490,3 +490,9 @@ instance Show UserFacingMessage where
   show NothingToDo             = "Nothing to do"
   show (InfrastructureError t) = "Internal error: " <> T.unpack t
 
+
+data Hook a
+  = Tactic a Judgement
+  | EmptyCase (HsExpr GhcPs) Type
+  deriving Functor
+