Finish implementing TPTP output

src/output/tptp.rs

@@ -33,6 +33,113 @@ impl std::fmt::Display for DomainDisplay
 	}
 }
 
+pub(crate) struct FunctionDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::traits::InputConstantDeclarationDomain
+{
+	function_declaration: &'a std::rc::Rc<foliage::FunctionDeclaration>,
+	context: &'b C,
+}
+
+pub(crate) fn display_function_declaration<'a, 'b, C>(
+	function_declaration: &'a std::rc::Rc<foliage::FunctionDeclaration>, context: &'b C)
+	-> FunctionDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::traits::InputConstantDeclarationDomain
+{
+	FunctionDeclarationDisplay
+	{
+		function_declaration,
+		context,
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Debug for FunctionDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::traits::InputConstantDeclarationDomain
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}:", self.function_declaration.name)?;
+
+		let domain = self.context.input_constant_declaration_domain(self.function_declaration);
+		let domain_identifier = match domain
+		{
+			crate::Domain::Integer => "$int",
+			crate::Domain::Program => "object",
+		};
+
+		let mut separator = "";
+
+		if self.function_declaration.arity > 0
+		{
+			write!(format, " (")?;
+
+			for _ in 0..self.function_declaration.arity
+			{
+				write!(format, "{}object", separator)?;
+				separator = " * ";
+			}
+
+			write!(format, ") >")?;
+		}
+
+		write!(format, " {}", domain_identifier)
+	}
+}
+
+impl<'a, 'b, C> std::fmt::Display for FunctionDeclarationDisplay<'a, 'b, C>
+where
+	C: crate::traits::InputConstantDeclarationDomain
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+pub(crate) struct PredicateDeclarationDisplay<'a>(&'a std::rc::Rc<foliage::PredicateDeclaration>);
+
+pub(crate) fn display_predicate_declaration<'a>(
+	predicate_declaration: &'a std::rc::Rc<foliage::PredicateDeclaration>)
+	-> PredicateDeclarationDisplay<'a>
+{
+	PredicateDeclarationDisplay(predicate_declaration)
+}
+
+impl<'a> std::fmt::Debug for PredicateDeclarationDisplay<'a>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}:", self.0.name)?;
+
+		let mut separator = "";
+
+		if self.0.arity > 0
+		{
+			write!(format, " (")?;
+
+			for _ in 0..self.0.arity
+			{
+				write!(format, "{}object", separator)?;
+				separator = " * ";
+			}
+
+			write!(format, ") >")?;
+		}
+
+		write!(format, " $o")
+	}
+}
+
+impl<'a> std::fmt::Display for PredicateDeclarationDisplay<'a>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
 pub(crate) struct VariableDeclarationDisplay<'a, 'b, C>
 where
 	C: crate::traits::VariableDeclarationDomain

src/traits.rs

@@ -1,8 +1,7 @@
 pub(crate) trait InputConstantDeclarationDomain
 {
 	fn input_constant_declaration_domain(&self,
-		declaration: &std::rc::Rc<foliage::FunctionDeclaration>)
+		declaration: &std::rc::Rc<foliage::FunctionDeclaration>) -> crate::Domain;
-		-> Option<crate::Domain>;
 }
 
 pub(crate) trait AssignVariableDeclarationDomain

src/translate/verify_properties.rs

@@ -156,6 +156,7 @@ where
 	};
 
 	let predicate_declarations = context.predicate_declarations.borrow();
+	let function_declarations = context.function_declarations.borrow();
 	let completed_definitions = predicate_declarations.iter()
 		// Don’t perform completion for any input predicate
 		.filter(|x| !context.input_predicate_declarations.borrow().contains(*x))
@@ -164,6 +165,13 @@ where
 	// Earlier log messages may have assigned IDs to the variable declarations, so reset them
 	context.variable_declaration_ids.borrow_mut().clear();
 
