Translate body of rules for verifying properties

Cargo.toml

@@ -6,6 +6,8 @@ edition = "2018"
 
 [dependencies]
 clingo = "0.6"
+log = "0.4"
+pretty_env_logger = "0.3"
 
 [dependencies.foliage]
 git = "ssh://gitea@git.luehne.de/patrick/foliage-rs.git"

src/error.rs

@@ -0,0 +1,97 @@
+pub type Source = Box<dyn std::error::Error>;
+
+pub enum Kind
+{
+	Logic(&'static str),
+	UnsupportedLanguageFeature(&'static str),
+	NotYetImplemented(&'static str),
+	DecodeIdentifier,
+}
+
+pub struct Error
+{
+	pub kind: Kind,
+	pub source: Option<Source>,
+}
+
+impl Error
+{
+	pub(crate) fn new(kind: Kind) -> Self
+	{
+		Self
+		{
+			kind,
+			source: None,
+		}
+	}
+
+	pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
+	{
+		self.source = Some(source.into());
+		self
+	}
+
+	pub(crate) fn new_logic(description: &'static str) -> Self
+	{
+		Self::new(Kind::Logic(description))
+	}
+
+	pub(crate) fn new_unsupported_language_feature(description: &'static str) -> Self
+	{
+		Self::new(Kind::UnsupportedLanguageFeature(description))
+	}
+
+	pub(crate) fn new_not_yet_implemented(description: &'static str) -> Self
+	{
+		Self::new(Kind::NotYetImplemented(description))
+	}
+
+	pub(crate) fn new_decode_identifier<S: Into<Source>>(source: S) -> Self
+	{
+		Self::new(Kind::DecodeIdentifier).with(source)
+	}
+}
+
+impl std::fmt::Debug for Error
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match &self.kind
+		{
+			Kind::Logic(ref description) => write!(formatter,
+				"logic error, please report to bug tracker ({})", description),
+			Kind::UnsupportedLanguageFeature(ref description) => write!(formatter,
+				"language feature not yet supported ({})", description),
+			Kind::NotYetImplemented(ref description) => write!(formatter,
+				"not yet implemented ({})", description),
+			Kind::DecodeIdentifier => write!(formatter, "could not decode identifier"),
+		}?;
+
+		if let Some(source) = &self.source
+		{
+			write!(formatter, "\nerror source: {}", source)?;
+		}
+
+		Ok(())
+	}
+}
+
+impl std::fmt::Display for Error
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(formatter, "{:?}", self)
+	}
+}
+
+impl std::error::Error for Error
+{
+	fn source(&self) -> Option<&(dyn std::error::Error + 'static)>
+	{
+		match &self.source
+		{
+			Some(source) => Some(source.as_ref()),
+			None => None,
+		}
+	}
+}

src/lib.rs

@@ -1,5 +1,4 @@
+pub mod error;
 pub mod translate;
 
-pub struct Context
-{
-}
+pub use error::Error;

src/main.rs

@@ -13,7 +13,7 @@ impl clingo::StatementHandler for StatementHandler<'_>
 			{
 				anthem::translate::verify_properties::read(rule, self.context)
 			},
-			_ => println!("got other kind of statement"),
+			_ => log::debug!("read statement (other kind)"),
 		}
 
 		true
@@ -26,12 +26,14 @@ impl clingo::Logger for Logger
 {
 	fn log(&mut self, code: clingo::Warning, message: &str)
 	{
-		println!("clingo warning ({:?}): {}", code, message);
+		log::warn!("clingo warning ({:?}): {}", code, message);
 	}
 }
 
 fn main() -> Result<(), Box<dyn std::error::Error>>
 {
+	pretty_env_logger::init();
+
 	let program = std::fs::read_to_string("test.lp")?;
 	let mut context = anthem::translate::verify_properties::Context::new();
 	let mut statement_handler = StatementHandler

src/translate.rs

@@ -1 +1,2 @@
+mod common;
 pub mod verify_properties;

src/translate/common.rs

@@ -0,0 +1,93 @@
+pub fn translate_comparison_operator(comparison_operator: clingo::ast::ComparisonOperator)
+	-> foliage::ComparisonOperator
+{
+	match comparison_operator
+	{
+		clingo::ast::ComparisonOperator::GreaterThan
+			=> foliage::ComparisonOperator::Greater,
+		clingo::ast::ComparisonOperator::LessThan
+			=> foliage::ComparisonOperator::Less,
+		clingo::ast::ComparisonOperator::LessEqual
+			=> foliage::ComparisonOperator::LessOrEqual,
+		clingo::ast::ComparisonOperator::GreaterEqual
+			=> foliage::ComparisonOperator::GreaterOrEqual,
+		clingo::ast::ComparisonOperator::NotEqual
+			=> foliage::ComparisonOperator::NotEqual,
+		clingo::ast::ComparisonOperator::Equal
+			=> foliage::ComparisonOperator::Equal,
+	}
+}
+
+pub fn choose_value_in_primitive(term: Box<foliage::Term>,
+	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>)
+	-> foliage::Comparison
+{
+	let variable = foliage::Variable
+	{
+		declaration: std::rc::Rc::clone(variable_declaration),
+	};
+
+	foliage::Comparison
+	{
+		operator: foliage::ComparisonOperator::Equal,
+		left: Box::new(foliage::Term::Variable(variable)),
+		right: term,
+	}
+}
+
+pub fn choose_value_in_term<F>(term: &clingo::ast::Term,
+	variable_declaration: &std::rc::Rc<foliage::VariableDeclaration>,
+	mut find_or_create_function_declaration: F)
+	-> Result<foliage::Formula, crate::Error>
+where
+	F: FnMut(&str, usize) -> std::rc::Rc<foliage::FunctionDeclaration>
+{
+	match term.term_type()
+	{
+		clingo::ast::TermType::Symbol(symbol) => match symbol.symbol_type()
+			.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
+		{
+			clingo::SymbolType::Number => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
+				Box::new(foliage::Term::Integer(symbol.number()
+					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?)),
+				variable_declaration))),
+			clingo::SymbolType::Infimum => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
+				Box::new(foliage::Term::SpecialInteger(foliage::SpecialInteger::Infimum)),
+				variable_declaration))),
+			clingo::SymbolType::Supremum => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
+				Box::new(foliage::Term::SpecialInteger(foliage::SpecialInteger::Supremum)),
+				variable_declaration))),
+			clingo::SymbolType::String => Ok(foliage::Formula::Comparison(choose_value_in_primitive(
+				Box::new(foliage::Term::String(symbol.string()
+					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?
+					.to_string())),
+				variable_declaration))),
+			clingo::SymbolType::Function =>
+			{
+				let arguments = symbol.arguments()
+					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
+
+				// Functions with arguments are represented as clingo::ast::Function by the parser.
+				// At this point, we only have to handle (0-ary) constants
+				if !arguments.is_empty()
+				{
+					return Err(crate::Error::new_logic("unexpected arguments, expected (0-ary) constant symbol"));
+				}
+
+				let constant_name = symbol.name()
+					.map_err(|error| crate::Error::new_logic("clingo error").with(error))?;
+
+				let constant_declaration = find_or_create_function_declaration(constant_name, 0);
+
+				let function = foliage::Term::Function(foliage::Function
+				{
+					declaration: constant_declaration,
+					arguments: vec![],
+				});
+
+				Ok(foliage::Formula::Comparison(choose_value_in_primitive(Box::new(function), variable_declaration)))
+			}
+		},
+		_ => Ok(foliage::Formula::Boolean(false))
+	}
+}

