foliage-rs/src/ast.rs

212 lines
3.7 KiB
Rust
Raw Normal View History

2020-01-24 18:43:42 +01:00
// Operators
pub enum BinaryOperator
{
Addition,
Subtraction,
Multiplication,
Division,
Modulo,
Exponentiation,
}
pub enum ComparisonOperator
{
Greater,
Less,
LessOrEqual,
GreaterOrEqual,
NotEqual,
Equal,
}
pub enum UnaryOperator
{
AbsoluteValue,
Negation,
}
// Primitives
2020-01-31 13:52:57 +01:00
#[derive(Eq, Hash, PartialEq)]
2020-01-24 18:43:42 +01:00
pub struct FunctionDeclaration
{
pub name: String,
pub arity: usize,
}
2020-01-31 13:52:57 +01:00
#[derive(Eq, Hash, PartialEq)]
pub struct PredicateDeclaration
{
pub name: String,
pub arity: usize,
}
2020-01-24 18:56:03 +01:00
#[derive(Eq, Hash, PartialEq)]
2020-01-24 18:43:42 +01:00
pub struct VariableDeclaration
{
2020-01-24 18:43:42 +01:00
pub name: String,
}
2020-01-24 18:56:03 +01:00
pub type VariableDeclarations = std::collections::HashSet<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 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.insert(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");
}
}
2020-01-24 18:43:42 +01:00
// Terms
pub struct BinaryOperation
{
pub operator: BinaryOperator,
pub left: Box<Term>,
pub right: Box<Term>,
}
pub struct Function
{
pub declaration: std::rc::Rc<FunctionDeclaration>,
pub arguments: Vec<Box<Term>>,
}
pub enum SpecialInteger
{
Infimum,
Supremum,
}
pub struct UnaryOperation
{
pub operator: UnaryOperator,
pub argument: Box<Term>,
}
pub struct Variable
{
pub declaration: std::rc::Rc<VariableDeclaration>,
}
// Formulas
pub struct Biconditional
{
pub left: Box<Formula>,
pub right: Box<Formula>,
}
pub struct Comparison
{
pub operator: ComparisonOperator,
pub left: Box<Term>,
pub right: Box<Term>,
}
pub struct Exists
{
2020-01-24 18:43:42 +01:00
pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
pub argument: Box<Formula>,
}
pub struct ForAll
{
2020-01-24 18:43:42 +01:00
pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
pub argument: Box<Formula>,
}
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-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-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>>;
pub enum Formula
{
And(Formulas),
Biconditional(Biconditional),
Boolean(bool),
Comparison(Comparison),
Exists(Exists),
ForAll(ForAll),
Implies(Implies),
Not(Box<Formula>),
Or(Formulas),
Predicate(Predicate),
}
pub type Formulas = Vec<Box<Formula>>;