// Operators

pub enum BinaryOperator
{
	Add,
	Subtract,
	Multiply,
	Divide,
	Modulo,
	Exponentiate,
}

pub enum ComparisonOperator
{
	Greater,
	Less,
	LessOrEqual,
	GreaterOrEqual,
	NotEqual,
	Equal,
}

pub enum UnaryOperator
{
	AbsoluteValue,
	Negative,
}

// Primitives

#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct FunctionDeclaration
{
	pub name: String,
	pub arity: usize,
}

impl FunctionDeclaration
{
	pub fn new(name: String, arity: usize) -> Self
	{
		Self
		{
			name,
			arity,
		}
	}
}

pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;

#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct PredicateDeclaration
{
	pub name: String,
	pub arity: usize,
}

impl PredicateDeclaration
{
	pub fn new(name: String, arity: usize) -> Self
	{
		Self
		{
			name,
			arity,
		}
	}
}

pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;

#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct VariableDeclaration
{
	pub name: String,
}

impl VariableDeclaration
{
	pub fn new(name: String) -> Self
	{
		Self
		{
			name,
		}
	}
}

pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;

pub struct VariableDeclarationStack
{
	pub free_variable_declarations: VariableDeclarations,
	bound_variable_declaration_stack: Vec<std::rc::Rc<VariableDeclarations>>,
}

impl VariableDeclarationStack
{
	pub fn new() -> Self
	{
		Self
		{
			free_variable_declarations: VariableDeclarations::new(),
			bound_variable_declaration_stack: vec![],
		}
	}

	pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<VariableDeclaration>>
	{
		for variable_declarations in self.bound_variable_declaration_stack.iter().rev()
		{
			if let Some(variable_declaration) = variable_declarations.iter().find(|x| x.name == variable_name)
			{
				return Some(std::rc::Rc::clone(&variable_declaration));
			}
		}

		if let Some(variable_declaration) = self.free_variable_declarations.iter().find(|x| x.name == variable_name)
		{
			return Some(std::rc::Rc::clone(&variable_declaration));
		}

		None
	}

	pub fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc<VariableDeclaration>
	{
		if let Some(variable_declaration) = self.find(variable_name)
		{
			return variable_declaration;
		}

		let variable_declaration = VariableDeclaration
		{
			name: variable_name.to_owned(),
		};
		let variable_declaration = std::rc::Rc::new(variable_declaration);

		self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));

		variable_declaration
	}

	pub fn push(&mut self, bound_variable_declarations: std::rc::Rc<VariableDeclarations>)
	{
		self.bound_variable_declaration_stack.push(bound_variable_declarations);
	}

	pub fn pop(&mut self)
	{
		// TODO: return error instead
		self.bound_variable_declaration_stack.pop().expect("bound variable is empty, cannot pop last element");
	}
}

// Terms

pub struct BinaryOperation
{
	pub operator: BinaryOperator,
	pub left: Box<Term>,
	pub right: Box<Term>,
}

impl BinaryOperation
{
	pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
	{
		Self
		{
			operator,
			left,
			right,
		}
	}
}

pub struct Function
{
	pub declaration: std::rc::Rc<FunctionDeclaration>,
	pub arguments: Vec<Box<Term>>,
}

impl Function
{
	pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
	{
		Self
		{
			declaration: std::rc::Rc::clone(declaration),
			arguments,
		}
	}
}

pub enum SpecialInteger
{
	Infimum,
	Supremum,
}

pub struct UnaryOperation
{
	pub operator: UnaryOperator,
	pub argument: Box<Term>,
}

impl UnaryOperation
{
	pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
	{
		Self
		{
			operator,
			argument,
		}
	}
}

pub struct Variable
{
	pub declaration: std::rc::Rc<VariableDeclaration>,
}

impl Variable
{
	pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
	{
		Self
		{
			declaration: std::rc::Rc::clone(declaration),
		}
	}
}

// Formulas

pub struct Compare
{
	pub operator: ComparisonOperator,
	pub left: Box<Term>,
	pub right: Box<Term>,
}

impl Compare
{
	pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
	{
		Self
		{
			operator,
			left,
			right,
		}
	}
}

pub struct Exists
{
	pub parameters: std::rc::Rc<VariableDeclarations>,
	pub argument: Box<Formula>,
}

impl Exists
{
	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
	{
		Self
		{
			parameters,
			argument,
		}
	}
}

pub struct ForAll
{
	pub parameters: std::rc::Rc<VariableDeclarations>,
	pub argument: Box<Formula>,
}

impl ForAll
{
	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
	{
		Self
		{
			parameters,
			argument,
		}
	}
}

pub struct IfAndOnlyIf
{
	pub left: Box<Formula>,
	pub right: Box<Formula>,
}

