Wingman.Metaprogramming.Parser

Documentation

nullary :: Text -> TacticsM () -> Parser (TacticsM ())

unary_occ :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())

unary_occM :: Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())

Like unary_occ, but runs directly in the Parser monad.

variadic_occ :: Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())

commands :: [SomeMetaprogramCommand]

oneTactic :: Parser (TacticsM ())

tactic :: Parser (TacticsM ())

bindOne :: TacticsM a -> TacticsM a -> TacticsM a

operators :: [[Operator Parser (TacticsM ())]]

tacticProgram :: Parser (TacticsM ())

wrapError :: String -> String

attempt_it :: Context -> Judgement -> String -> ReaderT ParserContext IO (Either String String)

Attempt to run a metaprogram tactic, returning the proof state, or the errors.

parseMetaprogram :: Text -> ReaderT ParserContext IO (TacticsM ())

getOccTy :: OccName -> Parser Type

Like getOccNameType, but runs in the Parser monad.

writeDocumentation :: IO ()

Automatically generate the metaprogram command reference.