Initial project file parser

.gitignore

@@ -0,0 +1,3 @@
+/target
+**/*.rs.bk
+Cargo.lock

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "foliage"]
+	path = foliage
+	url = ../foliage-rs.git

Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "ask_dracula"
+version = "0.1.0"
+authors = ["Patrick Lühne <patrick@luehne.de>"]
+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"

foliage

@@ -0,0 +1 @@
+Subproject commit a6fe4b9e0881fc1707fd6c83e419857ad8a653eb

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)
+	}
+}

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)
+	}
+}

src/lib.rs

@@ -0,0 +1,6 @@
+pub mod format;
+pub mod format_tptp;
+pub mod parse;
+mod project;
+
+pub use project::Project;

src/main.rs

@@ -0,0 +1,24 @@
+use ask_dracula::format_tptp::DisplayTPTP;
+
+fn main() -> Result<(), Box<dyn std::error::Error>>
+{
+	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(())
+}

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))
+}

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<StatementKind, Vec<foliage::Formula>>,
+}