Add option for human-readable output

src/main.rs

@@ -32,7 +32,8 @@ fn main()
 		}
 			=>
 		{
-			if let Err(error) = anthem::translate::verify_properties::translate(&input)
+			if let Err(error) = anthem::translate::verify_properties::translate(&input,
+				output_format)
 			{
 				log::error!("could not translate input program: {}", error);
 				std::process::exit(1)

src/output.rs

@@ -1,3 +1,4 @@
+pub(crate) mod human_readable;
 pub(crate) mod tptp;
 
 #[derive(Debug)]

src/output/human_readable.rs

@@ -0,0 +1,403 @@
+pub(crate) struct VariableDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	variable_declaration: &'a std::rc::Rc<foliage::VariableDeclaration>,
+	context: &'b C,
+}
+
+pub(crate) fn display_variable_declaration<'a, 'b, C>(
+	variable_declaration: &'a std::rc::Rc<foliage::VariableDeclaration>, context: &'b C)
+	-> VariableDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	VariableDeclarationDisplay
+	{
+		variable_declaration,
+		context,
+	}
+}
+
+pub(crate) struct TermDisplay<'a, 'b, C>
+{
+	parent_precedence: Option<i32>,
+	term: &'a foliage::Term,
+	context: &'b C,
+}
+
+pub(crate) fn display_term<'a, 'b, C>(term: &'a foliage::Term, parent_precedence: Option<i32>,
+	context: &'b C)
+	-> TermDisplay<'a, 'b, C>
+{
+	TermDisplay
+	{
+		parent_precedence,
+		term,
+		context,
+	}
+}
+
+pub(crate) struct FormulaDisplay<'a, 'b, C>
+{
+	parent_precedence: Option<i32>,
+	formula: &'a foliage::Formula,
+	context: &'b C,
+}
+
+pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula,
+	parent_precedence: Option<i32>, context: &'b C)
+	-> FormulaDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	FormulaDisplay
+	{
+		parent_precedence,
+		formula,
+		context,
+	}
+}
+
+trait Precedence
+{
+	fn precedence(&self) -> i32;
+}
+
+impl Precedence for foliage::Term
+{
+	fn precedence(&self) -> i32
+	{
+		match &self
+		{
+			Self::Boolean(_)
+			| Self::Function(_)
+			| Self::SpecialInteger(_)
+			| Self::Integer(_)
+			| Self::String(_)
+			| Self::Variable(_)
+				=> 0,
+			Self::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, ..})
+				=> 1,
+			Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, ..})
+				=> 2,
+			Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, ..})
+			| Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, ..})
+			| Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, ..})
+				=> 3,
+			Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, ..})
+			| Self::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, ..})
+				=> 4,
+			Self::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, ..})
+				=> 5,
+		}
+	}
+}
+
+impl Precedence for foliage::Formula
+{
+	fn precedence(&self) -> i32
+	{
+		match &self
+		{
+			Self::Predicate(_)
+			| Self::Boolean(_)
+			| Self::Compare(_)
+				=> 0,
+			Self::Exists(_)
+			| Self::ForAll(_)
+				=> 1,
+			Self::Not(_)
+				=> 2,
+			Self::And(_)
+				=> 3,
+			Self::Or(_)
+				=> 4,
+			Self::Implies(_)
+				=> 5,
+			Self::IfAndOnlyIf(_)
+				=> 6,
+		}
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let id = self.context.variable_declaration_id(self.variable_declaration);
+		let domain = self.context.variable_declaration_domain(self.variable_declaration)
+			.expect("unspecified variable domain");
+
+		let prefix = match domain
+		{
+			crate::translate::common::Domain::Integer => "N",
+			crate::translate::common::Domain::Program => "X",
+		};
+
+		write!(format, "{}{}", prefix, id + 1)
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let display_variable_declaration = |variable_declaration|
+			display_variable_declaration(variable_declaration, self.context);
+		let display_term = |term, precedence| display_term(term, precedence, self.context);
+
+		let precedence = self.term.precedence();
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match &self.term
+		{
+			foliage::Term::Boolean(true) => write!(format, "true"),
+			foliage::Term::Boolean(false) => write!(format, "false"),
+			foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum) => write!(format, "#inf"),
+			foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum) => write!(format, "#sup"),
+			foliage::Term::Integer(value) => write!(format, "{}", value),
+			foliage::Term::String(value) => write!(format, "\"{}\"", value),
+			foliage::Term::Variable(variable) => write!(format, "{:?}",
+				display_variable_declaration(&variable.declaration)),
+			foliage::Term::Function(function) =>
+			{
+				write!(format, "{}", function.declaration.name)?;
+
+				assert!(function.declaration.arity == function.arguments.len(),
+					"function has a different number of arguments than declared (expected {}, got {})",
+					function.declaration.arity, function.arguments.len());
+
+				if function.arguments.len() > 0
+				{
+					write!(format, "{}(", function.declaration.name)?;
+
+					let mut separator = "";
+
+					for argument in &function.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(&argument, None))?;
+
+						separator = ", ";
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Add, left, right})
+				=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
+			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Subtract, left, right})
+				=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
+			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Multiply, left, right})
+				=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
+			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Divide, left, right})
+				=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
+			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Modulo, left, right})
+				=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
+			foliage::Term::BinaryOperation(foliage::BinaryOperation{operator: foliage::BinaryOperator::Exponentiate, left, right})
+				=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
+			foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::Negative, argument})
+				=> write!(format, "-{:?}", display_term(argument, precedence)),
+			foliage::Term::UnaryOperation(foliage::UnaryOperation{operator: foliage::UnaryOperator::AbsoluteValue, argument})
+				=> write!(format, "|{:?}|", display_term(argument, precedence)),
+		}?;
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let display_variable_declaration = |variable_declaration|
+			display_variable_declaration(variable_declaration, self.context);
+		let display_term = |term, precedence| display_term(term, precedence, self.context);
+		let display_formula = |formula, precedence| display_formula(formula, precedence, self.context);
+
+		let precedence = self.formula.precedence();
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match &self.formula
+		{
+			foliage::Formula::Exists(exists) =>
+			{
+				assert!(!exists.parameters.is_empty());
+
+				write!(format, "exists")?;
+
+				let mut separator = " ";
+
+				for parameter in exists.parameters.iter()
+				{
+					write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
+			},
+			foliage::Formula::ForAll(for_all) =>
+			{
+				assert!(!for_all.parameters.is_empty());
+
+				write!(format, "forall")?;
+
+				let mut separator = " ";
+
+				for parameter in for_all.parameters.iter()
+				{
+					write!(format, "{}{:?}", separator, display_variable_declaration(parameter))?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
+			},
+			foliage::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
+			foliage::Formula::And(arguments) =>
+			{
+				let mut separator = "";
+
+				assert!(!arguments.is_empty());
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+
+					separator = " and "
+				}
+			},
+			foliage::Formula::Or(arguments) =>
+			{
+				let mut separator = "";
+
+				assert!(!arguments.is_empty());
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+
+					separator = " or "
+				}
+			},
+			foliage::Formula::Implies(foliage::Implies{antecedent, implication})
+				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
+			foliage::Formula::IfAndOnlyIf(foliage::IfAndOnlyIf{left, right})
+				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
+			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Less, left, right})
+				=> write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
+			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::LessOrEqual, left, right})
+				=> write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
+			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Greater, left, right})
+				=> write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
+			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::GreaterOrEqual, left, right})
+				=> write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
+			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::Equal, left, right})
+				=> write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
+			foliage::Formula::Compare(foliage::Compare{operator: foliage::ComparisonOperator::NotEqual, left, right})
+				=> write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
+			foliage::Formula::Boolean(true) => write!(format, "#true")?,
+			foliage::Formula::Boolean(false) => write!(format, "#false")?,
+			foliage::Formula::Predicate(predicate) =>
+			{
+				write!(format, "{}", predicate.declaration.name)?;
+
+				if !predicate.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &predicate.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(argument, None))?;
+
+						separator = ", "
+					}
+
+					write!(format, ")")?;
+				}
+			},
+		}
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}

