Use statement kind over section kind

This commit is contained in:
Patrick Lühne 2020-05-13 03:16:51 +02:00
parent 0dbf30bb1b
commit d35d0d1d98
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 130 additions and 78 deletions

View File

@ -1,31 +1,10 @@
mod proof_direction; mod proof_direction;
mod section_kind; mod section_kind;
mod statement;
pub use proof_direction::ProofDirection; pub use proof_direction::ProofDirection;
pub use section_kind::SectionKind; pub(crate) use section_kind::SectionKind;
pub(crate) use statement::{ProofStatus, Statement, StatementKind};
#[derive(Eq, PartialEq)]
pub enum StatementKind
{
Axiom,
CompletedDefinition(std::rc::Rc<foliage::PredicateDeclaration>),
IntegrityConstraint,
Assumption,
Lemma(ProofDirection),
Assertion,
}
#[derive(Copy, Clone, Eq, PartialEq)]
enum ProofStatus
{
AssumedProven,
Proven,
NotProven,
Disproven,
ToProveNow,
ToProveLater,
Ignored,
}
#[derive(Copy, Clone, Eq, PartialEq)] #[derive(Copy, Clone, Eq, PartialEq)]
pub enum ProofResult pub enum ProofResult
@ -35,15 +14,6 @@ pub enum ProofResult
Disproven, Disproven,
} }
pub struct Statement
{
kind: StatementKind,
name: Option<String>,
description: Option<String>,
formula: foliage::Formula,
proof_status: ProofStatus,
}
type VariableDeclarationIDs type VariableDeclarationIDs
= std::collections::BTreeMap::<std::rc::Rc<foliage::VariableDeclaration>, usize>; = std::collections::BTreeMap::<std::rc::Rc<foliage::VariableDeclaration>, usize>;
@ -58,33 +28,6 @@ struct FormatContext<'a, 'b>
pub variable_declaration_domains: &'b VariableDeclarationDomains, pub variable_declaration_domains: &'b VariableDeclarationDomains,
} }
impl Statement
{
pub fn new(kind: StatementKind, formula: foliage::Formula) -> Self
{
Self
{
kind,
name: None,
description: None,
formula,
proof_status: ProofStatus::ToProveLater,
}
}
pub fn with_name(mut self, name: String) -> Self
{
self.name = Some(name);
self
}
pub fn with_description(mut self, description: String) -> Self
{
self.description = Some(description);
self
}
}
type VariableDeclarationDomains type VariableDeclarationDomains
= std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>; = std::collections::BTreeMap<std::rc::Rc<foliage::VariableDeclaration>, crate::Domain>;
@ -131,7 +74,7 @@ impl Problem
} }
} }
pub fn add_statement(&self, section_kind: SectionKind, statement: Statement) pub(crate) fn add_statement(&self, section_kind: SectionKind, statement: Statement)
{ {
let mut statements = self.statements.borrow_mut(); let mut statements = self.statements.borrow_mut();
let section = statements.entry(section_kind).or_insert(vec![]); let section = statements.entry(section_kind).or_insert(vec![]);
@ -254,7 +197,7 @@ impl Problem
fn next_unproven_statement_do_mut<F, G>(&self, mut functor: F) -> Option<G> fn next_unproven_statement_do_mut<F, G>(&self, mut functor: F) -> Option<G>
where where
F: FnMut(SectionKind, &mut Statement) -> G, F: FnMut(&mut Statement) -> G,
{ {
for section in self.statements.borrow_mut().iter_mut() for section in self.statements.borrow_mut().iter_mut()
{ {
@ -263,7 +206,7 @@ impl Problem
if statement.proof_status == ProofStatus::ToProveNow if statement.proof_status == ProofStatus::ToProveNow
|| statement.proof_status == ProofStatus::ToProveLater || statement.proof_status == ProofStatus::ToProveLater
{ {
return Some(functor(*section.0, statement)); return Some(functor(statement));
} }
} }
} }
@ -283,7 +226,7 @@ impl Problem
variable_declaration_domains: &self.variable_declaration_domains.borrow(), variable_declaration_domains: &self.variable_declaration_domains.borrow(),
}; };
let display_statement = |section_kind: SectionKind, statement: &Statement, format_context| let display_statement = |statement: &Statement, format_context|
{ {
let step_title = match statement.proof_status let step_title = match statement.proof_status
{ {
@ -310,7 +253,7 @@ impl Problem
self.print_step_title(&step_title, &step_title_color); self.print_step_title(&step_title, &step_title_color);
self.shell.borrow_mut().print(&format!("{}: ", section_kind), self.shell.borrow_mut().print(&format!("{}: ", statement.kind),
&termcolor::ColorSpec::new()); &termcolor::ColorSpec::new());
match statement.kind match statement.kind
@ -325,12 +268,12 @@ impl Problem
}; };
// Show all statements that are assumed to be proven // Show all statements that are assumed to be proven
for (section_kind, statements) in self.statements.borrow_mut().iter_mut() for (_, statements) in self.statements.borrow_mut().iter_mut()
{ {
for statement in statements.iter_mut() for statement in statements.iter_mut()
.filter(|statement| statement.proof_status == ProofStatus::AssumedProven) .filter(|statement| statement.proof_status == ProofStatus::AssumedProven)
{ {
display_statement(*section_kind, statement, &format_context); display_statement(statement, &format_context);
println!(""); println!("");
} }
} }
@ -338,12 +281,12 @@ impl Problem
loop loop
{ {
match self.next_unproven_statement_do_mut( match self.next_unproven_statement_do_mut(
|section_kind, statement| |statement|
{ {
statement.proof_status = ProofStatus::ToProveNow; statement.proof_status = ProofStatus::ToProveNow;
print!("\x1b[s"); print!("\x1b[s");
display_statement(section_kind, statement, &format_context); display_statement(statement, &format_context);
print!("\x1b[u"); print!("\x1b[u");
use std::io::Write as _; use std::io::Write as _;
@ -369,7 +312,7 @@ impl Problem
Some(&["--mode", "casc", "--cores", "8", "--time_limit", "15"]))?; Some(&["--mode", "casc", "--cores", "8", "--time_limit", "15"]))?;
match self.next_unproven_statement_do_mut( match self.next_unproven_statement_do_mut(
|section_kind, statement| |statement|
{ {
statement.proof_status = match proof_result statement.proof_status = match proof_result
{ {
@ -380,7 +323,7 @@ impl Problem
self.shell.borrow_mut().erase_line(); self.shell.borrow_mut().erase_line();
display_statement(section_kind, statement, &format_context); display_statement(statement, &format_context);
match proof_result match proof_result
{ {
@ -531,9 +474,9 @@ impl Problem
for statement in statements.iter() for statement in statements.iter()
{ {
if let Some(ref description) = statement.description if let StatementKind::CompletedDefinition(_) = statement.kind
{ {
writeln!(formatter, "% {}", description)?; writeln!(formatter, "% {}", statement.kind)?;
} }
let name = match &statement.name let name = match &statement.name

112
src/problem/statement.rs Normal file
View File

@ -0,0 +1,112 @@
use super::ProofDirection;
#[derive(Eq, PartialEq)]
pub(crate) enum StatementKind
{
Axiom,
Assumption,
CompletedDefinition(std::rc::Rc<foliage::PredicateDeclaration>),
IntegrityConstraint,
Lemma(ProofDirection),
Assertion,
}
impl StatementKind
{
pub fn display_capitalized(&self) -> StatementKindCapitalizedDisplay
{
StatementKindCapitalizedDisplay(self)
}
}
impl std::fmt::Debug for StatementKind
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match self
{
Self::Axiom => write!(formatter, "axiom"),
Self::Assumption => write!(formatter, "assumption"),
Self::CompletedDefinition(ref predicate_declaration) =>
write!(formatter, "completed definition of {}", predicate_declaration),
Self::IntegrityConstraint => write!(formatter, "integrity constraint"),
Self::Lemma(_) => write!(formatter, "lemma"),
Self::Assertion => write!(formatter, "assertion"),
}
}
}
impl std::fmt::Display for StatementKind
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
pub(crate) struct StatementKindCapitalizedDisplay<'s>(&'s StatementKind);
impl<'s> std::fmt::Debug for StatementKindCapitalizedDisplay<'s>
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match self.0
{
StatementKind::Axiom => write!(formatter, "Axiom"),
StatementKind::Assumption => write!(formatter, "Assumption"),
StatementKind::CompletedDefinition(ref predicate_declaration) =>
write!(formatter, "Completed definition of {}", predicate_declaration),
StatementKind::IntegrityConstraint => write!(formatter, "Integrity constraint"),
StatementKind::Lemma(_) => write!(formatter, "Lemma"),
StatementKind::Assertion => write!(formatter, "Assertion"),
}
}
}
impl<'s> std::fmt::Display for StatementKindCapitalizedDisplay<'s>
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
#[derive(Copy, Clone, Eq, PartialEq)]
pub(crate) enum ProofStatus
{
AssumedProven,
Proven,
NotProven,
Disproven,
ToProveNow,
ToProveLater,
Ignored,
}
pub(crate) struct Statement
{
pub kind: StatementKind,
pub name: Option<String>,
pub formula: foliage::Formula,
pub proof_status: ProofStatus,
}
impl Statement
{
pub fn new(kind: StatementKind, formula: foliage::Formula) -> Self
{
Self
{
kind,
name: None,
formula,
proof_status: ProofStatus::ToProveLater,
}
}
pub fn with_name(mut self, name: String) -> Self
{
self.name = Some(name);
self
}
}

View File

@ -186,9 +186,7 @@ impl<'p> Translator<'p>
let statement = crate::problem::Statement::new(statement_kind, completed_definition) let statement = crate::problem::Statement::new(statement_kind, completed_definition)
.with_name(format!("completed_definition_{}_{}", predicate_declaration.name, .with_name(format!("completed_definition_{}_{}", predicate_declaration.name,
predicate_declaration.arity)) predicate_declaration.arity));
.with_description(format!("completed definition of {}/{}",
predicate_declaration.name, predicate_declaration.arity));
self.problem.add_statement(crate::problem::SectionKind::CompletedDefinitions, self.problem.add_statement(crate::problem::SectionKind::CompletedDefinitions,
statement); statement);
@ -327,8 +325,7 @@ impl<'p> Translator<'p>
let statement = crate::problem::Statement::new( let statement = crate::problem::Statement::new(
crate::problem::StatementKind::IntegrityConstraint, integrity_constraint) crate::problem::StatementKind::IntegrityConstraint, integrity_constraint)
.with_name("integrity_constraint".to_string()) .with_name("integrity_constraint".to_string());
.with_description("integrity constraint".to_string());
self.problem.add_statement(crate::problem::SectionKind::IntegrityConstraints, self.problem.add_statement(crate::problem::SectionKind::IntegrityConstraints,
statement); statement);