Catamorphism and collapse tactics (#1865)

* Perform lookups of terms in scope and context

* Cata and collapse

* Remove unused import

* Fix bug in intros wrt forall

* Assume a value for cata recursion if necessary

* Add tests

* Fix imports

* Add tests

* Cleanup and haddock

* Null case for letForEach

* mkFunTys'

* Simplify away single-use let bindings

* Use the applicative instance to implement letForEach

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

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

@@ -39,6 +39,7 @@ import           Wingman.Judgements.Theta
 import           Wingman.Machinery
 import           Wingman.Naming
 import           Wingman.Types
+import GHC.SourceGen (occNameToStr)
 
 
 destructMatches
@@ -274,3 +275,27 @@ mkApply occ (lhs : rhs : more)
   = noLoc $ foldl' (@@) (op lhs (coerceName occ) rhs) more
 mkApply occ args = noLoc $ foldl' (@@) (var' occ) args
 
+
+------------------------------------------------------------------------------
+-- | Run a tactic over each term in the given 'Hypothesis', binding the results
+-- of each in a let expression.
+letForEach
+    :: (OccName -> OccName)           -- ^ How to name bound variables
+    -> (HyInfo CType -> TacticsM ())  -- ^ The tactic to run
+    -> Hypothesis CType               -- ^ Terms to generate bindings for
+    -> Judgement                      -- ^ The goal of original hole
+    -> RuleM (Synthesized (LHsExpr GhcPs))
+letForEach rename solve (unHypothesis -> hy) jdg = do
+  case hy of
+    [] -> newSubgoal jdg
+    _ -> do
+      let g = jGoal jdg
+      terms <- fmap sequenceA $ for hy $ \hi -> do
+        let name = rename $ hi_name hi
+        res <- tacticToRule jdg $ solve hi
+        pure $ fmap ((name,) . unLoc) res
+      let hy' = fmap (g <$) $ syn_val terms
+          matches = fmap (fmap (\(occ, expr) -> valBind (occNameToStr occ) expr)) terms
+      g <- fmap (fmap unLoc) $ newSubgoal $ introduce (userHypothesis hy') jdg
+      pure $ fmap noLoc $ let' <$> matches <*> g
+

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

@@ -3,6 +3,7 @@
 
 module Wingman.GHC where
 
+import           Bag (bagToList)
 import           ConLike
 import           Control.Applicative (empty)
 import           Control.Monad.State
@@ -196,6 +197,15 @@ pattern AMatch ctx pats body <-
         }
 
 
+pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
+pattern SingleLet bind pats val expr <-
+  HsLet _
+    (L _ (HsValBinds _
+      (ValBinds _ (bagToList ->
+        [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _)))
+    (L _ expr)
+
+
 ------------------------------------------------------------------------------
 -- | A pattern over the otherwise (extremely) messy AST for lambdas.
 pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs

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

@@ -107,6 +107,12 @@ recursiveHypothesis :: [(OccName, a)] -> Hypothesis a
 recursiveHypothesis = introduceHypothesis $ const $ const RecursivePrv
 
 
+------------------------------------------------------------------------------
+-- | Introduce a binding in a recursive context.
+userHypothesis :: [(OccName, a)] -> Hypothesis a
+userHypothesis = introduceHypothesis $ const $ const UserPrv
+
+
 ------------------------------------------------------------------------------
 -- | Check whether any of the given occnames are an ancestor of the term.
 hasPositionalAncestry
@@ -302,6 +308,12 @@ jLocalHypothesis
   . jHypothesis
 
 
+------------------------------------------------------------------------------
+-- | Filter elements from the hypothesis
+hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a
+hyFilter f  = Hypothesis . filter f . unHypothesis
+
+
 ------------------------------------------------------------------------------
 -- | Given a judgment, return the hypotheses that are acceptable to destruct.
 --

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

@@ -8,7 +8,7 @@ import           Control.Lens ((<>~))
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
 import           Control.Monad.State.Class (gets, modify)
-import           Control.Monad.State.Strict (StateT (..))
+import           Control.Monad.State.Strict (StateT (..), execStateT)
 import           Data.Bool (bool)
 import           Data.Coerce
 import           Data.Either
@@ -55,6 +55,10 @@ newSubgoal j = do
       $ unsetIsTopHole j
 
 
+tacticToRule :: Judgement -> TacticsM () -> Rule
+tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom
+
+
 ------------------------------------------------------------------------------
 -- | Attempt to generate a term of the right type using in-scope bindings, and
 -- a given tactic.

plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs

@@ -68,6 +68,8 @@ oneTactic =
     , nullary   "sorry" sorry
     , nullary   "unary" $ nary 1
     , nullary   "binary" $ nary 2
+    , unary_occ "cata" $ useNameFromHypothesis cata
+    , nullary   "collapse" collapse
     , nullary   "recursion" $
         fmap listToMaybe getCurrentDefinitions >>= \case
           Just (self, _) -> useNameFromContext apply self

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

@@ -11,7 +11,7 @@ import Development.IDE.GHC.Compat
 import GHC.SourceGen (var)
 import GHC.SourceGen.Expr (lambda)
 import Wingman.CodeGen.Utils
-import Wingman.GHC (containsHsVar, fromPatCompat)
+import Wingman.GHC (containsHsVar, fromPatCompat, pattern SingleLet)
 
 
 ------------------------------------------------------------------------------
@@ -30,6 +30,7 @@ pattern Lambda pats body <-
     Lambda pats body = lambda pats body
 
 
+
 ------------------------------------------------------------------------------
 -- | Simlify an expression.
 simplify :: LHsExpr GhcPs -> LHsExpr GhcPs
@@ -41,6 +42,7 @@ simplify
     [ simplifyEtaReduce
     , simplifyRemoveParens
     , simplifyCompose
+    , simplifySingleLet
     ])
 
 
@@ -68,6 +70,13 @@ simplifyEtaReduce = mkT $ \case
     Lambda pats f
   x -> x
 
+------------------------------------------------------------------------------
+-- | Eliminates the unnecessary binding in @let a = b in a@
+simplifySingleLet :: GenericT
+simplifySingleLet = mkT $ \case
+  SingleLet bind [] val (HsVar _ (L _ a)) | a == bind -> val
+  x -> x
+
 
 ------------------------------------------------------------------------------
 -- | Perform an eta-reducing function composition. For example, transforms

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

@@ -111,9 +111,9 @@ intros'
 intros' names = rule $ \jdg -> do
   let g  = jGoal jdg
   ctx <- ask
-  case tcSplitFunTys $ unCType g of
-    ([], _) -> throwError $ GoalMismatch "intros" g
-    (as, b) -> do
+  case tacticsSplitFunTy $ unCType g of
+    (_, _, [], _) -> throwError $ GoalMismatch "intros" g
+    (_, _, as, b) -> do
       let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
           num_args = length vs
           top_hole = isTopHole ctx jdg
@@ -448,14 +448,14 @@ applyByType ty = tracing ("applyByType " <> show ty) $ do
   let (_, _, args, ret) = tacticsSplitFunTy ty'
   rule $ \jdg -> do
     unify g (CType ret)
-    app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg
     ext
         <- fmap unzipTrace
         $ traverse ( newSubgoal
                     . blacklistingDestruct
                     . flip withNewGoal jdg
                     . CType
                     ) args
+    app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg
     pure $
       fmap noLoc $
         foldl' (@@)
@@ -472,3 +472,39 @@ nary n =
     mkInvForAllTys [alphaTyVar, betaTyVar] $
       mkFunTys' (replicate n alphaTy) betaTy
 
+self :: TacticsM ()
+self =
+  fmap listToMaybe getCurrentDefinitions >>= \case
+    Just (self, _) -> useNameFromContext apply self
+    Nothing -> throwError $ TacticPanic "no defining function"
+
+
+cata :: HyInfo CType -> TacticsM ()
+cata hi = do
+  diff <- hyDiff $ destruct hi
+  rule $
+    letForEach
+      (mkVarOcc . flip mappend "_c" . occNameString)
+      (\hi -> self >> commit (apply hi) assumption)
+      diff
+
+collapse :: TacticsM ()
+collapse = do
+  g <- goal
+  let terms = unHypothesis $ hyFilter ((jGoal g ==) . hi_type) $ jLocalHypothesis g
+  case terms of
+    [hi] -> assume $ hi_name hi
+    _    -> nary (length terms) <@> fmap (assume . hi_name) terms
+
+
+------------------------------------------------------------------------------
+-- | Determine the difference in hypothesis due to running a tactic. Also, it
+-- runs the tactic.
+hyDiff :: TacticsM () -> TacticsM (Hypothesis CType)
+hyDiff m = do
+  g <- unHypothesis . jEntireHypothesis <$> goal
+  let g_len = length g
+  m
+  g' <- unHypothesis . jEntireHypothesis <$> goal
+  pure $ Hypothesis $ take (length g' - g_len) g'
+

plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs

@@ -31,4 +31,6 @@ spec = do
     metaTest  5 40 "MetaUseImport"
     metaTest  6 31 "MetaUseLocal"
     metaTest 11 11 "MetaUseMethod"
+    metaTest  9 38 "MetaCataCollapse"
+    metaTest  7 16 "MetaCataCollapseUnary"
 

plugins/hls-tactics-plugin/test/golden/MetaCataCollapse.expected.hs

@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeOperators #-}
+
+import GHC.Generics
+
+class Yo f where
+    yo :: f x -> Int
+
+instance (Yo f, Yo g) => Yo (f :*: g) where
+  yo (fx :*: gx)
+    = let
+        fx_c = yo fx
+        gx_c = yo gx
+      in _ fx_c gx_c
+

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

@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeOperators #-}
+
+import GHC.Generics
+
+class Yo f where
+    yo :: f x -> Int
+
+instance (Yo f, Yo g) => Yo (f :*: g) where
+  yo = [wingman| intros x, cata x, collapse |]
+

plugins/hls-tactics-plugin/test/golden/MetaCataCollapseUnary.expected.hs

@@ -0,0 +1,8 @@
+import GHC.Generics
+
+class Yo f where
+    yo :: f x -> Int
+
+instance (Yo f) => Yo (M1 _1 _2 f) where
+  yo (M1 fx) = yo fx
+

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

@@ -0,0 +1,8 @@
+import GHC.Generics
+
+class Yo f where
+    yo :: f x -> Int
+
+instance (Yo f) => Yo (M1 _1 _2 f) where
+  yo = [wingman| intros x, cata x, collapse |]
+