Refactoring to drop Context type

src/lib.rs

@@ -1,3 +1,5 @@
+#![feature(trait_alias)]
+
 pub mod error;
 pub mod translate;
 

src/main.rs

@@ -1,9 +1,6 @@
-struct StatementHandler<'context>
-{
-	context: &'context mut anthem::translate::verify_properties::Context,
-}
+struct StatementHandler;
 
-impl clingo::StatementHandler for StatementHandler<'_>
+impl clingo::StatementHandler for StatementHandler
 {
 	fn on_statement(&mut self, statement: &clingo::ast::Statement) -> bool
 	{
@@ -11,7 +8,7 @@ impl clingo::StatementHandler for StatementHandler<'_>
 		{
 			clingo::ast::StatementType::Rule(ref rule) =>
 			{
-				if let Err(error) = anthem::translate::verify_properties::read(rule, self.context)
+				if let Err(error) = anthem::translate::verify_properties::read(rule)
 				{
 					log::error!("could not translate input program: {}", error);
 					return false;
@@ -47,11 +44,8 @@ fn main()
 			std::process::exit(1);
 		},
 	};
-	let mut context = anthem::translate::verify_properties::Context::new();
-	let mut statement_handler = StatementHandler
-	{
-		context: &mut context
-	};
+
+	let mut statement_handler = StatementHandler{};
 
 	match clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)
 	{

src/translate/common.rs

@@ -1,4 +1,65 @@
-pub fn translate_comparison_operator(comparison_operator: clingo::ast::ComparisonOperator)
+pub(crate) trait FindOrCreateFunctionDeclaration = FnMut(&str, usize)
+	-> std::rc::Rc<foliage::FunctionDeclaration>;
+
+pub(crate) trait FindOrCreatePredicateDeclaration = FnMut(&str, usize)
+	-> std::rc::Rc<foliage::PredicateDeclaration>;
+
+pub(crate) trait FindOrCreateVariableDeclaration = FnMut(&str)
+	-> std::rc::Rc<foliage::VariableDeclaration>;
+
+pub(crate) fn find_or_create_predicate_declaration(predicate_declarations: &mut foliage::PredicateDeclarations,
+	name: &str, arity: usize)
+	-> std::rc::Rc<foliage::PredicateDeclaration>
+{
+	match predicate_declarations.iter()
+		.find(|x| x.name == name && x.arity == arity)
+	{
+		Some(value) => std::rc::Rc::clone(value),
+		None =>
+		{
+			let declaration = foliage::PredicateDeclaration
+			{
+				name: name.to_owned(),
+				arity,
+			};
+			let declaration = std::rc::Rc::new(declaration);
+
+			predicate_declarations.insert(std::rc::Rc::clone(&declaration));
+
+			log::debug!("new predicate declaration: {}/{}", name, arity);
+
+			declaration
+		},
+	}
+}
+
+pub(crate) fn find_or_create_function_declaration(function_declarations: &mut foliage::FunctionDeclarations,
+	name: &str, arity: usize)
+	-> std::rc::Rc<foliage::FunctionDeclaration>
+{
+	match function_declarations.iter()
+		.find(|x| x.name == name && x.arity == arity)
+	{
+		Some(value) => std::rc::Rc::clone(value),
+		None =>
+		{
+			let declaration = foliage::FunctionDeclaration
+			{
+				name: name.to_owned(),
+				arity,
+			};
+			let declaration = std::rc::Rc::new(declaration);
+
+			function_declarations.insert(std::rc::Rc::clone(&declaration));
+
+			log::debug!("new function declaration: {}/{}", name, arity);
+
+			declaration
+		},
+	}
+}
+
+pub(crate) fn translate_comparison_operator(comparison_operator: clingo::ast::ComparisonOperator)
 	-> foliage::ComparisonOperator
 {
 	match comparison_operator
@@ -18,7 +79,7 @@ pub fn translate_comparison_operator(comparison_operator: clingo::ast::Compariso
 	}
 }
 
-pub fn choose_value_in_primitive(term: Box<foliage::Term>,
+pub(crate) fn choose_value_in_primitive(term: Box<foliage::Term>,
 	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
 	-> foliage::Comparison
 {
@@ -35,12 +96,13 @@ pub fn choose_value_in_primitive(term: Box<foliage::Term>,
 	}
 }
 
-pub fn choose_value_in_term<F>(term: &clingo::ast::Term,
+pub(crate) fn choose_value_in_term<F1, F2>(term: &clingo::ast::Term,
 	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>,
-	mut find_or_create_function_declaration: F)
+	mut find_or_create_function_declaration: F1, mut find_or_create_variable_declaration: F2)
 	-> Result<foliage::Formula, crate::Error>
 where
-	F: FnMut(&str, usize) -> std::rc::Rc<foliage::FunctionDeclaration>
+	F1: FindOrCreateFunctionDeclaration,
+	F2: FindOrCreateVariableDeclaration,
 {
 	match term.term_type()
 	{
@@ -88,6 +150,8 @@ where
 				Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(function), variable_declaration)))
 			}
 		},
-		_ => Ok(foliage::Formula::Boolean(false))
+		clingo::ast::TermType::Variable(variable) =>
+			Err(crate::Error::new_not_yet_implemented("todo")),
+		_ => Err(crate::Error::new_not_yet_implemented("todo")),
 	}
 }

