From 10a0edb878cb151e5e237c3203d042e416dca0f4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 5 Sep 2021 20:23:44 -0700
Subject: [PATCH] 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>
---
plugins/hls-tactics-plugin/COMMANDS.md | 26 +++++++++++++++++++
.../hls-tactics-plugin/src/Wingman/CodeGen.hs | 21 +++++++++++++++
.../src/Wingman/Metaprogramming/Parser.hs | 16 ++++++++++++
.../hls-tactics-plugin/src/Wingman/Tactics.hs | 15 +++++++++++
.../test/CodeAction/RunMetaprogramSpec.hs | 2 ++
.../test/golden/MetaLetSimple.expected.hs | 7 +++++
.../test/golden/MetaLetSimple.hs | 2 ++
7 files changed, 89 insertions(+)
create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaLetSimple.expected.hs
create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs
diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md
index be3cc59b..6a1c00b5 100644
--- a/plugins/hls-tactics-plugin/COMMANDS.md
+++ b/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.
diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 57afba70..07b112e0 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/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
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
index d22c2036..c16b9dca 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs
+++ b/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)
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index a853335e..9075acb3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/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 ()
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index 94eb664a..2fdf6a89 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/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"
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.expected.hs
new file mode 100644
index 00000000..54c3678c
--- /dev/null
+++ b/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
diff --git a/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs
new file mode 100644
index 00000000..ae570bae
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/MetaLetSimple.hs
@@ -0,0 +1,2 @@
+test :: Int
+test = [wingman| let a b c |]
--
GitLab