foliage-rs/src/ast.rs

582 lines
10 KiB
Rust
Raw Normal View History

2020-01-24 18:43:42 +01:00
// Operators
pub enum BinaryOperator
{
2020-02-02 02:08:39 +01:00
Add,
Subtract,
Multiply,
Divide,
2020-01-24 18:43:42 +01:00
Modulo,
2020-02-02 02:08:39 +01:00
Exponentiate,
2020-01-24 18:43:42 +01:00
}
pub enum ComparisonOperator
{
Greater,
Less,
LessOrEqual,
GreaterOrEqual,
NotEqual,
Equal,
}
pub enum UnaryOperator
{
AbsoluteValue,
2020-02-02 02:08:39 +01:00
Negative,
2020-01-24 18:43:42 +01:00
}
// Primitives
2020-02-01 17:40:15 +01:00
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
2020-01-24 18:43:42 +01:00
pub struct FunctionDeclaration
{
pub name: String,
pub arity: usize,
}
2020-02-02 02:14:14 +01:00
impl FunctionDeclaration
{
pub fn new(name: String, arity: usize) -> Self
{
Self
{
name,
arity,
}
}
}
pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
2020-02-01 17:40:15 +01:00
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct PredicateDeclaration
{
pub name: String,
pub arity: usize,
}
2020-02-02 02:14:14 +01:00
impl PredicateDeclaration
{
pub fn new(name: String, arity: usize) -> Self
{
Self
{
name,
arity,
}
}
}
pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
2020-02-01 17:40:15 +01:00
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
2020-01-24 18:43:42 +01:00
pub struct VariableDeclaration
{
2020-01-24 18:43:42 +01:00
pub name: String,
}
2020-02-02 02:14:14 +01:00
impl VariableDeclaration
{
pub fn new(name: String) -> Self
{
Self
{
name,
}
}
}
pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
2020-01-24 18:56:03 +01:00
pub struct VariableDeclarationStack
{
pub free_variable_declarations: VariableDeclarations,
bound_variable_declaration_stack: Vec<std::rc::Rc<VariableDeclarations>>,
}
impl VariableDeclarationStack
{
2020-01-31 13:53:42 +01:00
pub fn new() -> Self
{
Self
{
free_variable_declarations: VariableDeclarations::new(),
bound_variable_declaration_stack: vec![],
}
}
2020-01-24 18:56:03 +01:00
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));
2020-01-24 18:56:03 +01:00
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");
}
}
2020-01-24 18:43:42 +01:00
// Terms
pub struct BinaryOperation
{
pub operator: BinaryOperator,
pub left: Box<Term>,
pub right: Box<Term>,
}
2020-02-02 02:14:14 +01:00
impl BinaryOperation
{
pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
{
Self
{
operator,
left,
right,
}
}
}
2020-01-24 18:43:42 +01:00
pub struct Function
{
pub declaration: std::rc::Rc<FunctionDeclaration>,
pub arguments: Vec<Box<Term>>,
}
2020-02-02 02:14:14 +01:00
impl Function
{
pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
{
Self
{
declaration: std::rc::Rc::clone(declaration),
arguments,
}
}
}
2020-01-24 18:43:42 +01:00
pub enum SpecialInteger
{
Infimum,
Supremum,
}
pub struct UnaryOperation
{
pub operator: UnaryOperator,
pub argument: Box<Term>,
}
2020-02-02 02:14:14 +01:00
impl UnaryOperation
{
pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
{
Self
{
operator,
argument,
}
}
}
2020-01-24 18:43:42 +01:00
pub struct Variable
{
pub declaration: std::rc::Rc<VariableDeclaration>,
}
2020-02-02 02:14:14 +01:00
impl Variable
{
pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
{
Self
{
declaration: std::rc::Rc::clone(declaration),
}
}
}
2020-01-24 18:43:42 +01:00
// Formulas
2020-02-02 02:08:39 +01:00
pub struct Compare
2020-01-24 18:43:42 +01:00
{
pub operator: ComparisonOperator,
pub left: Box<Term>,
pub right: Box<Term>,
}
2020-02-02 02:14:14 +01:00
impl Compare
{
pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
{
Self
{
operator,
left,
right,
}
}
}
pub struct Exists
{
pub parameters: VariableDeclarations,
pub argument: Box<Formula>,
}
2020-02-02 02:14:14 +01:00
impl Exists
{
pub fn new(parameters: VariableDeclarations, argument: Box<Formula>) -> Self
{
Self
{
parameters,
argument,
}
}
}
pub struct ForAll
{
pub parameters: VariableDeclarations,
pub argument: Box<Formula>,
}
2020-02-02 02:14:14 +01:00
impl ForAll
{
pub fn new(parameters: VariableDeclarations, argument: Box<Formula>) -> Self
{
Self
{
parameters,
argument,
}
}
}
2020-02-02 02:08:39 +01:00
pub struct IfAndOnlyIf
{
pub left: Box<Formula>,
pub right: Box<Formula>,
}
2020-02-02 02:14:14 +01:00
impl IfAndOnlyIf
{
pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
{
Self
{
left,
right,
}
}
}
2020-01-24 18:43:42 +01:00
pub struct Implies
{
2020-01-24 18:43:42 +01:00
pub antecedent: Box<Formula>,
pub implication: Box<Formula>,
}
2020-02-02 02:14:14 +01:00
impl Implies
{
pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
{
Self
{
antecedent,
implication,
}
}
}
2020-01-24 18:43:42 +01:00
pub struct Predicate
{
2020-01-24 18:43:42 +01:00
pub declaration: std::rc::Rc<PredicateDeclaration>,
pub arguments: Vec<Box<Term>>,
}
2020-02-02 02:14:14 +01:00
impl Predicate
{
pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
{
Self
{
declaration: std::rc::Rc::clone(declaration),
arguments,
}
}
}
2020-01-24 18:43:42 +01:00
// Variants
pub enum Term
{
2020-01-24 18:43:42 +01:00
BinaryOperation(BinaryOperation),
Boolean(bool),
Function(Function),
Integer(i32),
SpecialInteger(SpecialInteger),
String(String),
2020-01-24 18:43:42 +01:00
Symbolic(String),
UnaryOperation(UnaryOperation),
Variable(Variable),
}
2020-01-24 18:43:42 +01:00
pub type Terms = Vec<Box<Term>>;
2020-02-02 02:14:14 +01:00
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))
}
}
2020-01-24 18:43:42 +01:00
pub enum Formula
{
And(Formulas),
Boolean(bool),
2020-02-02 02:08:39 +01:00
Compare(Compare),
2020-01-24 18:43:42 +01:00
Exists(Exists),
ForAll(ForAll),
2020-02-02 02:08:39 +01:00
IfAndOnlyIf(IfAndOnlyIf),
2020-01-24 18:43:42 +01:00
Implies(Implies),
Not(Box<Formula>),
Or(Formulas),
Predicate(Predicate),
}
pub type Formulas = Vec<Box<Formula>>;
2020-02-02 02:14:14 +01:00
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: 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: 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)
}
}