From 80aafb2359ca9d1ece1e4b51c26fd77649a1a8fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Tue, 28 Apr 2020 02:36:53 +0200
Subject: [PATCH] Implement right-to-left implication

---
 src/parse/formulas.rs | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index 4201eb1..f7a57c4 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -222,14 +222,25 @@ impl<'i> FormulaStr<'i>
 				LogicalConnective::ImpliesLeftToRight =>
 					return implication_left_to_right(
 						self.split_at_logical_connective(top_level_logical_connective), level + 1),
-				/*LogicalConnective::ImpliesRightToLeft => unimplemented!(),*/
-				_ =>
+				LogicalConnective::ImpliesRightToLeft =>
 				{
-					println!("{}  TODO: parse implication", indentation);
+					let mut argument_iterator =
+						self.split_at_logical_connective(top_level_logical_connective);
+					let first_argument = argument_iterator.next().ok_or_else(||
+						crate::parse::Error::new_expected_logical_connective_argument(
+							"right-to-left implication".to_string(),
+							crate::parse::error::Location::new(0, Some(0))))?;
+					let first_argument = FormulaStr::new(first_argument?).parse(level + 1)?;
 
-					// TODO: implement correctly
-					return Ok(crate::Formula::true_());
-				}
+					return argument_iterator.try_fold(first_argument,
+						|accumulator, argument|
+						{
+							let argument = FormulaStr::new(argument?).parse(level + 1)?;
+
+							Ok(crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
+								Box::new(accumulator), Box::new(argument)))
+						});
+				},
 			}
 		}