Add lemma directives
This commit is contained in:
parent
e933c45079
commit
2411781728
|
@ -12,6 +12,9 @@ impl std::fmt::Debug for crate::project::StatementKind
|
||||||
=> write!(format, "completion(constraint)"),
|
=> write!(format, "completion(constraint)"),
|
||||||
crate::project::StatementKind::Assumption => write!(format, "assumption"),
|
crate::project::StatementKind::Assumption => write!(format, "assumption"),
|
||||||
crate::project::StatementKind::Assertion => write!(format, "assertion"),
|
crate::project::StatementKind::Assertion => write!(format, "assertion"),
|
||||||
|
crate::project::StatementKind::Lemma(None) => write!(format, "lemma"),
|
||||||
|
crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Forward)) => write!(format, "lemma(forward)"),
|
||||||
|
crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Backward)) => write!(format, "lemma(backward)"),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,10 +1,3 @@
|
||||||
#[derive(Clone, Copy, Eq, Hash, PartialEq)]
|
|
||||||
pub enum ProofDirection
|
|
||||||
{
|
|
||||||
Forward,
|
|
||||||
Backward,
|
|
||||||
}
|
|
||||||
|
|
||||||
pub trait DisplayTPTP<'a, DisplayType>
|
pub trait DisplayTPTP<'a, DisplayType>
|
||||||
where DisplayType: 'a + std::fmt::Debug + std::fmt::Display
|
where DisplayType: 'a + std::fmt::Debug + std::fmt::Display
|
||||||
{
|
{
|
||||||
|
@ -12,12 +5,14 @@ pub trait DisplayTPTP<'a, 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
|
proof_direction: crate::project::ProofDirection) -> bool
|
||||||
{
|
{
|
||||||
match (proof_direction, statement_kind)
|
match (proof_direction, statement_kind)
|
||||||
{
|
{
|
||||||
(ProofDirection::Forward, crate::project::StatementKind::Assertion) => true,
|
(crate::project::ProofDirection::Forward, crate::project::StatementKind::Assertion) => true,
|
||||||
(ProofDirection::Backward, crate::project::StatementKind::Completion(_)) => true,
|
(crate::project::ProofDirection::Backward, crate::project::StatementKind::Completion(_)) => true,
|
||||||
|
(_, crate::project::StatementKind::Lemma(None)) => true,
|
||||||
|
(proof_direction, crate::project::StatementKind::Lemma(Some(proof_direction_lemma))) => proof_direction == *proof_direction_lemma,
|
||||||
_ => false,
|
_ => false,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -242,13 +237,13 @@ struct FormulaDisplay<'a>(&'a foliage::Formula);
|
||||||
struct StatementKindDisplay<'a>
|
struct StatementKindDisplay<'a>
|
||||||
{
|
{
|
||||||
statement_kind: &'a crate::project::StatementKind,
|
statement_kind: &'a crate::project::StatementKind,
|
||||||
proof_direction: ProofDirection,
|
proof_direction: crate::project::ProofDirection,
|
||||||
}
|
}
|
||||||
pub struct ProjectDisplay<'a>
|
pub struct ProjectDisplay<'a>
|
||||||
{
|
{
|
||||||
project: &'a crate::project::Project,
|
project: &'a crate::project::Project,
|
||||||
conjecture: &'a crate::project::Statement,
|
conjecture: &'a crate::project::Statement,
|
||||||
proof_direction: ProofDirection,
|
proof_direction: crate::project::ProofDirection,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration
|
impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration
|
||||||
|
@ -284,7 +279,7 @@ impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula
|
||||||
}
|
}
|
||||||
|
|
||||||
fn display_statement_kind_tptp<'a>(statement_kind: &'a crate::project::StatementKind,
|
fn display_statement_kind_tptp<'a>(statement_kind: &'a crate::project::StatementKind,
|
||||||
proof_direction: ProofDirection)
|
proof_direction: crate::project::ProofDirection)
|
||||||
-> StatementKindDisplay<'a>
|
-> StatementKindDisplay<'a>
|
||||||
{
|
{
|
||||||
StatementKindDisplay
|
StatementKindDisplay
|
||||||
|
@ -295,7 +290,7 @@ fn display_statement_kind_tptp<'a>(statement_kind: &'a crate::project::Statement
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project,
|
pub fn display_project_with_conjecture_tptp<'a>(project: &'a crate::Project,
|
||||||
conjecture: &'a crate::project::Statement, proof_direction: ProofDirection)
|
conjecture: &'a crate::project::Statement, proof_direction: crate::project::ProofDirection)
|
||||||
-> ProjectDisplay<'a>
|
-> ProjectDisplay<'a>
|
||||||
{
|
{
|
||||||
ProjectDisplay
|
ProjectDisplay
|
||||||
|
@ -588,10 +583,17 @@ impl<'a> std::fmt::Debug for StatementKindDisplay<'a>
|
||||||
{
|
{
|
||||||
(crate::project::StatementKind::Axiom, _) => write!(format, "axiom, axiom"),
|
(crate::project::StatementKind::Axiom, _) => write!(format, "axiom, axiom"),
|
||||||
(crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"),
|
(crate::project::StatementKind::Assumption, _) => write!(format, "assumption, axiom"),
|
||||||
(crate::project::StatementKind::Completion(_), ProofDirection::Forward) => write!(format, "completion, axiom"),
|
(crate::project::StatementKind::Completion(_), crate::project::ProofDirection::Forward) => write!(format, "completion, axiom"),
|
||||||
(crate::project::StatementKind::Completion(_), ProofDirection::Backward) => write!(format, "completion, conjecture"),
|
(crate::project::StatementKind::Completion(_), crate::project::ProofDirection::Backward) => write!(format, "completion, conjecture"),
|
||||||
(crate::project::StatementKind::Assertion, ProofDirection::Forward) => write!(format, "assertion, conjecture"),
|
(crate::project::StatementKind::Assertion, crate::project::ProofDirection::Forward) => write!(format, "assertion, conjecture"),
|
||||||
(crate::project::StatementKind::Assertion, ProofDirection::Backward) => write!(format, "assertion, axiom"),
|
(crate::project::StatementKind::Assertion, crate::project::ProofDirection::Backward) => write!(format, "assertion, axiom"),
|
||||||
|
(crate::project::StatementKind::Lemma(None), _) => write!(format, "lemma, conjecture"),
|
||||||
|
(crate::project::StatementKind::Lemma(Some(proof_direction_lemma)), proof_direction) =>
|
||||||
|
match proof_direction == *proof_direction_lemma
|
||||||
|
{
|
||||||
|
true => write!(format, "lemma, conjecture"),
|
||||||
|
false => Ok(()),
|
||||||
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
10
src/main.rs
10
src/main.rs
|
@ -20,7 +20,7 @@ fn backup_file_path(file_path: &std::path::Path) -> Result<std::path::PathBuf, a
|
||||||
}
|
}
|
||||||
|
|
||||||
fn find_conjecture<'a>(project: &'a ask_dracula::Project,
|
fn find_conjecture<'a>(project: &'a ask_dracula::Project,
|
||||||
proof_direction: ask_dracula::format_tptp::ProofDirection)
|
proof_direction: ask_dracula::project::ProofDirection)
|
||||||
-> Option<&'a ask_dracula::project::Statement>
|
-> Option<&'a ask_dracula::project::Statement>
|
||||||
{
|
{
|
||||||
for block in &project.blocks
|
for block in &project.blocks
|
||||||
|
@ -38,7 +38,7 @@ fn find_conjecture<'a>(project: &'a ask_dracula::Project,
|
||||||
}
|
}
|
||||||
|
|
||||||
fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project,
|
fn find_conjecture_mut<'a>(project: &'a mut ask_dracula::Project,
|
||||||
proof_direction: ask_dracula::format_tptp::ProofDirection)
|
proof_direction: ask_dracula::project::ProofDirection)
|
||||||
-> Option<&'a mut ask_dracula::project::Statement>
|
-> Option<&'a mut ask_dracula::project::Statement>
|
||||||
{
|
{
|
||||||
for block in &mut project.blocks
|
for block in &mut project.blocks
|
||||||
|
@ -149,9 +149,9 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|
|
||||||
let proof_directions = match matches.value_of("proof-direction").unwrap()
|
let proof_directions = match matches.value_of("proof-direction").unwrap()
|
||||||
{
|
{
|
||||||
"forward" => vec![ask_dracula::format_tptp::ProofDirection::Forward],
|
"forward" => vec![ask_dracula::project::ProofDirection::Forward],
|
||||||
"backward" => vec![ask_dracula::format_tptp::ProofDirection::Backward],
|
"backward" => vec![ask_dracula::project::ProofDirection::Backward],
|
||||||
"both" => vec![ask_dracula::format_tptp::ProofDirection::Forward, ask_dracula::format_tptp::ProofDirection::Backward],
|
"both" => vec![ask_dracula::project::ProofDirection::Forward, ask_dracula::project::ProofDirection::Backward],
|
||||||
proof_direction => panic!("unrecognized proof direction “{}”", proof_direction),
|
proof_direction => panic!("unrecognized proof direction “{}”", proof_direction),
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
23
src/parse.rs
23
src/parse.rs
|
@ -42,6 +42,11 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind>
|
||||||
|_| crate::project::StatementKind::Axiom,
|
|_| crate::project::StatementKind::Axiom,
|
||||||
),
|
),
|
||||||
map
|
map
|
||||||
|
(
|
||||||
|
tag("completion(constraint):"),
|
||||||
|
|_| crate::project::StatementKind::Completion(crate::project::CompletionTarget::Constraint),
|
||||||
|
),
|
||||||
|
map
|
||||||
(
|
(
|
||||||
preceded
|
preceded
|
||||||
(
|
(
|
||||||
|
@ -71,13 +76,23 @@ fn statement_kind(i: &str) -> IResult<&str, crate::project::StatementKind>
|
||||||
),
|
),
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
tag("completion(constraint):"),
|
tag("assumption:"),
|
||||||
|_| crate::project::StatementKind::Completion(crate::project::CompletionTarget::Constraint),
|
|_| crate::project::StatementKind::Assumption,
|
||||||
),
|
),
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
tag("assumption:"),
|
tag("lemma(forward):"),
|
||||||
|_| crate::project::StatementKind::Assumption,
|
|_| crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Forward)),
|
||||||
|
),
|
||||||
|
map
|
||||||
|
(
|
||||||
|
tag("lemma(backward):"),
|
||||||
|
|_| crate::project::StatementKind::Lemma(Some(crate::project::ProofDirection::Backward)),
|
||||||
|
),
|
||||||
|
map
|
||||||
|
(
|
||||||
|
tag("lemma:"),
|
||||||
|
|_| crate::project::StatementKind::Lemma(None),
|
||||||
),
|
),
|
||||||
map
|
map
|
||||||
(
|
(
|
||||||
|
|
|
@ -1,3 +1,10 @@
|
||||||
|
#[derive(Clone, Copy, Eq, Hash, PartialEq)]
|
||||||
|
pub enum ProofDirection
|
||||||
|
{
|
||||||
|
Forward,
|
||||||
|
Backward,
|
||||||
|
}
|
||||||
|
|
||||||
#[derive(Eq, Hash, PartialEq)]
|
#[derive(Eq, Hash, PartialEq)]
|
||||||
pub enum CompletionTarget
|
pub enum CompletionTarget
|
||||||
{
|
{
|
||||||
|
@ -10,6 +17,7 @@ pub enum StatementKind
|
||||||
{
|
{
|
||||||
Axiom,
|
Axiom,
|
||||||
Completion(CompletionTarget),
|
Completion(CompletionTarget),
|
||||||
|
Lemma(Option<ProofDirection>),
|
||||||
Assumption,
|
Assumption,
|
||||||
Assertion,
|
Assertion,
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue