From e933c45079f01143631eb5e0881d028e58e02e78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 6 Nov 2019 21:20:06 -0600 Subject: [PATCH] Tag completion directives with source --- foliage | 2 +- src/format.rs | 6 +++++- src/format_tptp.rs | 35 +++++++++++++++++------------------ src/main.rs | 4 ++-- src/parse.rs | 33 +++++++++++++++++++++++++++++++-- src/project.rs | 11 +++++++++-- 6 files changed, 65 insertions(+), 26 deletions(-) diff --git a/foliage b/foliage index 8870cee..7af51e9 160000 --- a/foliage +++ b/foliage @@ -1 +1 @@ -Subproject commit 8870cee1793571a313ac4f0948e4d73c5589e671 +Subproject commit 7af51e9e64947a16f7f9c5c7923b77a8862139b5 diff --git a/src/format.rs b/src/format.rs index c4fbd57..3f71646 100644 --- a/src/format.rs +++ b/src/format.rs @@ -5,7 +5,11 @@ impl std::fmt::Debug for crate::project::StatementKind match &self { crate::project::StatementKind::Axiom => write!(format, "axiom"), - crate::project::StatementKind::Completion => write!(format, "completion"), + crate::project::StatementKind::Completion( + crate::project::CompletionTarget::Predicate(predicate_declaration)) + => write!(format, "completion({}/{})", predicate_declaration.name, predicate_declaration.arity), + crate::project::StatementKind::Completion(crate::project::CompletionTarget::Constraint) + => write!(format, "completion(constraint)"), crate::project::StatementKind::Assumption => write!(format, "assumption"), crate::project::StatementKind::Assertion => write!(format, "assertion"), } diff --git a/src/format_tptp.rs b/src/format_tptp.rs index a6e1cc2..eae4ecf 100644 --- a/src/format_tptp.rs +++ b/src/format_tptp.rs @@ -11,15 +11,14 @@ pub trait DisplayTPTP<'a, DisplayType> fn display_tptp(&'a self) -> DisplayType; } -pub fn is_statement_kind_conjecture(statement_kind: crate::project::StatementKind, +pub fn is_statement_kind_conjecture(statement_kind: &crate::project::StatementKind, proof_direction: ProofDirection) -> bool { - match proof_direction + match (proof_direction, statement_kind) { - ProofDirection::Forward => - statement_kind == crate::project::StatementKind::Assertion, - ProofDirection::Backward => - statement_kind == crate::project::StatementKind::Completion, + (ProofDirection::Forward, crate::project::StatementKind::Assertion) => true, + (ProofDirection::Backward, crate::project::StatementKind::Completion(_)) => true, + _ => false, } } @@ -240,9 +239,9 @@ struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration); struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration); struct TermDisplay<'a>(&'a foliage::Term); struct FormulaDisplay<'a>(&'a foliage::Formula); -struct StatementKindDisplay +struct StatementKindDisplay<'a> { - statement_kind: crate::project::StatementKind, + statement_kind: &'a crate::project::StatementKind, proof_direction: ProofDirection, } pub struct ProjectDisplay<'a> @@ -284,9 +283,9 @@ impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula } } -fn display_statement_kind_tptp(statement_kind: crate::project::StatementKind, +fn display_statement_kind_tptp<'a>(statement_kind: &'a crate::project::StatementKind, proof_direction: ProofDirection) - -> StatementKindDisplay + -> StatementKindDisplay<'a> { StatementKindDisplay { @@ -581,23 +580,23 @@ impl<'a> std::fmt::Display for FormulaDisplay<'a> } } -impl std::fmt::Debug for StatementKindDisplay +impl<'a> std::fmt::Debug for StatementKindDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { - match (self.statement_kind, self.proof_direction) + match (&self.statement_kind, self.proof_direction) { (crate::project::StatementKind::Axiom, _) => write!(format, "axiom, axiom"), (crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"), - (crate::project::StatementKind::Completion, ProofDirection::Forward) => write!(format, "completion, axiom"), - (crate::project::StatementKind::Completion, ProofDirection::Backward) => write!(format, "completion, conjecture"), + (crate::project::StatementKind::Completion(_), ProofDirection::Forward) => write!(format, "completion, axiom"), + (crate::project::StatementKind::Completion(_), ProofDirection::Backward) => write!(format, "completion, conjecture"), (crate::project::StatementKind::Assertion, ProofDirection::Forward) => write!(format, "assertion, conjecture"), (crate::project::StatementKind::Assertion, ProofDirection::Backward) => write!(format, "assertion, axiom"), } } } -impl std::fmt::Display for StatementKindDisplay +impl<'a> std::fmt::Display for StatementKindDisplay<'a> { fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -651,7 +650,7 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> { crate::project::Block::Whitespace(_) => None, crate::project::Block::Statement(ref statement) => - match is_statement_kind_conjecture(statement.kind, self.proof_direction) + match is_statement_kind_conjecture(&statement.kind, self.proof_direction) { false => Some(statement), true => None, @@ -661,13 +660,13 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a> for axiom in axioms { write!(format, "\ntff({:?}, {:?}).", - display_statement_kind_tptp(axiom.kind, self.proof_direction), axiom.formula.display_tptp())?; + display_statement_kind_tptp(&axiom.kind, self.proof_direction), axiom.formula.display_tptp())?; } write_title(format, "\n\n", "assertion")?; write!(format, "\ntff({:?}, {:?}).", - display_statement_kind_tptp(self.conjecture.kind, self.proof_direction), self.conjecture.formula.display_tptp())?; + display_statement_kind_tptp(&self.conjecture.kind, self.proof_direction), self.conjecture.formula.display_tptp())?; Ok(()) } diff --git a/src/main.rs b/src/main.rs index 94d15b6..511a92c 100644 --- a/src/main.rs +++ b/src/main.rs @@ -27,7 +27,7 @@ fn find_conjecture<'a>(project: &'a ask_dracula::Project, { if let ask_dracula::project::Block::Statement(ref statement) = block { - if ask_dracula::format_tptp::is_statement_kind_conjecture(statement.kind, proof_direction) + if ask_dracula::format_tptp::is_statement_kind_conjecture(&statement.kind, proof_direction) { return Some(statement) } @@ -45,7 +45,7 @@ fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project, { if let ask_dracula::project::Block::Statement(ref mut statement) = block { - if ask_dracula::format_tptp::is_statement_kind_conjecture(statement.kind, proof_direction) + if ask_dracula::format_tptp::is_statement_kind_conjecture(&statement.kind, proof_direction) { return Some(statement) } diff --git a/src/parse.rs b/src/parse.rs index 4fbb691..7d5307d 100644 --- a/src/parse.rs +++ b/src/parse.rs @@ -3,6 +3,7 @@ use nom:: IResult, sequence::{delimited, pair, preceded, terminated, tuple}, combinator::{map, recognize}, + character::complete::digit1, branch::alt, bytes::complete::tag, }; @@ -42,8 +43,36 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind> ), map ( - tag("completion:"), - |_| crate::project::StatementKind::Completion, + preceded + ( + tag("completion"), + delimited + ( + tag("("), + pair + ( + terminated + ( + foliage::parse::symbolic_identifier, + tag("/"), + ), + digit1, + ), + tag("):"), + ), + ), + |(name, arity)| + match arity.parse::() + { + Ok(arity) => crate::project::StatementKind::Completion( + crate::project::CompletionTarget::Predicate(foliage::PredicateDeclaration{name, arity})), + Err(error) => panic!("invalid arity “{}”: {}", arity, error), + } + ), + map + ( + tag("completion(constraint):"), + |_| crate::project::StatementKind::Completion(crate::project::CompletionTarget::Constraint), ), map ( diff --git a/src/project.rs b/src/project.rs index e6b5a89..b85c5c1 100644 --- a/src/project.rs +++ b/src/project.rs @@ -1,8 +1,15 @@ -#[derive(Clone, Copy, Eq, Hash, PartialEq)] +#[derive(Eq, Hash, PartialEq)] +pub enum CompletionTarget +{ + Predicate(foliage::PredicateDeclaration), + Constraint, +} + +#[derive(Eq, Hash, PartialEq)] pub enum StatementKind { Axiom, - Completion, + Completion(CompletionTarget), Assumption, Assertion, }