Recognize variables better

src/format.rs

@@ -58,12 +58,6 @@ 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)
 	}
 }

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 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},
-	sequence::{preceded, delimited, pair},
-	combinator::{map, map_res},
-	multi::{many0, separated_list},
+	character::complete::{digit1, multispace0, space1, not_line_ending, line_ending},
+	sequence::{preceded, delimited, pair, terminated},
+	combinator::{map, map_res, recognize},
+	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,6 +95,11 @@ fn is_lowercase_alphanumeric(c: char) -> bool
 	c.is_alphanumeric() && c.is_lowercase()
 }
 
+fn is_uppercase_alphanumeric(c: char) -> bool
+{
+	c.is_alphanumeric() && c.is_uppercase()
+}
+
 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,
-			preceded
+			whitespace0,
+			recognize
 			(
-				tag("X"),
-				take_while(char::is_alphanumeric)
+				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,
-		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Program})
-	)(i)
-}
+		variable_identifier,
+			|name|
+			{
+				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(other) => panic!("variable “{}” starts with character “{}”, which is not allowed", name, other),
+					None => panic!("unexpected variable name, please report to bug tracker"),
+				};
 
-fn integer_variable(i: &str) -> IResult<&str, crate::Term>
-{
-	map
-	(
-		integer_variable_identifier,
-		|s| crate::Term::Variable(crate::VariableDeclaration{name: s, domain: crate::Domain::Integer})
+				crate::VariableDeclaration{name, domain}
+			}
 	)(i)
 }
 
 fn variable(i: &str) -> IResult<&str, crate::Term>
 {
-	alt
-	((
-		program_variable,
-		integer_variable
-	))(i)
+	map
+	(
+		variable_declaration,
+		|variable_declaration| crate::Term::Variable(variable_declaration)
+	)(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)
 }
 
@@ -496,10 +503,14 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 	(
 		delimited
 		(
-			multispace0,
+			whitespace0,
 			preceded
 			(
-				tag("exists "),
+				terminated
+				(
+					tag("exists"),
+					whitespace_single,
+				),
 				pair
 				(
 					separated_list
@@ -510,7 +521,7 @@ fn exists(i: &str) -> IResult<&str, crate::Formula>
 					formula_precedence_1
 				)
 			),
-			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
 			(
-				tag("forall "),
+				terminated
+				(
+					tag("forall"),
+					whitespace_single,
+				),
 				pair
 				(
 					separated_list
@@ -541,7 +556,7 @@ fn for_all(i: &str) -> IResult<&str, crate::Formula>
 					formula_precedence_1
 				)
 			),
-			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,
-				preceded(tag("not "), formula_precedence_1),
-				multispace0
+				whitespace0,
+				preceded
+				(
+					terminated
+					(
+						tag("not"),
+						whitespace_single,
+					),
+					formula_precedence_1
+				),
+				whitespace0
 			),
 			|argument| crate::Formula::Not(Box::new(argument))
 		),