From 683236f4a8e4f980800b4375e6bbc0e85d73dcac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Tue, 5 Nov 2019 12:54:15 -0600
Subject: [PATCH] Recognize variables better

---
 src/format.rs |  6 ----
 src/parse.rs  | 95 ++++++++++++++++-----------------------------------
 2 files changed, 30 insertions(+), 71 deletions(-)

diff --git a/src/format.rs b/src/format.rs
index 5189259..e517a7f 100644
--- a/src/format.rs
+++ b/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)
 	}
 }
diff --git a/src/parse.rs b/src/parse.rs
index 0ab696f..f8de31e 100644
--- a/src/parse.rs
+++ b/src/parse.rs
@@ -4,7 +4,7 @@ use nom::
 	bytes::complete::{take_while, take_while_m_n, is_not},
 	character::complete::{digit1, multispace0, space1, not_line_ending, line_ending},
 	sequence::{preceded, delimited, pair, terminated},
-	combinator::{map, map_res},
+	combinator::{map, map_res, recognize},
 	multi::{many0, many0_count, separated_list},
 	branch::alt,
 	bytes::complete::tag,
@@ -95,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
@@ -138,17 +143,20 @@ fn string(i: &str) -> IResult<&str, crate::Term>
 	)(i)
 }
 
-fn program_variable_identifier(i: &str) -> IResult<&str, String>
+fn variable_identifier(i: &str) -> IResult<&str, String>
 {
 	map
 	(
 		delimited
 		(
 			whitespace0,
-			preceded
+			recognize
 			(
-				tag("X"),
-				take_while(char::is_alphanumeric)
+				pair
+				(
+					take_while_m_n(1, 1, is_uppercase_alphanumeric),
+					take_while(char::is_alphanumeric)
+				)
 			),
 			whitespace0
 		),
@@ -156,76 +164,33 @@ fn program_variable_identifier(i: &str) -> IResult<&str, String>
 	)(i)
 }
 
-fn integer_variable_identifier(i: &str) -> IResult<&str, String>
-{
-	map
-	(
-		delimited
-		(
-			whitespace0,
-			preceded
-			(
-				tag("N"),
-				take_while(char::is_alphanumeric)
-			),
-			whitespace0
-		),
-		|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>