From c15c6bf8212b892842591a604b14c12cc0215c7c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 14 Jun 2021 05:48:03 -0700 Subject: [PATCH 1/2] Add pointwise command to the metaprogram parser --- plugins/hls-tactics-plugin/COMMANDS.md | 23 ++++++++++++++ .../src/Wingman/KnownStrategies.hs | 2 -- .../src/Wingman/Metaprogramming/Parser.hs | 11 +++++++ .../Wingman/Metaprogramming/Parser.hs-boot | 7 +++++ .../Metaprogramming/Parser/Documentation.hs | 31 ++++++++++++------- .../test/CodeAction/RunMetaprogramSpec.hs | 1 + .../test/golden/MetaPointwise.expected.hs | 8 +++++ .../test/golden/MetaPointwise.hs | 7 +++++ 8 files changed, 76 insertions(+), 14 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs-boot create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaPointwise.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/MetaPointwise.hs diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md index 70ba07b654..e47ca3a20a 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 argument to the function. + + +### Example + +> In the context of `f a b = _`. The resulting first hole can see only 'a', and the second, only 'b'. + +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..ce7de85a9d 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 argument to the function." + (pure . flip restrictPositionForApplication (pure ())) + [ Example + (Just "In the context of `f a b = _`. The resulting first hole can see only 'a', and the second, only 'b'.") + ["(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 a54cd44999..121846a374 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs @@ -33,4 +33,5 @@ spec = do metaTest 11 11 "MetaUseMethod" metaTest 9 38 "MetaCataCollapse" metaTest 7 16 "MetaCataCollapseUnary" + metaTest 6 46 "MetaPointwise" 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|] + From 3af989add660ae3859b217189f2f0488a0fc2d58 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 14 Jun 2021 05:52:55 -0700 Subject: [PATCH 2/2] Fix documentation --- plugins/hls-tactics-plugin/COMMANDS.md | 4 ++-- .../hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md index e47ca3a20a..3405f664c1 100644 --- a/plugins/hls-tactics-plugin/COMMANDS.md +++ b/plugins/hls-tactics-plugin/COMMANDS.md @@ -394,12 +394,12 @@ running `obvious` will produce: 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 argument to the function. +> 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 a b = _`. The resulting first hole can see only 'a', and the second, only 'b'. +> 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: diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index ce7de85a9d..7d4da7aa6f 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -177,10 +177,10 @@ commands = ] , 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 argument to the function." + "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 a b = _`. The resulting first hole can see only 'a', and the second, only 'b'.") + (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