patrick
/
ask-dracula-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add completion, assumption, and assertion directives

This commit is contained in:
Patrick Lühne 2019-11-06 00:18:30 -06:00
parent beb4dbb693
commit 3bf78115cf
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
5 changed files with 36 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/format.rs
View File

@ -5,8 +5,9 @@ impl std::fmt::Debug for crate::project::StatementKind
match &self
{
crate::project::StatementKind::Axiom => write!(format, "axiom"),
crate::project::StatementKind::Lemma => write!(format, "lemma"),
crate::project::StatementKind::Conjecture => write!(format, "conjecture"),
crate::project::StatementKind::Completion => write!(format, "completion"),
crate::project::StatementKind::Assumption => write!(format, "assumption"),
crate::project::StatementKind::Assertion => write!(format, "assertion"),
}
}
}

45
src/format_tptp.rs
View File

@ -78,12 +78,7 @@ fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project)
match block
{
crate::project::Block::Whitespace(_) => None,
crate::project::Block::Statement(ref statement) =>
match statement.kind
{
crate::project::StatementKind::Axiom => Some(&statement.formula),
_ => None,
}
crate::project::Block::Statement(ref statement) => Some(&statement.formula),
});
for formula in formulas
@ -211,12 +206,7 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project)
match block
{
crate::project::Block::Whitespace(_) => None,
crate::project::Block::Statement(ref statement) =>
match statement.kind
{
crate::project::StatementKind::Axiom => Some(&statement.formula),
_ => None,
}
crate::project::Block::Statement(ref statement) => Some(&statement.formula),
});
for formula in formulas
@ -565,8 +555,9 @@ impl<'a> std::fmt::Debug for StatementKindDisplay<'a>
match &self.0
{
crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"),
crate::project::StatementKind::Lemma => write!(format, "lemma, conjecture"),
crate::project::StatementKind::Conjecture => write!(format, "conjecture, conjecture"),
crate::project::StatementKind::Completion => write!(format, "completion, axiom"),
crate::project::StatementKind::Assumption => write!(format, "assumption, axiom"),
crate::project::StatementKind::Assertion => write!(format, "assertion, conjecture"),
}
}
}
@ -627,35 +618,31 @@ impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input>
crate::project::Block::Statement(ref statement) =>
match statement.kind
{
crate::project::StatementKind::Axiom => Some(statement),
_ => None,
crate::project::StatementKind::Axiom
| crate::project::StatementKind::Completion
| crate::project::StatementKind::Assumption => Some(statement),
crate::project::StatementKind::Assertion => None,
}
});
for axiom in axioms
{
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Axiom.display_tptp(), axiom.formula.display_tptp())?;
write!(format, "\ntff({:?}, {:?}).", axiom.kind.display_tptp(), axiom.formula.display_tptp())?;
}
match self.conjecture.kind
{
crate::project::StatementKind::Lemma =>
crate::project::StatementKind::Assertion =>
{
write_title(format, "\n\n", "lemma")?;
write_title(format, "\n\n", "assertion")?;
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), self.conjecture.formula.display_tptp())?;
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Assertion.display_tptp(), self.conjecture.formula.display_tptp())?;
Ok(())
},
crate::project::StatementKind::Conjecture =>
{
write_title(format, "\n\n", "conjecture")?;
write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), self.conjecture.formula.display_tptp())?;
Ok(())
},
crate::project::StatementKind::Axiom => panic!("unexpected axiom"),
crate::project::StatementKind::Axiom => panic!("unexpected axiom statement"),
crate::project::StatementKind::Completion => panic!("unexpected completion statement"),
crate::project::StatementKind::Assumption => panic!("unexpected assumption statement"),
}
}
}

12
src/main.rs
View File

@ -25,8 +25,7 @@ fn find_conjecture<'a, 'input>(project: &'a ask_dracula::Project<'input>) -> Opt
{
if let ask_dracula::project::Block::Statement(ref statement) = block
{
if statement.kind == ask_dracula::project::StatementKind::Lemma
|| statement.kind == ask_dracula::project::StatementKind::Conjecture
if statement.kind == ask_dracula::project::StatementKind::Assertion
{
return Some(statement)
}
@ -42,8 +41,7 @@ fn find_conjecture_mut<'a, 'input>(project: &'a mut ask_dracula::Project<'input>
{
if let ask_dracula::project::Block::Statement(ref mut statement) = block
{
if statement.kind == ask_dracula::project::StatementKind::Lemma
|| statement.kind == ask_dracula::project::StatementKind::Conjecture
if statement.kind == ask_dracula::project::StatementKind::Assertion
{
return Some(statement)
}
@ -142,7 +140,7 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
{
None =>
{
eprintln!("no lemma or conjecture found, nothing to do");
eprintln!("nothing to prove, exiting");
return Ok(());
},
Some(ref conjecture) =>
@ -166,10 +164,10 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
},
ProofResult::Refutation =>
{
println!("conjecture proven");
println!("assertion proven");
conjecture.kind = ask_dracula::project::StatementKind::Axiom;
let replace_statement_kind_regex = regex::Regex::new(r"(conjecture|lemma)").unwrap();
let replace_statement_kind_regex = regex::Regex::new(r"(assertion)").unwrap();
let new_text = replace_statement_kind_regex.replace(conjecture.original_text, "axiom");
conjecture.original_text = &new_text;

13
src/parse.rs
View File

@ -42,13 +42,18 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind>
),
map
(
tag("lemma:"),
|_| crate::project::StatementKind::Lemma,
tag("completion:"),
|_| crate::project::StatementKind::Completion,
),
map
(
tag("conjecture:"),
|_| crate::project::StatementKind::Conjecture,
tag("assumption:"),
|_| crate::project::StatementKind::Assumption,
),
map
(
tag("assertion:"),
|_| crate::project::StatementKind::Assertion,
),
)),
whitespace0,

5
src/project.rs
View File

@ -2,8 +2,9 @@
pub enum StatementKind
{
Axiom,
Lemma,
Conjecture,
Completion,
Assumption,
Assertion,
}
pub struct Statement<'input>