Disallow reserved keywords as names

src/parse/names.rs

@@ -30,18 +30,32 @@ fn is_variable_name_character_body(c: char) -> bool
 
 pub fn function_or_predicate_name(i: &str) -> IResult<&str, &str>
 {
-	recognize
-	(
-		terminated
+	let (i, name) =
+		recognize
 		(
-			pair
+			terminated
 			(
-				take_while_m_n(1, 1, is_function_name_character_first),
-				take_while(is_function_name_character_body),
-			),
-			word_boundary,
-		)
-	)(i)
+				pair
+				(
+					take_while_m_n(1, 1, is_function_name_character_first),
+					take_while(is_function_name_character_body),
+				),
+				word_boundary,
+			)
+		)(i)?;
+
+	match name
+	{
+		"and"
+		| "exists"
+		| "false"
+		| "forall"
+		| "not"
+		| "or"
+		| "true"
+			=> Err(nom::Err::Error((i, nom::error::ErrorKind::Verify))),
+		name => Ok((i, name)),
+	}
 }
 
 pub fn variable_name(i: &str) -> IResult<&str, &str>
@@ -80,6 +94,22 @@ mod tests
 		assert!(function_or_predicate_name("_ rest").is_err());
 		assert!(function_or_predicate_name("_predicate_123 rest").is_err());
 		assert!(function_or_predicate_name(" ").is_err());
+		// Keywords aren’t valid names
+		assert!(function_or_predicate_name("and rest").is_err());
+		assert!(function_or_predicate_name("exists rest").is_err());
+		assert!(function_or_predicate_name("false rest").is_err());
+		assert!(function_or_predicate_name("forall rest").is_err());
+		assert!(function_or_predicate_name("or rest").is_err());
+		assert!(function_or_predicate_name("not rest").is_err());
+		assert!(function_or_predicate_name("true rest").is_err());
+		// Names that start with keywords are fine though
+		assert!(function_or_predicate_name("anda rest").is_ok());
+		assert!(function_or_predicate_name("existsa rest").is_ok());
+		assert!(function_or_predicate_name("falsea rest").is_ok());
+		assert!(function_or_predicate_name("foralla rest").is_ok());
+		assert!(function_or_predicate_name("ora rest").is_ok());
+		assert!(function_or_predicate_name("nota rest").is_ok());
+		assert!(function_or_predicate_name("truea rest").is_ok());
 	}
 
 	#[test]