Implemented head translation.

include/anthem/Head.h

@@ -0,0 +1,257 @@
+#ifndef __ANTHEM__HEAD_H
+#define __ANTHEM__HEAD_H
+
+#include <algorithm>
+
+#include <anthem/TermVisitor.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Head
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct TermCollectFunctionTermsVisitor
+{
+	void visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected");
+	}
+
+	void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &terms)
+	{
+		if (function.external)
+			throwErrorAtLocation(term.location, "external functions currently unsupported");
+
+		terms.reserve(terms.size() + function.arguments.size());
+
+		for (const auto &argument : function.arguments)
+			terms.emplace_back(&argument);
+	}
+
+	void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected");
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct LiteralCollectFunctionTermsVisitor
+{
+	void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals");
+	}
+
+	void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, std::vector<const Clingo::AST::Term *> &terms)
+	{
+		term.data.accept(TermCollectFunctionTermsVisitor(), term, terms);
+	}
+
+	void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals");
+	}
+
+	void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals");
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct HeadLiteralCollectFunctionTermsVisitor
+{
+	void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, std::vector<const Clingo::AST::Term *> &terms)
+	{
+		literal.data.accept(LiteralCollectFunctionTermsVisitor(), literal, terms);
+	}
+
+	void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, std::vector<const Clingo::AST::Term *> &terms)
+	{
+		for (const auto &conditionLiteral : disjunction.elements)
+		{
+			if (!conditionLiteral.condition.empty())
+				throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported");
+
+			conditionLiteral.literal.data.accept(LiteralCollectFunctionTermsVisitor(), conditionLiteral.literal, terms);
+		}
+	}
+
+	void visit(const Clingo::AST::Aggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(headLiteral.location, "“aggregate” head literals currently unsupported");
+	}
+
+	void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported");
+	}
+
+	void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported");
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct TermPrintSubstitutedVisitor
+{
+	void visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected");
+	}
+
+	void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected");
+	}
+
+	void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &terms)
+	{
+		if (function.external)
+			throwErrorAtLocation(term.location, "external functions currently unsupported");
+
+		std::cout << function.name;
+
+		if (function.arguments.empty())
+			return;
+
+		std::cout << "(";
+
+		for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
+		{
+			if (i != function.arguments.cbegin())
+				std::cout << ",";
+
+			const auto &argument = *i;
+
+			const auto matchingTerm = std::find(terms.cbegin(), terms.cend(), &argument);
+
+			assert(matchingTerm != terms.cend());
+
+			std::cout << AuxiliaryVariablePrefix << (matchingTerm - terms.cbegin());
+		}
+
+		std::cout << ")";
+	}
+
+	void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected");
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct LiteralPrintSubstitutedVisitor
+{
+	void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals");
+	}
+
+	void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, const std::vector<const Clingo::AST::Term *> &terms)
+	{
+		term.data.accept(TermPrintSubstitutedVisitor(), term, terms);
+	}
+
+	void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals");
+	}
+
+	void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals");
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct HeadLiteralPrintSubstitutedVisitor
+{
+	void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, const std::vector<const Clingo::AST::Term *> &terms)
+	{
+		literal.data.accept(LiteralPrintSubstitutedVisitor(), literal, terms);
+	}
+
+	void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, const std::vector<const Clingo::AST::Term *> &terms)
+	{
+		for (auto i = disjunction.elements.cbegin(); i != disjunction.elements.cend(); i++)
+		{
+			const auto &conditionLiteral = *i;
+
+			if (!conditionLiteral.condition.empty())
+				throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported");
+
+			if (i != disjunction.elements.cbegin())
+				std::cout << " or ";
+
+			conditionLiteral.literal.data.accept(LiteralPrintSubstitutedVisitor(), conditionLiteral.literal, terms);
+		}
+	}
+
+	void visit(const Clingo::AST::Aggregate &, const Clingo::AST::HeadLiteral &headLiteral, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(headLiteral.location, "“aggregate” head literals currently unsupported");
+	}
+
+	void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported");
+	}
+
+	void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, const std::vector<const Clingo::AST::Term *> &)
+	{
+		throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported");
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+
+#endif

include/anthem/HeadLiteralVisitor.h

@@ -15,7 +15,7 @@ namespace anthem
 
 void throwErrorUnsupportedHeadLiteral(const char *statementType, const Clingo::AST::HeadLiteral &headLiteral)
 {
-	const auto errorMessage = std::string("“") + statementType + "” head literals currently not supported";
+	const auto errorMessage = std::string("“") + statementType + "” head literals currently unsupported";
 
 	throwErrorAtLocation(headLiteral.location, errorMessage.c_str());
 
@@ -58,37 +58,6 @@ struct HeadLiteralVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct HeadLiteralCollectTermsVisitor
-{
-	void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, std::vector<Clingo::AST::Term> &terms)
-	{
-		literal.data.accept(LiteralCollectTermsVisitor(), literal, terms);
-	}
-
-	void visit(const Clingo::AST::Disjunction &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<Clingo::AST::Term> &)
-	{
-		// TODO: implement
-		throwErrorUnsupportedHeadLiteral("disjunction", headLiteral);
-	}
-
-	void visit(const Clingo::AST::Aggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<Clingo::AST::Term> &)
-	{
-		throwErrorUnsupportedHeadLiteral("aggregate", headLiteral);
-	}
-
-	void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<Clingo::AST::Term> &)
-	{
-		throwErrorUnsupportedHeadLiteral("head aggregate", headLiteral);
-	}
-
-	void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, std::vector<Clingo::AST::Term> &)
-	{
-		throwErrorUnsupportedHeadLiteral("theory", headLiteral);
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 
 #endif

include/anthem/LiteralVisitor.h

@@ -15,7 +15,7 @@ namespace anthem
 
 void throwErrorUnsupportedLiteral(const char *statementType, const Clingo::AST::Literal &literal)
 {
-	const auto errorMessage = std::string("“") + statementType + "” literals currently not supported";
+	const auto errorMessage = std::string("“") + statementType + "” literals currently unsupported";
 
 	throwErrorAtLocation(literal.location, errorMessage.c_str());
 
@@ -52,32 +52,6 @@ struct LiteralVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct LiteralCollectTermsVisitor
-{
-	void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &, std::vector<Clingo::AST::Term> &)
-	{
-	}
-
-	void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, std::vector<Clingo::AST::Term> &terms)
-	{
-		terms.push_back(term);
-	}
-
-	void visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &, std::vector<Clingo::AST::Term> &terms)
-	{
-		terms.reserve(terms.size() + 2);
-		terms.push_back(comparison.left);
-		terms.push_back(comparison.right);
-	}
-
-	void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, std::vector<Clingo::AST::Term> &)
-	{
-		throwErrorUnsupportedLiteral("CSP literal", literal);
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 
 #endif

include/anthem/StatementVisitor.h

@@ -2,7 +2,7 @@
 #define __ANTHEM__STATEMENT_VISITOR_H
 
 #include <anthem/BodyLiteralVisitor.h>
-#include <anthem/HeadLiteralVisitor.h>
+#include <anthem/Head.h>
 #include <anthem/Utils.h>
 
 namespace anthem
@@ -16,7 +16,7 @@ namespace anthem
 
 void throwErrorUnsupportedStatement(const char *statementType, const Clingo::AST::Statement &statement)
 {
-	const auto errorMessage = std::string("“") + statementType + "” statements currently not supported";
+	const auto errorMessage = std::string("“") + statementType + "” statements currently unsupported";
 
 	throwErrorAtLocation(statement.location, errorMessage.c_str());
 
@@ -32,30 +32,34 @@ struct StatementVisitor
 		std::cout << "[program] " << program.name << std::endl;
 
 		if (!program.parameters.empty())
-			throwErrorAtLocation(statement.location, "program parameters currently not supported");
+			throwErrorAtLocation(statement.location, "program parameters currently unsupported");
 	}
 
 	void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &)
 	{
-		std::vector<Clingo::AST::Term> headTerms;
+		// Concatenate all head terms
-		rule.head.data.accept(HeadLiteralCollectTermsVisitor(), rule.head, headTerms);
+		std::vector<const Clingo::AST::Term *> headTerms;
+		rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, headTerms);
 
