From bbbd0b65a40b88b9bd7dfcf92864ae82d9a6c30e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Tue, 6 Jun 2017 02:02:26 +0200 Subject: [PATCH] Added new option --parentheses=full to make parsing the output easier. --- app/main.cpp | 15 ++++++++ include/anthem/Context.h | 3 ++ include/anthem/output/AST.h | 48 ++++++++++++++++++++++++ include/anthem/output/ParenthesisStyle.h | 26 +++++++++++++ src/anthem/Translation.cpp | 2 +- 5 files changed, 93 insertions(+), 1 deletion(-) create mode 100644 include/anthem/output/ParenthesisStyle.h diff --git a/app/main.cpp b/app/main.cpp index ac01789..fd386d5 100644 --- a/app/main.cpp +++ b/app/main.cpp @@ -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()->default_value("auto"), "Colorize output (always, never, auto)") + ("parentheses", po::value()->default_value("normal"), "Parenthesis style (normal, full)") ("log-priority,p", po::value()->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(); + + 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(); try diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 7a966f0..44bc1dc 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -5,6 +5,7 @@ #include #include +#include namespace anthem { @@ -30,6 +31,8 @@ struct Context bool performCompletion = false; std::experimental::optional> visiblePredicateSignatures; + + ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index 0c21370..a6796af 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -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 userVariableIDs; std::map headVariableIDs; std::map 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 ¬_, 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; } diff --git a/include/anthem/output/ParenthesisStyle.h b/include/anthem/output/ParenthesisStyle.h new file mode 100644 index 0000000..9f1ee85 --- /dev/null +++ b/include/anthem/output/ParenthesisStyle.h @@ -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 diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 4317db6..9601a83 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -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) {