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