Work in progress
This commit is contained in:
commit
a7e8368634
2
.gitignore
vendored
Normal file
2
.gitignore
vendored
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
/Cargo.lock
|
||||||
|
/target
|
12
Cargo.toml
Normal file
12
Cargo.toml
Normal file
@ -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"
|
156
src/ast.rs
Normal file
156
src/ast.rs
Normal file
@ -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>>;
|
5
src/lib.rs
Normal file
5
src/lib.rs
Normal file
@ -0,0 +1,5 @@
|
|||||||
|
pub mod translate;
|
||||||
|
|
||||||
|
pub struct Context
|
||||||
|
{
|
||||||
|
}
|
45
src/main.rs
Normal file
45
src/main.rs
Normal file
@ -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(())
|
||||||
|
}
|
1
src/translate.rs
Normal file
1
src/translate.rs
Normal file
@ -0,0 +1 @@
|
|||||||
|
pub mod verify_properties;
|
8
src/translate/verify_properties.rs
Normal file
8
src/translate/verify_properties.rs
Normal file
@ -0,0 +1,8 @@
|
|||||||
|
struct Context
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
fn read(rule: &clingo::ast::Rule, context: &mut crate::Context)
|
||||||
|
{
|
||||||
|
|
||||||
|
}
|
Loading…
Reference in New Issue
Block a user