src/translate/verify_properties.rs

@@ -1,21 +1,60 @@
-mod context;
 mod head_type;
 mod translate_body;
 
-pub use context::Context;
-
 use head_type::*;
 use translate_body::*;
 
-pub fn read(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crate::Error>
+pub struct ScopedFormula
 {
-	let translated_body = translate_body(rule.body(), context)?;
+	free_variable_declarations: foliage::VariableDeclarations,
+	formula: foliage::Formula,
+}
+
+pub struct Definitions
+{
+	head_atom_parameters: foliage::VariableDeclarations,
+	definitions: Vec<ScopedFormula>,
+}
+
+pub fn read(rule: &clingo::ast::Rule) -> Result<(), crate::Error>
+{
+	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| context.find_or_create_predicate_declaration(name, arity))?;
+		|name, arity| super::common::find_or_create_predicate_declaration(
+			&mut predicate_declarations, name, arity))?;
+
+	let mut definitions
+		= std::collections::BTreeMap::<std::rc::Rc<foliage::PredicateDeclaration>, Definitions>::new();
+
+	let declare_predicate_parameters = |predicate_declaration: &foliage::PredicateDeclaration|
+	{
+		(0..predicate_declaration.arity)
+			.map(|_| std::rc::Rc::new(foliage::VariableDeclaration
+				{
+					name: "<anonymous>".to_string(),
+				}))
+			.collect()
+	};
 
 	match head_type
 	{
+		HeadType::SingleAtom(head_atom) =>
+		{
+			if !definitions.contains_key(&head_atom.predicate_declaration)
+			{
+				definitions.insert(std::rc::Rc::clone(&head_atom.predicate_declaration),
+					Definitions
+					{
+						head_atom_parameters: declare_predicate_parameters(&head_atom.predicate_declaration),
+						definitions: vec![],
+					});
+			}
+
+			let definitions = definitions.get(&head_atom.predicate_declaration).unwrap();
+		},
 		HeadType::ChoiceWithSingleAtom(test) =>
 			log::debug!("translating choice rule with single atom"),
 		HeadType::IntegrityConstraint =>
@@ -25,7 +64,6 @@ pub fn read(rule: &clingo::ast::Rule, context: &mut Context) -> Result<(), crate
 			log::debug!("skipping trivial rule");
 			return Ok(());
 		},
-		_ => (),
 	}
 
 	Ok(())

src/translate/verify_properties/context.rs

