Support hashing domains

src/ast.rs

@@ -1,4 +1,4 @@
-#[derive(PartialEq)]
+#[derive(Eq, Hash, PartialEq)]
 pub struct PredicateDeclaration
 {
 	pub name: String,
@@ -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),
@@ -46,7 +53,7 @@ pub enum Formula
 	Predicate(Predicate),
 }
 
-#[derive(PartialEq)]
+#[derive(Eq, Hash, PartialEq)]
 pub enum Domain
 {
 	Program,

src/format.rs

@@ -1,30 +1,30 @@
-struct TermDisplay<'term>
+struct TermDisplay<'parent>
 {
-	parent_precedence: u64,
+	parent: Option<&'parent crate::Term>,
-	term: &'term crate::Term,
+	term: &'parent crate::Term,
 }
 
-struct FormulaDisplay<'formula>
+struct FormulaDisplay<'parent>
 {
-	parent_precedence: u64,
+	parent: Option<&'parent crate::Formula>,
-	formula: &'formula 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)
+fn display_formula<'parent>(formula: &'parent crate::Formula, parent: Option<&'parent crate::Formula>)
-	-> FormulaDisplay<'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
@@ -49,21 +75,40 @@ 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,
 	}
 }
 
+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
 	{
-		match &self.domain
-		{
-			crate::Domain::Program => write!(format, "X")?,
-			crate::Domain::Integer => write!(format, "N")?,
-		};
-
 		write!(format, "{}", &self.name)
 	}
 }
@@ -72,13 +117,7 @@ impl std::fmt::Display for crate::VariableDeclaration
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		match &self.domain
+		write!(format, "{:?}", &self)
-		{
-			crate::Domain::Program => write!(format, "X")?,
-			crate::Domain::Integer => write!(format, "N")?,
-		};
-
-		write!(format, "{}", &self.name)
 	}
 }
 
@@ -86,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 = term_requires_parentheses(self.term, self.parent);
-		let requires_parentheses = precedence > self.parent_precedence;
 
 		if requires_parentheses
 		{
@@ -102,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::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, precedence), display_term(right, precedence)),
+			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, precedence), display_term(right, precedence)),
+			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, precedence)),
+			crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, Some(self.term))),
 		}?;
 
 		if requires_parentheses
@@ -129,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 = formula_requires_parentheses(self.formula, self.parent);
-		let requires_parentheses = precedence > self.parent_precedence;
 
 		if requires_parentheses
 		{
@@ -152,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) =>
 			{
@@ -167,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 "
 				}
@@ -187,19 +224,23 @@ 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::Implies(ref left, ref right, implication_direction) => match implication_direction
-			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::ImplicationDirection::LeftToRight => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
-			crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				crate::ImplicationDirection::RightToLeft => write!(format, "{:?} <- {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
-			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::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
-			crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Less(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, 1000), display_term(right, 1000))?,
+			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
 				{
@@ -218,7 +259,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 = ", "
 					}
@@ -249,7 +290,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))
 	}
 }
 
@@ -257,7 +298,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))
 	}
 }
 
@@ -265,7 +306,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))
 	}
 }
 
@@ -273,6 +314,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))
 	}
 }

src/lib.rs

@@ -1,6 +1,6 @@
 mod ast;
 pub mod format;
-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};

src/parse.rs

@@ -2,10 +2,10 @@ use nom::
 {
 	IResult,
 	bytes::complete::{take_while, take_while_m_n, is_not},
-	character::complete::{digit1, multispace0},
+	character::complete::{digit1, multispace0, space1, not_line_ending, line_ending},
-	sequence::{preceded, delimited, pair},
+	sequence::{preceded, delimited, pair, terminated},
-	combinator::{map, map_res},
+	combinator::{map, map_res, recognize},
-	multi::{many0, separated_list},
+	multi::{many0, many0_count, separated_list},
 	branch::alt,
 	bytes::complete::tag,
 };
@@ -17,11 +17,53 @@ enum TermOperator
 	Multiply,
 }
 
+fn comment(i: &str) -> IResult<&str, &str>
+{
+	terminated
+	(
+		preceded
+		(
+			tag("%"),
+			not_line_ending,
+		),
+		line_ending,
+	)(i)
+}
+
+pub fn whitespace0(i: &str) -> IResult<&str, ()>
+{
+	let (i, _) = preceded
+	(
+		multispace0,
+		many0_count
+		(
+			preceded
+			(
+				comment,
+				multispace0,
+			)
+		),
+	)(i)?;
+
+	Ok((i, ()))
+}
+
+pub fn whitespace_single(i: &str) -> IResult<&str, ()>
+{
+	let (i, _) = alt
+	((
+		space1,
+		line_ending,
+	))(i)?;
+
+	Ok((i, ()))
+}
+
 fn infimum(i: &str) -> IResult<&str, crate::Term>
 {
 	map
 	(
-		delimited(multispace0, tag("#inf"), multispace0),
+		delimited(whitespace0, tag("#inf"), whitespace0),
 		|_| crate::Term::Infimum
 	)(i)
 }