src/output/tptp.rs

@@ -83,6 +83,9 @@ pub(crate) struct FormulaDisplay<'a, 'b, C>
 
 pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula, context: &'b C)
 	-> FormulaDisplay<'a, 'b, C>
+where
+	C: crate::translate::common::VariableDeclarationDomain
+		+ crate::translate::common::VariableDeclarationID
 {
 	FormulaDisplay
 	{

src/translate/verify_properties.rs

@@ -176,14 +176,12 @@ impl crate::translate::common::VariableDeclarationID for Context
 		{
 			Some(id) =>
 			{
-				//log::trace!("{:p} → {} (already known)", *variable_declaration, id);
 				*id
 			}
 			None =>
 			{
 				let id = variable_declaration_ids.len();
 				variable_declaration_ids.insert(std::rc::Rc::clone(variable_declaration).into(), id);
-				//log::trace!("{:p} → {} (new)", *variable_declaration, id);
 				id
 			},
 		}
@@ -214,7 +212,7 @@ impl clingo::StatementHandler for StatementHandler
 		{
 			clingo::ast::StatementType::Rule(ref rule) =>
 			{
-				if let Err(error) = read_rule(rule, &mut self.context)
+				if let Err(error) = read_rule(rule, &self.context)
 				{
 					log::error!("could not translate input program: {}", error);
 					return false;
@@ -237,7 +235,8 @@ impl clingo::Logger for Logger
 	}
 }
 
-pub fn translate<P>(program_paths: &[P]) -> Result<(), crate::Error>
+pub fn translate<P>(program_paths: &[P], output_format: crate::output::Format)
+	-> Result<(), crate::Error>
 where
 	P: AsRef<std::path::Path>
 {
@@ -259,7 +258,7 @@ where
 		for definition in definitions.definitions.iter()
 		{
 			log::debug!("definition({}/{}): {}.", predicate_declaration.name, predicate_declaration.arity,
-				definition.formula);
+				crate::output::human_readable::display_formula(&definition.formula, None, &context));
 		}
 	}
 
@@ -331,24 +330,74 @@ where
 	let completed_definitions = predicate_declarations.iter()
 		.map(|x| (std::rc::Rc::clone(x), completed_definition(x)));
 
-	for (predicate_declaration, completed_definition) in completed_definitions
+	// Earlier log messages may have assigned IDs to the variable declarations, so reset them
-	{
+	context.variable_declaration_ids.borrow_mut().clear();
-		println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name,
-			predicate_declaration.arity,
-			crate::output::tptp::display_formula(&completed_definition, &context));
-	}
 
-	for integrity_constraint in context.integrity_constraints.borrow().iter()
+	match output_format
 	{
-		println!("tff(integrity_constraint, axiom, {}).",
+		crate::output::Format::HumanReadable =>
-			crate::output::tptp::display_formula(&integrity_constraint, &context));
+		{
+			let mut section_separator = "";
+
+			if !predicate_declarations.is_empty()
+			{
+				println!("{}% completed definitions", section_separator);
+				section_separator = "\n";
+			}
+
+			for (predicate_declaration, completed_definition) in completed_definitions
+			{
+				println!("%% completed definition of {}/{}\n{}", predicate_declaration.name,
+					predicate_declaration.arity, crate::output::human_readable::display_formula(
+						&completed_definition, None, &context));
+			}
+
+			if !context.integrity_constraints.borrow().is_empty()
+			{
+				println!("{}% integrity constraints", section_separator);
+			}
+
+			for integrity_constraint in context.integrity_constraints.borrow().iter()
+			{
+				println!("{}", crate::output::human_readable::display_formula(
+					&integrity_constraint, None, &context));
+			}
+		},
+		crate::output::Format::TPTP =>
+		{
+			let mut section_separator = "";
+
+			if !predicate_declarations.is_empty()
+			{
+				println!("{}% completed definitions", section_separator);
+				section_separator = "\n";
+			}
+
+			for (predicate_declaration, completed_definition) in completed_definitions
+			{
+				println!("tff(completion_{}_{}, axiom, {}).", predicate_declaration.name,
+					predicate_declaration.arity, crate::output::human_readable::display_formula(
+						&completed_definition, None, &context));
+			}
+
+			if !context.integrity_constraints.borrow().is_empty()
+			{
+				println!("{}% integrity constraints", section_separator);
+			}
+
+			for integrity_constraint in context.integrity_constraints.borrow().iter()
+			{
+				println!("tff(integrity_constraint, axiom, {}).",
+					crate::output::human_readable::display_formula(&integrity_constraint, None,
+						&context));
+			}
+		},
 	}
 
 	Ok(())
 }
 
-fn read_rule(rule: &clingo::ast::Rule, context: &Context)
+fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::Error>
-	-> Result<(), crate::Error>
 {
 	let head_type = determine_head_type(rule.head(), context)?;
 
@@ -434,7 +483,8 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context)
 				formula: definition,
 			};
 
-			log::debug!("translated rule with single atom in head: {:?}", definition.formula);
+			log::debug!("translated rule with single atom in head: {}",
+				crate::output::human_readable::display_formula(&definition.formula, None, context));
 
 			definitions.definitions.push(definition);
 		},
@@ -463,7 +513,9 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context)
 
 			let integrity_constraint = universal_closure(scoped_formula);
 
-			log::debug!("translated integrity constraint: {:?}", integrity_constraint);
+			log::debug!("translated integrity constraint: {}",
+				crate::output::human_readable::display_formula(&integrity_constraint, None,
+					context));
 
 			context.integrity_constraints.borrow_mut().push(integrity_constraint);
 		},