src/translate/verify_properties.rs

@@ -7,6 +7,9 @@ pub struct ScopedFormula
 pub struct Context
 {
 	scoped_formulas: Vec<ScopedFormula>,
+	function_declarations: foliage::FunctionDeclarations,
+	predicate_declarations: foliage::PredicateDeclarations,
+	variable_declaration_stack: foliage::VariableDeclarationStack,
 }
 
 impl Context
@@ -16,16 +19,223 @@ impl Context
 		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
+			},
 		}
 	}
 }
 
-pub fn translate_body ...
+pub fn translate_body_term(body_term: &clingo::ast::Term, sign: clingo::ast::Sign,
+	context: &mut Context)
+	-> Result<foliage::Formula, crate::Error>
+{
+	let function = match body_term.term_type()
+	{
+		clingo::ast::TermType::Function(value) => value,
+		_ => return Err(crate::Error::new_unsupported_language_feature("only functions supported as body terms")),
+	};
+
+	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,
+		function.arguments().len());
+
+	let parameters = function.arguments().iter().map(|_| std::rc::Rc::new(
+		foliage::VariableDeclaration
+		{
+			name: "<anonymous>".to_string(),
+		}))
+		.collect::<Vec<_>>();
+
+	let predicate_arguments = parameters.iter().map(
+		|parameter| Box::new(foliage::Term::Variable(foliage::Variable{declaration: std::rc::Rc::clone(parameter)})))
+		.collect::<Vec<_>>();
+
+	let predicate = foliage::Predicate
+	{
+		declaration: predicate_declaration,
+		arguments: predicate_arguments,
+	};
+
+	let predicate_literal = match sign
+	{
+		clingo::ast::Sign::None
+		| clingo::ast::Sign::DoubleNegation
+			=> foliage::Formula::Predicate(predicate),
+		clingo::ast::Sign::Negation
+			=> foliage::Formula::Not(Box::new(foliage::Formula::Predicate(predicate))),
+	};
+
+	if function.arguments().is_empty()
+	{
+		return Ok(predicate_literal);
+	}
+
+	let mut i = 0;
+
+	let mut arguments = function.arguments().iter().map(|x|
+		{
+			let result = super::common::choose_value_in_term(x, &parameters[i],
+				|name, arity| context.find_or_create_function_declaration(name, arity))
+				.map(|x| Box::new(x));
+			i += 1;
+			result
+		})
+		.collect::<Result<Vec<_>, _>>()?;
+
+	arguments.push(Box::new(predicate_literal));
+
+	let and = foliage::Formula::And(arguments);
+
+	Ok(foliage::Formula::Exists(foliage::Exists
+	{
+		parameters,
+		argument: Box::new(and),
+	}))
+}
+
+pub fn translate_body_literal(body_literal: &clingo::ast::BodyLiteral, context: &mut Context)
+	-> Result<foliage::Formula, crate::Error>
+{
+	match body_literal.sign()
+	{
+		clingo::ast::Sign::None => (),
+		_ => return Err(crate::Error::new_unsupported_language_feature(
+			"signed body literals")),
+	}
+
+	let literal = match body_literal.body_literal_type()
+	{
+		clingo::ast::BodyLiteralType::Literal(literal) => literal,
+		_ => return Err(crate::Error::new_unsupported_language_feature(
+			"only plain body literals supported")),
+	};
+
+	match literal.literal_type()
+	{
+		clingo::ast::LiteralType::Boolean(value) =>
+		{
+			match literal.sign()
+			{
+				clingo::ast::Sign::None => (),
+				_ => return Err(crate::Error::new_logic("unexpected negated Boolean value")),
+			}
+
+			Ok(foliage::Formula::Boolean(value))
+		},
+		clingo::ast::LiteralType::Symbolic(term) => translate_body_term(term, literal.sign(), context),
+		clingo::ast::LiteralType::Comparison(comparison) =>
+		{
+			let new_variable_declaration = || std::rc::Rc::new(foliage::VariableDeclaration
+			{
+				name: "<anonymous>".to_string()
+			});
+
+			let parameters = vec![new_variable_declaration(), new_variable_declaration()];
+
+			let parameter_z1 = &parameters[0];
+			let parameter_z2 = &parameters[1];
+
+			let choose_z1_in_t1 = super::common::choose_value_in_term(comparison.left(), &parameter_z1,
+				|name, arity| context.find_or_create_function_declaration(name, arity))?;
+			let choose_z2_in_t2 = super::common::choose_value_in_term(comparison.right(), &parameter_z2,
+				|name, arity| context.find_or_create_function_declaration(name, arity))?;
+
+			let variable_1 = foliage::Variable
+			{
+				declaration: std::rc::Rc::clone(&parameter_z1),
+			};
+
+			let variable_2 = foliage::Variable
+			{
+				declaration: std::rc::Rc::clone(&parameter_z2),
+			};
+
+			let comparison_operator
+				= super::common::translate_comparison_operator(comparison.comparison_type());
+
+			let compare_z1_and_z2 = foliage::Comparison
+			{
+				operator: comparison_operator,
+				left: Box::new(foliage::Term::Variable(variable_1)),
+				right: Box::new(foliage::Term::Variable(variable_2)),
+			};
+
+			let and = foliage::Formula::And(vec![Box::new(choose_z1_in_t1),
+				Box::new(choose_z2_in_t2), Box::new(foliage::Formula::Comparison(compare_z1_and_z2))]);
+
+			Ok(foliage::Formula::Exists(foliage::Exists
+			{
+				parameters,
+				argument: Box::new(and),
+			}))
+		},
+		_ => Err(crate::Error::new_unsupported_language_feature(
+			"body literals other than Booleans, terms, or comparisons")),
+	}
+}
+
+pub fn translate_body(body_literals: &[clingo::ast::BodyLiteral], context: &mut Context)
+	-> Result<foliage::Formulas, crate::Error>
+{
+	body_literals.iter()
+		.map(|body_literal| translate_body_literal(body_literal, context)
+			.map(|value| Box::new(value)))
+		.collect::<Result<foliage::Formulas, crate::Error>>()
+}
 
 pub fn read(rule: &clingo::ast::Rule, context: &mut Context)
 {
-	let mut variable_declaration_stack: foliage::VariableDeclarationStack;
-
-	println!("{:?}", rule.head());
-	println!("{:?}", rule.body());
+	println!("{:?}", translate_body(rule.body(), context));
 }