From 7d47910cfa088c40fbc8795a6c16ac77fe21cfe8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sat, 2 Nov 2019 02:13:45 +0100 Subject: [PATCH] Initial project file parser --- .gitignore | 3 + .gitmodules | 3 + Cargo.toml | 12 ++ foliage | 1 + src/format.rs | 74 ++++++++++++ src/format_tptp.rs | 289 +++++++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 6 + src/main.rs | 24 ++++ src/parse.rs | 100 ++++++++++++++++ src/project.rs | 12 ++ 10 files changed, 524 insertions(+) create mode 100644 .gitignore create mode 100644 .gitmodules create mode 100644 Cargo.toml create mode 160000 foliage create mode 100644 src/format.rs create mode 100644 src/format_tptp.rs create mode 100644 src/lib.rs create mode 100644 src/main.rs create mode 100644 src/parse.rs create mode 100644 src/project.rs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..6936990 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +/target +**/*.rs.bk +Cargo.lock diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..f69fb30 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "foliage"] + path = foliage + url = ../foliage-rs.git diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..0033c16 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "ask_dracula" +version = "0.1.0" +authors = ["Patrick Lühne "] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +clap = "2.33" +foliage = {path = "foliage"} +nom = "5.0" diff --git a/foliage b/foliage new file mode 160000 index 0000000..a6fe4b9 --- /dev/null +++ b/foliage @@ -0,0 +1 @@ +Subproject commit a6fe4b9e0881fc1707fd6c83e419857ad8a653eb diff --git a/src/format.rs b/src/format.rs new file mode 100644 index 0000000..4419a95 --- /dev/null +++ b/src/format.rs @@ -0,0 +1,74 @@ +impl std::fmt::Debug for crate::project::StatementKind +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self + { + crate::project::StatementKind::Axiom => write!(format, "axiom"), + crate::project::StatementKind::Lemma => write!(format, "lemma"), + crate::project::StatementKind::Conjecture => write!(format, "conjecture"), + } + } +} + +impl std::fmt::Display for crate::project::StatementKind +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} + +impl std::fmt::Debug for crate::Project +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + let mut line_separator = ""; + let mut section_separator = ""; + + if let Some(axioms) = self.statements.get(&crate::project::StatementKind::Axiom) + { + for axiom in axioms + { + write!(format, "{}{:?}: {:?}.", line_separator, crate::project::StatementKind::Axiom, axiom)?; + line_separator = "\n"; + } + + section_separator = "\n"; + } + + if let Some(lemmas) = self.statements.get(&crate::project::StatementKind::Lemma) + { + write!(format, "{}", section_separator)?; + + for lemma in lemmas + { + write!(format, "{}{:?}: {:?}.", line_separator, crate::project::StatementKind::Lemma, lemma)?; + line_separator = "\n"; + } + + section_separator = "\n"; + } + + if let Some(conjectures) = self.statements.get(&crate::project::StatementKind::Conjecture) + { + write!(format, "{}", section_separator)?; + + for conjecture in conjectures + { + write!(format, "{}{:?}: {:?}.", line_separator, crate::project::StatementKind::Conjecture, conjecture)?; + line_separator = "\n"; + } + } + + Ok(()) + } +} + +impl std::fmt::Display for crate::Project +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} diff --git a/src/format_tptp.rs b/src/format_tptp.rs new file mode 100644 index 0000000..8e39ce9 --- /dev/null +++ b/src/format_tptp.rs @@ -0,0 +1,289 @@ +pub trait DisplayTPTP<'a, DisplayType> + where DisplayType: 'a + std::fmt::Debug + std::fmt::Display +{ + fn display_tptp(&'a self) -> DisplayType; +} + +struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration); +struct TermDisplay<'a>(&'a foliage::Term); +struct FormulaDisplay<'a>(&'a foliage::Formula); +struct StatementKindDisplay<'a>(&'a crate::project::StatementKind); +pub struct ProjectDisplay<'a>(&'a crate::project::Project); + +impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration +{ + fn display_tptp(&'a self) -> VariableDeclarationDisplay<'a> + { + VariableDeclarationDisplay(self) + } +} + +impl<'a> DisplayTPTP<'a, TermDisplay<'a>> for foliage::Term +{ + fn display_tptp(&'a self) -> TermDisplay<'a> + { + TermDisplay(self) + } +} + +impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula +{ + fn display_tptp(&'a self) -> FormulaDisplay<'a> + { + FormulaDisplay(self) + } +} + +impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::StatementKind +{ + fn display_tptp(&'a self) -> StatementKindDisplay<'a> + { + StatementKindDisplay(self) + } +} + +impl<'a> DisplayTPTP<'a, ProjectDisplay<'a>> for crate::project::Project +{ + fn display_tptp(&'a self) -> ProjectDisplay<'a> + { + ProjectDisplay(self) + } +} + +impl<'a> std::fmt::Debug for VariableDeclarationDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self.0.domain + { + foliage::Domain::Program => write!(format, "X{}: object", self.0.name), + foliage::Domain::Integer => write!(format, "N{}: $int", self.0.name), + } + } +} + +impl<'a> std::fmt::Display for VariableDeclarationDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} + +impl<'a> std::fmt::Debug for TermDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match self.0 + { + foliage::Term::Infimum => write!(format, "#inf"), + foliage::Term::Supremum => write!(format, "#sup"), + foliage::Term::Integer(value) => write!(format, "{}", value), + foliage::Term::Symbolic(ref value) => write!(format, "{}", value), + foliage::Term::String(ref value) => write!(format, "\"{}\"", value), + foliage::Term::Variable(ref declaration) => match declaration.domain + { + foliage::Domain::Program => write!(format, "X{}", declaration.name), + foliage::Domain::Integer => write!(format, "N{}", declaration.name), + }, + foliage::Term::Add(ref left, ref right) => write!(format, "$sum({:?}, {:?})", (&**left).display_tptp(), right.display_tptp()), + foliage::Term::Subtract(ref left, ref right) => write!(format, "$difference({:?} - {:?})", left.display_tptp(), right.display_tptp()), + foliage::Term::Multiply(ref left, ref right) => write!(format, "$product({:?} * {:?})", left.display_tptp(), right.display_tptp()), + foliage::Term::Negative(ref argument) => write!(format, "$uminus({:?})", argument.display_tptp()), + } + } +} + +impl<'a> std::fmt::Display for TermDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", self) + } +} + +impl<'a> std::fmt::Debug for FormulaDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match self.0 + { + foliage::Formula::Exists(ref exists) => + { + write!(format, "?[")?; + + let mut separator = ""; + + for parameter in &exists.parameters + { + write!(format, "{}{:?}", separator, parameter.display_tptp())?; + + separator = ", " + } + + write!(format, "]: ({:?})", exists.argument.display_tptp()) + }, + foliage::Formula::ForAll(ref for_all) => + { + write!(format, "![")?; + + let mut separator = ""; + + for parameter in &for_all.parameters + { + write!(format, "{}{:?}", separator, parameter.display_tptp())?; + + separator = ", " + } + + write!(format, "]: ({:?})", for_all.argument.display_tptp()) + }, + foliage::Formula::Not(ref argument) => write!(format, "~({:?})", argument.display_tptp()), + foliage::Formula::And(ref arguments) => + { + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, argument.display_tptp())?; + + separator = " & " + } + + Ok(()) + }, + foliage::Formula::Or(ref arguments) => + { + let mut separator = ""; + + for argument in arguments + { + write!(format, "{}{:?}", separator, argument.display_tptp())?; + + separator = " | " + } + + Ok(()) + }, + foliage::Formula::Implies(ref left, ref right) => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Less(ref left, ref right) => write!(format, "$less({:?}, {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::LessOrEqual(ref left, ref right) => write!(format, "$lesseq({:?}, {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Greater(ref left, ref right) => write!(format, "$greater({:?}, {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "$greatereq({:?}, {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Equal(ref left, ref right) => write!(format, "({:?} = {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::NotEqual(ref left, ref right) => write!(format, "({:?} ~= {:?})", left.display_tptp(), right.display_tptp()), + foliage::Formula::Boolean(value) => + match value + { + true => write!(format, "$true"), + false => write!(format, "$false"), + }, + foliage::Formula::Predicate(ref predicate) => + { + write!(format, "{}", predicate.declaration.name)?; + + if !predicate.arguments.is_empty() + { + write!(format, "(")?; + + let mut separator = ""; + + for argument in &predicate.arguments + { + write!(format, "{}{:?}", separator, argument.display_tptp())?; + + separator = ", " + } + + write!(format, ")")?; + } + + Ok(()) + }, + } + } +} + +impl<'a> std::fmt::Display for FormulaDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", self) + } +} + +impl<'a> std::fmt::Debug for StatementKindDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + match &self.0 + { + crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"), + crate::project::StatementKind::Lemma => write!(format, "conjecture, lemma"), + crate::project::StatementKind::Conjecture => write!(format, "conjecture, conjecture"), + } + } +} + +impl<'a> std::fmt::Display for StatementKindDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} + +impl<'a> std::fmt::Debug for ProjectDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + let mut line_separator = ""; + let mut section_separator = ""; + + if let Some(axioms) = self.0.statements.get(&crate::project::StatementKind::Axiom) + { + for axiom in axioms + { + write!(format, "{}tff({:?}, {:?}).", line_separator, crate::project::StatementKind::Axiom.display_tptp(), axiom.display_tptp())?; + line_separator = "\n"; + } + + section_separator = "\n"; + } + + if let Some(lemmas) = self.0.statements.get(&crate::project::StatementKind::Lemma) + { + write!(format, "{}", section_separator)?; + + for lemma in lemmas + { + write!(format, "{}tff({:?}, {:?}).", line_separator, crate::project::StatementKind::Lemma.display_tptp(), lemma.display_tptp())?; + line_separator = "\n"; + } + + section_separator = "\n"; + } + + if let Some(conjectures) = self.0.statements.get(&crate::project::StatementKind::Conjecture) + { + write!(format, "{}", section_separator)?; + + for conjecture in conjectures + { + write!(format, "{}tff({:?}, {:?}).", line_separator, crate::project::StatementKind::Conjecture.display_tptp(), conjecture.display_tptp())?; + line_separator = "\n"; + } + } + + Ok(()) + } +} + +impl<'a> std::fmt::Display for ProjectDisplay<'a> +{ + fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result + { + write!(format, "{:?}", &self) + } +} diff --git a/src/lib.rs b/src/lib.rs new file mode 100644 index 0000000..552dd13 --- /dev/null +++ b/src/lib.rs @@ -0,0 +1,6 @@ +pub mod format; +pub mod format_tptp; +pub mod parse; +mod project; + +pub use project::Project; diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..7aad92e --- /dev/null +++ b/src/main.rs @@ -0,0 +1,24 @@ +use ask_dracula::format_tptp::DisplayTPTP; + +fn main() -> Result<(), Box> +{ + let matches = clap::App::new("Ask Dracula: Using Vampire as an interactive theorem prover") + .arg(clap::Arg::with_name("file").long("file").short("f").takes_value(true).required(true)) + .after_help("example: ask_dracula -f program") + .get_matches(); + + let file = matches.value_of("file").unwrap().to_string(); + let file_path = std::path::Path::new(&file); + + let file_content = std::fs::read_to_string(&file_path)?; + let (_, project) = ask_dracula::parse::project(&file_content) + .map_err(|_| "couldn’t parse input file")?; + + println!("{}", project); + + println!(""); + + println!("{}", project.display_tptp()); + + Ok(()) +} diff --git a/src/parse.rs b/src/parse.rs new file mode 100644 index 0000000..bc3d47f --- /dev/null +++ b/src/parse.rs @@ -0,0 +1,100 @@ +use nom:: +{ + IResult, + character::complete::multispace0, + sequence::{delimited, pair, terminated}, + combinator::map, + branch::alt, + bytes::complete::tag, +}; + +fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> +{ + let foo = delimited + ( + multispace0, + alt + (( + map + ( + tag("axiom:"), + |_| crate::project::StatementKind::Axiom, + ), + map + ( + tag("lemma:"), + |_| crate::project::StatementKind::Lemma, + ), + map + ( + tag("conjecture:"), + |_| crate::project::StatementKind::Conjecture, + ), + )), + multispace0, + )(i); + + foo +} + +fn statement(i: &str) -> IResult<&str, (crate::project::StatementKind, foliage::Formula)> +{ + terminated + ( + pair + ( + statement_kind, + foliage::formula, + ), + delimited + ( + multispace0, + tag("."), + multispace0, + ), + )(i) +} + +pub fn project(i: &str) -> IResult<&str, crate::Project> +{ + let mut statement_input = i.clone(); + let mut statements = std::collections::HashMap::new(); + + loop + { + let i_ = statement_input.clone(); + match statement(i_) + { + Ok((i, (statement_kind, formula))) => + { + // Iteration must always consume input (to prevent infinite loops) + if i == statement_input + { + return Err(nom::Err::Error(nom::error::ParseError::from_error_kind(statement_input, nom::error::ErrorKind::Many0))); + } + + let statements = statements.entry(statement_kind).or_insert_with(Vec::new); + statements.push(formula); + + statement_input = i; + }, + Err(nom::Err::Error(_)) => break, + Err(e) => return Err(e), + } + } + + let i = statement_input; + + // Verify that the whole file has been parsed + if i != "" + { + return Err(nom::Err::Error(nom::error::ParseError::from_error_kind(statement_input, nom::error::ErrorKind::Many0))); + } + + let project = crate::Project + { + statements, + }; + + Ok((i, project)) +} diff --git a/src/project.rs b/src/project.rs new file mode 100644 index 0000000..c4df427 --- /dev/null +++ b/src/project.rs @@ -0,0 +1,12 @@ +#[derive(Clone, Eq, Hash, PartialEq)] +pub enum StatementKind +{ + Axiom, + Lemma, + Conjecture, +} + +pub struct Project +{ + pub(crate) statements: std::collections::HashMap>, +}