Refactoring
This commit is contained in:
parent
f949c0f3f8
commit
680f17bda0
@ -29,7 +29,7 @@ impl std::fmt::Display for crate::PredicateDeclaration
|
|||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Clone, Copy, Eq, PartialEq)]
|
#[derive(Clone, Copy, Eq, PartialEq)]
|
||||||
enum FormulaChildPosition
|
enum FormulaPosition
|
||||||
{
|
{
|
||||||
Any,
|
Any,
|
||||||
ImpliesAntecedent,
|
ImpliesAntecedent,
|
||||||
@ -39,7 +39,7 @@ struct FormulaDisplay<'formula>
|
|||||||
{
|
{
|
||||||
formula: &'formula crate::Formula,
|
formula: &'formula crate::Formula,
|
||||||
parent_formula: Option<&'formula crate::Formula>,
|
parent_formula: Option<&'formula crate::Formula>,
|
||||||
position: FormulaChildPosition,
|
position: FormulaPosition,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'formula> FormulaDisplay<'formula>
|
impl<'formula> FormulaDisplay<'formula>
|
||||||
@ -97,7 +97,7 @@ impl<'formula> FormulaDisplay<'formula>
|
|||||||
{
|
{
|
||||||
// Implications with the same direction nested on the antecedent side
|
// Implications with the same direction nested on the antecedent side
|
||||||
// require parentheses because implication is considered right-associative
|
// require parentheses because implication is considered right-associative
|
||||||
self.position == FormulaChildPosition::ImpliesAntecedent
|
self.position == FormulaPosition::ImpliesAntecedent
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
@ -113,7 +113,7 @@ impl<'formula> FormulaDisplay<'formula>
|
|||||||
}
|
}
|
||||||
|
|
||||||
fn display_formula<'formula>(formula: &'formula crate::Formula,
|
fn display_formula<'formula>(formula: &'formula crate::Formula,
|
||||||
parent_formula: Option<&'formula crate::Formula>, position: FormulaChildPosition)
|
parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition)
|
||||||
-> FormulaDisplay<'formula>
|
-> FormulaDisplay<'formula>
|
||||||
{
|
{
|
||||||
FormulaDisplay
|
FormulaDisplay
|
||||||
@ -158,7 +158,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
}
|
}
|
||||||
|
|
||||||
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula),
|
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula),
|
||||||
FormulaChildPosition::Any))?;
|
FormulaPosition::Any))?;
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
crate::Formula::ForAll(for_all) =>
|
crate::Formula::ForAll(for_all) =>
|
||||||
@ -182,11 +182,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
}
|
}
|
||||||
|
|
||||||
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula),
|
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula),
|
||||||
FormulaChildPosition::Any))?;
|
FormulaPosition::Any))?;
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
||||||
display_formula(argument, Some(self.formula), FormulaChildPosition::Any))?,
|
display_formula(argument, Some(self.formula), FormulaPosition::Any))?,
|
||||||
crate::Formula::And(arguments) =>
|
crate::Formula::And(arguments) =>
|
||||||
{
|
{
|
||||||
if arguments.is_empty()
|
if arguments.is_empty()
|
||||||
@ -198,7 +198,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
let (parent_formula, position) = match arguments.len()
|
let (parent_formula, position) = match arguments.len()
|
||||||
{
|
{
|
||||||
1 => (self.parent_formula, self.position),
|
1 => (self.parent_formula, self.position),
|
||||||
_ => (Some(self.formula), FormulaChildPosition::Any),
|
_ => (Some(self.formula), FormulaPosition::Any),
|
||||||
};
|
};
|
||||||
|
|
||||||
let mut separator = "";
|
let mut separator = "";
|
||||||
@ -223,7 +223,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
let (parent_formula, position) = match arguments.len()
|
let (parent_formula, position) = match arguments.len()
|
||||||
{
|
{
|
||||||
1 => (self.parent_formula, self.position),
|
1 => (self.parent_formula, self.position),
|
||||||
_ => (Some(self.formula), FormulaChildPosition::Any),
|
_ => (Some(self.formula), FormulaPosition::Any),
|
||||||
};
|
};
|
||||||
|
|
||||||
let mut separator = "";
|
let mut separator = "";
|
||||||
@ -243,13 +243,13 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
{
|
{
|
||||||
write!(format, "{:?}",
|
write!(format, "{:?}",
|
||||||
display_formula(antecedent, Some(self.formula),
|
display_formula(antecedent, Some(self.formula),
|
||||||
FormulaChildPosition::ImpliesAntecedent))
|
FormulaPosition::ImpliesAntecedent))
|
||||||
};
|
};
|
||||||
|
|
||||||
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
|
||||||
{
|
{
|
||||||
write!(format, "{:?}",
|
write!(format, "{:?}",
|
||||||
display_formula(implication, Some(self.formula), FormulaChildPosition::Any))
|
display_formula(implication, Some(self.formula), FormulaPosition::Any))
|
||||||
};
|
};
|
||||||
|
|
||||||
match direction
|
match direction
|
||||||
@ -279,7 +279,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
let (parent_formula, position) = match arguments.len()
|
let (parent_formula, position) = match arguments.len()
|
||||||
{
|
{
|
||||||
1 => (self.parent_formula, self.position),
|
1 => (self.parent_formula, self.position),
|
||||||
_ => (Some(self.formula), FormulaChildPosition::Any),
|
_ => (Some(self.formula), FormulaPosition::Any),
|
||||||
};
|
};
|
||||||
|
|
||||||
let mut separator = "";
|
let mut separator = "";
|
||||||
@ -306,9 +306,9 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
};
|
};
|
||||||
|
|
||||||
write!(format, "{:?} {} {:?}",
|
write!(format, "{:?} {} {:?}",
|
||||||
display_term(&compare.left, None, TermChildPosition::Any),
|
display_term(&compare.left, None, TermPosition::Any),
|
||||||
operator_string,
|
operator_string,
|
||||||
display_term(&compare.right, None, TermChildPosition::Any))?
|
display_term(&compare.right, None, TermPosition::Any))?;
|
||||||
},
|
},
|
||||||
crate::Formula::Boolean(true) => write!(format, "true")?,
|
crate::Formula::Boolean(true) => write!(format, "true")?,
|
||||||
crate::Formula::Boolean(false) => write!(format, "false")?,
|
crate::Formula::Boolean(false) => write!(format, "false")?,
|
||||||
@ -325,7 +325,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||||||
for argument in &predicate.arguments
|
for argument in &predicate.arguments
|
||||||
{
|
{
|
||||||
write!(format, "{}{:?}", separator, display_term(argument, None,
|
write!(format, "{}{:?}", separator, display_term(argument, None,
|
||||||
TermChildPosition::Any))?;
|
TermPosition::Any))?;
|
||||||
|
|
||||||
separator = ", "
|
separator = ", "
|
||||||
}
|
}
|
||||||
@ -356,7 +356,7 @@ impl std::fmt::Debug for crate::Formula
|
|||||||
{
|
{
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||||
{
|
{
|
||||||
write!(format, "{:?}", display_formula(&self, None, FormulaChildPosition::Any))
|
write!(format, "{:?}", display_formula(&self, None, FormulaPosition::Any))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -364,7 +364,7 @@ impl std::fmt::Display for crate::Formula
|
|||||||
{
|
{
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||||
{
|
{
|
||||||
write!(format, "{}", display_formula(&self, None, FormulaChildPosition::Any))
|
write!(format, "{}", display_formula(&self, None, FormulaPosition::Any))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
#[derive(Clone, Copy, Eq, PartialEq)]
|
#[derive(Clone, Copy, Eq, PartialEq)]
|
||||||
pub(crate) enum TermChildPosition
|
pub(crate) enum TermPosition
|
||||||
{
|
{
|
||||||
Any,
|
Any,
|
||||||
Left,
|
Left,
|
||||||
@ -62,7 +62,7 @@ pub(crate) struct TermDisplay<'term>
|
|||||||
{
|
{
|
||||||
term: &'term crate::Term,
|
term: &'term crate::Term,
|
||||||
parent_term: Option<&'term crate::Term>,
|
parent_term: Option<&'term crate::Term>,
|
||||||
position: TermChildPosition,
|
position: TermPosition,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'term> TermDisplay<'term>
|
impl<'term> TermDisplay<'term>
|
||||||
@ -110,7 +110,7 @@ impl<'term> TermDisplay<'term>
|
|||||||
{
|
{
|
||||||
crate::BinaryOperator::Exponentiate =>
|
crate::BinaryOperator::Exponentiate =>
|
||||||
parent_binary_operation.operator == crate::BinaryOperator::Exponentiate
|
parent_binary_operation.operator == crate::BinaryOperator::Exponentiate
|
||||||
&& self.position == TermChildPosition::Left,
|
&& self.position == TermPosition::Left,
|
||||||
crate::BinaryOperator::Multiply
|
crate::BinaryOperator::Multiply
|
||||||
| crate::BinaryOperator::Divide
|
| crate::BinaryOperator::Divide
|
||||||
=> match parent_binary_operation.operator
|
=> match parent_binary_operation.operator
|
||||||
@ -118,7 +118,7 @@ impl<'term> TermDisplay<'term>
|
|||||||
crate::BinaryOperator::Exponentiate => true,
|
crate::BinaryOperator::Exponentiate => true,
|
||||||
crate::BinaryOperator::Divide
|
crate::BinaryOperator::Divide
|
||||||
| crate::BinaryOperator::Modulo
|
| crate::BinaryOperator::Modulo
|
||||||
=> self.position == TermChildPosition::Right,
|
=> self.position == TermPosition::Right,
|
||||||
_ => false,
|
_ => false,
|
||||||
},
|
},
|
||||||
crate::BinaryOperator::Modulo => match parent_binary_operation.operator
|
crate::BinaryOperator::Modulo => match parent_binary_operation.operator
|
||||||
@ -127,7 +127,7 @@ impl<'term> TermDisplay<'term>
|
|||||||
crate::BinaryOperator::Multiply
|
crate::BinaryOperator::Multiply
|
||||||
| crate::BinaryOperator::Divide
|
| crate::BinaryOperator::Divide
|
||||||
| crate::BinaryOperator::Modulo
|
| crate::BinaryOperator::Modulo
|
||||||
=> self.position == TermChildPosition::Right,
|
=> self.position == TermPosition::Right,
|
||||||
_ => false,
|
_ => false,
|
||||||
},
|
},
|
||||||
crate::BinaryOperator::Add
|
crate::BinaryOperator::Add
|
||||||
@ -140,7 +140,7 @@ impl<'term> TermDisplay<'term>
|
|||||||
| crate::BinaryOperator::Modulo
|
| crate::BinaryOperator::Modulo
|
||||||
=> true,
|
=> true,
|
||||||
crate::BinaryOperator::Subtract
|
crate::BinaryOperator::Subtract
|
||||||
=> self.position == TermChildPosition::Right,
|
=> self.position == TermPosition::Right,
|
||||||
_ => false,
|
_ => false,
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
@ -150,7 +150,7 @@ impl<'term> TermDisplay<'term>
|
|||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn display_term<'term>(term: &'term crate::Term, parent_term: Option<&'term crate::Term>,
|
pub(crate) fn display_term<'term>(term: &'term crate::Term, parent_term: Option<&'term crate::Term>,
|
||||||
position: TermChildPosition)
|
position: TermPosition)
|
||||||
-> TermDisplay<'term>
|
-> TermDisplay<'term>
|
||||||
{
|
{
|
||||||
TermDisplay
|
TermDisplay
|
||||||
@ -174,13 +174,13 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||||||
|
|
||||||
match &self.term
|
match &self.term
|
||||||
{
|
{
|
||||||
crate::Term::Boolean(true) => write!(format, "true"),
|
crate::Term::Boolean(true) => write!(format, "true")?,
|
||||||
crate::Term::Boolean(false) => write!(format, "false"),
|
crate::Term::Boolean(false) => write!(format, "false")?,
|
||||||
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
|
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value)?,
|
||||||
crate::Term::Integer(value) => write!(format, "{}", value),
|
crate::Term::Integer(value) => write!(format, "{}", value)?,
|
||||||
crate::Term::String(value) => write!(format, "\"{}\"",
|
crate::Term::String(value) => write!(format, "\"{}\"",
|
||||||
value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t")),
|
value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?,
|
||||||
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
|
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration)?,
|
||||||
crate::Term::Function(function) =>
|
crate::Term::Function(function) =>
|
||||||
{
|
{
|
||||||
write!(format, "{}", function.declaration.name)?;
|
write!(format, "{}", function.declaration.name)?;
|
||||||
@ -198,15 +198,13 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||||||
for argument in &function.arguments
|
for argument in &function.arguments
|
||||||
{
|
{
|
||||||
write!(format, "{}{:?}", separator,
|
write!(format, "{}{:?}", separator,
|
||||||
display_term(&argument, Some(self.term), TermChildPosition::Any))?;
|
display_term(&argument, Some(self.term), TermPosition::Any))?;
|
||||||
|
|
||||||
separator = ", ";
|
separator = ", ";
|
||||||
}
|
}
|
||||||
|
|
||||||
write!(format, ")")?;
|
write!(format, ")")?;
|
||||||
}
|
}
|
||||||
|
|
||||||
Ok(())
|
|
||||||
},
|
},
|
||||||
crate::Term::BinaryOperation(binary_operation) =>
|
crate::Term::BinaryOperation(binary_operation) =>
|
||||||
{
|
{
|
||||||
@ -221,19 +219,19 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||||||
};
|
};
|
||||||
|
|
||||||
write!(format, "{:?} {} {:?}",
|
write!(format, "{:?} {} {:?}",
|
||||||
display_term(&binary_operation.left, Some(self.term), TermChildPosition::Left),
|
display_term(&binary_operation.left, Some(self.term), TermPosition::Left),
|
||||||
operator_string,
|
operator_string,
|
||||||
display_term(&binary_operation.right, Some(self.term), TermChildPosition::Right))
|
display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?;
|
||||||
},
|
},
|
||||||
crate::Term::UnaryOperation(
|
crate::Term::UnaryOperation(
|
||||||
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
|
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
|
||||||
=> write!(format, "-{:?}",
|
=> write!(format, "-{:?}",
|
||||||
display_term(argument, Some(self.term), TermChildPosition::Any)),
|
display_term(argument, Some(self.term), TermPosition::Any))?,
|
||||||
crate::Term::UnaryOperation(
|
crate::Term::UnaryOperation(
|
||||||
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
|
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
|
||||||
=> write!(format, "|{:?}|",
|
=> write!(format, "|{:?}|",
|
||||||
display_term(argument, Some(self.term), TermChildPosition::Any)),
|
display_term(argument, Some(self.term), TermPosition::Any))?,
|
||||||
}?;
|
}
|
||||||
|
|
||||||
if requires_parentheses
|
if requires_parentheses
|
||||||
{
|
{
|
||||||
@ -256,7 +254,7 @@ impl std::fmt::Debug for crate::Term
|
|||||||
{
|
{
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||||
{
|
{
|
||||||
write!(format, "{:?}", display_term(&self, None, TermChildPosition::Any))
|
write!(format, "{:?}", display_term(&self, None, TermPosition::Any))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -264,7 +262,7 @@ impl std::fmt::Display for crate::Term
|
|||||||
{
|
{
|
||||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||||
{
|
{
|
||||||
write!(format, "{}", display_term(&self, None, TermChildPosition::Any))
|
write!(format, "{}", display_term(&self, None, TermPosition::Any))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user