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 ())

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

tacticProgram :: Parser (TacticsM ())

wrapError :: String -> String

fixErrorOffset :: RealSrcLoc -> ParseErrorBundle a b -> ParseErrorBundle a b

attempt_it :: RealSrcLoc -> Context -> Judgement -> String -> IO (Either String String)

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

parseMetaprogram :: Text -> TacticsM ()

writeDocumentation :: IO ()

Automatically generate the metaprogram command reference.