From 8870cee1793571a313ac4f0948e4d73c5589e671 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Wed, 6 Nov 2019 19:04:13 -0600
Subject: [PATCH] Support right-to-left implications

---
 src/ast.rs    |  9 ++++++++-
 src/format.rs | 10 +++++++---
 src/lib.rs    |  2 +-
 src/parse.rs  |  8 ++++++--
 4 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/ast.rs b/src/ast.rs
index 9f81d17..06ebb77 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -26,6 +26,13 @@ pub struct ForAll
 	pub argument: Box<Formula>,
 }
 
+#[derive(PartialEq)]
+pub enum ImplicationDirection
+{
+	LeftToRight,
+	RightToLeft,
+}
+
 #[derive(PartialEq)]
 pub enum Formula
 {
@@ -34,7 +41,7 @@ pub enum Formula
 	Not(Box<Formula>),
 	And(Vec<Box<Formula>>),
 	Or(Vec<Box<Formula>>),
-	Implies(Box<Formula>, Box<Formula>),
+	Implies(Box<Formula>, Box<Formula>, ImplicationDirection),
 	Biconditional(Box<Formula>, Box<Formula>),
 	Less(Term, Term),
 	LessOrEqual(Term, Term),
diff --git a/src/format.rs b/src/format.rs
index 9a281c1..1f8a197 100644
--- a/src/format.rs
+++ b/src/format.rs
@@ -75,7 +75,7 @@ fn formula_precedence(formula: &crate::Formula) -> u64
 		crate::Formula::Not(_) => 2,
 		crate::Formula::And(_) => 3,
 		crate::Formula::Or(_) => 4,
-		crate::Formula::Implies(_, _) => 5,
+		crate::Formula::Implies(_, _, _) => 5,
 		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
 			match parent
 			{
-				crate::Formula::Implies(_, _) => true,
+				crate::Formula::Implies(_, _, _) => true,
 				_ => false,
 			}
 		},
@@ -229,7 +229,11 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					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::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))?,
diff --git a/src/lib.rs b/src/lib.rs
index 1954948..94460dc 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -2,5 +2,5 @@ mod ast;
 pub mod format;
 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};
diff --git a/src/parse.rs b/src/parse.rs
index 0e81d0c..32f6809 100644
--- a/src/parse.rs
+++ b/src/parse.rs
@@ -647,8 +647,12 @@ fn formula_precedence_5(i: &str) -> IResult<&str, crate::Formula>
 
 	match preceded(tag("->"), formula_precedence_4)(i)
 	{
-		Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right)))),
-		Err(_) => Ok((i, left)),
+		Ok((i, right)) => Ok((i, crate::Formula::Implies(Box::new(left), Box::new(right), crate::ImplicationDirection::LeftToRight))),
+		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)),
+		},
 	}
 }