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

Support right-to-left implications

Browse Source
This commit is contained in:
Patrick Lühne 2019-11-06 19:04:13 -06:00
parent 9076ecd95d
commit 8870cee179
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 22 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/ast.rs
View File

@ -26,6 +26,13 @@ pub struct ForAll
pub argument: Box<Formula>, pub argument: Box<Formula>,
} }
#[derive(PartialEq)]
pub enum ImplicationDirection
{
LeftToRight,
RightToLeft,
}
#[derive(PartialEq)] #[derive(PartialEq)]
pub enum Formula pub enum Formula
{ {
@ -34,7 +41,7 @@ pub enum Formula
Not(Box<Formula>), Not(Box<Formula>),
And(Vec<Box<Formula>>), And(Vec<Box<Formula>>),
Or(Vec<Box<Formula>>), Or(Vec<Box<Formula>>),
Implies(Box<Formula>, Box<Formula>), Implies(Box<Formula>, Box<Formula>, ImplicationDirection),
Biconditional(Box<Formula>, Box<Formula>), Biconditional(Box<Formula>, Box<Formula>),
Less(Term, Term), Less(Term, Term),
LessOrEqual(Term, Term), LessOrEqual(Term, Term),

10
src/format.rs
View File

@ -75,7 +75,7 @@ fn formula_precedence(formula: &crate::Formula) -> u64
crate::Formula::Not(_) => 2, crate::Formula::Not(_) => 2,
crate::Formula::And(_) => 3, crate::Formula::And(_) => 3,
crate::Formula::Or(_) => 4, crate::Formula::Or(_) => 4,
crate::Formula::Implies(_, _) => 5, crate::Formula::Implies(_, _, _) => 5,
crate::Formula::Biconditional(_, _) => 6, crate::Formula::Biconditional(_, _) => 6,
} }
} }
@ -98,7 +98,7 @@ fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::F
// Implications aren’t associative, so handle them separately // Implications aren’t associative, so handle them separately
match parent match parent
{ {
crate::Formula::Implies(_, _) => true, crate::Formula::Implies(_, _, _) => true,
_ => false, _ => false,
} }
}, },
@ -229,7 +229,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
separator = " or " separator = " or "
} }
}, },
crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?, crate::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction
{
crate::ImplicationDirection::LeftToRight => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
crate::ImplicationDirection::RightToLeft => 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::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::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::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,

2
src/lib.rs
View File

@ -2,5 +2,5 @@ mod ast;
pub mod format; pub mod format;
pub mod parse; pub mod parse;
pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term}; pub use ast::{Domain, Exists, Formula, ForAll, ImplicationDirection, Predicate, PredicateDeclaration, VariableDeclaration, Term};
pub use parse::{formula, formulas, term}; pub use parse::{formula, formulas, term};

8
src/parse.rs
View File

@ -647,8 +647,12 @@ fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula>
match preceded(tag("->"), formula_precedence_4)(i) match preceded(tag("->"), formula_precedence_4)(i)
{ {
Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right)))), Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::LeftToRight))),
Err(_) => Ok((i, left)), Err(_) => match preceded(tag("<-"), formula_precedence_4)(i)
{
Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::RightToLeft))),
Err(_) => Ok((i, left)),
},
} }
} }