Refactor variable declaration stack usage

Cargo.toml

@@ -5,7 +5,7 @@ authors = ["Patrick Lühne <patrick@luehne.de>"]
 edition = "2018"
 
 [dependencies]
-foliage = {git = "https://github.com/pluehne/foliage", branch = "master"}
+foliage = {git = "https://github.com/pluehne/foliage", branch = "parser"}
 log = "0.4"
 pretty_env_logger = "0.4"
 structopt = "0.3"

src/traits.rs

@@ -33,9 +33,3 @@ pub(crate) trait GetOrCreatePredicateDeclaration
 	fn get_or_create_predicate_declaration(&self, name: &str, arity: usize)
 		-> std::rc::Rc<foliage::PredicateDeclaration>;
 }
-
-pub(crate) trait GetOrCreateVariableDeclaration
-{
-	fn get_or_create_variable_declaration(&self, name: &str)
-		-> std::rc::Rc<foliage::VariableDeclaration>;
-}

src/translate/common/choose_value_in_term.rs

@@ -8,11 +8,11 @@ pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
 }
 
 pub(crate) fn choose_value_in_term<C>(term: &clingo::ast::Term,
-	variable_declaration: std::rc::Rc<foliage::VariableDeclaration>, context: &C)
+	variable_declaration: std::rc::Rc<foliage::VariableDeclaration>, context: &C,
+	variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
 	-> Result<foliage::Formula, crate::Error>
 where
 	C: crate::traits::GetOrCreateFunctionDeclaration
-		+ crate::traits::GetOrCreateVariableDeclaration
 		+ crate::traits::AssignVariableDeclarationDomain
 {
 	match term.term_type()
@@ -58,8 +58,23 @@ where
 		},
 		clingo::ast::TermType::Variable(variable_name) =>
 		{
-			let other_variable_declaration = context.get_or_create_variable_declaration(
+			let other_variable_declaration = match variable_name
-				variable_name);
+			{
+				// TODO: check
+				// Every occurrence of anonymous variables is treated as if it introduced a fresh
+				// variable declaration
+				"_" => variable_declaration_stack.free_variable_declarations_do_mut(
+					|free_variable_declarations|
+					{
+						let variable_declaration = std::rc::Rc::new(
+							foliage::VariableDeclaration::new("_".to_owned()));
+
+						free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
+
+						variable_declaration
+					}),
+				_ => variable_declaration_stack.find_or_create(variable_name),
+			};
 			context.assign_variable_declaration_domain(&other_variable_declaration,
 				crate::Domain::Program);
 			let other_variable = foliage::Term::variable(other_variable_declaration);
@@ -100,10 +115,12 @@ where
 						Box::new(translated_binary_operation));
 
 					let choose_value_from_left_argument = choose_value_in_term(
-						binary_operation.left(), std::rc::Rc::clone(&parameter_1), context)?;
+						binary_operation.left(), std::rc::Rc::clone(&parameter_1), context,
+						variable_declaration_stack)?;
 
 					let choose_value_from_right_argument = choose_value_in_term(
-						binary_operation.right(), std::rc::Rc::clone(&parameter_2), context)?;
+						binary_operation.right(), std::rc::Rc::clone(&parameter_2), context,
+							variable_declaration_stack)?;
 
 					let and = foliage::Formula::And(vec![equals, choose_value_from_left_argument,
 						choose_value_from_right_argument]);
@@ -142,10 +159,10 @@ where
 						Box::new(j_times_q_plus_r));
 
 					let choose_i_in_t1 = choose_value_in_term(binary_operation.left(),
-						std::rc::Rc::clone(parameter_i), context)?;
+						std::rc::Rc::clone(parameter_i), context, variable_declaration_stack)?;
 
 					let choose_i_in_t2 = choose_value_in_term(binary_operation.left(),
-						std::rc::Rc::clone(parameter_j), context)?;
+						std::rc::Rc::clone(parameter_j), context, variable_declaration_stack)?;
 
 					let j_not_equal_to_0 = foliage::Formula::not_equal(
 						Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_j))),
@@ -205,7 +222,8 @@ where
 						Box::new(negative_z_prime));
 
 					let choose_z_prime_in_t_prime = choose_value_in_term(unary_operation.argument(),
-						std::rc::Rc::clone(&parameter_z_prime), context)?;
+						std::rc::Rc::clone(&parameter_z_prime), context,
+						variable_declaration_stack)?;
 
 					let and = foliage::Formula::and(vec![equals, choose_z_prime_in_t_prime]);
 
