From 26c1bde49b6a4941c00a1e41feec94ff9c6f737c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Wed, 5 Feb 2020 02:29:38 +0100
Subject: [PATCH] Move variable declaration stack from foliage crate

---
 src/translate/verify_properties/context.rs |  4 +-
 src/utils.rs                               |  2 +
 src/utils/variable_declaration_stack.rs    | 64 ++++++++++++++++++++++
 3 files changed, 68 insertions(+), 2 deletions(-)
 create mode 100644 src/utils/variable_declaration_stack.rs

diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs
index 31f43ae..9db2c6f 100644
--- a/src/translate/verify_properties/context.rs
+++ b/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()),
diff --git a/src/utils.rs b/src/utils.rs
index 3794f85..176626c 100644
--- a/src/utils.rs
+++ b/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
diff --git a/src/utils/variable_declaration_stack.rs b/src/utils/variable_declaration_stack.rs
new file mode 100644
index 0000000..a17f8c4
--- /dev/null
+++ b/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");
+	}
+}