From b95bda810a307f5b12fb46c70e75a9c6997bcaf5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sat, 25 Jan 2020 12:55:23 +0100
Subject: [PATCH] Work in progress

---
 src/main.rs                        | 15 +++++++--------
 src/translate/verify_properties.rs | 29 ++++++++++++++++++++++++++---
 2 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/src/main.rs b/src/main.rs
index 84129e6..ced6256 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,10 +1,6 @@
-struct Context
-{
-}
-
 struct StatementHandler<'context>
 {
-	context: &'context mut Context,
+	context: &'context mut anthem::translate::verify_properties::Context,
 }
 
 impl clingo::StatementHandler for StatementHandler<'_>
@@ -15,7 +11,7 @@ impl clingo::StatementHandler for StatementHandler<'_>
 		{
 			clingo::ast::StatementType::Rule(ref rule) =>
 			{
-				println!("got rule {:?}", rule)
+				anthem::translate::verify_properties::read(rule, self.context)
 			},
 			_ => println!("got other kind of statement"),
 		}
@@ -37,8 +33,11 @@ impl clingo::Logger for Logger
 fn main() -> Result<(), Box<dyn std::error::Error>>
 {
 	let program = std::fs::read_to_string("test.lp")?;
-	let mut context = Context{};
-	let mut statement_handler = StatementHandler{context: &mut context};
+	let mut context = anthem::translate::verify_properties::Context::new();
+	let mut statement_handler = StatementHandler
+	{
+		context: &mut context
+	};
 	clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)?;
 
 	Ok(())
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
index 7306348..9e37df2 100644
--- a/src/translate/verify_properties.rs
+++ b/src/translate/verify_properties.rs
@@ -1,8 +1,31 @@
-struct Context
+pub struct ScopedFormula
 {
+	free_variable_declarations: foliage::VariableDeclarations,
+	formula: foliage::Formula,
 }
 
-fn read(rule: &clingo::ast::Rule, context: &mut crate::Context)
+pub struct Context
 {
-	
+	scoped_formulas: Vec<ScopedFormula>,
+}
+
+impl Context
+{
+	pub fn new() -> Self
+	{
+		Self
+		{
+			scoped_formulas: vec![],
+		}
+	}
+}
+
+pub fn translate_body ...
+
+pub fn read(rule: &clingo::ast::Rule, context: &mut Context)
+{
+	let mut variable_declaration_stack: foliage::VariableDeclarationStack;
+
+	println!("{:?}", rule.head());
+	println!("{:?}", rule.body());
 }