@@ -1,77 +0,0 @@
-pub struct ScopedFormula
-{
-	free_variable_declarations: foliage::VariableDeclarations,
-	formula: foliage::Formula,
-}
-
-pub struct Context
-{
-	scoped_formulas: Vec<ScopedFormula>,
-	function_declarations: foliage::FunctionDeclarations,
-	predicate_declarations: foliage::PredicateDeclarations,
-	variable_declaration_stack: foliage::VariableDeclarationStack,
-}
-
-impl Context
-{
-	pub fn new() -> Self
-	{
-		Self
-		{
-			scoped_formulas: vec![],
-			function_declarations: foliage::FunctionDeclarations::new(),
-			predicate_declarations: foliage::PredicateDeclarations::new(),
-			variable_declaration_stack: foliage::VariableDeclarationStack::new(),
-		}
-	}
-
-	pub fn find_or_create_predicate_declaration(&mut self, name: &str, arity: usize)
-		-> std::rc::Rc<foliage::PredicateDeclaration>
-	{
-		match self.predicate_declarations.iter()
-			.find(|x| x.name == name && x.arity == arity)
-		{
-			Some(value) => std::rc::Rc::clone(value),
-			None =>
-			{
-				let declaration = foliage::PredicateDeclaration
-				{
-					name: name.to_owned(),
-					arity,
-				};
-				let declaration = std::rc::Rc::new(declaration);
-
-				self.predicate_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				log::debug!("new predicate declaration: {}/{}", name, arity);
-
-				declaration
-			},
-		}
-	}
-
-	pub fn find_or_create_function_declaration(&mut self, name: &str, arity: usize)
-		-> std::rc::Rc<foliage::FunctionDeclaration>
-	{
-		match self.function_declarations.iter()
-			.find(|x| x.name == name && x.arity == arity)
-		{
-			Some(value) => std::rc::Rc::clone(value),
-			None =>
-			{
-				let declaration = foliage::FunctionDeclaration
-				{
-					name: name.to_owned(),
-					arity,
-				};
-				let declaration = std::rc::Rc::new(declaration);
-
-				self.function_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				log::debug!("new function declaration: {}/{}", name, arity);
-
-				declaration
-			},
-		}
-	}
-}

src/translate/verify_properties/head_type.rs

@@ -1,10 +1,10 @@
-pub struct HeadAtom<'a>
+pub(crate) struct HeadAtom<'a>
 {
 	pub predicate_declaration: std::rc::Rc<foliage::PredicateDeclaration>,
 	pub arguments: &'a [clingo::ast::Term<'a>],
 }
 
-pub enum HeadType<'a>
+pub(crate) enum HeadType<'a>
 {
 	SingleAtom(HeadAtom<'a>),
 	ChoiceWithSingleAtom(HeadAtom<'a>),
@@ -12,7 +12,7 @@ pub enum HeadType<'a>
 	Trivial,
 }
 
-pub fn determine_head_type<'a, F>(head_literal: &'a clingo::ast::HeadLiteral,
+pub(crate) fn determine_head_type<'a, F>(head_literal: &'a clingo::ast::HeadLiteral,
 	mut find_or_create_predicate_declaration: F)
 	-> Result<HeadType<'a>, crate::Error>
 where

src/translate/verify_properties/translate_body.rs

@@ -1,6 +1,11 @@
-pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign,
-	context: &mut super::Context)
+pub(crate) fn translate_body_term<F1, F2, F3>(body_term: &clingo::ast::Term, sign: clingo::ast::Sign,
+	mut find_or_create_function_declaration: F1, mut find_or_create_predicate_declaration: F2,
+	mut find_or_create_variable_declaration: F3)
 	-> Result<foliage::Formula, crate::Error>
