Wingman: Let-bindings in metatactics (#2160)

* Add metatactic for let-bindings

* Add test for simple let bindings

* Label hole numbers in the documentation

* Sort imports

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

Author: isovector

plugins/hls-tactics-plugin/COMMANDS.md

@@ -382,6 +382,32 @@ running  `intros x y z w` will produce:
 \x y z -> (_ :: d)
 ```
 
+## let
+
+arguments: varadic binding.  
+deterministic.
+
+> Create let-bindings for each binder given to this tactic.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: x
+```
+
+running  `let a b c` will produce:
+
+```haskell
+let a = _1 :: a
+    b = _2 :: b
+    c = _3 :: c
+ in (_4 :: x)
+
+```
+
 ## nested
 
 arguments: single reference.  

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

@@ -15,6 +15,7 @@ import           Control.Lens ((%~), (<>~), (&))
 import           Control.Monad.Except
 import           Control.Monad.Reader (ask)
 import           Control.Monad.State
+import           Data.Bifunctor (second)
 import           Data.Bool (bool)
 import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
@@ -315,3 +316,23 @@ letForEach rename solve (unHypothesis -> hy) jdg = do
       g <- fmap (fmap unLoc) $ newSubgoal $ introduce ctx (userHypothesis hy') jdg
       pure $ fmap noLoc $ let' <$> matches <*> g
 
+
+------------------------------------------------------------------------------
+-- | Let-bind the given occname judgement pairs.
+nonrecLet
+    :: [(OccName, Judgement)]
+    -> Judgement
+    -> RuleM (Synthesized (LHsExpr GhcPs))
+nonrecLet occjdgs jdg = do
+  occexts <- traverse newSubgoal $ fmap snd occjdgs
+  ctx     <- ask
+  ext     <- newSubgoal
+           $ introduce ctx (userHypothesis $ fmap (second jGoal) occjdgs)
+           $ jdg
+  pure $ fmap noLoc $
+    let'
+      <$> traverse
+            (\(occ, ext) -> valBind (occNameToStr occ) <$> fmap unLoc ext)
+            (zip (fmap fst occjdgs) occexts)
+      <*> fmap unLoc ext
+

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

@@ -348,6 +348,22 @@ commands =
           "(_ :: a -> a -> a -> a) a1 a2 a3"
       ]
 
+  , command "let" Deterministic (Bind Many)
+      "Create let-bindings for each binder given to this tactic."
+      (pure . letBind)
+      [ Example
+          Nothing
+          ["a", "b", "c"]
+          [ ]
+          (Just "x")
+          $ T.pack $ unlines
+            [ "let a = _1 :: a"
+            , "    b = _2 :: b"
+            , "    c = _3 :: c"
+            , " in (_4 :: x)"
+            ]
+      ]
+
   , command "try" Nondeterministic Tactic
       "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states."
       (pure . R.try)

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

@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
 
 module Wingman.Tactics
   ( module Wingman.Tactics
@@ -23,6 +24,7 @@ import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Set (Set)
 import qualified Data.Set as S
+import           Data.Traversable (for)
 import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
@@ -579,6 +581,19 @@ cata hi = do
       $ Hypothesis unifiable_diff
 
 
+letBind :: [OccName] -> TacticsM ()
+letBind occs = do
+  jdg <- goal
+  occ_tys <- for occs
+           $ \occ
+          -> fmap (occ, )
+           $ fmap (<$ jdg)
+           $ fmap CType
+           $ freshTyvars
+           $ mkInvForAllTys [alphaTyVar] alphaTy
+  rule $ nonrecLet occ_tys
+
+
 ------------------------------------------------------------------------------
 -- | Deeply nest an unsaturated function onto itself
 nested :: OccName -> TacticsM ()

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

@@ -39,5 +39,7 @@ spec = do
     metaTest  4 28 "MetaUseSymbol"
     metaTest  7 53 "MetaDeepOf"
     metaTest  2 34 "MetaWithArg"
+    metaTest  2 18 "MetaLetSimple"
+
     metaTest  2 12 "IntrosTooMany"
 

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

@@ -0,0 +1,7 @@
+test :: Int
+test
+  = let
+      a = _w0
+      b = _w1
+      c = _w2
+    in _w3

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

@@ -0,0 +1,2 @@
+test :: Int
+test = [wingman| let a b c |]