impl IfAndOnlyIf
{
	pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
	{
		Self
		{
			left,
			right,
		}
	}
}

pub struct Implies
{
	pub antecedent: Box<Formula>,
	pub implication: Box<Formula>,
}

impl Implies
{
	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
	{
		Self
		{
			antecedent,
			implication,
		}
	}
}

pub struct Predicate
{
	pub declaration: std::rc::Rc<PredicateDeclaration>,
	pub arguments: Vec<Box<Term>>,
}

impl Predicate
{
	pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
	{
		Self
		{
			declaration: std::rc::Rc::clone(declaration),
			arguments,
		}
	}
}

// Variants

pub enum Term
{
	BinaryOperation(BinaryOperation),
	Boolean(bool),
	Function(Function),
	Integer(i32),
	SpecialInteger(SpecialInteger),
	String(String),
	Symbolic(String),
	UnaryOperation(UnaryOperation),
	Variable(Variable),
}

pub type Terms = Vec<Box<Term>>;

impl Term
{
	pub fn absolute_value(argument: Box<Term>) -> Self
	{
		Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
	}

	pub fn add(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::binary_operation(BinaryOperator::Add, left, right)
	}

	pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::BinaryOperation(BinaryOperation::new(operator, left, right))
	}

	pub fn boolean(value: bool) -> Self
	{
		Self::Boolean(value)
	}

	pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::binary_operation(BinaryOperator::Divide, left, right)
	}

	pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::binary_operation(BinaryOperator::Exponentiate, left, right)
	}

	pub fn false_() -> Self
	{
		Self::boolean(false)
	}

	pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
	{
		Self::Function(Function::new(declaration, arguments))
	}

	pub fn infimum() -> Self
	{
		Self::special_integer(SpecialInteger::Infimum)
	}

	pub fn integer(value: i32) -> Self
	{
		Self::Integer(value)
	}

	pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::binary_operation(BinaryOperator::Modulo, left, right)
	}

	pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::binary_operation(BinaryOperator::Multiply, left, right)
	}

	pub fn negative(argument: Box<Term>) -> Self
	{
		Self::unary_operation(UnaryOperator::Negative, argument)
	}

	pub fn special_integer(value: SpecialInteger) -> Self
	{
		Self::SpecialInteger(value)
	}

	pub fn string(value: String) -> Self
	{
		Self::String(value)
	}

	pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::binary_operation(BinaryOperator::Subtract, left, right)
	}

	pub fn supremum() -> Self
	{
		Self::special_integer(SpecialInteger::Supremum)
	}

	pub fn symbolic(value: String) -> Self
	{
		Self::Symbolic(value)
	}

	pub fn true_() -> Self
	{
		Self::boolean(true)
	}

	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
	{
		Self::UnaryOperation(UnaryOperation::new(operator, argument))
	}

	pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
	{
		Self::Variable(Variable::new(declaration))
	}
}

pub enum Formula
{
	And(Formulas),
	Boolean(bool),
	Compare(Compare),
	Exists(Exists),
	ForAll(ForAll),
	IfAndOnlyIf(IfAndOnlyIf),
	Implies(Implies),
	Not(Box<Formula>),
	Or(Formulas),
	Predicate(Predicate),
}

pub type Formulas = Vec<Box<Formula>>;

impl Formula
{
	pub fn and(arguments: Formulas) -> Self
	{
		Self::And(arguments)
	}

	pub fn boolean(value: bool) -> Self
	{
		Self::Boolean(value)
	}

	pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::Compare(Compare::new(operator, left, right))
	}

	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
	{
		Self::Exists(Exists::new(parameters, argument))
	}

	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::compare(ComparisonOperator::Equal, left, right)
	}

	pub fn false_() -> Self
	{
		Self::boolean(false)
	}

	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
	{
		Self::ForAll(ForAll::new(parameters, argument))
	}

	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::compare(ComparisonOperator::Greater, left, right)
	}

	pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
	}

	pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
	{
		Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
	}

	pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
	{
		Self::Implies(Implies::new(antecedent, consequent))
	}

	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::compare(ComparisonOperator::Less, left, right)
	}

	pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::compare(ComparisonOperator::LessOrEqual, left, right)
	}

	pub fn not(argument: Box<Formula>) -> Self
	{
		Self::Not(argument)
	}

	pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
	{
		Self::compare(ComparisonOperator::NotEqual, left, right)
	}

	pub fn or(arguments: Formulas) -> Self
	{
		Self::Or(arguments)
	}

	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
	{
		Self::Predicate(Predicate::new(declaration, arguments))
	}

	pub fn true_() -> Self
	{
		Self::boolean(true)
	}
}