From fc815e22b0f7c11ed72af5514463dc2641cfc9b6 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 10:58:27 -0700 Subject: [PATCH 1/6] Begin documenting the metaprogram parser --- .../src/Wingman/Metaprogramming/Parser.hs | 132 +++++++++++++++- .../Metaprogramming/Parser/Documentation.hs | 142 ++++++++++++++++++ 2 files changed, 267 insertions(+), 7 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index 0eb52007af..3f2a59b2d8 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -22,6 +22,7 @@ import Wingman.Metaprogramming.Lexer import Wingman.Metaprogramming.ProofState (proofState, layout) import Wingman.Tactics import Wingman.Types +import Wingman.Metaprogramming.Parser.Documentation nullary :: T.Text -> TacticsM () -> Parser (TacticsM ()) @@ -42,6 +43,123 @@ variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ()) variadic_occ name tac = tac <$> (identifier name *> P.many variable) +commands :: [SomeMetaprogramCommand] +commands = + [ command + "assumption" + Nullary + "Use any term in the hypothesis that can unify with the current goal." + (pure assumption) + [ Example + Nothing + [] + [EHI "some_a_val" "a"] + (Just "a") + "some_a_val" + ] + + , command + "assume" + (Ref One) + "Use the given term from the hypothesis, unifying it with the current goal" + (pure . assume) + [ Example + Nothing + ["some_a_val"] + [EHI "some_a_val" "a"] + (Just "a") + "some_a_val" + ] + + , command + "intros" + (Bind Many) + ( mconcat + [ "Construct a lambda expression, using the specific names if given, " + , "generating unique names otherwise. When no arguments are given, " + , "all of the function arguments will be bound; otherwise, this " + , "tactic will bind only enough to saturate the given names. Extra " + , "names are ignored." + ]) + (pure . \case + [] -> intros + names -> intros' $ Just names + ) + [ Example + Nothing + [] + [] + (Just "a -> b -> c -> d") + "\\a b c -> (_ :: d)" + , Example + Nothing + ["aye"] + [] + (Just "a -> b -> c -> d") + "\\aye -> (_ :: b -> c -> d)" + , Example + Nothing + ["x", "y", "z", "w"] + [] + (Just "a -> b -> c -> d") + "\\x y z -> (_ :: d)" + ] + + , command + "intro" + (Bind One) + "Construct a lambda expression, binding an argument with the given name." + (pure . intros' . Just . pure) + [ Example + Nothing + ["aye"] + [] + (Just "a -> b -> c -> d") + "\\aye -> (_ :: b -> c -> d)" + ] + + , command + "destruct_all" + Nullary + "Pattern match on every function paramater, in original binding order." + (pure destructAll) + [ Example + (Just "If `a` and `b` were bound via `f a b = _`, then:") + [] + [EHI "a" "Bool", EHI "b" "Maybe Int"] + Nothing $ + T.pack $ unlines + [ "case a of" + , " False -> case b of" + , " Nothing -> _" + , " Just i -> _" + , " True -> case b of" + , " Nothing -> _" + , " Just i -> _" + ] + ] + + , command + "destruct" + (Ref One) + "Pattern match on the argument." + (pure . useNameFromHypothesis destruct) + [ Example + Nothing + ["a"] + [EHI "a" "Bool"] + Nothing $ + T.pack $ unlines + [ "case a of" + , " False -> _" + , " True -> _" + ] + ] + + ] + + + oneTactic :: Parser (TacticsM ()) oneTactic = P.choice @@ -49,13 +167,13 @@ oneTactic = -- TODO(sandy): lean uses braces for control flow, but i always forget -- and want to use parens. is there a semantic difference? , parens tactic - , nullary "assumption" assumption - , unary_occ "assume" assume - , variadic_occ "intros" $ \case - [] -> intros - names -> intros' $ Just names - , unary_occ "intro" $ intros' . Just . pure - , nullary "destruct_all" destructAll + -- , nullary "assumption" assumption + -- , unary_occ "assume" assume + -- , variadic_occ "intros" $ \case + -- [] -> intros + -- names -> intros' $ Just names + -- , unary_occ "intro" $ intros' . Just . pure + -- , nullary "destruct_all" destructAll , unary_occ "destruct" $ useNameFromHypothesis destruct , unary_occ "homo" $ useNameFromHypothesis homo , nullary "application" application diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs new file mode 100644 index 0000000000..56807b205f --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -0,0 +1,142 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Wingman.Metaprogramming.Parser.Documentation where + +import Data.String (IsString) +import Data.Text (Text) +import GhcPlugins (OccName) +import Wingman.Metaprogramming.Lexer (Parser, identifier, variable) +import Wingman.Types (TacticsM) +import qualified Text.Megaparsec as P +import Data.Functor ((<&>)) +import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc.Render.String (renderString) + + +data Count a where + One :: Count OccName + Many :: Count [OccName] + +data Syntax a where + Nullary :: Syntax (Parser (TacticsM ())) + Ref :: Count a -> Syntax (a -> Parser (TacticsM ())) + Bind :: Count a -> Syntax (a -> Parser (TacticsM ())) + +data Example = Example + { ex_ctx :: Maybe Text + , ex_args :: [Var] + , ex_hyp :: [ExampleHyInfo] + , ex_goal :: Maybe ExampleType + , ex_result :: Text + } + + +data ExampleHyInfo = EHI + { ehi_name :: Var + , ehi_type :: ExampleType + } + +newtype Var = Var + { getVar :: Text + } + deriving newtype (IsString, Pretty) + +newtype ExampleType = ExampleType + { getExampleType :: Text + } + deriving newtype (IsString, Pretty) + + +data MetaprogramCommand a = MC + { mpc_name :: Text + , mpc_syntax :: Syntax a + , mpc_description :: Text + , mpc_tactic :: a + , mpc_examples :: [Example] + } + +data SomeMetaprogramCommand where + SMC :: MetaprogramCommand a -> SomeMetaprogramCommand + + +makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ()) +makeMPParser (MC name Nullary _ tactic _) = do + identifier name + tactic +makeMPParser (MC name (Ref One) _ tactic _) = do + identifier name + variable >>= tactic +makeMPParser (MC name (Ref Many) _ tactic _) = do + identifier name + P.many variable >>= tactic +makeMPParser (MC name (Bind One) _ tactic _) = do + identifier name + variable >>= tactic +makeMPParser (MC name (Bind Many) _ tactic _) = do + identifier name + P.many variable >>= tactic + + +makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ()) +makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp + +prettyCommand :: MetaprogramCommand a -> Doc b +prettyCommand (MC name syn desc _ exs) = vsep + [ "##" <+> pretty name + , mempty + , pretty desc + , mempty + , mempty + , "### Examples" + , mempty + , concatWith (\a b -> vsep [a, "---", b]) $ fmap (prettyExample name) exs + ] + + +prettyHyInfo :: ExampleHyInfo -> Doc a +prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi) + +prettyExample :: Text -> Example -> Doc a +prettyExample name (Example m_txt args hys goal res) = + align $ vsep + [ maybe mempty ((<> line) . pretty) m_txt + , codeFence $ vsep + $ fmap prettyHyInfo hys + <> [ mempty + , "_" <+> maybe mempty (("::" <+>). pretty) goal + ] + , mempty + , ">" <+> enclose "`" "`" (pretty name <+> hsep (fmap pretty args)) + , mempty + , codeFence $ align $ pretty res + ] + +codeFence :: Doc a -> Doc a +codeFence d = align $ vsep + [ "```haskell" + , d + , "```" + ] + +dump :: SomeMetaprogramCommand -> String +dump (SMC mc) + = renderString + . layoutPretty defaultLayoutOptions + $ prettyCommand mc + + + +-- makeReadme :: MetaprogramCommand a -> T.Text +-- m + + +command :: Text -> Syntax a -> Text -> a -> [Example] -> SomeMetaprogramCommand +command txt syn txt' a exs = SMC $ + MC + { mpc_name = txt + , mpc_syntax = syn + , mpc_description = txt' + , mpc_tactic = a + , mpc_examples = exs + } + From e151637136b89cbb257da2c8a04348891da39909 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 14:43:23 -0700 Subject: [PATCH 2/6] Finish documenting the actions --- .../hls-tactics-plugin.cabal | 1 + .../src/Wingman/Metaprogramming/Parser.hs | 228 ++++++++++++++---- .../Metaprogramming/Parser/Documentation.hs | 30 ++- 3 files changed, 196 insertions(+), 63 deletions(-) diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index 3a18e9393e..ee9bb2be28 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -47,6 +47,7 @@ library Wingman.Machinery Wingman.Metaprogramming.Lexer Wingman.Metaprogramming.Parser + Wingman.Metaprogramming.Parser.Documentation Wingman.Metaprogramming.ProofState Wingman.Naming Wingman.Plugin diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index 3f2a59b2d8..2d799bc716 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -45,9 +45,7 @@ variadic_occ name tac = tac <$> (identifier name *> P.many variable) commands :: [SomeMetaprogramCommand] commands = - [ command - "assumption" - Nullary + [ command "assumption" Nondeterministic Nullary "Use any term in the hypothesis that can unify with the current goal." (pure assumption) [ Example @@ -58,9 +56,7 @@ commands = "some_a_val" ] - , command - "assume" - (Ref One) + , command "assume" Deterministic (Ref One) "Use the given term from the hypothesis, unifying it with the current goal" (pure . assume) [ Example @@ -71,9 +67,7 @@ commands = "some_a_val" ] - , command - "intros" - (Bind Many) + , command "intros" Deterministic (Bind Many) ( mconcat [ "Construct a lambda expression, using the specific names if given, " , "generating unique names otherwise. When no arguments are given, " @@ -105,9 +99,7 @@ commands = "\\x y z -> (_ :: d)" ] - , command - "intro" - (Bind One) + , command "intro" Deterministic (Bind One) "Construct a lambda expression, binding an argument with the given name." (pure . intros' . Just . pure) [ Example @@ -118,9 +110,7 @@ commands = "\\aye -> (_ :: b -> c -> d)" ] - , command - "destruct_all" - Nullary + , command "destruct_all" Deterministic Nullary "Pattern match on every function paramater, in original binding order." (pure destructAll) [ Example @@ -139,9 +129,7 @@ commands = ] ] - , command - "destruct" - (Ref One) + , command "destruct" Deterministic (Ref One) "Pattern match on the argument." (pure . useNameFromHypothesis destruct) [ Example @@ -156,6 +144,175 @@ commands = ] ] + , command "homo" Deterministic (Ref One) + ( mconcat + [ "Pattern match on the argument, and fill the resulting hole in with" + , "the same data constructor." + ]) + (pure . useNameFromHypothesis homo) + [ Example + (Just $ mconcat + [ "Only applicable when the type constructor of the argument is " + , "the same as that of the hole." + ]) + ["e"] + [EHI "e" "Either a b"] + (Just "Either x y") $ + T.pack $ unlines + [ "case e of" + , " Left a -> Left (_ :: x)" + , " Right b -> Right (_ :: y)" + ] + ] + + , command "application" Nondeterministic Nullary + "Apply any function in the hypothesis that returns the correct type." + (pure application) + [ Example + Nothing + [] + [EHI "f" "a -> b"] + (Just "b") + "f (_ :: a)" + ] + + , command "apply" Deterministic (Ref One) + "Apply the given function from *local* scope." + (pure . useNameFromHypothesis apply) + [ Example + Nothing + ["f"] + [EHI "f" "a -> b"] + (Just "b") + "f (_ :: a)" + ] + + , command "split" Nondeterministic Nullary + "Produce a data constructor for the current goal." + (pure split) + [ Example + Nothing + [] + [] + (Just "Either a b") + "Right (_ :: b)" + ] + + , command "ctor" Deterministic (Ref One) + "Use the given data cosntructor." + (pure . userSplit) + [ Example + Nothing + ["Just"] + [] + (Just "Maybe a") + "Just (_ :: a)" + ] + + , command "obvious" Nondeterministic Nullary + "Produce a nullary data constructor for the current goal." + (pure obvious) + [ Example + Nothing + [] + [] + (Just "[a]") + "[]" + ] + + , command "auto" Nondeterministic Nullary + ( mconcat + [ "Repeatedly attempt to split, destruct, apply functions, and" + , "recurse in an attempt to fill the hole." + ]) + (pure auto) + [ Example + Nothing + [] + [EHI "f" "a -> b", EHI "g" "b -> c"] + (Just "a -> c") + "g . f" + ] + + , command "sorry" Deterministic Nullary + "\"Solve\" the goal by leaving a hole." + (pure sorry) + [ Example + Nothing + [] + [] + (Just "b") + "_ :: b" + ] + + , command "unary" Deterministic Nullary + ( mconcat + [ "Produce a hole for a single-parameter function, as well as a hole for" + , "its argument. The argument holes are completely unconstrained, and" + , "will be solved before the function." + ]) + (pure $ nary 1) + [ Example + (Just $ mconcat + [ "In the example below, the variable `a` is free, and will unify" + , "to the resulting extract from any subsequent tactic." + ]) + [] + [] + (Just "Int") + "(_2 :: a -> Int) (_1 :: a)" + ] + + , command "binary" Deterministic Nullary + ( mconcat + [ "Produce a hole for a two-parameter function, as well as holes for" + , "its arguments. The argument holes have the same type but are " + , "otherwise unconstrained, and will be solved before the function." + ]) + (pure $ nary 2) + [ Example + (Just $ mconcat + [ "In the example below, the variable `a` is free, and will unify" + , "to the resulting extract from any subsequent tactic." + ]) + [] + [] + (Just "Int") + "(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)" + ] + + , command "recursion" Deterministic Nullary + "Fill the current hole with a call to the defining function." + ( pure $ + fmap listToMaybe getCurrentDefinitions >>= \case + Just (self, _) -> useNameFromContext apply self + Nothing -> E.throwError $ TacticPanic "no defining function" + ) + [ Example + (Just "In the context of `foo (a :: Int) (b :: b) = _`:") + [] + [] + Nothing + "foo (_ :: Int) (_ :: b)" + ] + + , command "use" Deterministic (Ref One) + "Apply the given function from *module* scope." + ( \occ -> do + ctx <- asks ps_context + ty <- case lookupNameInContext occ ctx of + Just ty -> pure ty + Nothing -> CType <$> getOccTy occ + pure $ apply $ createImportedHyInfo occ ty + ) + [ Example + (Just "`import Data.Char (isSpace)`") + ["isSpace"] + [] + (Just "Bool") + "isSpace (_ :: Char)" + ] + ] @@ -163,39 +320,8 @@ commands = oneTactic :: Parser (TacticsM ()) oneTactic = P.choice - [ braces tactic - -- TODO(sandy): lean uses braces for control flow, but i always forget - -- and want to use parens. is there a semantic difference? - , parens tactic - -- , nullary "assumption" assumption - -- , unary_occ "assume" assume - -- , variadic_occ "intros" $ \case - -- [] -> intros - -- names -> intros' $ Just names - -- , unary_occ "intro" $ intros' . Just . pure - -- , nullary "destruct_all" destructAll - , unary_occ "destruct" $ useNameFromHypothesis destruct - , unary_occ "homo" $ useNameFromHypothesis homo - , nullary "application" application - , unary_occ "apply_module" $ useNameFromContext apply - , unary_occ "apply" $ useNameFromHypothesis apply - , nullary "split" split - , unary_occ "ctor" userSplit - , nullary "obvious" obvious - , nullary "auto" auto - , nullary "sorry" sorry - , nullary "unary" $ nary 1 - , nullary "binary" $ nary 2 - , nullary "recursion" $ - fmap listToMaybe getCurrentDefinitions >>= \case - Just (self, _) -> useNameFromContext apply self - Nothing -> E.throwError $ TacticPanic "no defining function" - , unary_occM "use" $ \occ -> do - ctx <- asks ps_context - ty <- case lookupNameInContext occ ctx of - Just ty -> pure ty - Nothing -> CType <$> getOccTy occ - pure $ apply $ createImportedHyInfo occ ty + [ parens tactic + , makeParser commands ] 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 56807b205f..c778e610f0 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -13,6 +13,10 @@ import Data.Text.Prettyprint.Doc import Data.Text.Prettyprint.Doc.Render.String (renderString) +data Determinism + = Deterministic + | Nondeterministic + data Count a where One :: Count OccName Many :: Count [OccName] @@ -50,6 +54,7 @@ newtype ExampleType = ExampleType data MetaprogramCommand a = MC { mpc_name :: Text , mpc_syntax :: Syntax a + , mpc_det :: Determinism , mpc_description :: Text , mpc_tactic :: a , mpc_examples :: [Example] @@ -60,19 +65,19 @@ data SomeMetaprogramCommand where makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ()) -makeMPParser (MC name Nullary _ tactic _) = do +makeMPParser (MC name Nullary _ _ tactic _) = do identifier name tactic -makeMPParser (MC name (Ref One) _ tactic _) = do +makeMPParser (MC name (Ref One) _ _ tactic _) = do identifier name variable >>= tactic -makeMPParser (MC name (Ref Many) _ tactic _) = do +makeMPParser (MC name (Ref Many) _ _ tactic _) = do identifier name P.many variable >>= tactic -makeMPParser (MC name (Bind One) _ tactic _) = do +makeMPParser (MC name (Bind One) _ _ tactic _) = do identifier name variable >>= tactic -makeMPParser (MC name (Bind Many) _ tactic _) = do +makeMPParser (MC name (Bind Many) _ _ tactic _) = do identifier name P.many variable >>= tactic @@ -81,15 +86,15 @@ makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ()) makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp prettyCommand :: MetaprogramCommand a -> Doc b -prettyCommand (MC name syn desc _ exs) = vsep - [ "##" <+> pretty name +prettyCommand (MC name det syn desc _ exs) = vsep + [ "###" <+> pretty name , mempty , pretty desc , mempty , mempty - , "### Examples" + , "#### Examples" , mempty - , concatWith (\a b -> vsep [a, "---", b]) $ fmap (prettyExample name) exs + , concatWith (\a b -> vsep [a, mempty, "---", b]) $ fmap (prettyExample name) exs ] @@ -106,7 +111,7 @@ prettyExample name (Example m_txt args hys goal res) = , "_" <+> maybe mempty (("::" <+>). pretty) goal ] , mempty - , ">" <+> enclose "`" "`" (pretty name <+> hsep (fmap pretty args)) + , ">" <+> enclose "`" "`" (pretty name <> hsep (mempty : fmap pretty args)) , mempty , codeFence $ align $ pretty res ] @@ -130,10 +135,11 @@ dump (SMC mc) -- m -command :: Text -> Syntax a -> Text -> a -> [Example] -> SomeMetaprogramCommand -command txt syn txt' a exs = SMC $ +command :: Text -> Determinism -> Syntax a -> Text -> a -> [Example] -> SomeMetaprogramCommand +command txt det syn txt' a exs = SMC $ MC { mpc_name = txt + , mpc_det = det , mpc_syntax = syn , mpc_description = txt' , mpc_tactic = a From 63d3dd3e8d70f7048f2d03ec648acd254ba4395a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 15:37:40 -0700 Subject: [PATCH 3/6] Finish documentation --- .../src/Wingman/Metaprogramming/Parser.hs | 34 ++++--- .../Metaprogramming/Parser/Documentation.hs | 89 +++++++++++++------ 2 files changed, 84 insertions(+), 39 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index 2d799bc716..5b5d329c29 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -19,10 +19,10 @@ import Wingman.Auto import Wingman.Context (getCurrentDefinitions) import Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext) import Wingman.Metaprogramming.Lexer +import Wingman.Metaprogramming.Parser.Documentation import Wingman.Metaprogramming.ProofState (proofState, layout) import Wingman.Tactics import Wingman.Types -import Wingman.Metaprogramming.Parser.Documentation nullary :: T.Text -> TacticsM () -> Parser (TacticsM ()) @@ -114,11 +114,11 @@ commands = "Pattern match on every function paramater, in original binding order." (pure destructAll) [ Example - (Just "If `a` and `b` were bound via `f a b = _`, then:") + (Just "Assume `a` and `b` were bound via `f a b = _`.") [] [EHI "a" "Bool", EHI "b" "Maybe Int"] Nothing $ - T.pack $ unlines + T.pack $ init $ unlines [ "case a of" , " False -> case b of" , " Nothing -> _" @@ -137,7 +137,7 @@ commands = ["a"] [EHI "a" "Bool"] Nothing $ - T.pack $ unlines + T.pack $ init $ unlines [ "case a of" , " False -> _" , " True -> _" @@ -146,7 +146,7 @@ commands = , command "homo" Deterministic (Ref One) ( mconcat - [ "Pattern match on the argument, and fill the resulting hole in with" + [ "Pattern match on the argument, and fill the resulting hole in with " , "the same data constructor." ]) (pure . useNameFromHypothesis homo) @@ -158,7 +158,7 @@ commands = ["e"] [EHI "e" "Either a b"] (Just "Either x y") $ - T.pack $ unlines + T.pack $ init $ unlines [ "case e of" , " Left a -> Left (_ :: x)" , " Right b -> Right (_ :: y)" @@ -222,7 +222,7 @@ commands = , command "auto" Nondeterministic Nullary ( mconcat - [ "Repeatedly attempt to split, destruct, apply functions, and" + [ "Repeatedly attempt to split, destruct, apply functions, and " , "recurse in an attempt to fill the hole." ]) (pure auto) @@ -247,14 +247,14 @@ commands = , command "unary" Deterministic Nullary ( mconcat - [ "Produce a hole for a single-parameter function, as well as a hole for" - , "its argument. The argument holes are completely unconstrained, and" + [ "Produce a hole for a single-parameter function, as well as a hole for " + , "its argument. The argument holes are completely unconstrained, and " , "will be solved before the function." ]) (pure $ nary 1) [ Example (Just $ mconcat - [ "In the example below, the variable `a` is free, and will unify" + [ "In the example below, the variable `a` is free, and will unify " , "to the resulting extract from any subsequent tactic." ]) [] @@ -265,14 +265,14 @@ commands = , command "binary" Deterministic Nullary ( mconcat - [ "Produce a hole for a two-parameter function, as well as holes for" + [ "Produce a hole for a two-parameter function, as well as holes for " , "its arguments. The argument holes have the same type but are " , "otherwise unconstrained, and will be solved before the function." ]) (pure $ nary 2) [ Example (Just $ mconcat - [ "In the example below, the variable `a` is free, and will unify" + [ "In the example below, the variable `a` is free, and will unify " , "to the resulting extract from any subsequent tactic." ]) [] @@ -389,3 +389,13 @@ getOccTy occ = do mty <- liftIO $ getOccNameType hscenv rdrenv modul occ maybe (fail $ occNameString occ <> " is not in scope") pure mty + +writeDocumentation :: IO () +writeDocumentation = + writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $ + unlines + [ "# Wingman Metaprogram Command Reference" + , "" + , prettyReadme commands + ] + 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 c778e610f0..79cf64bb02 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -2,29 +2,45 @@ module Wingman.Metaprogramming.Parser.Documentation where -import Data.String (IsString) -import Data.Text (Text) -import GhcPlugins (OccName) -import Wingman.Metaprogramming.Lexer (Parser, identifier, variable) -import Wingman.Types (TacticsM) -import qualified Text.Megaparsec as P -import Data.Functor ((<&>)) +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.Render.String (renderString) +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.Types (TacticsM) data Determinism = Deterministic | Nondeterministic +prettyDeterminism :: Determinism -> Doc b +prettyDeterminism Deterministic = "deterministic" +prettyDeterminism Nondeterministic = "non-deterministic" + data Count a where - One :: Count OccName + One :: Count OccName Many :: Count [OccName] +prettyCount :: Count a -> Doc b +prettyCount One = "single" +prettyCount Many = "varadic" + + data Syntax a where Nullary :: Syntax (Parser (TacticsM ())) - Ref :: Count a -> Syntax (a -> Parser (TacticsM ())) - Bind :: Count a -> Syntax (a -> Parser (TacticsM ())) + Ref :: Count a -> Syntax (a -> Parser (TacticsM ())) + Bind :: Count a -> Syntax (a -> Parser (TacticsM ())) + +prettySyntax :: Syntax a -> Doc b +prettySyntax Nullary = "none" +prettySyntax (Ref co) = prettyCount co <+> "reference" +prettySyntax (Bind co) = prettyCount co <+> "binding" + data Example = Example { ex_ctx :: Maybe Text @@ -85,37 +101,51 @@ makeMPParser (MC name (Bind Many) _ _ tactic _) = do makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ()) makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp + prettyCommand :: MetaprogramCommand a -> Doc b -prettyCommand (MC name det syn desc _ exs) = vsep - [ "###" <+> pretty name - , mempty - , pretty desc +prettyCommand (MC name syn det desc _ exs) = vsep + [ "##" <+> pretty name , mempty + , "arguments:" <+> prettySyntax syn <> "." + , prettyDeterminism det <> "." , mempty - , "#### Examples" + , ">" <+> align (pretty desc) , mempty - , concatWith (\a b -> vsep [a, mempty, "---", b]) $ fmap (prettyExample name) exs + , vsep $ fmap (prettyExample name) exs ] prettyHyInfo :: ExampleHyInfo -> Doc a prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi) +mappendIfNotNull :: [a] -> a -> [a] +mappendIfNotNull [] _ = [] +mappendIfNotNull as a = as <> [a] + + prettyExample :: Text -> Example -> Doc a prettyExample name (Example m_txt args hys goal res) = align $ vsep - [ maybe mempty ((<> line) . pretty) m_txt + [ mempty + , "### Example" + , maybe mempty ((line <>) . (<> line) . (">" <+>) . align . pretty) m_txt + , "Given:" + , mempty , codeFence $ vsep - $ fmap prettyHyInfo hys - <> [ mempty - , "_" <+> maybe mempty (("::" <+>). pretty) goal + $ mappendIfNotNull (fmap prettyHyInfo hys) mempty + <> [ "_" <+> maybe mempty (("::" <+>). pretty) goal ] , mempty - , ">" <+> enclose "`" "`" (pretty name <> hsep (mempty : fmap pretty args)) + , hsep + [ "running " + , enclose "`" "`" $ pretty name <> hsep (mempty : fmap pretty args) + , "will produce:" + ] , mempty , codeFence $ align $ pretty res ] + codeFence :: Doc a -> Doc a codeFence d = align $ vsep [ "```haskell" @@ -123,6 +153,16 @@ codeFence d = align $ vsep , "```" ] + +prettyReadme :: [SomeMetaprogramCommand] -> String +prettyReadme + = renderString + . layoutPretty defaultLayoutOptions + . vsep + . fmap (\case SMC c -> prettyCommand c) + . sortOn (\case SMC c -> mpc_name c) + + dump :: SomeMetaprogramCommand -> String dump (SMC mc) = renderString @@ -130,11 +170,6 @@ dump (SMC mc) $ prettyCommand mc - --- makeReadme :: MetaprogramCommand a -> T.Text --- m - - command :: Text -> Determinism -> Syntax a -> Text -> a -> [Example] -> SomeMetaprogramCommand command txt det syn txt' a exs = SMC $ MC From 2dd9f9c02563d0af0d2f16df14e7126ac01841d2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 15:37:48 -0700 Subject: [PATCH 4/6] Add generated documentation --- plugins/hls-tactics-plugin/COMMANDS.md | 448 +++++++++++++++++++++++++ 1 file changed, 448 insertions(+) create mode 100644 plugins/hls-tactics-plugin/COMMANDS.md diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md new file mode 100644 index 0000000000..e773c2f471 --- /dev/null +++ b/plugins/hls-tactics-plugin/COMMANDS.md @@ -0,0 +1,448 @@ +# Wingman Metaprogram Command Reference + +## application + +arguments: none. +non-deterministic. + +> Apply any function in the hypothesis that returns the correct type. + + +### Example + +Given: + +```haskell +f :: a -> b + +_ :: b +``` + +running `application` will produce: + +```haskell +f (_ :: a) +``` +## apply + +arguments: single reference. +deterministic. + +> Apply the given function from *local* scope. + + +### Example + +Given: + +```haskell +f :: a -> b + +_ :: b +``` + +running `apply f` will produce: + +```haskell +f (_ :: a) +``` +## assume + +arguments: single reference. +deterministic. + +> Use the given term from the hypothesis, unifying it with the current goal + + +### Example + +Given: + +```haskell +some_a_val :: a + +_ :: a +``` + +running `assume some_a_val` will produce: + +```haskell +some_a_val +``` +## assumption + +arguments: none. +non-deterministic. + +> Use any term in the hypothesis that can unify with the current goal. + + +### Example + +Given: + +```haskell +some_a_val :: a + +_ :: a +``` + +running `assumption` will produce: + +```haskell +some_a_val +``` +## auto + +arguments: none. +non-deterministic. + +> Repeatedly attempt to split, destruct, apply functions, andrecurse in an attempt to fill the hole. + + +### Example + +Given: + +```haskell +f :: a -> b +g :: b -> c + +_ :: a -> c +``` + +running `auto` will produce: + +```haskell +g . f +``` +## binary + +arguments: none. +deterministic. + +> Produce a hole for a two-parameter function, as well as holes forits arguments. The argument holes have the same type but are otherwise unconstrained, and will be solved before the function. + + +### Example + +> In the example below, the variable `a` is free, and will unifyto the resulting extract from any subsequent tactic. + +Given: + +```haskell +_ :: Int +``` + +running `binary` will produce: + +```haskell +(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a) +``` +## ctor + +arguments: single reference. +deterministic. + +> Use the given data cosntructor. + + +### Example + +Given: + +```haskell +_ :: Maybe a +``` + +running `ctor Just` will produce: + +```haskell +Just (_ :: a) +``` +## destruct + +arguments: single reference. +deterministic. + +> Pattern match on the argument. + + +### Example + +Given: + +```haskell +a :: Bool + +_ +``` + +running `destruct a` will produce: + +```haskell +case a of + False -> _ + True -> _ +``` +## destruct_all + +arguments: none. +deterministic. + +> Pattern match on every function paramater, in original binding order. + + +### Example + +> Assume `a` and `b` were bound via `f a b = _`. + +Given: + +```haskell +a :: Bool +b :: Maybe Int + +_ +``` + +running `destruct_all` will produce: + +```haskell +case a of + False -> case b of + Nothing -> _ + Just i -> _ + True -> case b of + Nothing -> _ + Just i -> _ +``` +## homo + +arguments: single reference. +deterministic. + +> Pattern match on the argument, and fill the resulting hole in withthe same data constructor. + + +### Example + +> Only applicable when the type constructor of the argument is the same as that of the hole. + +Given: + +```haskell +e :: Either a b + +_ :: Either x y +``` + +running `homo e` will produce: + +```haskell +case e of + Left a -> Left (_ :: x) + Right b -> Right (_ :: y) +``` +## intro + +arguments: single binding. +deterministic. + +> Construct a lambda expression, binding an argument with the given name. + + +### Example + +Given: + +```haskell +_ :: a -> b -> c -> d +``` + +running `intro aye` will produce: + +```haskell +\aye -> (_ :: b -> c -> d) +``` +## intros + +arguments: varadic binding. +deterministic. + +> Construct a lambda expression, using the specific names if given, generating unique names otherwise. When no arguments are given, all of the function arguments will be bound; otherwise, this tactic will bind only enough to saturate the given names. Extra names are ignored. + + +### Example + +Given: + +```haskell +_ :: a -> b -> c -> d +``` + +running `intros` will produce: + +```haskell +\a b c -> (_ :: d) +``` + +### Example + +Given: + +```haskell +_ :: a -> b -> c -> d +``` + +running `intros aye` will produce: + +```haskell +\aye -> (_ :: b -> c -> d) +``` + +### Example + +Given: + +```haskell +_ :: a -> b -> c -> d +``` + +running `intros x y z w` will produce: + +```haskell +\x y z -> (_ :: d) +``` +## obvious + +arguments: none. +non-deterministic. + +> Produce a nullary data constructor for the current goal. + + +### Example + +Given: + +```haskell +_ :: [a] +``` + +running `obvious` will produce: + +```haskell +[] +``` +## recursion + +arguments: none. +deterministic. + +> Fill the current hole with a call to the defining function. + + +### Example + +> In the context of `foo (a :: Int) (b :: b) = _`: + +Given: + +```haskell +_ +``` + +running `recursion` will produce: + +```haskell +foo (_ :: Int) (_ :: b) +``` +## sorry + +arguments: none. +deterministic. + +> "Solve" the goal by leaving a hole. + + +### Example + +Given: + +```haskell +_ :: b +``` + +running `sorry` will produce: + +```haskell +_ :: b +``` +## split + +arguments: none. +non-deterministic. + +> Produce a data constructor for the current goal. + + +### Example + +Given: + +```haskell +_ :: Either a b +``` + +running `split` will produce: + +```haskell +Right (_ :: b) +``` +## unary + +arguments: none. +deterministic. + +> Produce a hole for a single-parameter function, as well as a hole forits argument. The argument holes are completely unconstrained, andwill be solved before the function. + + +### Example + +> In the example below, the variable `a` is free, and will unifyto the resulting extract from any subsequent tactic. + +Given: + +```haskell +_ :: Int +``` + +running `unary` will produce: + +```haskell +(_2 :: a -> Int) (_1 :: a) +``` +## use + +arguments: single reference. +deterministic. + +> Apply the given function from *module* scope. + + +### Example + +> `import Data.Char (isSpace)` + +Given: + +```haskell +_ :: Bool +``` + +running `use isSpace` will produce: + +```haskell +isSpace (_ :: Char) +``` From 63302cf548a2a9d4c1f8303a103e82bfd44ca22f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 15:49:03 -0700 Subject: [PATCH 5/6] Haddockify --- .../src/Wingman/Metaprogramming/Parser.hs | 2 + .../Metaprogramming/Parser/Documentation.hs | 85 ++++++++++++++----- 2 files changed, 67 insertions(+), 20 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index 5b5d329c29..e43c823e9c 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -390,6 +390,8 @@ getOccTy occ = do maybe (fail $ occNameString occ <> " is not in scope") pure mty +------------------------------------------------------------------------------ +-- | Automatically generate the metaprogram command reference. writeDocumentation :: IO () writeDocumentation = writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $ 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 79cf64bb02..8919e61099 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -14,6 +14,8 @@ import Wingman.Metaprogramming.Lexer (Parser, identifier, variable) import Wingman.Types (TacticsM) +------------------------------------------------------------------------------ +-- | Is a tactic deterministic or not? data Determinism = Deterministic | Nondeterministic @@ -22,6 +24,9 @@ prettyDeterminism :: Determinism -> Doc b prettyDeterminism Deterministic = "deterministic" prettyDeterminism Nondeterministic = "non-deterministic" + +------------------------------------------------------------------------------ +-- | How many arguments does the tactic take? data Count a where One :: Count OccName Many :: Count [OccName] @@ -31,6 +36,12 @@ prettyCount One = "single" prettyCount Many = "varadic" +------------------------------------------------------------------------------ +-- | What sorts of arguments does the tactic take? Currently there is no +-- distincion between 'Ref' and 'Bind', other than documentation. +-- +-- The type index here is used for the shape of the function the parser should +-- take. data Syntax a where Nullary :: Syntax (Parser (TacticsM ())) Ref :: Count a -> Syntax (a -> Parser (TacticsM ())) @@ -42,44 +53,60 @@ prettySyntax (Ref co) = prettyCount co <+> "reference" prettySyntax (Bind co) = prettyCount co <+> "binding" +------------------------------------------------------------------------------ +-- | An example for the documentation. data Example = Example - { ex_ctx :: Maybe Text - , ex_args :: [Var] - , ex_hyp :: [ExampleHyInfo] - , ex_goal :: Maybe ExampleType - , ex_result :: Text + { ex_ctx :: Maybe Text -- ^ Specific context information about when the tactic is applicable + , ex_args :: [Var] -- ^ Arguments the tactic was called with + , ex_hyp :: [ExampleHyInfo] -- ^ The hypothesis + , ex_goal :: Maybe ExampleType -- ^ Current goal. Nothing indicates it's uninteresting. + , ex_result :: Text -- ^ Resulting extract. } +------------------------------------------------------------------------------ +-- | An example 'HyInfo'. data ExampleHyInfo = EHI - { ehi_name :: Var - , ehi_type :: ExampleType + { ehi_name :: Var -- ^ Name of the variable + , ehi_type :: ExampleType -- ^ Type of the variable } + +------------------------------------------------------------------------------ +-- | A variable newtype Var = Var { getVar :: Text } deriving newtype (IsString, Pretty) + +------------------------------------------------------------------------------ +-- | A type newtype ExampleType = ExampleType { getExampleType :: Text } deriving newtype (IsString, Pretty) +------------------------------------------------------------------------------ +-- | A command to expose to the parser data MetaprogramCommand a = MC - { mpc_name :: Text - , mpc_syntax :: Syntax a - , mpc_det :: Determinism - , mpc_description :: Text - , mpc_tactic :: a - , mpc_examples :: [Example] + { mpc_name :: Text -- ^ Name of the command. This is the token necessary to run the command. + , mpc_syntax :: Syntax a -- ^ The command's arguments + , mpc_det :: Determinism -- ^ Determinism of the command + , mpc_description :: Text -- ^ User-facing description + , mpc_tactic :: a -- ^ Tactic to run + , mpc_examples :: [Example] -- ^ Collection of documentation examples } +------------------------------------------------------------------------------ +-- | Existentialize the pain away data SomeMetaprogramCommand where SMC :: MetaprogramCommand a -> SomeMetaprogramCommand +------------------------------------------------------------------------------ +-- | Run the 'Parser' of a 'MetaprogramCommand' makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ()) makeMPParser (MC name Nullary _ _ tactic _) = do identifier name @@ -98,10 +125,14 @@ makeMPParser (MC name (Bind Many) _ _ tactic _) = do P.many variable >>= tactic +------------------------------------------------------------------------------ +-- | Compile a collection of metaprogram commands into a parser. makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ()) makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp +------------------------------------------------------------------------------ +-- | Pretty print a command. prettyCommand :: MetaprogramCommand a -> Doc b prettyCommand (MC name syn det desc _ exs) = vsep [ "##" <+> pretty name @@ -115,14 +146,21 @@ prettyCommand (MC name syn det desc _ exs) = vsep ] +------------------------------------------------------------------------------ +-- | Pretty print a hypothesis. prettyHyInfo :: ExampleHyInfo -> Doc a prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi) + +------------------------------------------------------------------------------ +-- | Append the given term only if the first argument has elements. mappendIfNotNull :: [a] -> a -> [a] mappendIfNotNull [] _ = [] mappendIfNotNull as a = as <> [a] +------------------------------------------------------------------------------ +-- | Pretty print an example. prettyExample :: Text -> Example -> Doc a prettyExample name (Example m_txt args hys goal res) = align $ vsep @@ -146,6 +184,8 @@ prettyExample name (Example m_txt args hys goal res) = ] +------------------------------------------------------------------------------ +-- | Make a haskell code fence. codeFence :: Doc a -> Doc a codeFence d = align $ vsep [ "```haskell" @@ -154,6 +194,8 @@ codeFence d = align $ vsep ] +------------------------------------------------------------------------------ +-- | Render all of the commands. prettyReadme :: [SomeMetaprogramCommand] -> String prettyReadme = renderString @@ -163,14 +205,17 @@ prettyReadme . sortOn (\case SMC c -> mpc_name c) -dump :: SomeMetaprogramCommand -> String -dump (SMC mc) - = renderString - . layoutPretty defaultLayoutOptions - $ prettyCommand mc - -command :: Text -> Determinism -> Syntax a -> Text -> a -> [Example] -> SomeMetaprogramCommand +------------------------------------------------------------------------------ +-- | Helper function to build a 'SomeMetaprogramCommand'. +command + :: Text + -> Determinism + -> Syntax a + -> Text + -> a + -> [Example] + -> SomeMetaprogramCommand command txt det syn txt' a exs = SMC $ MC { mpc_name = txt From 2fd4fbfe62a329691b4fd045a4f83ee635d3ab1e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 25 May 2021 16:43:36 -0700 Subject: [PATCH 6/6] Add trailing spaces to the arguments field --- plugins/hls-tactics-plugin/COMMANDS.md | 48 +++++++++---------- .../Metaprogramming/Parser/Documentation.hs | 2 +- 2 files changed, 25 insertions(+), 25 deletions(-) diff --git a/plugins/hls-tactics-plugin/COMMANDS.md b/plugins/hls-tactics-plugin/COMMANDS.md index e773c2f471..4b2e7aa9f6 100644 --- a/plugins/hls-tactics-plugin/COMMANDS.md +++ b/plugins/hls-tactics-plugin/COMMANDS.md @@ -2,7 +2,7 @@ ## application -arguments: none. +arguments: none. non-deterministic. > Apply any function in the hypothesis that returns the correct type. @@ -25,7 +25,7 @@ f (_ :: a) ``` ## apply -arguments: single reference. +arguments: single reference. deterministic. > Apply the given function from *local* scope. @@ -48,7 +48,7 @@ f (_ :: a) ``` ## assume -arguments: single reference. +arguments: single reference. deterministic. > Use the given term from the hypothesis, unifying it with the current goal @@ -71,7 +71,7 @@ some_a_val ``` ## assumption -arguments: none. +arguments: none. non-deterministic. > Use any term in the hypothesis that can unify with the current goal. @@ -94,10 +94,10 @@ some_a_val ``` ## auto -arguments: none. +arguments: none. non-deterministic. -> Repeatedly attempt to split, destruct, apply functions, andrecurse in an attempt to fill the hole. +> Repeatedly attempt to split, destruct, apply functions, and recurse in an attempt to fill the hole. ### Example @@ -118,15 +118,15 @@ g . f ``` ## binary -arguments: none. +arguments: none. deterministic. -> Produce a hole for a two-parameter function, as well as holes forits arguments. The argument holes have the same type but are otherwise unconstrained, and will be solved before the function. +> Produce a hole for a two-parameter function, as well as holes for its arguments. The argument holes have the same type but are otherwise unconstrained, and will be solved before the function. ### Example -> In the example below, the variable `a` is free, and will unifyto the resulting extract from any subsequent tactic. +> In the example below, the variable `a` is free, and will unify to the resulting extract from any subsequent tactic. Given: @@ -141,7 +141,7 @@ running `binary` will produce: ``` ## ctor -arguments: single reference. +arguments: single reference. deterministic. > Use the given data cosntructor. @@ -162,7 +162,7 @@ Just (_ :: a) ``` ## destruct -arguments: single reference. +arguments: single reference. deterministic. > Pattern match on the argument. @@ -187,7 +187,7 @@ case a of ``` ## destruct_all -arguments: none. +arguments: none. deterministic. > Pattern match on every function paramater, in original binding order. @@ -219,10 +219,10 @@ case a of ``` ## homo -arguments: single reference. +arguments: single reference. deterministic. -> Pattern match on the argument, and fill the resulting hole in withthe same data constructor. +> Pattern match on the argument, and fill the resulting hole in with the same data constructor. ### Example @@ -246,7 +246,7 @@ case e of ``` ## intro -arguments: single binding. +arguments: single binding. deterministic. > Construct a lambda expression, binding an argument with the given name. @@ -267,7 +267,7 @@ running `intro aye` will produce: ``` ## intros -arguments: varadic binding. +arguments: varadic binding. deterministic. > Construct a lambda expression, using the specific names if given, generating unique names otherwise. When no arguments are given, all of the function arguments will be bound; otherwise, this tactic will bind only enough to saturate the given names. Extra names are ignored. @@ -316,7 +316,7 @@ running `intros x y z w` will produce: ``` ## obvious -arguments: none. +arguments: none. non-deterministic. > Produce a nullary data constructor for the current goal. @@ -337,7 +337,7 @@ running `obvious` will produce: ``` ## recursion -arguments: none. +arguments: none. deterministic. > Fill the current hole with a call to the defining function. @@ -360,7 +360,7 @@ foo (_ :: Int) (_ :: b) ``` ## sorry -arguments: none. +arguments: none. deterministic. > "Solve" the goal by leaving a hole. @@ -381,7 +381,7 @@ _ :: b ``` ## split -arguments: none. +arguments: none. non-deterministic. > Produce a data constructor for the current goal. @@ -402,15 +402,15 @@ Right (_ :: b) ``` ## unary -arguments: none. +arguments: none. deterministic. -> Produce a hole for a single-parameter function, as well as a hole forits argument. The argument holes are completely unconstrained, andwill be solved before the function. +> Produce a hole for a single-parameter function, as well as a hole for its argument. The argument holes are completely unconstrained, and will be solved before the function. ### Example -> In the example below, the variable `a` is free, and will unifyto the resulting extract from any subsequent tactic. +> In the example below, the variable `a` is free, and will unify to the resulting extract from any subsequent tactic. Given: @@ -425,7 +425,7 @@ running `unary` will produce: ``` ## use -arguments: single reference. +arguments: single reference. deterministic. > Apply the given function from *module* scope. 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 8919e61099..9347c944ab 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -137,7 +137,7 @@ prettyCommand :: MetaprogramCommand a -> Doc b prettyCommand (MC name syn det desc _ exs) = vsep [ "##" <+> pretty name , mempty - , "arguments:" <+> prettySyntax syn <> "." + , "arguments:" <+> prettySyntax syn <> ". " , prettyDeterminism det <> "." , mempty , ">" <+> align (pretty desc)