diff --git a/Cargo.toml b/Cargo.toml index ba18db6..4cc43fb 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,11 +5,13 @@ authors = ["Patrick Lühne "] edition = "2018" [dependencies] +atty = "0.2" foliage = {git = "https://github.com/pluehne/foliage", branch = "parser-new"} log = "0.4" pretty_env_logger = "0.4" regex = "1" structopt = "0.3" +termcolor = "1.1" [dependencies.clingo] git = "https://github.com/potassco/clingo-rs" diff --git a/src/output.rs b/src/output.rs index 6f5aedb..e097a73 100644 --- a/src/output.rs +++ b/src/output.rs @@ -1,5 +1,8 @@ +pub(crate) mod shell; pub(crate) mod tptp; +pub(crate) use shell::Shell; + #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] pub enum Format { diff --git a/src/output/shell.rs b/src/output/shell.rs new file mode 100644 index 0000000..bc4ba87 --- /dev/null +++ b/src/output/shell.rs @@ -0,0 +1,126 @@ +pub struct Shell +{ + output: ShellOutput, +} + +enum ShellOutput +{ + Basic(Box), + WithColorSupport + { + stream: termcolor::StandardStream, + color_choice: ColorChoice, + is_a_tty: bool, + }, +} + +#[derive(Clone, Copy, Eq, PartialEq)] +pub enum ColorChoice +{ + Always, + Never, + Auto, +} + +impl Shell +{ + pub fn from_stdout() -> Self + { + Self + { + output: ShellOutput::WithColorSupport + { + stream: + termcolor::StandardStream::stdout(ColorChoice::Auto.to_termcolor_color_choice()), + color_choice: ColorChoice::Auto, + is_a_tty: atty::is(atty::Stream::Stdout), + }, + } + } + + pub fn print(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec) + -> std::io::Result<()> + { + self.output.print(text, color) + } + + pub fn println(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec) + -> std::io::Result<()> + { + self.output.println(text, color) + } + + pub fn erase_line(&mut self) + { + self.output.erase_line(); + } +} + +impl ShellOutput +{ + fn print(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec) + -> std::io::Result<()> + { + use std::io::Write as _; + use termcolor::WriteColor as _; + + match *self + { + Self::Basic(ref mut write) => write!(write, "{}", text), + Self::WithColorSupport{ref mut stream, ..} => + { + stream.reset()?; + stream.set_color(color)?; + + write!(stream, "{}", text)?; + + stream.reset() + }, + } + } + + fn println(&mut self, text: &dyn std::fmt::Display, color: &termcolor::ColorSpec) + -> std::io::Result<()> + { + self.print(text, color)?; + + use std::io::Write as _; + + match *self + { + Self::Basic(ref mut write) => writeln!(write, ""), + Self::WithColorSupport{ref mut stream, ..} => writeln!(stream, ""), + } + } + + #[cfg(unix)] + pub fn erase_line(&mut self) + { + let erase_sequence = b"\x1b[2K"; + + use std::io::Write as _; + + let _ = match *self + { + Self::Basic(ref mut write) => write.write_all(erase_sequence), + Self::WithColorSupport{ref mut stream, ..} => stream.write_all(erase_sequence), + }; + } +} + +impl ColorChoice +{ + fn to_termcolor_color_choice(self) -> termcolor::ColorChoice + { + match self + { + Self::Always => termcolor::ColorChoice::Always, + Self::Never => termcolor::ColorChoice::Never, + Self::Auto => match atty::is(atty::Stream::Stdout) + { + true => termcolor::ColorChoice::Auto, + false => termcolor::ColorChoice::Never, + }, + } + } +} diff --git a/src/problem.rs b/src/problem.rs index cce171a..8ffd863 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -18,6 +18,9 @@ pub enum StatementKind enum ProofStatus { AssumedProven, + Proven, + NotProven, + Disproven, ToProveNow, ToProveLater, Ignored, @@ -96,6 +99,8 @@ pub struct Problem pub input_predicate_declarations: std::cell::RefCell, // TODO: clean up as variable declarations are dropped variable_declaration_domains: std::cell::RefCell, + + shell: std::cell::RefCell, } impl Problem @@ -117,6 +122,8 @@ impl Problem std::cell::RefCell::new(foliage::PredicateDeclarations::new()), variable_declaration_domains: std::cell::RefCell::new(VariableDeclarationDomains::new()), + + shell: std::cell::RefCell::new(crate::output::Shell::from_stdout()), } } @@ -128,12 +135,25 @@ impl Problem section.push(statement); } + fn print_step_title(&self, step_title: &str, color: &termcolor::ColorSpec) + { + let longest_possible_key = " Finished"; + + self.shell.borrow_mut().print( + &format!("{:>step_title_width$} ", step_title, + step_title_width = longest_possible_key.chars().count()), + color); + } + pub fn prove(&self, proof_direction: ProofDirection) -> Result<(), crate::Error> { if proof_direction == ProofDirection::Forward || proof_direction == ProofDirection::Both { - println!("Verifying assertions from completed definitions"); + self.print_step_title("Started", + termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green))); + self.shell.borrow_mut().println(&"verification of assertions from completed definitions", + &termcolor::ColorSpec::new()); let mut statements = self.statements.borrow_mut(); @@ -157,10 +177,20 @@ impl Problem drop(statements); - self.prove_unproven_statements()?; + let proof_result = self.prove_unproven_statements()?; - print_step_title("Finished proof"); - println!(""); + let mut step_title_color = termcolor::ColorSpec::new(); + step_title_color.set_bold(true); + + match proof_result + { + ProofResult::Proven => step_title_color.set_fg(Some(termcolor::Color::Green)), + ProofResult::NotProven => step_title_color.set_fg(Some(termcolor::Color::Yellow)), + ProofResult::Disproven => step_title_color.set_fg(Some(termcolor::Color::Red)), + }; + + self.print_step_title("Finished", &step_title_color); + println!("verification of assertions from completed definitions"); } if proof_direction == ProofDirection::Both @@ -171,7 +201,10 @@ impl Problem if proof_direction == ProofDirection::Backward || proof_direction == ProofDirection::Both { - println!("Verifying completed definitions from assertions"); + self.print_step_title("Started", + termcolor::ColorSpec::new().set_bold(true).set_fg(Some(termcolor::Color::Green))); + self.shell.borrow_mut().println(&"verification of completed definitions from assertions", + &termcolor::ColorSpec::new()); let mut statements = self.statements.borrow_mut(); @@ -195,10 +228,20 @@ impl Problem drop(statements); - self.prove_unproven_statements()?; + let proof_result = self.prove_unproven_statements()?; - print_step_title("Finished proof"); - println!(""); + let mut step_title_color = termcolor::ColorSpec::new(); + step_title_color.set_bold(true); + + match proof_result + { + ProofResult::Proven => step_title_color.set_fg(Some(termcolor::Color::Green)), + ProofResult::NotProven => step_title_color.set_fg(Some(termcolor::Color::Yellow)), + ProofResult::Disproven => step_title_color.set_fg(Some(termcolor::Color::Red)), + }; + + self.print_step_title("Finished", &step_title_color); + println!("verification of completed definitions from assertions"); } Ok(()) @@ -223,7 +266,7 @@ impl Problem None } - fn prove_unproven_statements(&self) -> Result<(), crate::Error> + fn prove_unproven_statements(&self) -> Result { let format_context = FormatContext { @@ -239,21 +282,39 @@ impl Problem { let step_title = match statement.proof_status { - ProofStatus::AssumedProven => format!("{}", section_kind.display_capitalized()), - ProofStatus::ToProveNow => format!("Verifying {}", section_kind), - ProofStatus::ToProveLater => format!("Skipping {}", section_kind), - ProofStatus::Ignored => format!("Ignoring {}", section_kind), + ProofStatus::AssumedProven => format!("Established"), + ProofStatus::Proven => format!("Verified"), + ProofStatus::NotProven + | ProofStatus::Disproven + | ProofStatus::ToProveNow => format!("Verifying"), + ProofStatus::ToProveLater => format!("Skipped"), + ProofStatus::Ignored => format!("Ignored"), }; - print_step_title(&step_title); + let mut step_title_color = termcolor::ColorSpec::new(); + step_title_color.set_bold(true); + + match statement.proof_status + { + ProofStatus::AssumedProven + | ProofStatus::Proven => step_title_color.set_fg(Some(termcolor::Color::Green)), + ProofStatus::NotProven => step_title_color.set_fg(Some(termcolor::Color::Yellow)), + ProofStatus::Disproven => step_title_color.set_fg(Some(termcolor::Color::Red)), + _ => step_title_color.set_fg(Some(termcolor::Color::Cyan)), + }; + + self.print_step_title(&step_title, &step_title_color); + + self.shell.borrow_mut().print(&format!("{}: ", section_kind), + &termcolor::ColorSpec::new()); match statement.kind { StatementKind::Program => - println!("{}", + print!("{}", foliage::format::display_formula(&statement.formula, format_context)), _ => - println!("{}", statement.formula), + print!("{}", statement.formula), } }; @@ -264,6 +325,7 @@ impl Problem .filter(|statement| statement.proof_status == ProofStatus::AssumedProven) { display_statement(*section_kind, statement, &format_context); + println!(""); } } @@ -274,7 +336,12 @@ impl Problem { statement.proof_status = ProofStatus::ToProveNow; + print!("\x1b[s"); display_statement(section_kind, statement, &format_context); + print!("\x1b[u"); + + use std::io::Write as _; + std::io::stdout().flush(); }) { Some(_) => (), @@ -293,50 +360,49 @@ impl Problem // TODO: make configurable again let (proof_result, proof_time_seconds) = run_vampire(&tptp_problem_to_prove_next_statement, - Some(&["--mode", "casc", "--cores", "8", "--time_limit", "300"]))?; - - match proof_result - { - ProofResult::NotProven => - { - print_step_title(""); - println!("⌛ could not prove statement"); - - return Ok(()); - }, - ProofResult::Disproven => - { - print_step_title(""); - println!("× statement disproven"); - - return Ok(()); - }, - _ => (), - } + Some(&["--mode", "casc", "--cores", "8", "--time_limit", "15"]))?; match self.next_unproven_statement_do_mut( - |_, statement| statement.proof_status = ProofStatus::AssumedProven) + |section_kind, statement| + { + statement.proof_status = match proof_result + { + ProofResult::Proven => ProofStatus::Proven, + ProofResult::NotProven => ProofStatus::NotProven, + ProofResult::Disproven => ProofStatus::Disproven, + }; + + self.shell.borrow_mut().erase_line(); + + display_statement(section_kind, statement, &format_context); + + match proof_result + { + ProofResult::Proven => (), + ProofResult::NotProven => print!(" (not proven)"), + ProofResult::Disproven => print!(" (disproven)"), + } + + if let Some(proof_time_seconds) = proof_time_seconds + { + self.shell.borrow_mut().print(&format!(" in {} seconds", proof_time_seconds), + termcolor::ColorSpec::new().set_fg(Some(termcolor::Color::Black)).set_intense(true)); + } + }) { Some(_) => (), - None => unreachable!("could not set the statement to proven"), + None => unreachable!(), } - match proof_time_seconds + self.shell.borrow_mut().println(&"", &termcolor::ColorSpec::new()); + + if proof_result != ProofResult::Proven { - None => - { - print_step_title(""); - println!("✓ statement proven"); - }, - Some(proof_time_seconds) => - { - print_step_title(""); - println!("✓ statement proven in {} seconds", proof_time_seconds); - }, + return Ok(proof_result); } } - Ok(()) + Ok(ProofResult::Proven) } fn write_tptp_problem_to_prove_next_statement(&self, formatter: &mut String) -> std::fmt::Result @@ -476,7 +542,10 @@ impl Problem let statement_type = match statement.proof_status { - ProofStatus::AssumedProven => "axiom", + ProofStatus::AssumedProven + | ProofStatus::Proven => "axiom", + ProofStatus::NotProven + | ProofStatus::Disproven => unreachable!(), ProofStatus::ToProveNow => "conjecture", // Skip statements that will be proven later ProofStatus::ToProveLater => continue, @@ -673,13 +742,6 @@ impl<'a, 'b> foliage::format::Format for FormatContext<'a, 'b> } } -fn print_step_title(title: &str) -{ - let longest_possible_key = "Verifying completed definition"; - - print!("{:>title_width$} ", title, title_width = longest_possible_key.chars().count()) -} - fn run_vampire(input: &str, arguments: Option) -> Result<(ProofResult, Option), crate::Error> where