commit 1b9654f44f158184342c59a0e1788986d54b81f3
Author: Patrick Lühne <patrick@luehne.de>
Date:   Fri Nov 1 03:36:38 2019 +0100

    Implement term parsing

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..6936990
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+/target
+**/*.rs.bk
+Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..91238cc
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "fol_parser"
+version = "0.1.0"
+authors = ["Patrick Lühne <patrick@luehne.de>"]
+edition = "2018"
+
+[dependencies]
+nom = "5.0"
diff --git a/src/lib.rs b/src/lib.rs
new file mode 100644
index 0000000..7dc9315
--- /dev/null
+++ b/src/lib.rs
@@ -0,0 +1,929 @@
+use nom::
+{
+	IResult,
+	bytes::complete::{take_while, take_while1, take_while_m_n, is_not},
+	character::is_alphanumeric,
+	character::complete::{digit1, multispace0},
+	sequence::{preceded, delimited, pair},
+	combinator::{map, map_res},
+	multi::{many0, separated_list},
+	branch::alt,
+	bytes::complete::tag,
+};
+
+#[derive(PartialEq)]
+pub struct PredicateDeclaration
+{
+	name: String,
+	arity: usize,
+}
+
+#[derive(PartialEq)]
+pub struct Predicate
+{
+	declaration: PredicateDeclaration,
+	arguments: Vec<Term>,
+}
+
+#[derive(PartialEq)]
+pub struct Exists
+{
+	parameters: Vec<VariableDeclaration>,
+	argument: Box<Formula>,
+}
+
+#[derive(PartialEq)]
+pub struct ForAll
+{
+	parameters: Vec<VariableDeclaration>,
+	argument: Box<Formula>,
+}
+
+#[derive(PartialEq)]
+pub enum Formula
+{
+	Exists(Exists),
+	ForAll(ForAll),
+	Not(Box<Formula>),
+	And(Vec<Box<Formula>>),
+	Or(Vec<Box<Formula>>),
+	Implies(Box<Formula>, Box<Formula>),
+	Biconditional(Box<Formula>, Box<Formula>),
+	Less(Term, Term),
+	LessOrEqual(Term, Term),
+	Greater(Term, Term),
+	GreaterOrEqual(Term, Term),
+	Equal(Term, Term),
+	NotEqual(Term, Term),
+	Boolean(bool),
+	Predicate(Predicate),
+}
+
+#[derive(PartialEq)]
+pub enum Domain
+{
+	Program,
+	Integer,
+}
+
+#[derive(PartialEq)]
+pub struct VariableDeclaration
+{
+	name: String,
+	domain: Domain,
+}
+
+#[derive(PartialEq)]
+pub enum Term
+{
+	Infimum,
+	Supremum,
+	Integer(i64),
+	Symbolic(String),
+	String(String),
+	Variable(VariableDeclaration),
+	Add(Box<Term>, Box<Term>),
+	Subtract(Box<Term>, Box<Term>),
+	Multiply(Box<Term>, Box<Term>),
+	Negative(Box<Term>),
+}
+
+pub enum TermOperator
+{
+	Add,
+	Subtract,
+	Multiply,
+}
+
+impl std::fmt::Debug for VariableDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match &self.domain
+		{
+			Domain::Program => write!(format, "X")?,
+			Domain::Integer => write!(format, "N")?,
+		};
+
+		write!(format, "{}", &self.name)
+	}
+}
+
+impl std::fmt::Display for VariableDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match &self.domain
+		{
+			Domain::Program => write!(format, "X")?,
+			Domain::Integer => write!(format, "N")?,
+		};
+
+		write!(format, "{}", &self.name)
+	}
+}
+
+fn term_precedence(term: &Term) -> u64
+{
+	match term
+	{
+		Term::Infimum | Term::Supremum | Term::Integer(_) | Term::Symbolic(_) | Term::String(_) | Term::Variable(_) => 0,
+		Term::Negative(_) => 1,
+		Term::Multiply(_, _) => 2,
+		Term::Add(_, _) | Term::Subtract(_, _) => 3,
+	}
+}
+
+fn formula_precedence(formula: &Formula) -> u64
+{
+	match formula
+	{
+		Formula::Predicate(_) | Formula::Boolean(_) | Formula::Less(_, _) | Formula::LessOrEqual(_, _) | Formula::Greater(_, _) | Formula::GreaterOrEqual(_, _) | Formula::Equal(_, _) | Formula::NotEqual(_, _) => 0,
+		Formula::Not(_) => 1,
+		Formula::And(_) => 2,
+		Formula::Or(_) => 3,
+		Formula::Implies(_, _) => 4,
+		Formula::Biconditional(_, _) => 5,
+		Formula::Exists(_) | Formula::ForAll(_) => 6,
+	}
+}
+
+impl std::fmt::Debug for Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match *self
+		{
+			Term::Infimum => write!(format, "#inf"),
+			Term::Supremum => write!(format, "#sup"),
+			Term::Integer(value) => write!(format, "{}", value),
+			Term::Symbolic(ref value) => write!(format, "{}", value),
+			Term::String(ref value) => write!(format, "\"{}\"", value),
+			Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
+			Term::Add(ref left, ref right) => write!(format, "({:?} + {:?})", left, right),
+			Term::Subtract(ref left, ref right) => write!(format, "({:?} - {:?})", left, right),
+			Term::Multiply(ref left, ref right) => write!(format, "({:?} * {:?})", left, right),
+			Term::Negative(ref argument) => write!(format, "-({:?})", argument),
+		}
+	}
+}
+
+impl std::fmt::Display for Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match *self
+		{
+			Term::Infimum => write!(format, "#inf"),
+			Term::Supremum => write!(format, "#sup"),
+			Term::Integer(value) => write!(format, "{}", value),
+			Term::Symbolic(ref value) => write!(format, "{}", value),
+			Term::String(ref value) => write!(format, "\"{}\"", value),
+			Term::Variable(ref declaration) => write!(format, "{}", declaration),
+			Term::Add(ref left, ref right) => write!(format, "({} + {})", left, right),
+			Term::Subtract(ref left, ref right) => write!(format, "({} - {})", left, right),
+			Term::Multiply(ref left, ref right) => write!(format, "({} * {})", left, right),
+			Term::Negative(ref argument) => write!(format, "-({})", argument),
+		}
+	}
+}
+
+impl std::fmt::Debug for Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match *self
+		{
+			Formula::Exists(ref exists) =>
+			{
+				write!(format, "exists")?;
+
+				let mut separator = " ";
+
+				for parameter in &exists.parameters
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " ({:?})", exists.argument)
+			},
+			Formula::ForAll(ref for_all) =>
+			{
+				write!(format, "forall")?;
+
+				let mut separator = " ";
+
+				for parameter in &for_all.parameters
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " ({:?})", for_all.argument)
+			},
+			Formula::Not(ref argument) => write!(format, "not {:?}", argument),
+			Formula::And(ref arguments) =>
+			{
+				write!(format, "(")?;
+
+				let mut separator = "";
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, argument)?;
+
+					separator = " and "
+				}
+
+				write!(format, ")")
+			},
+			Formula::Or(ref arguments) =>
+			{
+				write!(format, "(")?;
+
+				let mut separator = "";
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, argument)?;
+
+					separator = " or "
+				}
+
+				write!(format, ")")
+			},
+			Formula::Implies(ref left, ref right) => write!(format, "({:?} -> {:?})", left, right),
+			Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <-> {:?})", left, right),
+			Formula::Less(ref left, ref right) => write!(format, "({:?} < {:?})", left, right),
+			Formula::LessOrEqual(ref left, ref right) => write!(format, "({:?} <= {:?})", left, right),
+			Formula::Greater(ref left, ref right) => write!(format, "({:?} > {:?})", left, right),
+			Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({:?} >= {:?})", left, right),
+			Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left, right),
+			Formula::NotEqual(ref left, ref right) => write!(format, "({:?} != {:?})", left, right),
+			Formula::Boolean(value) =>
+				match value
+				{
+					true => write!(format, "#true"),
+					false => write!(format, "#false"),
+				},
+			Formula::Predicate(ref predicate) =>
+			{
+				write!(format, "{}", predicate.declaration.name)?;
+
+				if !predicate.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &predicate.arguments
+					{
+						write!(format, "{}{:?}", separator, argument)?;
+
+						separator = ", "
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+		}
+	}
+}
+
+impl std::fmt::Display for Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match *self
+		{
+			Formula::Exists(ref exists) =>
+			{
+				write!(format, "exists")?;
+
+				let mut separator = " ";
+
+				for parameter in &exists.parameters
+				{
+					write!(format, "{}{}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " ({})", exists.argument)
+			},
+			Formula::ForAll(ref for_all) =>
+			{
+				write!(format, "forall")?;
+
+				let mut separator = " ";
+
+				for parameter in &for_all.parameters
+				{
+					write!(format, "{}{}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " ({})", for_all.argument)
+			},
+			Formula::Not(ref argument) => write!(format, "not {}", argument),
+			Formula::And(ref arguments) =>
+			{
+				write!(format, "(")?;
+
+				let mut separator = "";
+
+				for argument in arguments
+				{
+					write!(format, "{}{}", separator, argument)?;
+
+					separator = " and "
+				}
+
+				write!(format, ")")
+			},
+			Formula::Or(ref arguments) =>
+			{
+				write!(format, "(")?;
+
+				let mut separator = "";
+
+				for argument in arguments
+				{
+					write!(format, "{}{}", separator, argument)?;
+
+					separator = " or "
+				}
+
+				write!(format, ")")
+			},
+			Formula::Implies(ref left, ref right) => write!(format, "({} -> {})", left, right),
+			Formula::Biconditional(ref left, ref right) => write!(format, "({} <-> {})", left, right),
+			Formula::Less(ref left, ref right) => write!(format, "({} < {})", left, right),
+			Formula::LessOrEqual(ref left, ref right) => write!(format, "({} <= {})", left, right),
+			Formula::Greater(ref left, ref right) => write!(format, "({} > {})", left, right),
+			Formula::GreaterOrEqual(ref left, ref right) => write!(format, "({} >= {})", left, right),
+			Formula::Equal(ref left, ref right) => write!(format, "({} = {})", left, right),
+			Formula::NotEqual(ref left, ref right) => write!(format, "({} != {})", left, right),
+			Formula::Boolean(value) =>
+				match value
+				{
+					true => write!(format, "#true"),
+					false => write!(format, "#false"),
+				},
+			Formula::Predicate(ref predicate) =>
+			{
+				write!(format, "{}", predicate.declaration.name)?;
+
+				if !predicate.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &predicate.arguments
+					{
+						write!(format, "{}{}", separator, argument)?;
+
+						separator = ", "
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+		}
+	}
+}
+
+fn infimum(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		delimited(multispace0, tag("#inf"), multispace0),
+		|_| Term::Infimum
+	)(i)
+}
+
+fn supremum(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		delimited(multispace0, tag("#sup"), multispace0),
+		|_| Term::Supremum
+	)(i)
+}
+
+fn integer(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		map_res
+		(
+			delimited(multispace0, digit1, multispace0),
+			std::str::FromStr::from_str
+		),
+		Term::Integer
+	)(i)
+}
+
+fn is_lowercase_alphanumeric(c: char) -> bool
+{
+	c.is_alphanumeric() && c.is_lowercase()
+}
+
+fn symbolic_identifier(i: &str) -> IResult<&str, String>
+{
+	map
+	(
+		pair
+		(
+			take_while_m_n(1, 1, is_lowercase_alphanumeric),
+			take_while(char::is_alphanumeric)
+		),
+		|(s0, s1)| format!("{}{}", s0, s1)
+	)(i)
+}
+
+fn symbolic(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		delimited(multispace0, symbolic_identifier, multispace0),
+		Term::Symbolic
+	)(i)
+}
+
+fn string(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			delimited
+			(
+				tag("\""),
+				is_not("\""),
+				tag("\""),
+			),
+			multispace0
+		),
+		|s: &str| Term::String(s.to_string())
+	)(i)
+}
+
+fn program_variable_identifier(i: &str) -> IResult<&str, String>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			preceded
+			(
+				tag("X"),
+				take_while1(char::is_alphanumeric)
+			),
+			multispace0
+		),
+		|s: &str| s.to_string()
+	)(i)
+}
+
+fn integer_variable_identifier(i: &str) -> IResult<&str, String>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			preceded
+			(
+				tag("N"),
+				take_while1(char::is_alphanumeric)
+			),
+			multispace0
+		),
+		|s: &str| s.to_string()
+	)(i)
+}
+
+fn program_variable_declaration(i: &str) -> IResult<&str, VariableDeclaration>
+{
+	map
+	(
+		program_variable_identifier,
+		|s| VariableDeclaration{name: s, domain: Domain::Program}
+	)(i)
+}
+
+fn integer_variable_declaration(i: &str) -> IResult<&str, VariableDeclaration>
+{
+	map
+	(
+		integer_variable_identifier,
+		|s| VariableDeclaration{name: s, domain: Domain::Integer}
+	)(i)
+}
+
+fn variable_declaration(i: &str) -> IResult<&str, VariableDeclaration>
+{
+	alt
+	((
+		program_variable_declaration,
+		integer_variable_declaration
+	))(i)
+}
+
+fn program_variable(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		program_variable_identifier,
+		|s| Term::Variable(VariableDeclaration{name: s, domain: Domain::Program})
+	)(i)
+}
+
+fn integer_variable(i: &str) -> IResult<&str, Term>
+{
+	map
+	(
+		integer_variable_identifier,
+		|s| Term::Variable(VariableDeclaration{name: s, domain: Domain::Integer})
+	)(i)
+}
+
+fn variable(i: &str) -> IResult<&str, Term>
+{
+	alt
+	((
+		program_variable,
+		integer_variable
+	))(i)
+}
+
+fn predicate_0_ary(i: &str) -> IResult<&str, Formula>
+{
+	map
+	(
+		delimited(multispace0, symbolic_identifier, multispace0),
+		|name| Formula::Predicate(
+			Predicate
+			{
+				declaration:
+					PredicateDeclaration
+					{
+						name: name,
+						arity: 0,
+					},
+				arguments: vec![],
+			})
+	)(i)
+}
+
+fn predicate_n_ary(i: &str) -> IResult<&str, Formula>
+{
+	map
+	(
+		pair
+		(
+			delimited(multispace0, symbolic_identifier, multispace0),
+			delimited
+			(
+				tag("("),
+				separated_list(tag(","), term),
+				tag(")")
+			)
+		),
+		|(name, arguments)| Formula::Predicate(
+				Predicate
+				{
+					declaration:
+						PredicateDeclaration
+						{
+							name: name,
+							arity: arguments.len(),
+						},
+					arguments: arguments,
+				})
+	)(i)
+}
+
+fn predicate(i: &str) -> IResult<&str, Formula>
+{
+	alt
+	((
+		predicate_n_ary,
+		predicate_0_ary
+	))(i)
+}
+
+fn boolean(i: &str) -> IResult<&str, Formula>
+{
+	map
+	(
+		delimited
+		(
+			multispace0,
+			alt
+			((
+				map(tag("#true"), |_| true),
+				map(tag("#false"), |_| false)
+			)),
+			multispace0
+		),
+		|value| Formula::Boolean(value)
+	)(i)
+}
+
+
+
+
+
+
+fn term_parenthesized(i: &str) -> IResult<&str, Term>
+{
+	delimited
+	(
+		multispace0,
+		delimited
+		(
+			tag("("),
+			term,
+			tag(")")
+		),
+		multispace0
+	)(i)
+}
+
+fn fold_terms(initial: Term, remainder: Vec<(TermOperator, Term)>) -> Term
+{
+	remainder.into_iter().fold(initial,
+		|accumulator, pair|
+		{
+			let (term_operator, term) = pair;
+
+			match term_operator
+			{
+				TermOperator::Add => Term::Add(Box::new(accumulator), Box::new(term)),
+				TermOperator::Subtract => Term::Subtract(Box::new(accumulator), Box::new(term)),
+				TermOperator::Multiply => Term::Multiply(Box::new(accumulator), Box::new(term)),
+			}
+		})
+}
+
+fn term_precedence_0(i: &str) -> IResult<&str, Term>
+{
+	alt
+	((
+		infimum,
+		supremum,
+		integer,
+		symbolic,
+		string,
+		variable,
+		term_parenthesized
+	))(i)
+}
+
+fn term_precedence_1(i: &str) -> IResult<&str, Term>
+{
+	alt
+	((
+		map
+		(
+			delimited
+			(
+				multispace0,
+				preceded(tag("-"), term_precedence_0),
+				multispace0
+			),
+			|term| Term::Negative(Box::new(term))
+		),
+		term_precedence_0
+	))(i)
+}
+
+fn term_precedence_2(i: &str) -> IResult<&str, Term>
+{
+	let (i, initial) = term_precedence_1(i)?;
+	let (i, remainder) =
+		many0
+		(
+			|i|
+			{
+				let (i, term) = preceded(tag("*"), term_precedence_1)(i)?;
+				Ok((i, (TermOperator::Multiply, term)))
+			}
+		)(i)?;
+
+	Ok((i, fold_terms(initial, remainder)))
+}
+
+fn term_precedence_3(i: &str) -> IResult<&str, Term>
+{
+	let (i, initial) = term_precedence_2(i)?;
+	let (i, remainder) =
+		many0
+		(
+			alt
+			((
+				|i|
+				{
+					let (i, term) = preceded(tag("+"), term_precedence_2)(i)?;
+					Ok((i, (TermOperator::Add, term)))
+				},
+				|i|
+				{
+					let (i, term) = preceded(tag("-"), term_precedence_2)(i)?;
+					Ok((i, (TermOperator::Subtract, term)))
+				}
+			))
+		)(i)?;
+
+	Ok((i, fold_terms(initial, remainder)))
+}
+
+fn term(i: &str) -> IResult<&str, Term>
+{
+	term_precedence_3(i)
+}
+
+#[cfg(test)]
+mod tests
+{
+	#[test]
+	fn parse_integer()
+	{
+		assert_eq!(crate::integer("12345"), Ok(("", crate::Term::Integer(12345))));
+	}
+
+	#[test]
+	fn parse_variable_declaration()
+	{
+		assert_eq!(crate::variable_declaration("X5"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})));
+		assert_eq!(crate::variable_declaration("NX3"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})));
+	}
+
+	#[test]
+	fn parse_variable()
+	{
+		assert_eq!(crate::variable("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
+		assert_eq!(crate::variable("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
+	}
+
+	#[test]
+	fn parse_string()
+	{
+		assert_eq!(crate::string(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string()))));
+	}
+
+	#[test]
+	fn parse_boolean()
+	{
+		assert_eq!(crate::boolean(" #true "), Ok(("", crate::Formula::Boolean(true))));
+		assert_eq!(crate::boolean(" #false "), Ok(("", crate::Formula::Boolean(false))));
+	}
+
+	#[test]
+	fn parse_term()
+	{
+		assert_eq!(crate::term(" 5 + 3"), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Integer(3)),
+			))));
+
+		assert_eq!(crate::term(" -5"), Ok(("",
+				crate::Term::Negative
+				(
+					Box::new(crate::Term::Integer(5))
+				)
+			)));
+
+		assert_eq!(crate::term(" 5+3 * -(9+ 1)  + 2 "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Add
+				(
+					Box::new(crate::Term::Integer(5)),
+					Box::new(crate::Term::Multiply
+					(
+						Box::new(crate::Term::Integer(3)),
+						Box::new(crate::Term::Negative
+						(
+							Box::new(crate::Term::Add
+							(
+								Box::new(crate::Term::Integer(9)),
+								Box::new(crate::Term::Integer(1)),
+							))
+						)),
+					)),
+				)),
+				Box::new(crate::Term::Integer(2)),
+			))));
+
+		assert_eq!(crate::term(" 5 + a "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Symbolic("a".to_string())),
+			))));
+
+		assert_eq!(crate::term(" 5 + #sup "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Supremum),
+			))));
+
+		assert_eq!(crate::term(" 5 + #inf "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Infimum),
+			))));
+
+		assert_eq!(crate::term(" 5 + \" text \" "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::String(" text ".to_string())),
+			))));
+
+		assert_eq!(crate::term(" 5 + X1 "), Ok(("",
+			crate::Term::Add
+			(
+				Box::new(crate::Term::Integer(5)),
+				Box::new(crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "1".to_string()})),
+			))));
+	}
+
+	#[test]
+	fn parse_predicate()
+	{
+		assert_eq!(crate::predicate("p"), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));
+
+		assert_eq!(crate::predicate_n_ary("p(5, 6, 7)"), Ok(("",
+			crate::Formula::Predicate
+			(
+				crate::Predicate
+				{
+					declaration:
+						crate::PredicateDeclaration
+						{
+							name: "p".to_string(),
+							arity: 3,
+						},
+					arguments:
+						vec!
+						[
+							crate::Term::Integer(5),
+							crate::Term::Integer(6),
+							crate::Term::Integer(7),
+						]
+				}
+			))));
+
+		assert_eq!(crate::predicate("p(1, 3+4*5+6, \"test\")"), Ok(("",
+			crate::Formula::Predicate
+			(
+				crate::Predicate
+				{
+					declaration:
+						crate::PredicateDeclaration
+						{
+							name: "p".to_string(),
+							arity: 3,
+						},
+					arguments:
+						vec!
+						[
+							crate::Term::Integer(1),
+							crate::Term::Add
+							(
+								Box::new(crate::Term::Add
+								(
+									Box::new(crate::Term::Integer(3)),
+									Box::new(crate::Term::Multiply
+									(
+										Box::new(crate::Term::Integer(4)),
+										Box::new(crate::Term::Integer(5)),
+									)),
+								)),
+								Box::new(crate::Term::Integer(6)),
+							),
+							crate::Term::String("test".to_string()),
+						]
+				}
+			))));
+	}
+}