patrick
/
anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Added new option --parentheses=full to make parsing the output easier.

This commit is contained in:
Patrick Lühne 2017-06-06 02:02:26 +02:00
parent 0285c1cbbb
commit bbbd0b65a4
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
5 changed files with 93 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
app/main.cpp
View File

@ -20,6 +20,7 @@ int main(int argc, char **argv)
("simplify,s", po::bool_switch(&context.performSimplification), "Simplify the output")
("complete,c", po::bool_switch(&context.performCompletion), "Perform completion")
("color", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)")
("parentheses", po::value<std::string>()->default_value("normal"), "Parenthesis style (normal, full)")
("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)");
po::positional_options_description positionalOptionsDescription;
@ -80,6 +81,20 @@ int main(int argc, char **argv)
return EXIT_FAILURE;
}
const auto parenthesisStyle = variablesMap["parentheses"].as<std::string>();
if (parenthesisStyle == "normal")
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Normal;
else if (parenthesisStyle == "full")
context.parenthesisStyle = anthem::ast::ParenthesisStyle::Full;
else
{
context.logger.log(anthem::output::Priority::Error) << "unknown parenthesis style “" << parenthesisStyle << "”";
context.logger.errorStream() << std::endl;
printHelp();
return EXIT_FAILURE;
}
const auto logPriorityString = variablesMap["log-priority"].as<std::string>();
try

3
include/anthem/Context.h
View File

@ -5,6 +5,7 @@
#include <anthem/AST.h>
#include <anthem/output/Logger.h>
#include <anthem/output/ParenthesisStyle.h>
namespace anthem
{
@ -30,6 +31,8 @@ struct Context
bool performCompletion = false;
std::experimental::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
};
////////////////////////////////////////////////////////////////////////////////////////////////////

48
include/anthem/output/AST.h
View File

@ -22,9 +22,21 @@ namespace ast
struct PrintContext
{
PrintContext(const Context &context)
: context{context}
{
}
PrintContext(const PrintContext &other) = delete;
PrintContext &operator=(const PrintContext &other) = delete;
PrintContext(PrintContext &&other) = delete;
PrintContext &operator=(PrintContext &&other) = delete;
std::map<const VariableDeclaration *, size_t> userVariableIDs;
std::map<const VariableDeclaration *, size_t> headVariableIDs;
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
const Context &context;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
@ -130,12 +142,18 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera
inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, comparison.left, printContext);
stream << " ";
print(stream, comparison.operator_, printContext);
stream << " ";
print(stream, comparison.right, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
@ -177,10 +195,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, in.element, printContext);
stream << " " << output::Keyword("in") << " ";
print(stream, in.set, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
@ -195,10 +219,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Integer &in
inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
print(stream, interval.from, printContext);
stream << "..";
print(stream, interval.to, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
@ -329,6 +359,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Bicondition
inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
stream << output::Keyword("exists") << " ";
for (auto i = exists.variables.cbegin(); i != exists.variables.cend(); i++)
@ -342,6 +375,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi
stream << " ";
print(stream, exists.argument, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
@ -349,6 +385,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi
inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
stream << output::Keyword("forall") << " ";
for (auto i = forAll.variables.cbegin(); i != forAll.variables.cend(); i++)
@ -362,6 +401,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for
stream << " ";
print(stream, forAll.argument, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}
@ -382,9 +424,15 @@ inline output::ColorStream &print(output::ColorStream &stream, const Implies &im
inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext)
{
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << "(";
stream << output::Keyword("not") << " ";
print(stream, not_.argument, printContext);
if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
stream << ")";
return stream;
}

26
include/anthem/output/ParenthesisStyle.h Normal file
View File

@ -0,0 +1,26 @@
#ifndef __ANTHEM__OUTPUT__PARENTHESIS_STYLE_H
#define __ANTHEM__OUTPUT__PARENTHESIS_STYLE_H
namespace anthem
{
namespace ast
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// ParenthesisStyle
//
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class ParenthesisStyle
{
Normal,
Full
};
////////////////////////////////////////////////////////////////////////////////////////////////////
}
}
#endif

2
src/anthem/Translation.cpp
View File

@ -62,7 +62,7 @@ void translate(const char *fileName, std::istream &stream, Context &context)
for (auto &scopedFormula : scopedFormulas)
simplify(scopedFormula.formula);
ast::PrintContext printContext;
ast::PrintContext printContext(context);
if (!context.performCompletion)
{