+		// Print auxiliary variables replacing the head atom’s arguments
 		if (!headTerms.empty())
 		{
-			std::cout << "exists ";
-
 			for (auto i = headTerms.cbegin(); i != headTerms.cend(); i++)
 			{
+				const auto &headTerm = **i;
+
 				if (i != headTerms.cbegin())
 					std::cout << ", ";
 
-				std::cout << "AUX" << (i - headTerms.cbegin());
+				std::cout
+					<< AuxiliaryVariablePrefix << (i - headTerms.cbegin())
+					<< " in " << headTerm;
 			}
 
-			std::cout << ": ";
+			std::cout << " and ";
 		}
 
-		std::cout << "body -> ";
+		std::cout << "[body] -> ";
 
 		/*rule.head.data.accept(HeadLiteralVisitor(), rule.head);
 
@@ -66,6 +70,9 @@ struct StatementVisitor
 
 			bodyLiteral.data.accept(BodyLiteralVisitor(), bodyLiteral);
 		}*/
+
+		// Print consequent of the implication
+		rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, headTerms);
 	}
 
 	void visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement)

include/anthem/TermVisitor.h

@@ -12,17 +12,6 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void throwErrorUnsupportedTerm(const char *statementType, const Clingo::AST::Term &term)
-{
-	const auto errorMessage = std::string("“") + statementType + "” terms currently not supported";
-
-	throwErrorAtLocation(term.location, errorMessage.c_str());
-
-	throw std::runtime_error(errorMessage);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 struct TermVisitor
 {
 	void visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &)
@@ -32,34 +21,34 @@ struct TermVisitor
 
 	void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term)
 	{
-		throwErrorUnsupportedTerm("variable", term);
+		throwErrorAtLocation(term.location, "“variable” terms currently unsupported");
 	}
 
 	void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term)
 	{
-		throwErrorUnsupportedTerm("unary operation", term);
+		throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported");
 	}
 
 	void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term)
 	{
-		throwErrorUnsupportedTerm("binary operation", term);
+		throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported");
 	}
 
 	void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term)
 	{
-		throwErrorUnsupportedTerm("interval", term);
+		throwErrorAtLocation(term.location, "“interval” terms currently unsupported");
 	}
 
 	void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term)
 	{
 		std::cout << "[" << function.name << "]";
 
-		throwErrorUnsupportedTerm("function", term);
+		throwErrorAtLocation(term.location, "“function” terms currently unsupported");
 	}
 
 	void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term)
 	{
-		throwErrorUnsupportedTerm("pool", term);
+		throwErrorAtLocation(term.location, "“pool” terms currently unsupported");
 	}
 };
 

include/anthem/Utils.h

@@ -21,10 +21,16 @@ inline void throwErrorAtLocation(const Clingo::Location &location, const char *e
 		<< location.begin_line() << ":" << location.begin_column()
 		<< ": error: "
 		<< errorMessage << std::endl;
+
+	throw std::runtime_error(errorMessage);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+constexpr const auto AuxiliaryVariablePrefix = "AUX";
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 
 #endif