Fix precedence rules for nested subtractions and implications
This commit is contained in:
parent
683236f4a8
commit
4e3e3689d0
GPG Key ID:
05F3611E97A70ABF
123
src/format.rs
123
src/format.rs
|
|
@ -1,30 +1,30 @@
|
|||
struct TermDisplay<'term>
|
||||
struct TermDisplay<'parent>
|
||||
{
|
||||
parent_precedence: u64,
|
||||
term: &'term crate::Term,
|
||||
parent: Option<&'parent crate::Term>,
|
||||
term: &'parent crate::Term,
|
||||
}
|
||||
|
||||
struct FormulaDisplay<'formula>
|
||||
struct FormulaDisplay<'parent>
|
||||
{
|
||||
parent_precedence: u64,
|
||||
formula: &'formula crate::Formula,
|
||||
parent: Option<&'parent crate::Formula>,
|
||||
formula: &'parent crate::Formula,
|
||||
}
|
||||
|
||||
fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> TermDisplay<'term>
|
||||
fn display_term<'parent>(term: &'parent crate::Term, parent: Option<&'parent crate::Term>) -> TermDisplay<'parent>
|
||||
{
|
||||
TermDisplay
|
||||
{
|
||||
parent_precedence,
|
||||
parent,
|
||||
term,
|
||||
}
|
||||
}
|
||||
|
||||
fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: u64)
|
||||
-> FormulaDisplay<'formula>
|
||||
fn display_formula<'parent>(formula: &'parent crate::Formula, parent: Option<&'parent crate::Formula>)
|
||||
-> FormulaDisplay<'parent>
|
||||
{
|
||||
FormulaDisplay
|
||||
{
|
||||
parent_precedence,
|
||||
parent,
|
||||
formula,
|
||||
}
|
||||
}
|
||||
|
|
@ -40,6 +40,32 @@ fn term_precedence(term: &crate::Term) -> u64
|
|||
}
|
||||
}
|
||||
|
||||
fn term_requires_parentheses(child: &crate::Term, parent: Option<&crate::Term>) -> bool
|
||||
{
|
||||
match parent
|
||||
{
|
||||
None => false,
|
||||
Some(parent) =>
|
||||
{
|
||||
let child_precedence = term_precedence(child);
|
||||
let parent_precedence = term_precedence(parent);
|
||||
|
||||
if child_precedence != parent_precedence
|
||||
{
|
||||
return child_precedence > parent_precedence;
|
||||
}
|
||||
|
||||
// Subtraction isn’t associative, so handle them separately
|
||||
// TODO: only do this for right-hand side of subtractions
|
||||
match parent
|
||||
{
|
||||
crate::Term::Subtract(_, _) => true,
|
||||
_ => false,
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
fn formula_precedence(formula: &crate::Formula) -> u64
|
||||
{
|
||||
match formula
|
||||
|
|
@ -54,6 +80,31 @@ fn formula_precedence(formula: &crate::Formula) -> u64
|
|||
}
|
||||
}
|
||||
|
||||
fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::Formula>) -> bool
|
||||
{
|
||||
match parent
|
||||
{
|
||||
None => false,
|
||||
Some(parent) =>
|
||||
{
|
||||
let child_precedence = formula_precedence(child);
|
||||
let parent_precedence = formula_precedence(parent);
|
||||
|
||||
if child_precedence != parent_precedence
|
||||
{
|
||||
return child_precedence > parent_precedence;
|
||||
}
|
||||
|
||||
// Implications aren’t associative, so handle them separately
|
||||
match parent
|
||||
{
|
||||
crate::Formula::Implies(_, _) => true,
|
||||
_ => false,
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::VariableDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
|
|
@ -74,8 +125,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
let precedence = term_precedence(self.term);
|
||||
let requires_parentheses = precedence > self.parent_precedence;
|
||||
let requires_parentheses = term_requires_parentheses(self.term, self.parent);
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
|
|
@ -90,10 +140,10 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
|
|||
crate::Term::Symbolic(ref value) => write!(format, "{}", value),
|
||||
crate::Term::String(ref value) => write!(format, "\"{}\"", value),
|
||||
crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
|
||||
crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
|
||||
crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, precedence)),
|
||||
crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
|
||||
crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
|
||||
crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
|
||||
crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, Some(self.term))),
|
||||
}?;
|
||||
|
||||
if requires_parentheses
|
||||
|
|
@ -117,8 +167,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
let precedence = formula_precedence(self.formula);
|
||||
let requires_parentheses = precedence > self.parent_precedence;
|
||||
let requires_parentheses = formula_requires_parentheses(self.formula, self.parent);
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
|
|
@ -140,7 +189,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
|
||||
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
|
||||
},
|
||||
crate::Formula::ForAll(ref for_all) =>
|
||||
{
|
||||
|
|
@ -155,16 +204,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
|
||||
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
|
||||
},
|
||||
crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
|
||||
crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, Some(self.formula)))?,
|
||||
crate::Formula::And(ref arguments) =>
|
||||
{
|
||||
let mut separator = "";
|
||||
|
||||
for argument in arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
|
||||
|
||||
separator = " and "
|
||||
}
|
||||
|
|
@ -175,19 +224,19 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
|
||||
for argument in arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
|
||||
|
||||
separator = " or "
|
||||
}
|
||||
},
|
||||
crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
|
||||
crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
|
||||
crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?,
|
||||
crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?,
|
||||
crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?,
|
||||
crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?,
|
||||
crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?,
|
||||
crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?,
|
||||
crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
|
||||
crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
|
||||
crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
|
||||
crate::Formula::Boolean(value) =>
|
||||
match value
|
||||
{
|
||||
|
|
@ -206,7 +255,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
|||
|
||||
for argument in &predicate.arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_term(argument, 1000))?;
|
||||
write!(format, "{}{:?}", separator, display_term(argument, None))?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
|
|
@ -237,7 +286,7 @@ impl std::fmt::Debug for crate::Formula
|
|||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", display_formula(&self, 1000))
|
||||
write!(format, "{:?}", display_formula(&self, None))
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -245,7 +294,7 @@ impl std::fmt::Display for crate::Formula
|
|||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}", display_formula(&self, 1000))
|
||||
write!(format, "{}", display_formula(&self, None))
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -253,7 +302,7 @@ impl std::fmt::Debug for crate::Term
|
|||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", display_term(&self, 1000))
|
||||
write!(format, "{:?}", display_term(&self, None))
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -261,6 +310,6 @@ impl std::fmt::Display for crate::Term
|
|||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}", display_term(&self, 1000))
|
||||
write!(format, "{}", display_term(&self, None))
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue