Wingman.Metaprogramming.Parser.Documentation

Documentation

data Determinism

Is a tactic deterministic or not?

Constructors

Deterministic

Nondeterministic

prettyDeterminism :: Determinism -> Doc b

data Count a where

How many arguments does the tactic take?

Constructors

One :: Count OccName

Many :: Count [OccName]

prettyCount :: Count a -> Doc b

data Syntax a where

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.

Constructors

Nullary :: Syntax (Parser (TacticsM ()))

Ref :: Count a -> Syntax (a -> Parser (TacticsM ()))

Bind :: Count a -> Syntax (a -> Parser (TacticsM ()))

prettySyntax :: Syntax a -> Doc b

data Example

An example for the documentation.

Constructors

Example

Fields

• 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.

data ExampleHyInfo

An example HyInfo.

Constructors

EHI

Fields

• ehi_name :: Var

  Name of the variable

• ehi_type :: ExampleType

  Type of the variable

newtype Var

A variable

Constructors

Var

Fields

• getVar :: Text

Instances

IsString Var

Defined in Wingman.Metaprogramming.Parser.Documentation

Methods

fromString :: String -> Var

Pretty Var

Defined in Wingman.Metaprogramming.Parser.Documentation

Methods

pretty :: Var -> Doc ann

prettyList :: [Var] -> Doc ann

newtype ExampleType

A type

Constructors

ExampleType

Fields

• getExampleType :: Text

Instances

IsString ExampleType

Defined in Wingman.Metaprogramming.Parser.Documentation

Methods

fromString :: String -> ExampleType

Pretty ExampleType

Defined in Wingman.Metaprogramming.Parser.Documentation

Methods

pretty :: ExampleType -> Doc ann

prettyList :: [ExampleType] -> Doc ann

data MetaprogramCommand a

A command to expose to the parser

Constructors

MC

Fields

• 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

data SomeMetaprogramCommand where

Existentialize the pain away

Constructors

SMC :: MetaprogramCommand a -> SomeMetaprogramCommand

makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())

Run the Parser of a MetaprogramCommand

makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ())

Compile a collection of metaprogram commands into a parser.

prettyCommand :: MetaprogramCommand a -> Doc b

Pretty print a command.

prettyHyInfo :: ExampleHyInfo -> Doc a

Pretty print a hypothesis.

mappendIfNotNull :: [a] -> a -> [a]

Append the given term only if the first argument has elements.

prettyExample :: Text -> Example -> Doc a

Pretty print an example.

codeFence :: Doc a -> Doc a

Make a haskell code fence.

prettyReadme :: [SomeMetaprogramCommand] -> String

Render all of the commands.

command :: Text -> Determinism -> Syntax a -> Text -> a -> [Example] -> SomeMetaprogramCommand

Helper function to build a SomeMetaprogramCommand.