Persist declarations between rules

src/main.rs

@@ -1,36 +1,3 @@
-struct StatementHandler;
-
-impl clingo::StatementHandler for StatementHandler
-{
-	fn on_statement(&mut self, statement: &clingo::ast::Statement) -> bool
-	{
-		match statement.statement_type()
-		{
-			clingo::ast::StatementType::Rule(ref rule) =>
-			{
-				if let Err(error) = anthem::translate::verify_properties::read(rule)
-				{
-					log::error!("could not translate input program: {}", error);
-					return false;
-				}
-			},
-			_ => log::debug!("read statement (other kind)"),
-		}
-
-		true
-	}
-}
-
-struct Logger;
-
-impl clingo::Logger for Logger
-{
-	fn log(&mut self, code: clingo::Warning, message: &str)
-	{
-		log::warn!("clingo warning ({:?}): {}", code, message);
-	}
-}
-
 fn main()
 {
 	pretty_env_logger::init();
@@ -45,15 +12,5 @@ fn main()
 		},
 	};
 
-	let mut statement_handler = StatementHandler{};
+	std::process::exit(anthem::translate::verify_properties::translate(&program));
-
-	match clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)
-	{
-		Ok(()) => (),
-		Err(error) =>
-		{
-			log::error!("could not translate input program: {}", error);
-			std::process::exit(1);
-		},
-	}
 }

src/translate/verify_properties.rs

@@ -4,28 +4,106 @@ mod translate_body;
 use head_type::*;
 use translate_body::*;
 
-pub struct ScopedFormula
+struct ScopedFormula
 {
 	free_variable_declarations: foliage::VariableDeclarations,
 	formula: foliage::Formula,
 }
 
-pub struct Definitions
+struct Definitions
 {
 	head_atom_parameters: std::rc::Rc<foliage::VariableDeclarations>,
 	definitions: Vec<ScopedFormula>,
 }
 
-pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
+struct Context
+{
+	pub function_declarations: foliage::FunctionDeclarations,
+	pub predicate_declarations: foliage::PredicateDeclarations,
+	pub variable_declaration_stack: foliage::VariableDeclarationStack,
+}
+
+impl Context
+{
+	fn new() -> Self
+	{
+		Self
+		{
+			function_declarations: foliage::FunctionDeclarations::new(),
+			predicate_declarations: foliage::PredicateDeclarations::new(),
+			variable_declaration_stack: foliage::VariableDeclarationStack::new(),
+		}
+	}
+}
+
+struct StatementHandler
+{
+	context: Context,
+}
+
+impl StatementHandler
+{
+	fn new() -> Self
+	{
+		Self
+		{
+			context: Context::new(),
+		}
+	}
+}
+
+impl clingo::StatementHandler for StatementHandler
+{
+	fn on_statement(&mut self, statement: &clingo::ast::Statement) -> bool
+	{
+		match statement.statement_type()
+		{
+			clingo::ast::StatementType::Rule(ref rule) =>
+			{
+				if let Err(error) = read_rule(rule, &mut self.context)
+				{
+					log::error!("could not translate input program: {}", error);
+					return false;
+				}
+			},
+			_ => log::debug!("read statement (other kind)"),
+		}
+
+		true
+	}
+}
+
+struct Logger;
+
+impl clingo::Logger for Logger
+{
+	fn log(&mut self, code: clingo::Warning, message: &str)
+	{
+		log::warn!("clingo warning ({:?}): {}", code, message);
+	}
+}
+
+pub fn translate(program: &str) -> i32
+{
+	let mut statement_handler = StatementHandler::new();
+
+	match clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)
+	{
+		Ok(()) => 0,
+		Err(error) =>
+		{
+			log::error!("could not translate input program: {}", error);
+			1
+		},
+	}
+}
+
+fn read_rule(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crate::Error>
 {
 	use super::common::FindOrCreatePredicateDeclaration;
 
-	let mut function_declarations = foliage::FunctionDeclarations::new();
-	let mut predicate_declarations = foliage::PredicateDeclarations::new();
-	let mut variable_declaration_stack = foliage::VariableDeclarationStack::new();
-
 	let head_type = determine_head_type(rule.head(),
-		|name, arity| predicate_declarations.find_or_create(name, arity))?;
+		|name, arity| context.predicate_declarations.find_or_create(name, arity))?;
 
 	let mut definitions
 		= std::collections::BTreeMap::<std::rc::Rc<foliage::PredicateDeclaration>, Definitions>::new();
@@ -53,10 +131,12 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
 
 			let definitions = definitions.get_mut(&head_atom.predicate_declaration).unwrap();
 
-			variable_declaration_stack.push(std::rc::Rc::clone(&definitions.head_atom_parameters));
+			context.variable_declaration_stack.push(std::rc::Rc::clone(
+				&definitions.head_atom_parameters));
 
-			let mut definition_arguments = translate_body(rule.body(), &mut function_declarations,
+			let mut definition_arguments = translate_body(rule.body(),
-				&mut predicate_declarations, &mut variable_declaration_stack)?;
+				&mut context.function_declarations, &mut context.predicate_declarations,
+				&mut context.variable_declaration_stack)?;
 
 			assert_eq!(definitions.head_atom_parameters.len(), head_atom.arguments.len());
 
@@ -67,30 +147,35 @@ pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
 				let head_atom_argument = head_atom_arguments_iterator.next().unwrap();
 
 				let translated_head_term = crate::translate::common::choose_value_in_term(
-					head_atom_argument, head_atom_parameter, &mut function_declarations,
+					head_atom_argument, head_atom_parameter, &mut context.function_declarations,
-					&mut variable_declaration_stack)?;
+					&mut context.variable_declaration_stack)?;
 
 				definition_arguments.push(Box::new(translated_head_term));
 			}
 
-			variable_declaration_stack.pop();
+			context.variable_declaration_stack.pop();
+
+			let mut free_variable_declarations = vec![];
+
+			std::mem::swap(&mut context.variable_declaration_stack.free_variable_declarations,
+				&mut free_variable_declarations);
 
 			let definition = foliage::Formula::And(definition_arguments);
 
 			let definition = ScopedFormula
 			{
-				free_variable_declarations: variable_declaration_stack.free_variable_declarations,
+				free_variable_declarations,
 				formula: definition,
 			};
 
-			log::trace!("translated formula: {:?}", definition.formula);
+			log::trace!("translated rule with single atom in head: {:?}", definition.formula);
 
 			definitions.definitions.push(definition);
 		},
 		HeadType::ChoiceWithSingleAtom(_) =>
 			log::debug!("translating choice rule with single atom"),
 		HeadType::IntegrityConstraint =>
-			log::debug!("translating integrity constraint"),
+			log::debug!("translated integrity constraint"),
 		HeadType::Trivial => log::debug!("skipping trivial rule"),
 	}