@@ -234,10 +252,10 @@ where
 			let parameter_k = &parameters[2];
 
 			let choose_i_in_t_1 = choose_value_in_term(interval.left(),
-				std::rc::Rc::clone(parameter_i), context)?;
+				std::rc::Rc::clone(parameter_i), context, variable_declaration_stack)?;
 
 			let choose_j_in_t_2 = choose_value_in_term(interval.right(),
-				std::rc::Rc::clone(parameter_j), context)?;
+				std::rc::Rc::clone(parameter_j), context, variable_declaration_stack)?;
 
 			let i_less_than_or_equal_to_k = foliage::Formula::less_or_equal(
 				Box::new(foliage::Term::variable(std::rc::Rc::clone(parameter_i))),

src/translate/verify_properties.rs

@@ -333,11 +333,6 @@ 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
@@ -371,10 +366,14 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 			let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap();
 
 			let head_atom_parameters = std::rc::Rc::clone(&definitions.head_atom_parameters);
-			let variable_declaration_stack_guard = foliage::VariableDeclarationStack::push(
+			let free_variable_declarations = std::cell::RefCell::new(vec![]);
-				&context.variable_declaration_stack, head_atom_parameters);
+			let free_layer =
+				foliage::VariableDeclarationStackLayer::Free(free_variable_declarations);
+			let head_atom_parameters_layer = foliage::VariableDeclarationStackLayer::bound(
+				&free_layer, head_atom_parameters);
 
-			let mut definition_arguments = translate_body(rule.body(), context)?;
+			let mut definition_arguments = translate_body(rule.body(), context,
+				&head_atom_parameters_layer)?;
 
 			assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len());
 
@@ -397,16 +396,19 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 				let head_atom_argument = head_atom_arguments_iterator.next().unwrap();
 
 				let translated_head_term = crate::translate::common::choose_value_in_term(
-					head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context)?;
+					head_atom_argument, std::rc::Rc::clone(head_atom_parameter), context,
+					&head_atom_parameters_layer)?;
 
 				definition_arguments.push(translated_head_term);
 			}
 
-			drop(variable_declaration_stack_guard);
+			// TODO: refactor
-
+			let free_variable_declarations = match free_layer
-			let free_variable_declarations = std::mem::replace(
+			{
-				&mut context.variable_declaration_stack.borrow_mut().free_variable_declarations,
+				foliage::VariableDeclarationStackLayer::Free(free_variable_declarations)
-				vec![]);
+					=> free_variable_declarations.into_inner(),
+				_ => unreachable!(),
+			};
 
 			let definition = match definition_arguments.len()
 			{
@@ -428,11 +430,19 @@ fn read_rule(rule: &clingo::ast::Rule, context: &Context) -> Result<(), crate::E
 		},
 		HeadType::IntegrityConstraint =>
 		{
-			let mut arguments = translate_body(rule.body(), context)?;
+			let free_variable_declarations = std::cell::RefCell::new(vec![]);
+			let free_layer =
+				foliage::VariableDeclarationStackLayer::Free(free_variable_declarations);
 
-			let free_variable_declarations = std::mem::replace(
+			let mut arguments = translate_body(rule.body(), context, &free_layer)?;
-				&mut context.variable_declaration_stack.borrow_mut().free_variable_declarations,
+
-				vec![]);
+			// TODO: refactor
+			let free_variable_declarations = match free_layer
+			{
+				foliage::VariableDeclarationStackLayer::Free(free_variable_declarations)
+					=> free_variable_declarations.into_inner(),
+				_ => unreachable!(),
+			};
 
 			let formula = match arguments.len()
 			{

src/translate/verify_properties/context.rs

@@ -22,7 +22,6 @@ 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_domains: std::cell::RefCell<VariableDeclarationDomains>,
 	pub program_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
 	pub integer_variable_declaration_ids: std::cell::RefCell<VariableDeclarationIDs>,
@@ -44,8 +43,6 @@ 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()),
 			variable_declaration_domains:
 				std::cell::RefCell::new(VariableDeclarationDomains::new()),
 			program_variable_declaration_ids:
@@ -121,29 +118,6 @@ impl crate::traits::GetOrCreatePredicateDeclaration for Context
 	}
 }
 
-impl crate::traits::GetOrCreateVariableDeclaration for Context
-{
-	fn get_or_create_variable_declaration(&self, name: &str)
-		-> std::rc::Rc<foliage::VariableDeclaration>
-	{
-		let mut variable_declaration_stack = self.variable_declaration_stack.borrow_mut();
-
-		// TODO: check correctness
-		if name == "_"
-		{
-			let variable_declaration = std::rc::Rc::new(foliage::VariableDeclaration::new(
-				"_".to_owned()));
-
-			variable_declaration_stack.free_variable_declarations.push(
-				std::rc::Rc::clone(&variable_declaration));
-
-			return variable_declaration;
-		}
-
-		variable_declaration_stack.find_or_create(name)
-	}
-}
-
 impl crate::traits::AssignVariableDeclarationDomain for Context
 {
 	fn assign_variable_declaration_domain(&self,

src/translate/verify_properties/translate_body.rs

@@ -1,9 +1,8 @@
 pub(crate) fn translate_body_term<C>(body_term: &clingo::ast::Term, sign: clingo::ast::Sign,
-	context: &C)
+	context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
 	-> Result<foliage::Formula, crate::Error>
 where
-	C: crate::traits::GetOrCreateVariableDeclaration
+	C: crate::traits::GetOrCreateFunctionDeclaration
-		+ crate::traits::GetOrCreateFunctionDeclaration
 		+ crate::traits::GetOrCreatePredicateDeclaration
 		+ crate::traits::AssignVariableDeclarationDomain
 {
@@ -54,7 +53,8 @@ where
 	let mut parameters_iterator = parameters.iter();
 	let mut arguments = function.arguments().iter().map(
 		|x| crate::translate::common::choose_value_in_term(x,
-			std::rc::Rc::clone(&parameters_iterator.next().unwrap()), context))
+			std::rc::Rc::clone(&parameters_iterator.next().unwrap()), context,
+			variable_declaration_stack))
 		.collect::<Result<Vec<_>, _>>()?;
 
 	arguments.push(predicate_literal);
@@ -65,11 +65,10 @@ where
 }
 
 pub(crate) fn translate_body_literal<C>(body_literal: &clingo::ast::BodyLiteral,
-	context: &C)
+	context: &C, variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
 	-> Result<foliage::Formula, crate::Error>
 where
-	C: crate::traits::GetOrCreateVariableDeclaration
+	C: crate::traits::GetOrCreateFunctionDeclaration
-		+ crate::traits::GetOrCreateFunctionDeclaration
 		+ crate::traits::GetOrCreatePredicateDeclaration
 		+ crate::traits::AssignVariableDeclarationDomain
 {
@@ -100,7 +99,7 @@ where
 			Ok(foliage::Formula::Boolean(value))
 		},
 		clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(),
-			context),
+			context, variable_declaration_stack),
 		clingo::ast::LiteralType::Comparison(comparison) =>
 		{
 			let parameters = (0..2).map(|_|
@@ -119,9 +118,9 @@ where
 			let parameter_z2 = &parameters_iterator.next().unwrap();
 
 			let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(),
-				std::rc::Rc::clone(parameter_z1), context)?;
+				std::rc::Rc::clone(parameter_z1), context, variable_declaration_stack)?;
 			let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(),
-				std::rc::Rc::clone(parameter_z2), context)?;
+				std::rc::Rc::clone(parameter_z2), context, variable_declaration_stack)?;
 
 			let variable_1 = foliage::Term::variable(std::rc::Rc::clone(parameter_z1));
 			let variable_2 = foliage::Term::variable(std::rc::Rc::clone(parameter_z2));
@@ -142,16 +141,16 @@ where
 	}
 }
 
-pub(crate) fn translate_body<C>(body_literals: &[clingo::ast::BodyLiteral],
+pub(crate) fn translate_body<C>(body_literals: &[clingo::ast::BodyLiteral], context: &C,
-	context: &C)
+	variable_declaration_stack: &foliage::VariableDeclarationStackLayer)
 	-> Result<foliage::Formulas, crate::Error>
 where
-	C: crate::traits::GetOrCreateVariableDeclaration
+	C: crate::traits::GetOrCreateFunctionDeclaration
-		+ crate::traits::GetOrCreateFunctionDeclaration
 		+ crate::traits::GetOrCreatePredicateDeclaration
 		+ crate::traits::AssignVariableDeclarationDomain
 {
 	body_literals.iter()
-		.map(|body_literal| translate_body_literal(body_literal, context))
+		.map(|body_literal| translate_body_literal(body_literal, context,
+			variable_declaration_stack))
 		.collect::<Result<foliage::Formulas, crate::Error>>()
 }