From c7d79e7b079721d061fab1bce2ed5dc611a30968 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Tue, 19 May 2020 15:39:20 +0200 Subject: [PATCH] Make inner types customizable --- src/ast.rs | 234 +++++++++++++++++++++++++---------------- src/flavor.rs | 100 ++++++++++++++++++ src/format.rs | 35 ------ src/format/formulas.rs | 91 ++++++++-------- src/format/terms.rs | 70 ++++++------ src/lib.rs | 1 + src/parse/formulas.rs | 31 +++--- src/parse/terms.rs | 42 +++++--- src/utils.rs | 117 ++++++++++++--------- 9 files changed, 434 insertions(+), 287 deletions(-) create mode 100644 src/flavor.rs diff --git a/src/ast.rs b/src/ast.rs index c7320bf..15cf7f4 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,3 +1,5 @@ +use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _}; + // Operators #[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)] @@ -59,7 +61,8 @@ impl FunctionDeclaration } } -pub type FunctionDeclarations = std::collections::BTreeSet>; +pub type FunctionDeclarations = + std::collections::BTreeSet::FunctionDeclaration>>; #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] pub struct PredicateDeclaration @@ -80,7 +83,8 @@ impl PredicateDeclaration } } -pub type PredicateDeclarations = std::collections::BTreeSet>; +pub type PredicateDeclarations = + std::collections::BTreeSet::PredicateDeclaration>>; pub struct VariableDeclaration { @@ -149,21 +153,26 @@ impl VariableDeclaration } } -pub type VariableDeclarations = Vec>; +pub type VariableDeclarations = + Vec::VariableDeclaration>>; // Terms #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct BinaryOperation +pub struct BinaryOperation +where + F: crate::flavor::Flavor, { pub operator: BinaryOperator, - pub left: Box, - pub right: Box, + pub left: Box>, + pub right: Box>, } -impl BinaryOperation +impl BinaryOperation +where + F: crate::flavor::Flavor, { - pub fn new(operator: BinaryOperator, left: Box, right: Box) -> Self + pub fn new(operator: BinaryOperator, left: Box>, right: Box>) -> Self { Self { @@ -175,17 +184,21 @@ impl BinaryOperation } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct Function +pub struct Function +where + F: crate::flavor::Flavor, { - pub declaration: std::rc::Rc, - pub arguments: Terms, + pub declaration: std::rc::Rc, + pub arguments: Terms, } -impl Function +impl Function +where + F: crate::flavor::Flavor, { - pub fn new(declaration: std::rc::Rc, arguments: Terms) -> Self + pub fn new(declaration: std::rc::Rc, arguments: Terms) -> Self { - assert_eq!(declaration.arity, arguments.len(), + assert_eq!(declaration.arity(), arguments.len(), "function has a different number of arguments then declared"); Self @@ -204,15 +217,19 @@ pub enum SpecialInteger } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct UnaryOperation +pub struct UnaryOperation +where + F: crate::flavor::Flavor, { pub operator: UnaryOperator, - pub argument: Box, + pub argument: Box>, } -impl UnaryOperation +impl UnaryOperation +where + F: crate::flavor::Flavor, { - pub fn new(operator: UnaryOperator, argument: Box) -> Self + pub fn new(operator: UnaryOperator, argument: Box>) -> Self { Self { @@ -223,14 +240,18 @@ impl UnaryOperation } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct Variable +pub struct Variable +where + F: crate::flavor::Flavor, { - pub declaration: std::rc::Rc, + pub declaration: std::rc::Rc, } -impl Variable +impl Variable +where + F: crate::flavor::Flavor, { - pub fn new(declaration: std::rc::Rc) -> Self + pub fn new(declaration: std::rc::Rc) -> Self { Self { @@ -242,16 +263,20 @@ impl Variable // Formulas #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct Compare +pub struct Compare +where + F: crate::flavor::Flavor, { pub operator: ComparisonOperator, - pub left: Box, - pub right: Box, + pub left: Box>, + pub right: Box>, } -impl Compare +impl Compare +where + F: crate::flavor::Flavor, { - pub fn new(operator: ComparisonOperator, left: Box, right: Box) -> Self + pub fn new(operator: ComparisonOperator, left: Box>, right: Box>) -> Self { Self { @@ -263,15 +288,19 @@ impl Compare } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct QuantifiedFormula +pub struct QuantifiedFormula +where + F: crate::flavor::Flavor, { - pub parameters: std::rc::Rc, - pub argument: Box, + pub parameters: std::rc::Rc>, + pub argument: Box>, } -impl QuantifiedFormula +impl QuantifiedFormula +where + F: crate::flavor::Flavor, { - pub fn new(parameters: std::rc::Rc, argument: Box) -> Self + pub fn new(parameters: std::rc::Rc>, argument: Box>) -> Self { Self { @@ -282,16 +311,21 @@ impl QuantifiedFormula } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct Implies +pub struct Implies +where + F: crate::flavor::Flavor, { pub direction: ImplicationDirection, - pub antecedent: Box, - pub implication: Box, + pub antecedent: Box>, + pub implication: Box>, } -impl Implies +impl Implies +where + F: crate::flavor::Flavor, { - pub fn new(direction: ImplicationDirection, antecedent: Box, implication: Box) + pub fn new(direction: ImplicationDirection, antecedent: Box>, + implication: Box>) -> Self { Self @@ -304,17 +338,21 @@ impl Implies } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub struct Predicate +pub struct Predicate +where + F: crate::flavor::Flavor, { - pub declaration: std::rc::Rc, - pub arguments: Terms, + pub declaration: std::rc::Rc, + pub arguments: Terms, } -impl Predicate +impl Predicate +where + F: crate::flavor::Flavor, { - pub fn new(declaration: std::rc::Rc, arguments: Terms) -> Self + pub fn new(declaration: std::rc::Rc, arguments: Terms) -> Self { - assert_eq!(declaration.arity, arguments.len(), + assert_eq!(declaration.arity(), arguments.len(), "predicate has a different number of arguments then declared"); Self @@ -328,33 +366,37 @@ impl Predicate // Variants #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub enum Term +pub enum Term +where + F: crate::flavor::Flavor, { - BinaryOperation(BinaryOperation), + BinaryOperation(BinaryOperation), Boolean(bool), - Function(Function), + Function(Function), Integer(i32), SpecialInteger(SpecialInteger), String(String), - UnaryOperation(UnaryOperation), - Variable(Variable), + UnaryOperation(UnaryOperation), + Variable(Variable), } -pub type Terms = Vec; +pub type Terms = Vec>; -impl Term +impl Term +where + F: crate::flavor::Flavor, { - pub fn absolute_value(argument: Box) -> Self + pub fn absolute_value(argument: Box>) -> Self { Self::unary_operation(UnaryOperator::AbsoluteValue, argument) } - pub fn add(left: Box, right: Box) -> Self + pub fn add(left: Box>, right: Box>) -> Self { Self::binary_operation(BinaryOperator::Add, left, right) } - pub fn binary_operation(operator: BinaryOperator, left: Box, right: Box) -> Self + pub fn binary_operation(operator: BinaryOperator, left: Box>, right: Box>) -> Self { Self::BinaryOperation(BinaryOperation::new(operator, left, right)) } @@ -364,12 +406,12 @@ impl Term Self::Boolean(value) } - pub fn divide(left: Box, right: Box) -> Self + pub fn divide(left: Box>, right: Box>) -> Self { Self::binary_operation(BinaryOperator::Divide, left, right) } - pub fn exponentiate(left: Box, right: Box) -> Self + pub fn exponentiate(left: Box>, right: Box>) -> Self { Self::binary_operation(BinaryOperator::Exponentiate, left, right) } @@ -379,7 +421,7 @@ impl Term Self::boolean(false) } - pub fn function(declaration: std::rc::Rc, arguments: Terms) -> Self + pub fn function(declaration: std::rc::Rc, arguments: Terms) -> Self { Self::Function(Function::new(declaration, arguments)) } @@ -394,17 +436,17 @@ impl Term Self::Integer(value) } - pub fn modulo(left: Box, right: Box) -> Self + pub fn modulo(left: Box>, right: Box>) -> Self { Self::binary_operation(BinaryOperator::Modulo, left, right) } - pub fn multiply(left: Box, right: Box) -> Self + pub fn multiply(left: Box>, right: Box>) -> Self { Self::binary_operation(BinaryOperator::Multiply, left, right) } - pub fn negative(argument: Box) -> Self + pub fn negative(argument: Box>) -> Self { Self::unary_operation(UnaryOperator::Negative, argument) } @@ -419,7 +461,7 @@ impl Term Self::String(value) } - pub fn subtract(left: Box, right: Box) -> Self + pub fn subtract(left: Box>, right: Box>) -> Self { Self::binary_operation(BinaryOperator::Subtract, left, right) } @@ -434,37 +476,41 @@ impl Term Self::boolean(true) } - pub fn unary_operation(operator: UnaryOperator, argument: Box) -> Self + pub fn unary_operation(operator: UnaryOperator, argument: Box>) -> Self { Self::UnaryOperation(UnaryOperation::new(operator, argument)) } - pub fn variable(declaration: std::rc::Rc) -> Self + pub fn variable(declaration: std::rc::Rc) -> Self { Self::Variable(Variable::new(declaration)) } } #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] -pub enum Formula +pub enum Formula +where + F: crate::flavor::Flavor, { - And(Formulas), + And(Formulas), Boolean(bool), - Compare(Compare), - Exists(QuantifiedFormula), - ForAll(QuantifiedFormula), - IfAndOnlyIf(Formulas), - Implies(Implies), - Not(Box), - Or(Formulas), - Predicate(Predicate), + Compare(Compare), + Exists(QuantifiedFormula), + ForAll(QuantifiedFormula), + IfAndOnlyIf(Formulas), + Implies(Implies), + Not(Box>), + Or(Formulas), + Predicate(Predicate), } -pub type Formulas = Vec; +pub type Formulas = Vec>; -impl Formula +impl Formula +where + F: crate::flavor::Flavor, { - pub fn and(arguments: Formulas) -> Self + pub fn and(arguments: Formulas) -> Self { Self::And(arguments) } @@ -474,17 +520,17 @@ impl Formula Self::Boolean(value) } - pub fn compare(operator: ComparisonOperator, left: Box, right: Box) -> Self + pub fn compare(operator: ComparisonOperator, left: Box>, right: Box>) -> Self { Self::Compare(Compare::new(operator, left, right)) } - pub fn exists(parameters: std::rc::Rc, argument: Box) -> Self + pub fn exists(parameters: std::rc::Rc>, argument: Box>) -> Self { Self::Exists(QuantifiedFormula::new(parameters, argument)) } - pub fn equal(left: Box, right: Box) -> Self + pub fn equal(left: Box>, right: Box>) -> Self { Self::compare(ComparisonOperator::Equal, left, right) } @@ -494,58 +540,58 @@ impl Formula Self::boolean(false) } - pub fn for_all(parameters: std::rc::Rc, argument: Box) -> Self + pub fn for_all(parameters: std::rc::Rc>, argument: Box>) -> Self { Self::ForAll(QuantifiedFormula::new(parameters, argument)) } - pub fn greater(left: Box, right: Box) -> Self + pub fn greater(left: Box>, right: Box>) -> Self { Self::compare(ComparisonOperator::Greater, left, right) } - pub fn greater_or_equal(left: Box, right: Box) -> Self + pub fn greater_or_equal(left: Box>, right: Box>) -> Self { Self::compare(ComparisonOperator::GreaterOrEqual, left, right) } - pub fn if_and_only_if(arguments: Formulas) -> Self + pub fn if_and_only_if(arguments: Formulas) -> Self { Self::IfAndOnlyIf(arguments) } - pub fn implies(direction: ImplicationDirection, antecedent: Box, - consequent: Box) -> Self + pub fn implies(direction: ImplicationDirection, antecedent: Box>, + consequent: Box>) -> Self { Self::Implies(Implies::new(direction, antecedent, consequent)) } - pub fn less(left: Box, right: Box) -> Self + pub fn less(left: Box>, right: Box>) -> Self { Self::compare(ComparisonOperator::Less, left, right) } - pub fn less_or_equal(left: Box, right: Box) -> Self + pub fn less_or_equal(left: Box>, right: Box>) -> Self { Self::compare(ComparisonOperator::LessOrEqual, left, right) } - pub fn not(argument: Box) -> Self + pub fn not(argument: Box>) -> Self { Self::Not(argument) } - pub fn not_equal(left: Box, right: Box) -> Self + pub fn not_equal(left: Box>, right: Box>) -> Self { Self::compare(ComparisonOperator::NotEqual, left, right) } - pub fn or(arguments: Formulas) -> Self + pub fn or(arguments: Formulas) -> Self { Self::Or(arguments) } - pub fn predicate(declaration: std::rc::Rc, arguments: Terms) -> Self + pub fn predicate(declaration: std::rc::Rc, arguments: Terms) -> Self { Self::Predicate(Predicate::new(declaration, arguments)) } @@ -556,8 +602,10 @@ impl Formula } } -pub struct OpenFormula +pub struct OpenFormula +where + F: crate::flavor::Flavor, { - pub free_variable_declarations: std::rc::Rc, - pub formula: Formula, + pub free_variable_declarations: std::rc::Rc>, + pub formula: Formula, } diff --git a/src/flavor.rs b/src/flavor.rs new file mode 100644 index 0000000..a619c3c --- /dev/null +++ b/src/flavor.rs @@ -0,0 +1,100 @@ +pub trait FunctionDeclaration +{ + fn new(name: String, arity: usize) -> Self; + + fn name(&self) -> &str; + fn arity(&self) -> usize; +} + +impl FunctionDeclaration for crate::FunctionDeclaration +{ + fn new(name: String, arity: usize) -> Self + { + Self + { + name, + arity, + } + } + + fn name(&self) -> &str + { + &self.name + } + + fn arity(&self) -> usize + { + self.arity + } +} + +pub trait PredicateDeclaration +{ + fn new(name: String, arity: usize) -> Self; + + fn name(&self) -> &str; + fn arity(&self) -> usize; +} + +impl PredicateDeclaration for crate::PredicateDeclaration +{ + fn new(name: String, arity: usize) -> Self + { + Self + { + name, + arity, + } + } + + fn name(&self) -> &str + { + &self.name + } + + fn arity(&self) -> usize + { + self.arity + } +} + +pub trait VariableDeclaration +{ + fn new(name: String) -> Self; + + fn name(&self) -> &str; +} + +impl VariableDeclaration for crate::VariableDeclaration +{ + fn new(name: String) -> Self + { + Self + { + name + } + } + + fn name(&self) -> &str + { + &self.name + } +} + +pub trait Flavor +{ + type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash; + type PredicateDeclaration: + PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash; + type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash + + std::fmt::Display; +} + +pub struct DefaultFlavor; + +impl Flavor for DefaultFlavor +{ + type FunctionDeclaration = crate::FunctionDeclaration; + type PredicateDeclaration = crate::PredicateDeclaration; + type VariableDeclaration = crate::VariableDeclaration; +} diff --git a/src/format.rs b/src/format.rs index 427878e..2361d0b 100644 --- a/src/format.rs +++ b/src/format.rs @@ -1,37 +1,2 @@ pub mod formulas; pub mod terms; - -pub trait Format -{ - fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter, - variable_declaration: &std::rc::Rc) - -> std::fmt::Result; -} - -pub struct DefaultFormat; - -impl Format for DefaultFormat -{ - fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter, - variable_declaration: &std::rc::Rc) - -> std::fmt::Result - { - write!(formatter, "{:?}", variable_declaration) - } -} - -pub fn display_term<'term, 'format, F>(term: &'term crate::Term, format: &'format F) - -> terms::TermDisplay<'term, 'format, F> -where - F: Format, -{ - terms::display_term(term, None, terms::TermPosition::Any, format) -} - -pub fn display_formula<'formula, 'format, F>(formula: &'formula crate::Formula, format: &'format F) - -> formulas::FormulaDisplay<'formula, 'format, F> -where - F: Format, -{ - formulas::display_formula(formula, None, formulas::FormulaPosition::Any, format) -} diff --git a/src/format/formulas.rs b/src/format/formulas.rs index 25dd927..e436d7c 100644 --- a/src/format/formulas.rs +++ b/src/format/formulas.rs @@ -1,3 +1,4 @@ +use crate::flavor::PredicateDeclaration as _; use super::terms::*; impl std::fmt::Debug for crate::ComparisonOperator @@ -53,19 +54,19 @@ pub(crate) enum FormulaPosition ImpliesAntecedent, } -pub struct FormulaDisplay<'formula, 'format, F> +pub struct FormulaDisplay<'formula, F> where - F: super::Format, + F: crate::flavor::Flavor, { - formula: &'formula crate::Formula, - parent_formula: Option<&'formula crate::Formula>, + formula: &'formula crate::Formula, + parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition, - format: &'format F, + //declarations: &'d D, } -impl<'formula, 'format, F> FormulaDisplay<'formula, 'format, F> +impl<'formula, F> FormulaDisplay<'formula, F> where - F: super::Format, + F: crate::flavor::Flavor, { fn requires_parentheses(&self) -> bool { @@ -135,24 +136,23 @@ where } } -pub(crate) fn display_formula<'formula, 'format, F>(formula: &'formula crate::Formula, - parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition, format: &'format F) - -> FormulaDisplay<'formula, 'format, F> +pub(crate) fn display_formula<'formula, F>(formula: &'formula crate::Formula, + parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition) + -> FormulaDisplay<'formula, F> where - F: super::Format, + F: crate::flavor::Flavor, { FormulaDisplay { formula, parent_formula, position, - format, } } -impl<'formula, 'format, F> std::fmt::Debug for FormulaDisplay<'formula, 'format, F> +impl<'formula, F> std::fmt::Debug for FormulaDisplay<'formula, F> where - F: super::Format, + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -169,8 +169,8 @@ where { if exists.parameters.is_empty() { - write!(formatter, "{:?}", display_formula(&exists.argument, self.parent_formula, - self.position, self.format))?; + write!(formatter, "{:?}", display_formula::(&exists.argument, + self.parent_formula, self.position))?; } else { @@ -180,14 +180,13 @@ where for parameter in exists.parameters.iter() { - write!(formatter, "{}", separator)?; - self.format.display_variable_declaration(formatter, ¶meter)?; + write!(formatter, "{}{}", separator, parameter)?; separator = ", " } write!(formatter, " {:?}", display_formula(&exists.argument, Some(self.formula), - FormulaPosition::Any, self.format))?; + FormulaPosition::Any))?; } }, crate::Formula::ForAll(for_all) => @@ -195,7 +194,7 @@ where if for_all.parameters.is_empty() { write!(formatter, "{:?}", display_formula(&for_all.argument, - self.parent_formula, self.position, self.format))?; + self.parent_formula, self.position))?; } else { @@ -205,18 +204,17 @@ where for parameter in for_all.parameters.iter() { - write!(formatter, "{}", separator)?; - self.format.display_variable_declaration(formatter, ¶meter)?; + write!(formatter, "{}{}", separator, parameter)?; separator = ", " } write!(formatter, " {:?}", display_formula(&for_all.argument, - Some(self.formula), FormulaPosition::Any, self.format))?; + Some(self.formula), FormulaPosition::Any))?; } }, crate::Formula::Not(argument) => write!(formatter, "not {:?}", - display_formula(argument, Some(self.formula), FormulaPosition::Any, self.format))?, + display_formula(argument, Some(self.formula), FormulaPosition::Any))?, crate::Formula::And(arguments) => { if arguments.is_empty() @@ -236,7 +234,7 @@ where for argument in arguments { write!(formatter, "{}{:?}", separator, - display_formula(argument, parent_formula, position, self.format))?; + display_formula(argument, parent_formula, position))?; separator = " and " } @@ -261,7 +259,7 @@ where for argument in arguments { write!(formatter, "{}{:?}", separator, - display_formula(argument, parent_formula, position, self.format))?; + display_formula(argument, parent_formula, position))?; separator = " or " } @@ -273,14 +271,13 @@ where { write!(formatter, "{:?}", display_formula(antecedent, Some(self.formula), - FormulaPosition::ImpliesAntecedent, self.format)) + FormulaPosition::ImpliesAntecedent)) }; let format_implication = |formatter: &mut std::fmt::Formatter| -> Result<_, _> { write!(formatter, "{:?}", - display_formula(implication, Some(self.formula), FormulaPosition::Any, - self.format)) + display_formula(implication, Some(self.formula), FormulaPosition::Any)) }; match direction @@ -318,7 +315,7 @@ where for argument in arguments { write!(formatter, "{}{:?}", separator, - display_formula(argument, parent_formula, position, self.format))?; + display_formula(argument, parent_formula, position))?; separator = " <-> " } @@ -337,15 +334,14 @@ where }; write!(formatter, "{:?} {} {:?}", - display_term(&compare.left, None, TermPosition::Any, self.format), - operator_string, - display_term(&compare.right, None, TermPosition::Any, self.format))?; + display_term(&compare.left, None, TermPosition::Any), operator_string, + display_term(&compare.right, None, TermPosition::Any))?; }, crate::Formula::Boolean(true) => write!(formatter, "true")?, crate::Formula::Boolean(false) => write!(formatter, "false")?, crate::Formula::Predicate(predicate) => { - write!(formatter, "{}", predicate.declaration.name)?; + write!(formatter, "{}", predicate.declaration.name())?; if !predicate.arguments.is_empty() { @@ -356,7 +352,7 @@ where for argument in &predicate.arguments { write!(formatter, "{}{:?}", separator, display_term(argument, None, - TermPosition::Any, self.format))?; + TermPosition::Any))?; separator = ", " } @@ -375,9 +371,9 @@ where } } -impl<'formula, 'format, F> std::fmt::Display for FormulaDisplay<'formula, 'format, F> +impl<'formula, F> std::fmt::Display for FormulaDisplay<'formula, F> where - F: super::Format, + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -385,21 +381,23 @@ where } } -impl std::fmt::Debug for crate::Formula +impl std::fmt::Debug for crate::Formula +where + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any, - &super::DefaultFormat)) + write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any)) } } -impl std::fmt::Display for crate::Formula +impl std::fmt::Display for crate::Formula +where + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any, - &super::DefaultFormat)) + write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any)) } } @@ -407,7 +405,10 @@ impl std::fmt::Display for crate::Formula mod tests { use crate::*; - use crate::format::terms::tests::*; + use format::terms::tests::*; + type Formula = crate::Formula; + type Term = crate::Term; + type VariableDeclarations = crate::VariableDeclarations; macro_rules! assert { @@ -442,7 +443,7 @@ mod tests }; } - fn format(formula: Box) -> String + fn format(formula: Box) -> String { format!("{}", formula) } diff --git a/src/format/terms.rs b/src/format/terms.rs index 970553c..db28842 100644 --- a/src/format/terms.rs +++ b/src/format/terms.rs @@ -1,3 +1,5 @@ +use crate::flavor::FunctionDeclaration as _; + impl std::fmt::Debug for crate::SpecialInteger { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result @@ -58,19 +60,18 @@ pub(crate) enum TermPosition Right, } -pub struct TermDisplay<'term, 'format, F> +pub struct TermDisplay<'term, F> where - F: super::Format, + F: crate::flavor::Flavor, { - term: &'term crate::Term, - parent_term: Option<&'term crate::Term>, + term: &'term crate::Term, + parent_term: Option<&'term crate::Term>, position: TermPosition, - format: &'format F, } -impl<'term, 'format, F> TermDisplay<'term, 'format, F> +impl<'term, F> TermDisplay<'term, F> where - F: super::Format, + F: crate::flavor::Flavor, { fn requires_parentheses(&self) -> bool { @@ -154,24 +155,23 @@ where } } -pub(crate) fn display_term<'term, 'format, F>(term: &'term crate::Term, - parent_term: Option<&'term crate::Term>, position: TermPosition, format: &'format F) - -> TermDisplay<'term, 'format, F> +pub(crate) fn display_term<'term, F>(term: &'term crate::Term, + parent_term: Option<&'term crate::Term>, position: TermPosition) + -> TermDisplay<'term, F> where - F: super::Format, + F: crate::flavor::Flavor, { TermDisplay { term, parent_term, position, - format, } } -impl<'term, 'format, F> std::fmt::Debug for TermDisplay<'term, 'format, F> +impl<'term, F> std::fmt::Debug for TermDisplay<'term, F> where - F: super::Format, + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -190,15 +190,14 @@ where crate::Term::Integer(value) => write!(formatter, "{}", value)?, crate::Term::String(value) => write!(formatter, "\"{}\"", value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?, - crate::Term::Variable(variable) => - self.format.display_variable_declaration(formatter, &variable.declaration)?, + crate::Term::Variable(variable) => write!(formatter, "{}", variable.declaration)?, crate::Term::Function(function) => { - write!(formatter, "{}", function.declaration.name)?; + write!(formatter, "{}", function.declaration.name())?; - assert!(function.declaration.arity == function.arguments.len(), + assert!(function.declaration.arity() == function.arguments.len(), "number of function arguments differs from declaration (expected {}, got {})", - function.declaration.arity, function.arguments.len()); + function.declaration.arity(), function.arguments.len()); if !function.arguments.is_empty() { @@ -209,8 +208,7 @@ where for argument in &function.arguments { write!(formatter, "{}{:?}", separator, - display_term(&argument, Some(self.term), TermPosition::Any, - self.format))?; + display_term(&argument, Some(self.term), TermPosition::Any))?; separator = ", "; } @@ -231,20 +229,18 @@ where }; write!(formatter, "{:?} {} {:?}", - display_term(&binary_operation.left, Some(self.term), TermPosition::Left, - self.format), + display_term(&binary_operation.left, Some(self.term), TermPosition::Left), operator_string, - display_term(&binary_operation.right, Some(self.term), TermPosition::Right, - self.format))?; + display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?; }, crate::Term::UnaryOperation( crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument}) => write!(formatter, "-{:?}", - display_term(argument, Some(self.term), TermPosition::Any, self.format))?, + display_term(argument, Some(self.term), TermPosition::Any))?, crate::Term::UnaryOperation( crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument}) => write!(formatter, "|{:?}|", - display_term(argument, Some(self.term), TermPosition::Any, self.format))?, + display_term(argument, Some(self.term), TermPosition::Any))?, } if requires_parentheses @@ -256,9 +252,9 @@ where } } -impl<'term, 'format, F> std::fmt::Display for TermDisplay<'term, 'format, F> +impl<'term, F> std::fmt::Display for TermDisplay<'term, F> where - F: super::Format, + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -266,20 +262,23 @@ where } } -impl std::fmt::Debug for crate::Term +impl std::fmt::Debug for crate::Term +where + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any, - &super::DefaultFormat)) + write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any)) } } -impl std::fmt::Display for crate::Term +impl std::fmt::Display for crate::Term +where + F: crate::flavor::Flavor, { fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(formatter, "{}", display_term(&self, None, TermPosition::Any, &super::DefaultFormat)) + write!(formatter, "{}", display_term(&self, None, TermPosition::Any)) } } @@ -287,6 +286,7 @@ impl std::fmt::Display for crate::Term pub(crate) mod tests { use crate::*; + type Term = crate::Term; macro_rules! assert { @@ -296,7 +296,7 @@ pub(crate) mod tests }; } - fn format(term: Box) -> String + fn format(term: Box) -> String { format!("{}", term) } diff --git a/src/lib.rs b/src/lib.rs index 1f131f1..8c29c8c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,4 +1,5 @@ mod ast; +pub mod flavor; pub mod format; pub mod parse; mod utils; diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs index 0bf8f23..7049f6f 100644 --- a/src/parse/formulas.rs +++ b/src/parse/formulas.rs @@ -1,9 +1,11 @@ use super::terms::*; use super::tokens::*; -pub fn formula(input: &str, declarations: &D) -> Result +pub fn formula(input: &str, declarations: &D) + -> Result, crate::parse::Error> where - D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration, + F: crate::flavor::Flavor, + D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration, { let variable_declaration_stack = crate::VariableDeclarationStackLayer::free(); @@ -69,19 +71,22 @@ impl std::fmt::Debug for LogicalConnective } } -struct FormulaStr<'i, 'd, 'p, 'v, D> +struct FormulaStr<'i, 'd, 'p, 'v, F, D> +where + F: crate::flavor::Flavor, { input: &'i str, declarations: &'d D, - variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>, + variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>, } -impl<'i, 'd, 'p, 'v, D> FormulaStr<'i, 'd, 'p, 'v, D> +impl<'i, 'd, 'p, 'v, F, D> FormulaStr<'i, 'd, 'p, 'v, F, D> where - D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration, + F: crate::flavor::Flavor, + D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration, { pub fn new(input: &'i str, declarations: &'d D, - variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>) + variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>) -> Self { Self @@ -189,7 +194,7 @@ where Tokens::new_filter_map(self.input, functor) } - pub fn parse(&self, level: usize) -> Result + pub fn parse(&self, level: usize) -> Result, crate::parse::Error> { let indentation = " ".repeat(level); let input = trim_start(self.input); @@ -395,7 +400,7 @@ where // TODO: refactor fn implication_left_to_right_inner(&self, mut argument_iterator: T, level: usize) - -> Result, crate::parse::Error> + -> Result>, crate::parse::Error> where T: std::iter::Iterator> { @@ -418,7 +423,7 @@ where } fn implication_left_to_right(&self, mut argument_iterator: T, level: usize) - -> Result + -> Result, crate::parse::Error> where T: std::iter::Iterator> { @@ -446,9 +451,9 @@ where // TODO: refactor without input argument fn quantified_formula(&self, input: &str, quantifier: Quantifier, level: usize) - -> Result + -> Result, crate::parse::Error> { - let (parameters, input) = match variable_declarations(input)? + let (parameters, input) = match variable_declarations::(input)? { Some(variable_declarations) => variable_declarations, None => return Err(crate::parse::Error::new_expected_variable_declaration( @@ -500,7 +505,7 @@ mod tests #[test] fn tokenize_formula_logical_connectives() { - let declarations = crate::Declarations::new(); + let declarations = crate::Declarations::::new(); let variable_declaration_stack = crate::VariableDeclarationStackLayer::free(); let formula_str = |input| FormulaStr::new(input, &declarations, diff --git a/src/parse/terms.rs b/src/parse/terms.rs index 58a89b6..c893630 100644 --- a/src/parse/terms.rs +++ b/src/parse/terms.rs @@ -1,3 +1,4 @@ +use crate::flavor::VariableDeclaration as _; use super::tokens::*; pub(crate) fn function_name(input: &str) -> Option<(&str, &str)> @@ -82,19 +83,23 @@ fn is_variable_name(identifier: &str) -> bool false } -pub(crate) fn variable_declaration(input: &str) -> Option<(crate::VariableDeclaration, &str)> +pub(crate) fn variable_declaration(input: &str) -> Option<(F::VariableDeclaration, &str)> +where + F: crate::flavor::Flavor, { variable_name(input) .map(|(variable_name, remaining_input)| - (crate::VariableDeclaration::new(variable_name.to_string()), remaining_input)) + (F::VariableDeclaration::new(variable_name.to_string()), remaining_input)) } -pub(crate) fn variable_declarations(input: &str) - -> Result, crate::parse::Error> +pub(crate) fn variable_declarations(input: &str) + -> Result, &str)>, crate::parse::Error> +where + F: crate::flavor::Flavor, { let mut variable_declarations = vec![]; - let (first_variable_declaration, mut input) = match variable_declaration(input) + let (first_variable_declaration, mut input) = match variable_declaration::(input) { Some(first_variable_declaration) => first_variable_declaration, None => return Ok(None), @@ -115,7 +120,7 @@ pub(crate) fn variable_declarations(input: &str) input = trim_start(input); - let (variable_declaration, remaining_input) = match variable_declaration(input) + let (variable_declaration, remaining_input) = match variable_declaration::(input) { Some(variable_declaration) => variable_declaration, None => return Err(crate::parse::Error::new_expected_variable_declaration( @@ -162,19 +167,22 @@ impl std::fmt::Debug for ArithmeticOperatorClass } } -pub(crate) struct TermStr<'i, 'd, 'v, 'p, D> +pub(crate) struct TermStr<'i, 'd, 'v, 'p, F, D> +where + F: crate::flavor::Flavor, { input: &'i str, declarations: &'d D, - variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>, + variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>, } -impl<'i, 'd, 'v, 'p, D> TermStr<'i, 'd, 'v, 'p, D> +impl<'i, 'd, 'v, 'p, F, D> TermStr<'i, 'd, 'v, 'p, F, D> where - D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration, + F: crate::flavor::Flavor, + D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration, { pub fn new(input: &'i str, declarations: &'d D, - variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>) + variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>) -> Self { Self @@ -299,7 +307,7 @@ where Ok(top_level_arithmetic_operator_class) } - pub fn parse(&self, level: usize) -> Result + pub fn parse(&self, level: usize) -> Result, crate::parse::Error> { let indentation = " ".repeat(level); log::trace!("{}- parsing term: {}", indentation, self.input); @@ -497,7 +505,7 @@ where // TODO: refactor fn exponentiate_inner(&self, mut argument_iterator: T, level: usize) - -> Result, crate::parse::Error> + -> Result>, crate::parse::Error> where T: std::iter::Iterator> { @@ -521,7 +529,7 @@ where } fn exponentiate(&self, mut argument_iterator: T, level: usize) - -> Result + -> Result, crate::parse::Error> where T: std::iter::Iterator> { @@ -572,6 +580,9 @@ mod tests #[test] fn parse_variable_declaration() { + let variable_declaration = + |x| super::variable_declaration::(x); + let v = variable_declaration("X").unwrap(); assert_eq!((v.0.name.as_str(), v.1), ("X", "")); let v = variable_declaration("_X").unwrap(); @@ -601,6 +612,9 @@ mod tests #[test] fn parse_variable_declarations() { + let variable_declarations = + |x| super::variable_declarations::(x); + let v = variable_declarations("X.").unwrap().unwrap(); assert_eq!(v.0.len(), 1); assert_eq!(v.0[0].name.as_str(), "X"); diff --git a/src/utils.rs b/src/utils.rs index 9edfa55..a57c1a2 100644 --- a/src/utils.rs +++ b/src/utils.rs @@ -1,25 +1,36 @@ -pub trait FindOrCreateFunctionDeclaration +use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, VariableDeclaration as _}; + +// Group with implementations +pub trait FindOrCreateFunctionDeclaration +where + F: crate::flavor::Flavor, { fn find_or_create_function_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc; + -> std::rc::Rc; } -pub trait FindOrCreatePredicateDeclaration +pub trait FindOrCreatePredicateDeclaration +where + F: crate::flavor::Flavor, { fn find_or_create_predicate_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc; + -> std::rc::Rc; } -pub struct BoundVariableDeclarations<'p> +pub struct BoundVariableDeclarations<'p, F> +where + F: crate::flavor::Flavor, { - parent: &'p VariableDeclarationStackLayer<'p>, - variable_declarations: std::rc::Rc, + parent: &'p VariableDeclarationStackLayer<'p, F>, + variable_declarations: std::rc::Rc>, } -impl<'p> BoundVariableDeclarations<'p> +impl<'p, F> BoundVariableDeclarations<'p, F> +where + F: crate::flavor::Flavor, { - pub fn new(parent: &'p VariableDeclarationStackLayer<'p>, - variable_declarations: std::rc::Rc) -> Self + pub fn new(parent: &'p VariableDeclarationStackLayer<'p, F>, + variable_declarations: std::rc::Rc>) -> Self { Self { @@ -29,33 +40,37 @@ impl<'p> BoundVariableDeclarations<'p> } } -pub enum VariableDeclarationStackLayer<'p> +pub enum VariableDeclarationStackLayer<'p, F> +where + F: crate::flavor::Flavor, { - Free(std::cell::RefCell), - Bound(BoundVariableDeclarations<'p>), + Free(std::cell::RefCell>), + Bound(BoundVariableDeclarations<'p, F>), } -impl<'p> VariableDeclarationStackLayer<'p> +impl<'p, F> VariableDeclarationStackLayer<'p, F> +where + F: crate::flavor::Flavor, { pub fn free() -> Self { Self::Free(std::cell::RefCell::new(vec![])) } - pub fn bound(parent: &'p VariableDeclarationStackLayer<'p>, - variable_declarations: std::rc::Rc) -> Self + pub fn bound(parent: &'p VariableDeclarationStackLayer<'p, F>, + variable_declarations: std::rc::Rc>) -> Self { Self::Bound(BoundVariableDeclarations::new(parent, variable_declarations)) } - pub fn find(&self, variable_name: &str) -> Option> + pub fn find(&self, variable_name: &str) -> Option> { match self { VariableDeclarationStackLayer::Free(free_variable_declarations) => { if let Some(variable_declaration) = free_variable_declarations.borrow().iter() - .find(|x| x.name == variable_name) + .find(|x| x.name() == variable_name) { return Some(std::rc::Rc::clone(&variable_declaration)); } @@ -66,7 +81,7 @@ impl<'p> VariableDeclarationStackLayer<'p> { if let Some(variable_declaration) = bound_variable_declarations .variable_declarations.iter() - .find(|x| x.name == variable_name) + .find(|x| x.name() == variable_name) { return Some(std::rc::Rc::clone(&variable_declaration)); } @@ -76,22 +91,19 @@ impl<'p> VariableDeclarationStackLayer<'p> } } - pub fn find_or_create(&self, variable_name: &str) -> std::rc::Rc + pub fn find_or_create(&self, variable_name: &str) -> std::rc::Rc { match self { VariableDeclarationStackLayer::Free(free_variable_declarations) => { if let Some(variable_declaration) = free_variable_declarations.borrow().iter() - .find(|x| x.name == variable_name) + .find(|x| x.name() == variable_name) { return std::rc::Rc::clone(&variable_declaration); } - let variable_declaration = crate::VariableDeclaration - { - name: variable_name.to_owned(), - }; + let variable_declaration = F::VariableDeclaration::new(variable_name.to_owned()); let variable_declaration = std::rc::Rc::new(variable_declaration); free_variable_declarations.borrow_mut() @@ -103,7 +115,7 @@ impl<'p> VariableDeclarationStackLayer<'p> { if let Some(variable_declaration) = bound_variable_declarations .variable_declarations.iter() - .find(|x| x.name == variable_name) + .find(|x| x.name() == variable_name) { return std::rc::Rc::clone(&variable_declaration); } @@ -113,9 +125,9 @@ impl<'p> VariableDeclarationStackLayer<'p> } } - pub fn free_variable_declarations_do_mut(&self, f: F) -> G + pub fn free_variable_declarations_do_mut(&self, f: F1) -> F2 where - F: Fn(&mut crate::VariableDeclarations) -> G + F1: Fn(&mut crate::VariableDeclarations) -> F2, { match self { @@ -126,9 +138,9 @@ impl<'p> VariableDeclarationStackLayer<'p> } } - pub fn free_variable_declarations_do(&self, f: F) -> G + pub fn free_variable_declarations_do(&self, f: F1) -> F2 where - F: Fn(&crate::VariableDeclarations) -> G + F1: Fn(&crate::VariableDeclarations) -> F2, { match self { @@ -140,41 +152,44 @@ impl<'p> VariableDeclarationStackLayer<'p> } } -pub struct Declarations +pub struct Declarations +where + F: crate::flavor::Flavor, { - function_declarations: std::cell::RefCell, - predicate_declarations: std::cell::RefCell, + function_declarations: std::cell::RefCell>, + predicate_declarations: std::cell::RefCell>, } -impl Declarations +impl Declarations +where + F: crate::flavor::Flavor, { pub fn new() -> Self { Self { - function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()), - predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()), + function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::::new()), + predicate_declarations: + std::cell::RefCell::new(crate::PredicateDeclarations::::new()), } } } -impl FindOrCreateFunctionDeclaration for Declarations +impl FindOrCreateFunctionDeclaration for Declarations +where + F: crate::flavor::Flavor, { fn find_or_create_function_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc + -> std::rc::Rc { let mut function_declarations = self.function_declarations.borrow_mut(); - match function_declarations.iter().find(|x| x.name == name && x.arity == arity) + match function_declarations.iter().find(|x| x.name() == name && x.arity() == arity) { Some(declaration) => std::rc::Rc::clone(&declaration), None => { - let declaration = crate::FunctionDeclaration - { - name: name.to_string(), - arity, - }; + let declaration = F::FunctionDeclaration::new(name.to_string(), arity); let declaration = std::rc::Rc::new(declaration); function_declarations.insert(std::rc::Rc::clone(&declaration)); @@ -185,23 +200,21 @@ impl FindOrCreateFunctionDeclaration for Declarations } } -impl FindOrCreatePredicateDeclaration for Declarations +impl FindOrCreatePredicateDeclaration for Declarations +where + F: crate::flavor::Flavor, { fn find_or_create_predicate_declaration(&self, name: &str, arity: usize) - -> std::rc::Rc + -> std::rc::Rc { let mut predicate_declarations = self.predicate_declarations.borrow_mut(); - match predicate_declarations.iter().find(|x| x.name == name && x.arity == arity) + match predicate_declarations.iter().find(|x| x.name() == name && x.arity() == arity) { Some(declaration) => std::rc::Rc::clone(&declaration), None => { - let declaration = crate::PredicateDeclaration - { - name: name.to_string(), - arity, - }; + let declaration = F::PredicateDeclaration::new(name.to_string(), arity); let declaration = std::rc::Rc::new(declaration); predicate_declarations.insert(std::rc::Rc::clone(&declaration));