diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md index 70ba07b654..3405f664c1 100644 --- a/plugins/hls-tactics-plugin/COMMANDS.md +++ b/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. diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs index 2ad926ce74..9966118308 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs +++ b/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 diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index a2f503109d..7d4da7aa6f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/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) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs-boot b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs-boot new file mode 100644 index 0000000000..607db0e6f3 --- /dev/null +++ b/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 ()) + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs index 9347c944ab..632c5cad1a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs +++ b/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 ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index e87ed0560d..f62a0568b0 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/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" - diff --git a/plugins/hls-tactics-plugin/test/golden/MetaPointwise.expected.hs b/plugins/hls-tactics-plugin/test/golden/MetaPointwise.expected.hs new file mode 100644 index 0000000000..f92e7d40af --- /dev/null +++ b/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) + diff --git a/plugins/hls-tactics-plugin/test/golden/MetaPointwise.hs b/plugins/hls-tactics-plugin/test/golden/MetaPointwise.hs new file mode 100644 index 0000000000..77572569ff --- /dev/null +++ b/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|] +