1{-# LANGUAGE OverloadedStrings #-}
2
3module Wingman.Metaprogramming.Parser.Documentation where
4
5import           Data.Functor ((<&>))
6import           Data.List (sortOn)
7import           Data.String (IsString)
8import           Data.Text (Text)
9import           Data.Text.Prettyprint.Doc hiding (parens)
10import           Data.Text.Prettyprint.Doc.Render.String (renderString)
11import           GhcPlugins (OccName)
12import qualified Text.Megaparsec as P
13import           Wingman.Metaprogramming.Lexer (Parser, identifier, variable, parens)
14import           Wingman.Types (TacticsM)
15
16import {-# SOURCE #-} Wingman.Metaprogramming.Parser (tactic)
17
18
19------------------------------------------------------------------------------
20-- | Is a tactic deterministic or not?
21data Determinism
22  = Deterministic
23  | Nondeterministic
24
25prettyDeterminism :: Determinism -> Doc b
26prettyDeterminism Deterministic = "deterministic"
27prettyDeterminism Nondeterministic = "non-deterministic"
28
29
30------------------------------------------------------------------------------
31-- | How many arguments does the tactic take?
32data Count a where
33  One  :: Count OccName
34  Many :: Count [OccName]
35
36prettyCount :: Count a -> Doc b
37prettyCount One  = "single"
38prettyCount Many = "varadic"
39
40
41------------------------------------------------------------------------------
42-- | What sorts of arguments does the tactic take? Currently there is no
43-- distincion between 'Ref' and 'Bind', other than documentation.
44--
45-- The type index here is used for the shape of the function the parser should
46-- take.
47data Syntax a where
48  Nullary :: Syntax (Parser (TacticsM ()))
49  Ref     :: Count a -> Syntax (a -> Parser (TacticsM ()))
50  Bind    :: Count a -> Syntax (a -> Parser (TacticsM ()))
51  Tactic  :: Syntax (TacticsM () -> Parser (TacticsM ()))
52
53prettySyntax :: Syntax a -> Doc b
54prettySyntax Nullary   = "none"
55prettySyntax (Ref co)  = prettyCount co <+> "reference"
56prettySyntax (Bind co) = prettyCount co <+> "binding"
57prettySyntax Tactic    = "tactic"
58
59
60------------------------------------------------------------------------------
61-- | An example for the documentation.
62data Example = Example
63  { ex_ctx    :: Maybe Text         -- ^ Specific context information about when the tactic is applicable
64  , ex_args   :: [Var]              -- ^ Arguments the tactic was called with
65  , ex_hyp    :: [ExampleHyInfo]    -- ^ The hypothesis
66  , ex_goal   :: Maybe ExampleType  -- ^ Current goal. Nothing indicates it's uninteresting.
67  , ex_result :: Text               -- ^ Resulting extract.
68  }
69
70
71------------------------------------------------------------------------------
72-- | An example 'HyInfo'.
73data ExampleHyInfo = EHI
74  { ehi_name :: Var          -- ^ Name of the variable
75  , ehi_type :: ExampleType  -- ^ Type of the variable
76  }
77
78
79------------------------------------------------------------------------------
80-- | A variable
81newtype Var = Var
82  { getVar :: Text
83  }
84  deriving newtype (IsString, Pretty)
85
86
87------------------------------------------------------------------------------
88-- | A type
89newtype ExampleType = ExampleType
90  { getExampleType :: Text
91  }
92  deriving newtype (IsString, Pretty)
93
94
95------------------------------------------------------------------------------
96-- | A command to expose to the parser
97data MetaprogramCommand a = MC
98  { mpc_name        :: Text         -- ^ Name of the command. This is the token necessary to run the command.
99  , mpc_syntax      :: Syntax a     -- ^ The command's arguments
100  , mpc_det         :: Determinism  -- ^ Determinism of the command
101  , mpc_description :: Text         -- ^ User-facing description
102  , mpc_tactic      :: a            -- ^ Tactic to run
103  , mpc_examples    :: [Example]    -- ^ Collection of documentation examples
104  }
105
106------------------------------------------------------------------------------
107-- | Existentialize the pain away
108data SomeMetaprogramCommand where
109  SMC :: MetaprogramCommand a -> SomeMetaprogramCommand
110
111
112------------------------------------------------------------------------------
113-- | Run the 'Parser' of a 'MetaprogramCommand'
114makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())
115makeMPParser (MC name Nullary _ _ t _) = do
116  identifier name
117  t
118makeMPParser (MC name (Ref One) _ _ t _) = do
119  identifier name
120  variable >>= t
121makeMPParser (MC name (Ref Many) _ _ t _) = do
122  identifier name
123  P.many variable >>= t
124makeMPParser (MC name (Bind One) _ _ t _) = do
125  identifier name
126  variable >>= t
127makeMPParser (MC name (Bind Many) _ _ t _) = do
128  identifier name
129  P.many variable >>= t
130makeMPParser (MC name Tactic _ _ t _) = do
131  identifier name
132  parens tactic >>= t
133
134
135------------------------------------------------------------------------------
136-- | Compile a collection of metaprogram commands into a parser.
137makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ())
138makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp
139
140
141------------------------------------------------------------------------------
142-- | Pretty print a command.
143prettyCommand :: MetaprogramCommand a -> Doc b
144prettyCommand (MC name syn det desc _ exs) = vsep
145  [ "##" <+> pretty name
146  , mempty
147  , "arguments:" <+> prettySyntax syn <> ".  "
148  , prettyDeterminism det <> "."
149  , mempty
150  , ">" <+> align (pretty desc)
151  , mempty
152  , vsep $ fmap (prettyExample name) exs
153  , mempty
154  ]
155
156
157------------------------------------------------------------------------------
158-- | Pretty print a hypothesis.
159prettyHyInfo :: ExampleHyInfo -> Doc a
160prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi)
161
162
163------------------------------------------------------------------------------
164-- | Append the given term only if the first argument has elements.
165mappendIfNotNull :: [a] -> a -> [a]
166mappendIfNotNull [] _ = []
167mappendIfNotNull as a = as <> [a]
168
169
170------------------------------------------------------------------------------
171-- | Pretty print an example.
172prettyExample :: Text -> Example -> Doc a
173prettyExample name (Example m_txt args hys goal res) =
174  align $ vsep
175    [ mempty
176    , "### Example"
177    , maybe mempty ((line <>) . (<> line) . (">" <+>) . align . pretty) m_txt
178    , "Given:"
179    , mempty
180    , codeFence $ vsep
181        $ mappendIfNotNull (fmap prettyHyInfo hys) mempty
182           <> [ "_" <+> maybe mempty (("::" <+>). pretty) goal
183              ]
184    , mempty
185    , hsep
186        [ "running "
187        , enclose "`" "`" $ pretty name <> hsep (mempty : fmap pretty args)
188        , "will produce:"
189        ]
190    , mempty
191    , codeFence $ align $ pretty res
192    ]
193
194
195------------------------------------------------------------------------------
196-- | Make a haskell code fence.
197codeFence :: Doc a -> Doc a
198codeFence d = align $ vsep
199  [ "```haskell"
200  , d
201  , "```"
202  ]
203
204
205------------------------------------------------------------------------------
206-- | Render all of the commands.
207prettyReadme :: [SomeMetaprogramCommand] -> String
208prettyReadme
209  = renderString
210  . layoutPretty defaultLayoutOptions
211  . vsep
212  . fmap (\case SMC c -> prettyCommand c)
213  . sortOn (\case SMC c -> mpc_name c)
214
215
216
217------------------------------------------------------------------------------
218-- | Helper function to build a 'SomeMetaprogramCommand'.
219command
220    :: Text
221    -> Determinism
222    -> Syntax a
223    -> Text
224    -> a
225    -> [Example]
226    -> SomeMetaprogramCommand
227command txt det syn txt' a exs = SMC $
228  MC
229    { mpc_name        = txt
230    , mpc_det         = det
231    , mpc_syntax      = syn
232    , mpc_description = txt'
233    , mpc_tactic      = a
234    , mpc_examples    = exs
235    }
236
237