Move variable declaration stack from foliage crate

src/translate/verify_properties/context.rs

@@ -24,7 +24,7 @@ pub(crate) struct Context
 
 	pub function_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
 	pub predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
-	pub variable_declaration_stack: std::cell::RefCell<foliage::VariableDeclarationStack>,
+	pub variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
 	pub variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>,
 	pub variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
 }
@@ -46,7 +46,7 @@ impl Context
 			function_declarations: std::cell::RefCell::new(foliage::FunctionDeclarations::new()),
 			predicate_declarations: std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
 			variable_declaration_stack:
-				std::cell::RefCell::new(foliage::VariableDeclarationStack::new()),
+				std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
 			variable_declaration_domains:
 				std::cell::RefCell::new(VariableDeclarationDomains::new()),
 			variable_declaration_ids: std::cell::RefCell::new(VariableDeclarationIDs::new()),

src/utils.rs

@@ -1,6 +1,8 @@
 mod arithmetic_terms;
+mod variable_declaration_stack;
 
 pub(crate) use arithmetic_terms::*;
+pub(crate) use variable_declaration_stack::*;
 
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
 pub(crate) enum OperatorNotation

src/utils/variable_declaration_stack.rs

@@ -0,0 +1,64 @@
+pub(crate) struct VariableDeclarationStack
+{
+	pub free_variable_declarations: foliage::VariableDeclarations,
+	bound_variable_declaration_stack: Vec<std::rc::Rc<foliage::VariableDeclarations>>,
+}
+
+impl VariableDeclarationStack
+{
+	pub fn new() -> Self
+	{
+		Self
+		{
+			free_variable_declarations: foliage::VariableDeclarations::new(),
+			bound_variable_declaration_stack: vec![],
+		}
+	}
+
+	pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<foliage::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<foliage::VariableDeclaration>
+	{
+		if let Some(variable_declaration) = self.find(variable_name)
+		{
+			return variable_declaration;
+		}
+
+		let variable_declaration = foliage::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));
+
+		variable_declaration
+	}
+
+	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)
+	{
+		// TODO: return error instead
+		self.bound_variable_declaration_stack.pop().expect("bound variable is empty, cannot pop last element");
+	}
+}