From a7e8368634e2871fa2ac796e66455eca61ce8dfc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 24 Jan 2020 13:32:43 +0100
Subject: [PATCH] Work in progress

---
 .gitignore                         |   2 +
 Cargo.toml                         |  12 +++
 src/ast.rs                         | 156 +++++++++++++++++++++++++++++
 src/lib.rs                         |   5 +
 src/main.rs                        |  45 +++++++++
 src/translate.rs                   |   1 +
 src/translate/verify_properties.rs |   8 ++
 7 files changed, 229 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Cargo.toml
 create mode 100644 src/ast.rs
 create mode 100644 src/lib.rs
 create mode 100644 src/main.rs
 create mode 100644 src/translate.rs
 create mode 100644 src/translate/verify_properties.rs

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1b72444
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+/Cargo.lock
+/target
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..c4c1d26
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "anthem"
+version = "0.3.0"
+authors = ["Patrick Lühne <patrick@luehne.de>"]
+edition = "2018"
+
+[dependencies]
+clingo = "0.6"
+
+[dependencies.foliage]
+git = "ssh://gitea@git.luehne.de/patrick/foliage-rs.git"
+branch = "refactoring"
diff --git a/src/ast.rs b/src/ast.rs
new file mode 100644
index 0000000..4890bcd
--- /dev/null
+++ b/src/ast.rs
@@ -0,0 +1,156 @@
+// Operators
+
+pub enum BinaryOperator
+{
+	Plus,
+	Minus,
+	Multiplication,
+	Division,
+	Modulo,
+	Power,
+}
+
+pub enum ComparisonOperator
+{
+	GreaterThan,
+	LessThan,
+	LessEqual,
+	GreaterEqual,
+	NotEqual,
+	Equal,
+}
+
+pub enum UnaryOperator
+{
+	AbsoluteValue,
+	Minus,
+}
+
+// Primitives
+
+pub struct FunctionDeclaration
+{
+	pub name: String,
+	pub arity: usize,
+}
+
+pub struct PredicateDeclaration
+{
+	pub name: String,
+	pub arity: usize,
+}
+
+pub struct VariableDeclaration
+{
+	pub name: String,
+}
+
+// Terms
+
+pub struct BinaryOperation
+{
+	pub operator: BinaryOperator,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
+}
+
+pub struct Function
+{
+	pub declaration: std::rc::Rc<FunctionDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+pub struct Interval
+{
+	pub from: Box<Term>,
+	pub to: Box<Term>,
+}
+
+pub enum SpecialInteger
+{
+	Infimum,
+	Supremum,
+}
+
+pub struct UnaryOperation
+{
+	pub operator: UnaryOperator,
+	pub argument: Box<Term>,
+}
+
+pub struct Variable
+{
+	pub declaration: std::rc::Rc<VariableDeclaration>,
+}
+
+// Formulas
+
+pub struct Biconditional
+{
+	pub left: Box<Formula>,
+	pub right: Box<Formula>,
+}
+
+pub struct Comparison
+{
+	pub operator: ComparisonOperator,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
+}
+
+pub struct Exists
+{
+	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
+	pub argument: Box<Formula>,
+}
+
+pub struct ForAll
+{
+	pub parameters: Vec<std::rc::Rc<VariableDeclaration>>,
+	pub argument: Box<Formula>,
+}
+
+pub struct Implies
+{
+	pub left: Box<Formula>,
+	pub right: Box<Formula>,
+}
+
+pub struct Predicate
+{
+	pub declaration: std::rc::Rc<PredicateDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+// Variants
+
+pub enum Term
+{
+	BinaryOperation(BinaryOperation),
+	Boolean(bool),
+	Function(Function),
+	Integer(i32),
+	Interval(Interval),
+	SpecialInteger(SpecialInteger),
+	String(String),
+	UnaryOperation(UnaryOperation),
+	Variable(Variable),
+}
+
+pub type Terms = Vec<Box<Term>>;
+
+pub enum Formula
+{
+	And(Formulas),
+	Biconditional(Biconditional),
+	Boolean(bool),
+	Comparison(Comparison),
+	Exists(Exists),
+	ForAll(ForAll),
+	Implies(Implies),
+	Not(Box<Formula>),
+	Or(Formulas),
+	Predicate(Predicate),
+}
+
+pub type Formulas = Vec<Box<Formula>>;
diff --git a/src/lib.rs b/src/lib.rs
new file mode 100644
index 0000000..242a0ca
--- /dev/null
+++ b/src/lib.rs
@@ -0,0 +1,5 @@
+pub mod translate;
+
+pub struct Context
+{
+}
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 0000000..84129e6
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,45 @@
+struct Context
+{
+}
+
+struct StatementHandler<'context>
+{
+	context: &'context mut Context,
+}
+
+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) =>
+			{
+				println!("got rule {:?}", rule)
+			},
+			_ => println!("got other kind of statement"),
+		}
+
+		true
+	}
+}
+
+struct Logger;
+
+impl clingo::Logger for Logger
+{
+	fn log(&mut self, code: clingo::Warning, message: &str)
+	{
+		println!("clingo warning ({:?}): {}", code, message);
+	}
+}
+
+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};
+	clingo::parse_program_with_logger(&program, &mut statement_handler, &mut Logger, std::u32::MAX)?;
+
+	Ok(())
+}
diff --git a/src/translate.rs b/src/translate.rs
new file mode 100644
index 0000000..84b1437
--- /dev/null
+++ b/src/translate.rs
@@ -0,0 +1 @@
+pub mod verify_properties;
diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs
new file mode 100644
index 0000000..7306348
--- /dev/null
+++ b/src/translate/verify_properties.rs
@@ -0,0 +1,8 @@
+struct Context
+{
+}
+
+fn read(rule: &clingo::ast::Rule, context: &mut crate::Context)
+{
+	
+}