Support hashing domains

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),
@@ -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,11 +75,36 @@ 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
@@ -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 = term_requires_parentheses(self.term, self.parent);
-		let requires_parentheses = precedence > self.parent_precedence;
 
 		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::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
@@ -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 = formula_requires_parentheses(self.formula, self.parent);
-		let requires_parentheses = precedence > self.parent_precedence;
 
 		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,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
 				{
@@ -206,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 = ", "
 					}
@@ -237,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))
 	}
 }
 
@@ -245,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))
 	}
 }
 
@@ -253,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))
 	}
 }
 
@@ -261,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

@@ -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};

src/parse.rs

@@ -100,7 +100,7 @@ fn is_uppercase_alphanumeric(c: char) -> bool
 	c.is_alphanumeric() && c.is_uppercase()
 }
 
-fn symbolic_identifier(i: &str) -> IResult<&str, String>
+pub fn symbolic_identifier(i: &str) -> IResult<&str, String>
 {
 	let (i, symbolic_identifier) = map
 	(
@@ -174,7 +174,7 @@ fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
 				let domain = match name.chars().next()
 				{
 					Some('X') | Some('Y') | Some('Z') => crate::Domain::Program,
-					Some('I') | Some('N') | Some('M') => 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"),
 				};
@@ -518,7 +518,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 						tag(","),
 						variable_declaration
 					),
-					formula_precedence_1
+					formula_precedence_2
 				)
 			),
 			whitespace0
@@ -553,7 +553,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
 						tag(","),
 						variable_declaration
 					),
-					formula_precedence_1
+					formula_precedence_2
 				)
 			),
 			whitespace0
@@ -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)))),
+		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)),
+		},
 	}
 }