diff --git a/src/problem.rs b/src/problem.rs index e9263c7..fe8aaeb 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -1,31 +1,10 @@ mod proof_direction; mod section_kind; +mod statement; pub use proof_direction::ProofDirection; -pub use section_kind::SectionKind; - -#[derive(Eq, PartialEq)] -pub enum StatementKind -{ - Axiom, - CompletedDefinition(std::rc::Rc), - IntegrityConstraint, - Assumption, - Lemma(ProofDirection), - Assertion, -} - -#[derive(Copy, Clone, Eq, PartialEq)] -enum ProofStatus -{ - AssumedProven, - Proven, - NotProven, - Disproven, - ToProveNow, - ToProveLater, - Ignored, -} +pub(crate) use section_kind::SectionKind; +pub(crate) use statement::{ProofStatus, Statement, StatementKind}; #[derive(Copy, Clone, Eq, PartialEq)] pub enum ProofResult @@ -35,15 +14,6 @@ pub enum ProofResult Disproven, } -pub struct Statement -{ - kind: StatementKind, - name: Option, - description: Option, - formula: foliage::Formula, - proof_status: ProofStatus, -} - type VariableDeclarationIDs = std::collections::BTreeMap::, usize>; @@ -58,33 +28,6 @@ struct FormatContext<'a, 'b> 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 = std::collections::BTreeMap, 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 section = statements.entry(section_kind).or_insert(vec![]); @@ -254,7 +197,7 @@ impl Problem fn next_unproven_statement_do_mut(&self, mut functor: F) -> Option where - F: FnMut(SectionKind, &mut Statement) -> G, + F: FnMut(&mut Statement) -> G, { for section in self.statements.borrow_mut().iter_mut() { @@ -263,7 +206,7 @@ impl Problem if statement.proof_status == ProofStatus::ToProveNow || 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(), }; - let display_statement = |section_kind: SectionKind, statement: &Statement, format_context| + let display_statement = |statement: &Statement, format_context| { let step_title = match statement.proof_status { @@ -310,7 +253,7 @@ impl Problem 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()); match statement.kind @@ -325,12 +268,12 @@ impl Problem }; // 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() .filter(|statement| statement.proof_status == ProofStatus::AssumedProven) { - display_statement(*section_kind, statement, &format_context); + display_statement(statement, &format_context); println!(""); } } @@ -338,12 +281,12 @@ impl Problem loop { match self.next_unproven_statement_do_mut( - |section_kind, statement| + |statement| { statement.proof_status = ProofStatus::ToProveNow; print!("\x1b[s"); - display_statement(section_kind, statement, &format_context); + display_statement(statement, &format_context); print!("\x1b[u"); use std::io::Write as _; @@ -369,7 +312,7 @@ impl Problem Some(&["--mode", "casc", "--cores", "8", "--time_limit", "15"]))?; match self.next_unproven_statement_do_mut( - |section_kind, statement| + |statement| { statement.proof_status = match proof_result { @@ -380,7 +323,7 @@ impl Problem self.shell.borrow_mut().erase_line(); - display_statement(section_kind, statement, &format_context); + display_statement(statement, &format_context); match proof_result { @@ -531,9 +474,9 @@ impl Problem 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 diff --git a/src/problem/statement.rs b/src/problem/statement.rs new file mode 100644 index 0000000..3cc2788 --- /dev/null +++ b/src/problem/statement.rs @@ -0,0 +1,112 @@ +use super::ProofDirection; + +#[derive(Eq, PartialEq)] +pub(crate) enum StatementKind +{ + Axiom, + Assumption, + CompletedDefinition(std::rc::Rc), + 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, + 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 + } +} diff --git a/src/translate/verify_properties.rs b/src/translate/verify_properties.rs index b03426e..25d74a8 100644 --- a/src/translate/verify_properties.rs +++ b/src/translate/verify_properties.rs @@ -186,9 +186,7 @@ impl<'p> Translator<'p> let statement = crate::problem::Statement::new(statement_kind, completed_definition) .with_name(format!("completed_definition_{}_{}", predicate_declaration.name, - predicate_declaration.arity)) - .with_description(format!("completed definition of {}/{}", - predicate_declaration.name, predicate_declaration.arity)); + predicate_declaration.arity)); self.problem.add_statement(crate::problem::SectionKind::CompletedDefinitions, statement); @@ -327,8 +325,7 @@ impl<'p> Translator<'p> let statement = crate::problem::Statement::new( crate::problem::StatementKind::IntegrityConstraint, integrity_constraint) - .with_name("integrity_constraint".to_string()) - .with_description("integrity constraint".to_string()); + .with_name("integrity_constraint".to_string()); self.problem.add_statement(crate::problem::SectionKind::IntegrityConstraints, statement);