foliage-rs/src/ast.rs

564 lines
9.5 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-01-24 18:43:42 +01:00
pub struct VariableDeclaration
{
2020-01-24 18:43:42 +01:00
pub name: String,
}
impl std::cmp::PartialEq for VariableDeclaration
{
#[inline(always)]
fn eq(&self, other: &VariableDeclaration) -> bool
{
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
l.eq(&r)
}
}
impl std::cmp::Eq for VariableDeclaration
{
}
impl std::cmp::PartialOrd for VariableDeclaration
{
#[inline(always)]
fn partial_cmp(&self, other: &VariableDeclaration) -> Option<std::cmp::Ordering>
{
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
l.partial_cmp(&r)
}
}
impl std::cmp::Ord for VariableDeclaration
{
#[inline(always)]
fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering
{
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
l.cmp(&r)
}
}
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
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
{
assert_eq!(declaration.arity, arguments.len(),
"function has a different number of arguments then declared");
2020-02-02 02:14:14 +01:00
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: std::rc::Rc<VariableDeclarations>,
pub argument: Box<Formula>,
}
2020-02-02 02:14:14 +01:00
impl Exists
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
2020-02-02 02:14:14 +01:00
{
Self
{
parameters,
argument,
}
}
}
pub struct ForAll
{
pub parameters: std::rc::Rc<VariableDeclarations>,
pub argument: Box<Formula>,
}
2020-02-02 02:14:14 +01:00
impl ForAll
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
2020-02-02 02:14:14 +01:00
{
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
{
assert_eq!(declaration.arity, arguments.len(),
"predicate has a different number of arguments then declared");
2020-02-02 02:14:14 +01:00
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
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 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
{
assert!(!arguments.is_empty());
2020-02-02 02:14:14 +01:00
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
2020-02-02 02:14:14 +01:00
{
2020-02-02 20:06:41 +01:00
assert!(!parameters.is_empty());
2020-02-02 02:14:14 +01:00
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
2020-02-02 02:14:14 +01:00
{
2020-02-02 20:06:41 +01:00
assert!(!parameters.is_empty());
2020-02-02 02:14:14 +01:00
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
{
assert!(!arguments.is_empty());
2020-02-02 02:14:14 +01:00
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)
}
}