@@ -30,7 +72,7 @@ fn supremum(i: &str) -> IResult<&str, crate::Term>
 {
 	map
 	(
-		delimited(multispace0, tag("#sup"), multispace0),
+		delimited(whitespace0, tag("#sup"), whitespace0),
 		|_| crate::Term::Supremum
 	)(i)
 }
@@ -41,7 +83,7 @@ fn integer(i: &str) -> IResult<&str, crate::Term>
 	(
 		map_res
 		(
-			delimited(multispace0, digit1, multispace0),
+			delimited(whitespace0, digit1, whitespace0),
 			std::str::FromStr::from_str
 		),
 		crate::Term::Integer
@@ -53,7 +95,12 @@ fn is_lowercase_alphanumeric(c: char) -> bool
 	c.is_alphanumeric() && c.is_lowercase()
 }
 
-fn symbolic_identifier(i: &str) -> IResult<&str, String>
+fn is_uppercase_alphanumeric(c: char) -> bool
+{
+	c.is_alphanumeric() && c.is_uppercase()
+}
+
+pub fn symbolic_identifier(i: &str) -> IResult<&str, String>
 {
 	let (i, symbolic_identifier) = map
 	(
@@ -72,7 +119,7 @@ fn symbolic(i: &str) -> IResult<&str, crate::Term>
 {
 	map
 	(
-		delimited(multispace0, symbolic_identifier, multispace0),
+		delimited(whitespace0, symbolic_identifier, whitespace0),
 		crate::Term::Symbolic
 	)(i)
 }
@@ -83,114 +130,74 @@ fn string(i: &str) -> IResult<&str, crate::Term>
 	(
 		delimited
 		(
-			multispace0,
+			whitespace0,
 			delimited
 			(
 				tag("\""),
 				is_not("\""),
 				tag("\""),
 			),
-			multispace0
+			whitespace0
 		),
 		|s: &str| crate::Term::String(s.to_string())
 	)(i)
 }
 
-fn program_variable_identifier(i: &str) -> IResult<&str, String>
+fn variable_identifier(i: &str) -> IResult<&str, String>
 {
 	map
 	(
 		delimited
 		(
-			multispace0,
+			whitespace0,
-			preceded
+			recognize
 			(
-				tag("X"),
+				pair
+				(
+					take_while_m_n(1, 1, is_uppercase_alphanumeric),
 					take_while(char::is_alphanumeric)
+				)
 			),
-			multispace0
+			whitespace0
 		),
 		|s: &str| s.to_string()
 	)(i)
 }
 
-fn integer_variable_identifier(i: &str) -> IResult<&str, String>
-{
-	map
-	(
-		delimited
-		(
-			multispace0,
-			preceded
-			(
-				tag("N"),
-				take_while(char::is_alphanumeric)
-			),
-			multispace0
-		),
-		|s: &str| s.to_string()
-	)(i)
-}
-
-fn program_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
-{
-	map
-	(
-		program_variable_identifier,
-		|s| crate::VariableDeclaration{name: s, domain: crate::Domain::Program}
-	)(i)
-}
-
-fn integer_variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
-{
-	map
-	(
-		integer_variable_identifier,
-		|s| crate::VariableDeclaration{name: s, domain: crate::Domain::Integer}
-	)(i)
-}
-
 fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
-{
-	alt
-	((
-		program_variable_declaration,
-		integer_variable_declaration
-	))(i)
-}
-
-fn program_variable(i: &str) -> IResult<&str, crate::Term>
 {
 	map
 	(
-		program_variable_identifier,
+		variable_identifier,
-		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
+			|name|
-	)(i)
-}
-
-fn integer_variable(i: &str) -> IResult<&str, crate::Term>
 			{
-	map
+				let domain = match name.chars().next()
-	(
+				{
-		integer_variable_identifier,
+					Some('X') | Some('Y') | Some('Z') => crate::Domain::Program,
-		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer})
+					Some('I') | Some('J') | Some('K') | Some('L') | Some('M') | Some('N') => crate::Domain::Integer,
+					Some(other) => panic!("variable “{}” starts with character “{}”, which is not allowed", name, other),
+					None => panic!("unexpected variable name, please report to bug tracker"),
+				};
+
+				crate::VariableDeclaration{name, domain}
+			}
 	)(i)
 }
 
 fn variable(i: &str) -> IResult<&str, crate::Term>
 {
-	alt
+	map
-	((
+	(
-		program_variable,
+		variable_declaration,
-		integer_variable
+		|variable_declaration| crate::Term::Variable(variable_declaration)
-	))(i)
+	)(i)
 }
 
 fn predicate_0_ary(i: &str) -> IResult<&str, crate::Formula>
 {
 	map
 	(
-		delimited(multispace0, symbolic_identifier, multispace0),
+		delimited(whitespace0, symbolic_identifier, whitespace0),
 		|name| crate::Formula::Predicate(
 			crate::Predicate
 			{
@@ -211,17 +218,17 @@ fn predicate_n_ary(i: &str) -> IResult<&str, crate::Formula>
 	(
 		pair
 		(
-			delimited(multispace0, symbolic_identifier, multispace0),
+			delimited(whitespace0, symbolic_identifier, whitespace0),
 			delimited
 			(
-				multispace0,
+				whitespace0,
 				delimited
 				(
 					tag("("),
 					separated_list(tag(","), term),
 					tag(")")
 				),
-				multispace0
+				whitespace0
 			)
 		),
 		|(name, arguments)| crate::Formula::Predicate(
@@ -253,13 +260,13 @@ fn boolean(i: &str) -> IResult<&str, crate::Formula>
 	(
 		delimited
 		(
-			multispace0,
+			whitespace0,
 			alt
 			((
 				map(tag("#true"), |_| true),
 				map(tag("#false"), |_| false)
 			)),
-			multispace0
+			whitespace0
 		),
 		|value| crate::Formula::Boolean(value)
 	)(i)
@@ -360,14 +367,14 @@ fn term_parenthesized(i: &str) -> IResult<&str, crate::Term>
 {
 	delimited
 	(
-		multispace0,
+		whitespace0,
 		delimited
 		(
 			tag("("),
 			term,
 			tag(")")
 		),
-		multispace0
+		whitespace0
 	)(i)
 }
 
@@ -409,9 +416,9 @@ fn term_precedence_1(i: &str) -> IResult<&str, crate::Term>
 		(
 			delimited
 			(
-				multispace0,
+				whitespace0,
 				preceded(tag("-"), term_precedence_0),
-				multispace0
+				whitespace0
 			),
 			|term| crate::Term::Negative(Box::new(term))
 		),
@@ -468,14 +475,14 @@ fn formula_parenthesized(i: &str) -> IResult<&str, crate::Formula>
 {
 	delimited
 	(
-		multispace0,
+		whitespace0,
 		delimited
 		(
 			tag("("),
 			formula,
 			tag(")")
 		),
-		multispace0
+		whitespace0
 	)(i)
 }
 
@@ -483,9 +490,9 @@ fn formula_precedence_0(i: &str) -> IResult<&str, crate::Formula>
 {
 	alt
 	((
+		comparison,
 		predicate,
 		boolean,
-		comparison,
 		formula_parenthesized
 	))(i)
 }
@@ -496,10 +503,14 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 	(
 		delimited
 		(
-			multispace0,
+			whitespace0,
 			preceded
+			(
+				terminated
 				(
 					tag("exists"),
+					whitespace_single,
+				),
 				pair
 				(
 					separated_list
@@ -507,10 +518,10 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 						tag(","),
 						variable_declaration
 					),
-					formula_precedence_1
+					formula_precedence_2
 				)
 			),
-			multispace0
+			whitespace0
 		),
 		|(parameters, argument)| crate::Formula::Exists(
 			crate::Exists
@@ -527,10 +538,14 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
 	(
 		delimited
 		(
-			multispace0,
+			whitespace0,
 			preceded
+			(
+				terminated
 				(
 					tag("forall"),
+					whitespace_single,
+				),
 				pair
 				(
 					separated_list
@@ -538,10 +553,10 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
 						tag(","),
 						variable_declaration
 					),
-					formula_precedence_1
+					formula_precedence_2
 				)
 			),
-			multispace0
+			whitespace0
 		),
 		|(parameters, argument)| crate::Formula::ForAll(
 			crate::ForAll
@@ -570,9 +585,17 @@ fn formula_precedence_2(i: &str) -> IResult<&str, crate::Formula>
 		(
 			delimited
 			(
-				multispace0,
+				whitespace0,
-				preceded(tag("not "), formula_precedence_1),
+				preceded
-				multispace0
+				(
+					terminated
+					(
+						tag("not"),
+						whitespace_single,
+					),
+					formula_precedence_1
+				),
+				whitespace0
 			),
 			|argument| crate::Formula::Not(Box::new(argument))
 		),
@@ -624,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)))),
+		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)),
+		},
 	}
 }
 
@@ -845,6 +872,13 @@ mod tests
 					Box::new(crate::Term::Integer(9)),
 				),
 			))));
+
+		assert_eq!(crate::formula("n = 5"), Ok(("",
+			crate::Formula::Equal
+			(
+				crate::Term::Symbolic("n".to_string()),
+				crate::Term::Integer(5),
+			))));
 	}
 
 	#[test]