From d7f04da0bd05708a533c214f56bf21209eca521c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Tue, 4 Feb 2020 16:53:52 +0100 Subject: [PATCH] Restructure project --- src/lib.rs | 1 + src/output/human_readable.rs | 36 ++++++++--------- src/output/tptp.rs | 40 +++++++++---------- src/traits.rs | 35 ++++++++++++++++ src/translate/common.rs | 36 ----------------- src/translate/common/choose_value_in_term.rs | 6 +-- src/translate/verify_properties.rs | 2 +- src/translate/verify_properties/context.rs | 12 +++--- src/translate/verify_properties/head_type.rs | 2 +- .../verify_properties/translate_body.rs | 24 +++++------ 10 files changed, 97 insertions(+), 97 deletions(-) create mode 100644 src/traits.rs diff --git a/src/lib.rs b/src/lib.rs index 256bbb3..a192ad8 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -2,6 +2,7 @@ pub mod error; pub mod output; +pub(crate) mod traits; pub mod translate; mod utils; diff --git a/src/output/human_readable.rs b/src/output/human_readable.rs index eb761ea..cb5ab04 100644 --- a/src/output/human_readable.rs +++ b/src/output/human_readable.rs @@ -1,7 +1,7 @@ pub(crate) struct VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { variable_declaration: &'a std::rc::Rc, context: &'b C, @@ -11,8 +11,8 @@ pub(crate) fn display_variable_declaration<'a, 'b, C>( variable_declaration: &'a std::rc::Rc, context: &'b C) -> VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { VariableDeclarationDisplay { @@ -51,8 +51,8 @@ pub(crate) fn display_formula<'a, 'b, C>(formula: &'a foliage::Formula, parent_precedence: Option, context: &'b C) -> FormulaDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { FormulaDisplay { @@ -126,8 +126,8 @@ impl Precedence for foliage::Formula impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -147,8 +147,8 @@ where impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -158,8 +158,8 @@ where impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -245,8 +245,8 @@ where impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -256,8 +256,8 @@ where impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -393,8 +393,8 @@ where impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/output/tptp.rs b/src/output/tptp.rs index 3324cce..fbccc02 100644 --- a/src/output/tptp.rs +++ b/src/output/tptp.rs @@ -35,8 +35,8 @@ impl std::fmt::Display for DomainDisplay pub(crate) struct VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { variable_declaration: &'a std::rc::Rc, context: &'b C, @@ -46,8 +46,8 @@ pub(crate) fn display_variable_declaration<'a, 'b, C>( variable_declaration: &'a std::rc::Rc, context: &'b C) -> VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { VariableDeclarationDisplay { @@ -65,8 +65,8 @@ pub(crate) struct TermDisplay<'a, 'b, C> pub(crate) fn display_term<'a, 'b, C>(term: &'a foliage::Term, context: &'b C) -> TermDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { TermDisplay { @@ -84,8 +84,8 @@ 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 + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { FormulaDisplay { @@ -96,8 +96,8 @@ where impl<'a, 'b, C> std::fmt::Debug for VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -117,8 +117,8 @@ where impl<'a, 'b, C> std::fmt::Display for VariableDeclarationDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -128,8 +128,8 @@ where impl<'a, 'b, C> std::fmt::Debug for TermDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -199,8 +199,8 @@ where impl<'a, 'b, C> std::fmt::Display for TermDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -210,8 +210,8 @@ where impl<'a, 'b, C> std::fmt::Debug for FormulaDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -342,8 +342,8 @@ where impl<'a, 'b, C> std::fmt::Display for FormulaDisplay<'a, 'b, C> where - C: crate::translate::common::VariableDeclarationDomain - + crate::translate::common::VariableDeclarationID + C: crate::traits::VariableDeclarationDomain + + crate::traits::VariableDeclarationID { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { diff --git a/src/traits.rs b/src/traits.rs new file mode 100644 index 0000000..8ac1b10 --- /dev/null +++ b/src/traits.rs @@ -0,0 +1,35 @@ +pub(crate) trait AssignVariableDeclarationDomain +{ + fn assign_variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc, domain: crate::Domain); +} + +pub(crate) trait VariableDeclarationDomain +{ + fn variable_declaration_domain(&self, + variable_declaration: &std::rc::Rc) -> Option; +} + +pub(crate) trait VariableDeclarationID +{ + fn variable_declaration_id(&self, + variable_declaration: &std::rc::Rc) -> usize; +} + +pub(crate) trait GetOrCreateFunctionDeclaration +{ + fn get_or_create_function_declaration(&self, name: &str, arity: usize) + -> std::rc::Rc; +} + +pub(crate) trait GetOrCreatePredicateDeclaration +{ + fn get_or_create_predicate_declaration(&self, name: &str, arity: usize) + -> std::rc::Rc; +} + +pub(crate) trait GetOrCreateVariableDeclaration +{ + fn get_or_create_variable_declaration(&self, name: &str) + -> std::rc::Rc; +} diff --git a/src/translate/common.rs b/src/translate/common.rs index 4bffe8e..b1d094a 100644 --- a/src/translate/common.rs +++ b/src/translate/common.rs @@ -3,39 +3,3 @@ mod operators; pub(crate) use choose_value_in_term::*; pub(crate) use operators::*; - -pub(crate) trait AssignVariableDeclarationDomain -{ - fn assign_variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc, domain: crate::Domain); -} - -pub(crate) trait VariableDeclarationDomain -{ - fn variable_declaration_domain(&self, - variable_declaration: &std::rc::Rc) -> Option; -} - -pub(crate) trait VariableDeclarationID -{ - fn variable_declaration_id(&self, - variable_declaration: &std::rc::Rc) -> usize; -} - -pub(crate) trait GetOrCreateFunctionDeclaration -{ - fn get_or_create_function_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc; -} - -pub(crate) trait GetOrCreatePredicateDeclaration -{ - fn get_or_create_predicate_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc; -} - -pub(crate) trait GetOrCreateVariableDeclaration -{ - fn get_or_create_variable_declaration(&self, name: &str) - -> std::rc::Rc; -} diff --git a/src/translate/common/choose_value_in_term.rs b/src/translate/common/choose_value_in_term.rs index 0edd621..3eeab70 100644 --- a/src/translate/common/choose_value_in_term.rs +++ b/src/translate/common/choose_value_in_term.rs @@ -11,9 +11,9 @@ pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, variable_declaration: &std::rc::Rc, context: &C) -> Result where - C: crate::translate::common::GetOrCreateFunctionDeclaration - + crate::translate::common::GetOrCreateVariableDeclaration - + crate::translate::common::AssignVariableDeclarationDomain + C: crate::traits::GetOrCreateFunctionDeclaration + + crate::traits::GetOrCreateVariableDeclaration + + crate::traits::AssignVariableDeclarationDomain { match term.term_type() { diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index e908a64..91f71ab 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -5,7 +5,7 @@ mod translate_body; use context::*; use head_type::*; use translate_body::*; -use crate::translate::common::AssignVariableDeclarationDomain as _; +use crate::traits::AssignVariableDeclarationDomain as _; struct StatementHandler { diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs index 48de482..1bdb835 100644 --- a/src/translate/verify_properties/context.rs +++ b/src/translate/verify_properties/context.rs @@ -41,7 +41,7 @@ impl Context } } -impl crate::translate::common::GetOrCreateFunctionDeclaration for Context +impl crate::traits::GetOrCreateFunctionDeclaration for Context { fn get_or_create_function_declaration(&self, name: &str, arity: usize) -> std::rc::Rc @@ -67,7 +67,7 @@ impl crate::translate::common::GetOrCreateFunctionDeclaration for Context } } -impl crate::translate::common::GetOrCreatePredicateDeclaration for Context +impl crate::traits::GetOrCreatePredicateDeclaration for Context { fn get_or_create_predicate_declaration(&self, name: &str, arity: usize) -> std::rc::Rc @@ -93,7 +93,7 @@ impl crate::translate::common::GetOrCreatePredicateDeclaration for Context } } -impl crate::translate::common::GetOrCreateVariableDeclaration for Context +impl crate::traits::GetOrCreateVariableDeclaration for Context { fn get_or_create_variable_declaration(&self, name: &str) -> std::rc::Rc @@ -116,7 +116,7 @@ impl crate::translate::common::GetOrCreateVariableDeclaration for Context } } -impl crate::translate::common::AssignVariableDeclarationDomain for Context +impl crate::traits::AssignVariableDeclarationDomain for Context { fn assign_variable_declaration_domain(&self, variable_declaration: &std::rc::Rc, domain: crate::Domain) @@ -136,7 +136,7 @@ impl crate::translate::common::AssignVariableDeclarationDomain for Context } } -impl crate::translate::common::VariableDeclarationDomain for Context +impl crate::traits::VariableDeclarationDomain for Context { fn variable_declaration_domain(&self, variable_declaration: &std::rc::Rc) @@ -149,7 +149,7 @@ impl crate::translate::common::VariableDeclarationDomain for Context } } -impl crate::translate::common::VariableDeclarationID for Context +impl crate::traits::VariableDeclarationID for Context { fn variable_declaration_id(&self, variable_declaration: &std::rc::Rc) diff --git a/src/translate/verify_properties/head_type.rs b/src/translate/verify_properties/head_type.rs index c687f35..9ee4436 100644 --- a/src/translate/verify_properties/head_type.rs +++ b/src/translate/verify_properties/head_type.rs @@ -15,7 +15,7 @@ pub(crate) enum HeadType<'a> pub(crate) fn determine_head_type<'a, C>(head_literal: &'a clingo::ast::HeadLiteral, context: &C) -> Result, crate::Error> where - C: crate::translate::common::GetOrCreatePredicateDeclaration + C: crate::traits::GetOrCreatePredicateDeclaration { let create_head_atom = |function: &'a clingo::ast::Function| -> Result<_, crate::Error> { diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index 1ebadd9..ff6a221 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/src/translate/verify_properties/translate_body.rs @@ -2,10 +2,10 @@ pub(crate) fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo context: &C) -> Result where - C: crate::translate::common::GetOrCreateVariableDeclaration - + crate::translate::common::GetOrCreateFunctionDeclaration - + crate::translate::common::GetOrCreatePredicateDeclaration - + crate::translate::common::AssignVariableDeclarationDomain + C: crate::traits::GetOrCreateVariableDeclaration + + crate::traits::GetOrCreateFunctionDeclaration + + crate::traits::GetOrCreatePredicateDeclaration + + crate::traits::AssignVariableDeclarationDomain { let function = match body_term.term_type() { @@ -69,10 +69,10 @@ pub(crate) fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context: &C) -> Result where - C: crate::translate::common::GetOrCreateVariableDeclaration - + crate::translate::common::GetOrCreateFunctionDeclaration - + crate::translate::common::GetOrCreatePredicateDeclaration - + crate::translate::common::AssignVariableDeclarationDomain + C: crate::traits::GetOrCreateVariableDeclaration + + crate::traits::GetOrCreateFunctionDeclaration + + crate::traits::GetOrCreatePredicateDeclaration + + crate::traits::AssignVariableDeclarationDomain { match body_literal.sign() { @@ -147,10 +147,10 @@ pub(crate) fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &C) -> Result where - C: crate::translate::common::GetOrCreateVariableDeclaration - + crate::translate::common::GetOrCreateFunctionDeclaration - + crate::translate::common::GetOrCreatePredicateDeclaration - + crate::translate::common::AssignVariableDeclarationDomain + C: crate::traits::GetOrCreateVariableDeclaration + + crate::traits::GetOrCreateFunctionDeclaration + + crate::traits::GetOrCreatePredicateDeclaration + + crate::traits::AssignVariableDeclarationDomain { body_literals.iter() .map(|body_literal| translate_body_literal(body_literal, context)