+where
+	F1: crate::translate::common::FindOrCreateFunctionDeclaration,
+	F2: crate::translate::common::FindOrCreatePredicateDeclaration,
+	F3: crate::translate::common::FindOrCreateVariableDeclaration,
 {
 	let function = match body_term.term_type()
 	{
@@ -10,7 +15,7 @@ pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sig
 
 	let function_name = function.name().map_err(|error| crate::Error::new_decode_identifier(error))?;
 
-	let predicate_declaration = context.find_or_create_predicate_declaration(function_name,
+	let predicate_declaration = find_or_create_predicate_declaration(function_name,
 		function.arguments().len());
 
 	let parameters = function.arguments().iter().map(|_| std::rc::Rc::new(
@@ -49,7 +54,7 @@ pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sig
 	let mut arguments = function.arguments().iter().map(|x|
 		{
 			let result = crate::translate::common::choose_value_in_term(x, &parameters[i],
-				|name, arity| context.find_or_create_function_declaration(name, arity))
+				&mut find_or_create_function_declaration, &mut find_or_create_variable_declaration)
 				.map(|x| Box::new(x));
 			i += 1;
 			result
@@ -67,8 +72,14 @@ pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sig
 	}))
 }
 
-pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context: &mut super::Context)
+pub(crate) fn translate_body_literal<F1, F2, F3>(body_literal: &clingo::ast::BodyLiteral,
+	mut find_or_create_function_declaration: F1, mut find_or_create_predicate_declaration: F2,
+	mut find_or_create_variable_declaration: F3)
 	-> Result<foliage::Formula, crate::Error>
+where
+	F1: crate::translate::common::FindOrCreateFunctionDeclaration,
+	F2: crate::translate::common::FindOrCreatePredicateDeclaration,
+	F3: crate::translate::common::FindOrCreateVariableDeclaration,
 {
 	match body_literal.sign()
 	{
@@ -96,7 +107,9 @@ pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context:
 
 			Ok(foliage::Formula::Boolean(value))
 		},
-		clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), context),
+		clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(),
+			&mut find_or_create_function_declaration, &mut find_or_create_predicate_declaration,
+			&mut find_or_create_variable_declaration),
 		clingo::ast::LiteralType::Comparison(comparison) =>
 		{
 			let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration
@@ -110,9 +123,9 @@ pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context:
 			let parameter_z2 = &parameters[1];
 
 			let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), &parameter_z1,
-				|name, arity| context.find_or_create_function_declaration(name, arity))?;
+				&mut find_or_create_function_declaration, &mut find_or_create_variable_declaration)?;
 			let choose_z2_in_t2 = crate::translate::common::choose_value_in_term(comparison.right(), &parameter_z2,
-				|name, arity| context.find_or_create_function_declaration(name, arity))?;
+				&mut find_or_create_function_declaration, &mut find_or_create_variable_declaration)?;
 
 			let variable_1 = foliage::Variable
 			{
@@ -148,11 +161,19 @@ pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context:
 	}
 }
 
-pub fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &mut super::Context)
+pub(crate) fn translate_body<F1, F2, F3>(body_literals: &[clingo::ast::BodyLiteral],
+	mut find_or_create_function_declaration: F1, mut find_or_create_predicate_declaration: F2,
+	mut find_or_create_variable_declaration: F3)
 	-> Result<foliage::Formulas, crate::Error>
+where
+	F1: crate::translate::common::FindOrCreateFunctionDeclaration,
+	F2: crate::translate::common::FindOrCreatePredicateDeclaration,
+	F3: crate::translate::common::FindOrCreateVariableDeclaration,
 {
 	body_literals.iter()
-		.map(|body_literal| translate_body_literal(body_literal, context)
+		.map(|body_literal| translate_body_literal(body_literal,
+			&mut find_or_create_function_declaration, &mut find_or_create_predicate_declaration,
+			&mut find_or_create_variable_declaration)
 			.map(|value| Box::new(value)))
 		.collect::<Result<foliage::Formulas, crate::Error>>()
 }