patrick/foliage-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix precedence of implication

Browse Source
This commit is contained in:
Patrick Lühne 2020-04-06 21:57:10 +02:00
parent e0dbb8b75f
commit b6308695f6
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 43 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
src/format/formulas.rs
View File

@ -28,10 +28,18 @@ impl std::fmt::Display for crate::PredicateDeclaration
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
enum ChildPosition
{
Any,
ImpliesAntecedent,
}
struct FormulaDisplay<'formula>
{
formula: &'formula crate::Formula,
parent_formula: Option<&'formula crate::Formula>,
position: ChildPosition,
}
impl<'formula> FormulaDisplay<'formula>
@ -84,16 +92,17 @@ impl<'formula> FormulaDisplay<'formula>
| Formula::And(_)
| Formula::Or(_)
=> true,
Formula::Implies(crate::Implies{direction: parent_direction,
antecedent: parent_antecedent, ..}) =>
Formula::Implies(crate::Implies{direction: parent_direction, ..}) =>
if direction == parent_direction
{
// Implications with the same direction nested on the antecedent side require
// parentheses because implication is considered right-associative
std::ptr::eq(self.formula, &**parent_antecedent)
// Implications with the same direction nested on the antecedent side
// require parentheses because implication is considered right-associative
self.position == ChildPosition::ImpliesAntecedent
}
else
{
// Nested implications with opposite direction always require parentheses
// because the order of formulas like p <- q -> r would be ambiguous
true
},
_ => false,
@ -114,13 +123,14 @@ impl<'formula> FormulaDisplay<'formula>
}
fn display_formula<'formula>(formula: &'formula crate::Formula,
parent_formula: Option<&'formula crate::Formula>)
parent_formula: Option<&'formula crate::Formula>, position: ChildPosition)
-> FormulaDisplay<'formula>
{
FormulaDisplay
{
formula,
parent_formula,
position,
}
}
@ -152,7 +162,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
separator = ", "
}
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
write!(format, " {:?}",
display_formula(&exists.argument, Some(self.formula), ChildPosition::Any))?;
},
crate::Formula::ForAll(for_all) =>
{
@ -169,25 +180,27 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
separator = ", "
}
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
write!(format, " {:?}",
display_formula(&for_all.argument, Some(self.formula), ChildPosition::Any))?;
},
crate::Formula::Not(argument) => write!(format, "not {:?}",
display_formula(argument, Some(self.formula)))?,
display_formula(argument, Some(self.formula), ChildPosition::Any))?,
crate::Formula::And(arguments) =>
{
let mut separator = "";
assert!(!arguments.is_empty());
let parent_formula = match arguments.len()
let (parent_formula, position) = match arguments.len()
{
0 | 1 => self.parent_formula,
_ => Some(self.formula),
0 | 1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " and "
}
@ -198,15 +211,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
assert!(!arguments.is_empty());
let parent_formula = match arguments.len()
let (parent_formula, position) = match arguments.len()
{
0 | 1 => self.parent_formula,
_ => Some(self.formula),
0 | 1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " or "
}
@ -215,12 +229,15 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
{
write!(format, "{:?}", display_formula(antecedent, Some(self.formula)))
write!(format, "{:?}",
display_formula(antecedent, Some(self.formula),
ChildPosition::ImpliesAntecedent))
};
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
{
write!(format, "{:?}", display_formula(implication, Some(self.formula)))
write!(format, "{:?}",
display_formula(implication, Some(self.formula), ChildPosition::Any))
};
match direction
@ -245,15 +262,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
assert!(!arguments.is_empty());
let parent_formula = match arguments.len()
let (parent_formula, position) = match arguments.len()
{
0 | 1 => self.parent_formula,
_ => Some(self.formula),
0 | 1 => (self.parent_formula, self.position),
_ => (Some(self.formula), ChildPosition::Any),
};
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, parent_formula))?;
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " <-> "
}
@ -328,7 +346,7 @@ impl std::fmt::Debug for crate::Formula
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", display_formula(&self, None))
write!(format, "{:?}", display_formula(&self, None, ChildPosition::Any))
}
}
@ -336,7 +354,7 @@ impl std::fmt::Display for crate::Formula
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}", display_formula(&self, None))
write!(format, "{}", display_formula(&self, None, ChildPosition::Any))
}
}