Refactor proof output

This commit is contained in:
Patrick Lühne 2020-05-11 03:11:10 +02:00
parent e03628ec66
commit 17d2373e0d
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 74 additions and 92 deletions

View File

@ -1,3 +1,7 @@
mod section_kind;
pub use section_kind::SectionKind;
#[derive(Copy, Clone, Eq, PartialEq)] #[derive(Copy, Clone, Eq, PartialEq)]
pub enum StatementKind pub enum StatementKind
{ {
@ -72,17 +76,6 @@ impl Statement
} }
} }
#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)]
pub enum SectionKind
{
CompletedDefinitions,
IntegrityConstraints,
Axioms,
Assumptions,
Lemmas,
Assertions,
}
type VariableDeclarationDomains type VariableDeclarationDomains
= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>; = std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
@ -133,17 +126,6 @@ impl Problem
pub fn prove(&self, proof_direction: crate::ProofDirection) -> Result<(), crate::Error> pub fn prove(&self, proof_direction: crate::ProofDirection) -> Result<(), crate::Error>
{ {
// TODO: refactor
let format_context = FormatContext
{
program_variable_declaration_ids:
std::cell::RefCell::new(VariableDeclarationIDs::new()),
integer_variable_declaration_ids:
std::cell::RefCell::new(VariableDeclarationIDs::new()),
input_constant_declaration_domains: &self.input_constant_declaration_domains.borrow(),
variable_declaration_domains: &self.variable_declaration_domains.borrow(),
};
if proof_direction == crate::ProofDirection::Forward if proof_direction == crate::ProofDirection::Forward
|| proof_direction == crate::ProofDirection::Both || proof_direction == crate::ProofDirection::Both
{ {
@ -152,7 +134,7 @@ impl Problem
let mut statements = self.statements.borrow_mut(); let mut statements = self.statements.borrow_mut();
// Initially reset all proof statuses // Initially reset all proof statuses
for (section_kind, statements) in statements.iter_mut() for (_, statements) in statements.iter_mut()
{ {
for statement in statements.iter_mut() for statement in statements.iter_mut()
{ {
@ -161,31 +143,7 @@ impl Problem
StatementKind::Axiom StatementKind::Axiom
| StatementKind::Assumption | StatementKind::Assumption
| StatementKind::Program => | StatementKind::Program =>
{ statement.proof_status = ProofStatus::AssumedProven,
// TODO: avoid code duplication
let statement_type_output = match section_kind
{
SectionKind::CompletedDefinitions => "completed definition",
SectionKind::IntegrityConstraints => "integrity constraint",
SectionKind::Axioms => "axiom",
SectionKind::Assumptions => "assumption",
SectionKind::Lemmas => "lemma",
SectionKind::Assertions => "assertion",
};
// TODO: refactor
match statement.kind
{
StatementKind::Program => println!(" - {}: {}",
statement_type_output,
foliage::format::display_formula(&statement.formula,
&format_context)),
_ => println!(" - {}: {}", statement_type_output,
statement.formula),
}
statement.proof_status = ProofStatus::AssumedProven;
},
StatementKind::Lemma(crate::ProofDirection::Backward) => StatementKind::Lemma(crate::ProofDirection::Backward) =>
statement.proof_status = ProofStatus::Ignored, statement.proof_status = ProofStatus::Ignored,
_ => statement.proof_status = ProofStatus::ToProveLater, _ => statement.proof_status = ProofStatus::ToProveLater,
@ -208,7 +166,7 @@ impl Problem
let mut statements = self.statements.borrow_mut(); let mut statements = self.statements.borrow_mut();
// Initially reset all proof statuses // Initially reset all proof statuses
for (section_kind, statements) in statements.iter_mut() for (_, statements) in statements.iter_mut()
{ {
for statement in statements.iter_mut() for statement in statements.iter_mut()
{ {
@ -217,31 +175,7 @@ impl Problem
StatementKind::Axiom StatementKind::Axiom
| StatementKind::Assumption | StatementKind::Assumption
| StatementKind::Assertion => | StatementKind::Assertion =>
{ statement.proof_status = ProofStatus::AssumedProven,
// TODO: avoid code duplication
let statement_type_output = match section_kind
{
SectionKind::CompletedDefinitions => "completed definition",
SectionKind::IntegrityConstraints => "integrity constraint",
SectionKind::Axioms => "axiom",
SectionKind::Assumptions => "assumption",
SectionKind::Lemmas => "lemma",
SectionKind::Assertions => "assertion",
};
// TODO: refactor
match statement.kind
{
StatementKind::Program => println!(" - {}: {}",
statement_type_output,
foliage::format::display_formula(&statement.formula,
&format_context)),
_ => println!(" - {}: {}", statement_type_output,
statement.formula),
}
statement.proof_status = ProofStatus::AssumedProven;
},
StatementKind::Lemma(crate::ProofDirection::Forward) => StatementKind::Lemma(crate::ProofDirection::Forward) =>
statement.proof_status = ProofStatus::Ignored, statement.proof_status = ProofStatus::Ignored,
_ => statement.proof_status = ProofStatus::ToProveLater, _ => statement.proof_status = ProofStatus::ToProveLater,
@ -290,6 +224,36 @@ impl Problem
variable_declaration_domains: &self.variable_declaration_domains.borrow(), variable_declaration_domains: &self.variable_declaration_domains.borrow(),
}; };
let display_statement = |section_kind, statement: &Statement, format_context|
{
let proof_status_output = match statement.proof_status
{
ProofStatus::AssumedProven => "",
ProofStatus::ToProveNow => "verifying ",
ProofStatus::ToProveLater => "not yet verifying ",
ProofStatus::Ignored => "ignoring ",
};
match statement.kind
{
StatementKind::Program =>
println!(" - {}{}: {}", proof_status_output, section_kind,
foliage::format::display_formula(&statement.formula, format_context)),
_ =>
println!(" - {}{}: {}", proof_status_output, section_kind, statement.formula),
}
};
// Show all statements that are assumed to be proven
for (section_kind, statements) in self.statements.borrow_mut().iter_mut()
{
for statement in statements.iter_mut()
.filter(|statement| statement.proof_status == ProofStatus::AssumedProven)
{
display_statement(*section_kind, statement, &format_context);
}
}
loop loop
{ {
match self.next_unproven_statement_do_mut( match self.next_unproven_statement_do_mut(
@ -297,27 +261,11 @@ impl Problem
{ {
statement.proof_status = ProofStatus::ToProveNow; statement.proof_status = ProofStatus::ToProveNow;
let statement_type_output = match section_kind display_statement(section_kind, statement, &format_context);
{
SectionKind::CompletedDefinitions => "completed definition",
SectionKind::IntegrityConstraints => "integrity constraint",
SectionKind::Axioms => "axiom",
SectionKind::Assumptions => "assumption",
SectionKind::Lemmas => "lemma",
SectionKind::Assertions => "assertion",
};
match statement.kind
{
StatementKind::Program => println!(" - verifying {}: {}",
statement_type_output,
foliage::format::display_formula(&statement.formula, &format_context)),
_ => println!(" - verifying {}: {}", statement_type_output,
statement.formula),
}
}) })
{ {
Some(_) => (), Some(_) => (),
// If there are no more unproven statements left, were done
None => break, None => break,
} }

View File

@ -0,0 +1,34 @@
#[derive(Clone, Copy, Eq, Ord, PartialEq, PartialOrd)]
pub enum SectionKind
{
CompletedDefinitions,
IntegrityConstraints,
Axioms,
Assumptions,
Lemmas,
Assertions,
}
impl std::fmt::Debug for SectionKind
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match self
{
Self::CompletedDefinitions => write!(formatter, "completed definition"),
Self::IntegrityConstraints => write!(formatter, "integrity constraint"),
Self::Axioms => write!(formatter, "axiom"),
Self::Assumptions => write!(formatter, "assumption"),
Self::Lemmas => write!(formatter, "lemma"),
Self::Assertions => write!(formatter, "assertion"),
}
}
}
impl std::fmt::Display for SectionKind
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}