Check variable declaration stack before using it

src/ast.rs

@@ -1,156 +0,0 @@
-// Operators
-
-pub enum BinaryOperator
-{
-	Plus,
-	Minus,
-	Multiplication,
-	Division,
-	Modulo,
-	Power,
-}
-
-pub enum ComparisonOperator
-{
-	GreaterThan,
-	LessThan,
-	LessEqual,
-	GreaterEqual,
-	NotEqual,
-	Equal,
-}
-
-pub enum UnaryOperator
-{
-	AbsoluteValue,
-	Minus,
-}
-
-// Primitives
-
-pub struct FunctionDeclaration
-{
-	pub name: String,
-	pub arity: usize,
-}
-
-pub struct PredicateDeclaration
-{
-	pub name: String,
-	pub arity: usize,
-}
-
-pub struct VariableDeclaration
-{
-	pub name: String,
-}
-
-// 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 struct Interval
-{
-	pub from: Box<Term>,
-	pub to: 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
-{
-	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
-	pub argument: Box<Formula>,
-}
-
-pub struct ForAll
-{
-	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
-	pub argument: Box<Formula>,
-}
-
-pub struct Implies
-{
-	pub left: Box<Formula>,
-	pub right: Box<Formula>,
-}
-
-pub struct Predicate
-{
-	pub declaration: std::rc::Rc<PredicateDeclaration>,
-	pub arguments: Vec<Box<Term>>,
-}
-
-// Variants
-
-pub enum Term
-{
-	BinaryOperation(BinaryOperation),
-	Boolean(bool),
-	Function(Function),
-	Integer(i32),
-	Interval(Interval),
-	SpecialInteger(SpecialInteger),
-	String(String),
-	UnaryOperation(UnaryOperation),
-	Variable(Variable),
-}
-
-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>>;

src/translate/verify_properties.rs

@@ -333,6 +333,11 @@ where
 
 fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::Error>
 {
+	if !context.variable_declaration_stack.borrow().is_empty()
+	{
+		return Err(crate::Error::new_logic("variable declaration stack in unexpected state"));
+	}
+
 	let head_type = determine_head_type(rule.head(), context)?;
 
 	match &head_type
@@ -396,7 +401,7 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 				definition_arguments.push(Box::new(translated_head_term));
 			}
 
-			context.variable_declaration_stack.borrow_mut().pop();
+			context.variable_declaration_stack.borrow_mut().pop()?;
 
 			let free_variable_declarations = std::mem::replace(
 				&mut context.variable_declaration_stack.borrow_mut().free_variable_declarations,

src/utils/variable_declaration_stack.rs

@@ -51,14 +51,20 @@ impl VariableDeclarationStack
 		variable_declaration
 	}
 
+	pub fn is_empty(&self) -> bool
+	{
+		self.free_variable_declarations.is_empty()
+			&& self.bound_variable_declaration_stack.is_empty()
+	}
+
 	pub fn push(&mut self, bound_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>)
 	{
 		self.bound_variable_declaration_stack.push(bound_variable_declarations);
 	}
 
-	pub fn pop(&mut self)
+	pub fn pop(&mut self) -> Result<(), crate::Error>
 	{
-		// TODO: return error instead
+		self.bound_variable_declaration_stack.pop().map(|_| ())
-		self.bound_variable_declaration_stack.pop().expect("bound variable is empty, cannot pop last element");
+			.ok_or(crate::Error::new_logic("variable stack not in expected state"))
 	}
 }