#[derive(Clone, Copy, Eq, Hash, PartialEq)]
pub enum ProofDirection
{
	Forward,
	Backward,
}

#[derive(Eq, Hash, PartialEq)]
pub enum CompletionTarget
{
	Predicate(foliage::PredicateDeclaration),
	Constraint,
}

#[derive(Eq, Hash, PartialEq)]
pub enum FormulaStatementKind
{
	Axiom,
	Completion(CompletionTarget),
	Lemma(Option<ProofDirection>),
	Assumption,
	Assertion,
}

pub struct FormulaStatement
{
	pub kind: FormulaStatementKind,
	pub original_text: String,
	pub formula: foliage::Formula,
	pub proven: bool,
}

pub struct InputStatement
{
	pub original_text: String,
}

#[derive(Eq, Hash, PartialEq)]
pub struct InputConstantDeclaration
{
	pub name: String,
	pub domain: foliage::Domain,
}

pub enum InputSymbol
{
	Constant(InputConstantDeclaration),
	Predicate(foliage::PredicateDeclaration),
}

pub enum Block
{
	FormulaStatement(FormulaStatement),
	InputStatement(InputStatement),
	Whitespace(String),
}

pub struct Project
{
	pub blocks: Vec<Block>,
	pub input_constants: std::collections::HashSet<InputConstantDeclaration>,
	pub input_predicates: std::collections::HashSet<foliage::PredicateDeclaration>,
}