diff --git a/src/lib.rs b/src/lib.rs index c746c8d..947a9ed 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,3 +1,5 @@ +#![feature(trait_alias)] + pub mod error; pub mod translate; diff --git a/src/main.rs b/src/main.rs index 70128d9..97729b5 100644 --- a/src/main.rs +++ b/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) { diff --git a/src/translate/common.rs b/src/translate/common.rs index c63a7f8..5d6aecb 100644 --- a/src/translate/common.rs +++ b/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; + +pub(crate) trait FindOrCreatePredicateDeclaration = FnMut(&str, usize) + -> std::rc::Rc; + +pub(crate) trait FindOrCreateVariableDeclaration = FnMut(&str) + -> std::rc::Rc; + +pub(crate) fn find_or_create_predicate_declaration(predicate_declarations: &mut foliage::PredicateDeclarations, + name: &str, arity: usize) + -> std::rc::Rc +{ + 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 +{ + 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, +pub(crate) fn choose_value_in_primitive(term: Box, variable_declaration: &std::rc::Rc) -> foliage::Comparison { @@ -35,12 +96,13 @@ pub fn choose_value_in_primitive(term: Box, } } -pub fn choose_value_in_term(term: &clingo::ast::Term, +pub(crate) fn choose_value_in_term(term: &clingo::ast::Term, variable_declaration: &std::rc::Rc, - mut find_or_create_function_declaration: F) + mut find_or_create_function_declaration: F1, mut find_or_create_variable_declaration: F2) -> Result where - F: FnMut(&str, usize) -> std::rc::Rc + 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")), } } diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index de5ec27..6ed2bbd 100644 --- a/src/translate/verify_properties.rs +++ b/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, +} + +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::, Definitions>::new(); + + let declare_predicate_parameters = |predicate_declaration: &foliage::PredicateDeclaration| + { + (0..predicate_declaration.arity) + .map(|_| std::rc::Rc::new(foliage::VariableDeclaration + { + name: "".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(()) diff --git a/src/translate/verify_properties/context.rs b/src/translate/verify_properties/context.rs deleted file mode 100644 index 294eb49..0000000 --- a/src/translate/verify_properties/context.rs +++ /dev/null @@ -1,77 +0,0 @@ -pub struct ScopedFormula -{ - free_variable_declarations: foliage::VariableDeclarations, - formula: foliage::Formula, -} - -pub struct Context -{ - scoped_formulas: Vec, - 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 - { - 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 - { - 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 - }, - } - } -} diff --git a/src/translate/verify_properties/head_type.rs b/src/translate/verify_properties/head_type.rs index da8996d..d08843d 100644 --- a/src/translate/verify_properties/head_type.rs +++ b/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, 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, crate::Error> where diff --git a/src/translate/verify_properties/translate_body.rs b/src/translate/verify_properties/translate_body.rs index c64a1bb..773e112 100644 --- a/src/translate/verify_properties/translate_body.rs +++ b/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(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 +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, ¶meters[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(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 +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 = ¶meters[1]; let choose_z1_in_t1 = crate::translate::common::choose_value_in_term(comparison.left(), ¶meter_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(), ¶meter_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(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 +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::>() }