+	let print_title = |title, section_separator|
+	{
+		print!("{}{}", section_separator, "%".repeat(80));
+		print!("\n% {}", title);
+		println!("\n{}", "%".repeat(80));
+	};
+
 	let print_formula = |formula: &foliage::Formula|
 	{
 		match output_format
@@ -177,14 +185,60 @@ where
 
 	let mut section_separator = "";
 
+	if output_format == crate::output::Format::TPTP
+	{
+		print_title("anthem types", section_separator);
+		section_separator = "\n";
+
+		let tptp_preamble_anthem_types
+			= include_str!("../output/tptp/preamble_types.tptp").trim_end();
+		println!("{}", tptp_preamble_anthem_types);
+
+		print_title("anthem axioms", section_separator);
+
+		let tptp_preamble_anthem_types
+			= include_str!("../output/tptp/preamble_axioms.tptp").trim_end();
+		println!("{}", tptp_preamble_anthem_types);
+
+		if !predicate_declarations.is_empty() || !function_declarations.is_empty()
+		{
+			print_title("types", section_separator);
+
+			if !predicate_declarations.is_empty()
+			{
+				println!("% predicate types")
+			}
+
+			for predicate_declaration in &*predicate_declarations
+			{
+				println!("tff(type, type, {}).",
+					crate::output::tptp::display_predicate_declaration(predicate_declaration));
+			}
+
+			if !function_declarations.is_empty()
+			{
+				println!("% function types")
+			}
+
+			for function_declaration in &*function_declarations
+			{
+				println!("tff(type, type, {}).",
+					crate::output::tptp::display_function_declaration(function_declaration,
+						&context));
+			}
+		}
+	}
+
 	for (i, (predicate_declaration, completed_definition)) in completed_definitions.enumerate()
 	{
 		if i == 0
 		{
-			println!("{}% completed definitions", section_separator);
+			print_title("completed definitions", section_separator);
 		}
 
-		println!("%% completed definition of {}/{}", predicate_declaration.name,
+		section_separator = "\n";
+
+		println!("% completed definition of {}/{}", predicate_declaration.name,
 			predicate_declaration.arity);
 
 		if output_format == crate::output::Format::TPTP
@@ -201,17 +255,17 @@ where
 		}
 
 		println!("");
-
-		section_separator = "\n";
 	}
 
 	for (i, integrity_constraint) in context.integrity_constraints.borrow().iter().enumerate()
 	{
 		if i == 0
 		{
-			println!("{}% integrity constraints", section_separator);
+			print_title("integrity constraints", section_separator);
 		}
 
+		section_separator = "\n";
+
 		if output_format == crate::output::Format::TPTP
 		{
 			print!("tff(integrity_constraint, axiom, ");
@@ -225,8 +279,6 @@ where
 		}
 
 		println!("");
-
-		section_separator = "\n";
 	}
 
 	Ok(())

src/translate/verify_properties/context.rs

@@ -57,12 +57,13 @@ impl Context
 impl crate::traits::InputConstantDeclarationDomain for Context
 {
 	fn input_constant_declaration_domain(&self,
-		declaration: &std::rc::Rc<foliage::FunctionDeclaration>)
+		declaration: &std::rc::Rc<foliage::FunctionDeclaration>) -> crate::Domain
-		-> Option<crate::Domain>
 	{
 		let input_constant_declaration_domains = self.input_constant_declaration_domains.borrow();
 
+		// Assume the program domain if not specified otherwise
 		input_constant_declaration_domains.get(declaration).map(|x| *x)
+			.unwrap_or(crate::Domain::Program)
 	}
 }
 

src/utils/arithmetic_terms.rs

@@ -18,9 +18,7 @@ where
 					crate::Error::new_unsupported_language_feature("functions with arguments"));
 			}
 
-			// Assume the program domain if not specified otherwise
+			let domain = context.input_constant_declaration_domain(&function.declaration);
-			let domain = context.input_constant_declaration_domain(&function.declaration)
-				.unwrap_or(crate::Domain::Program);
 
 			Ok(domain == crate::Domain::Integer)
 		},