Add pointwise command to the metaprogram parser (#1921)

* Add pointwise command to the metaprogram parser

* Fix documentation

Author: isovector

plugins/hls-tactics-plugin/COMMANDS.md

@@ -389,6 +389,29 @@ running  `obvious` will produce:
 ```haskell
 []
 ```
+## pointwise
+
+arguments: tactic.  
+deterministic.
+
+> Restrict the hypothesis in the holes of the given tactic to align up with the top-level bindings. This will ensure, eg, that the first hole can see only terms that came from the first position in any terms destructed from the top-level bindings.
+
+
+### Example
+
+> In the context of `f (a1, b1) (a2, b2) = _`. The resulting first hole can see only 'a1' and 'a2', and the second, only 'b1' and 'b2'.
+
+Given:
+
+```haskell
+_ 
+```
+
+running  `pointwise (use mappend)` will produce:
+
+```haskell
+mappend _ _
+```
 ## recursion
 
 arguments: none.  

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

@@ -1,8 +1,6 @@
 module Wingman.KnownStrategies where
 
-import Control.Applicative (empty)
 import Control.Monad.Error.Class
-import Control.Monad.Reader.Class (asks)
 import Data.Foldable (for_)
 import OccName (mkVarOcc)
 import Refinery.Tactic

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

@@ -176,6 +176,17 @@ commands =
           "f (_ :: a)"
       ]
 
+  , command "pointwise" Deterministic Tactic
+      "Restrict the hypothesis in the holes of the given tactic to align up with the top-level bindings. This will ensure, eg, that the first hole can see only terms that came from the first position in any terms destructed from the top-level bindings."
+      (pure . flip restrictPositionForApplication (pure ()))
+      [ Example
+          (Just "In the context of `f (a1, b1) (a2, b2) = _`. The resulting first hole can see only 'a1' and 'a2', and the second, only 'b1' and 'b2'.")
+          ["(use mappend)"]
+          []
+          Nothing
+          "mappend _ _"
+      ]
+
   , command "apply" Deterministic (Ref One)
       "Apply the given function from *local* scope."
       (pure . useNameFromHypothesis apply)

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

@@ -0,0 +1,7 @@
+module Wingman.Metaprogramming.Parser where
+
+import Wingman.Metaprogramming.Lexer
+import Wingman.Types
+
+tactic :: Parser (TacticsM ())
+

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

@@ -6,13 +6,15 @@ import           Data.Functor ((<&>))
 import           Data.List (sortOn)
 import           Data.String (IsString)
 import           Data.Text (Text)
-import           Data.Text.Prettyprint.Doc
+import           Data.Text.Prettyprint.Doc hiding (parens)
 import           Data.Text.Prettyprint.Doc.Render.String (renderString)
 import           GhcPlugins (OccName)
 import qualified Text.Megaparsec as P
-import           Wingman.Metaprogramming.Lexer (Parser, identifier, variable)
+import           Wingman.Metaprogramming.Lexer (Parser, identifier, variable, parens)
 import           Wingman.Types (TacticsM)
 
+import {-# SOURCE #-} Wingman.Metaprogramming.Parser (tactic)
+
 
 ------------------------------------------------------------------------------
 -- | Is a tactic deterministic or not?
@@ -46,11 +48,13 @@ data Syntax a where
   Nullary :: Syntax (Parser (TacticsM ()))
   Ref     :: Count a -> Syntax (a -> Parser (TacticsM ()))
   Bind    :: Count a -> Syntax (a -> Parser (TacticsM ()))
+  Tactic  :: Syntax (TacticsM () -> Parser (TacticsM ()))
 
 prettySyntax :: Syntax a -> Doc b
 prettySyntax Nullary   = "none"
 prettySyntax (Ref co)  = prettyCount co <+> "reference"
 prettySyntax (Bind co) = prettyCount co <+> "binding"
+prettySyntax Tactic    = "tactic"
 
 
 ------------------------------------------------------------------------------
@@ -108,21 +112,24 @@ data SomeMetaprogramCommand where
 ------------------------------------------------------------------------------
 -- | Run the 'Parser' of a 'MetaprogramCommand'
 makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())
-makeMPParser (MC name Nullary _ _ tactic _) = do
+makeMPParser (MC name Nullary _ _ t _) = do
+  identifier name
+  t
+makeMPParser (MC name (Ref One) _ _ t _) = do
   identifier name
-  tactic
-makeMPParser (MC name (Ref One) _ _ tactic _) = do
+  variable >>= t
+makeMPParser (MC name (Ref Many) _ _ t _) = do
   identifier name
-  variable >>= tactic
-makeMPParser (MC name (Ref Many) _ _ tactic _) = do
+  P.many variable >>= t
+makeMPParser (MC name (Bind One) _ _ t _) = do
   identifier name
-  P.many variable >>= tactic
-makeMPParser (MC name (Bind One) _ _ tactic _) = do
+  variable >>= t
+makeMPParser (MC name (Bind Many) _ _ t _) = do
   identifier name
-  variable >>= tactic
-makeMPParser (MC name (Bind Many) _ _ tactic _) = do
+  P.many variable >>= t
+makeMPParser (MC name Tactic _ _ t _) = do
   identifier name
-  P.many variable >>= tactic
+  parens tactic >>= t
 
 
 ------------------------------------------------------------------------------

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

@@ -33,5 +33,5 @@ spec = do
     metaTest 11 11 "MetaUseMethod"
     metaTest  9 38 "MetaCataCollapse"
     metaTest  7 16 "MetaCataCollapseUnary"
+    metaTest  6 46 "MetaPointwise"
     metaTest  4 28 "MetaUseSymbol"
-

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

@@ -0,0 +1,8 @@
+import Data.Monoid
+
+data Foo = Foo (Sum Int) (Sum Int)
+
+mappend2 :: Foo -> Foo -> Foo
+mappend2 (Foo sum sum') (Foo sum2 sum3)
+  = Foo (mappend sum sum2) (mappend sum' sum3)
+

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

@@ -0,0 +1,7 @@
+import Data.Monoid
+
+data Foo = Foo (Sum Int) (Sum Int)
+
+mappend2 :: Foo -> Foo -> Foo
+mappend2 = [wingman| intros f1 f2, destruct_all, ctor Foo; pointwise (use mappend); assumption|]
+