diff --git a/src/output/tptp.rs b/src/output/tptp.rs index 7056ce0..5364572 100644 --- a/src/output/tptp.rs +++ b/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, + context: &'b C, +} + +pub(crate) fn display_function_declaration<'a, 'b, C>( + function_declaration: &'a std::rc::Rc, 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); + +pub(crate) fn display_predicate_declaration<'a>( + predicate_declaration: &'a std::rc::Rc) + -> 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 diff --git a/src/traits.rs b/src/traits.rs index 09f4a8b..d31034f 100644 --- a/src/traits.rs +++ b/src/traits.rs @@ -1,8 +1,7 @@ pub(crate) trait InputConstantDeclarationDomain { fn input_constant_declaration_domain(&self, - declaration: &std::rc::Rc) - -> Option; + declaration: &std::rc::Rc) -> crate::Domain; } pub(crate) trait AssignVariableDeclarationDomain diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index ad2e816..1aac8e3 100644 --- a/src/translate/verify_properties.rs +++ b/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(()) diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index 8458ec6..31f43ae 100644 --- a/src/translate/verify_properties/context.rs +++ b/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) - -> Option + declaration: &std::rc::Rc) -> 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) } } diff --git a/src/utils/arithmetic_terms.rs b/src/utils/arithmetic_terms.rs index e1bd2d6..6795892 100644 --- a/src/utils/arithmetic_terms.rs +++ b/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) - .unwrap_or(crate::Domain::Program); + let domain = context.input_constant_declaration_domain(&function.declaration); Ok(domain == crate::Domain::Integer) },