diff --git a/src/main.rs b/src/main.rs index 9b537fa..d120503 100644 --- a/src/main.rs +++ b/src/main.rs @@ -20,8 +20,8 @@ fn main() " .into(); - let prop: Body = "integer(s(X))".into(); - //let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); + //let prop: Body = "integer(s(X))".into(); + let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into(); for c in module.prove(&prop) { println!("true:"); diff --git a/src/prover.rs b/src/prover.rs index 9208a3d..fd52146 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -3,14 +3,15 @@ pub mod tracing; pub mod unification; use std::cell::Cell; +use std::fmt::Write; use std::rc::Rc; use litemap::LiteMap; -use log::info; use owo_colors::OwoColorize; +use owo_colors::Style; use owo_colors::colors::Green; use owo_colors::colors::Red; -use owo_colors::colors::css::Gray; +use owo_colors::colors::Yellow; use crate::ast::Body; use crate::ast::Clause; @@ -79,6 +80,7 @@ pub struct AndProver<'a, T: Tracer> bodies: Vec, constraints: Constraints, tracer: T, + current_tracer: Option, global_counter: GlobalCounter, sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, @@ -111,6 +113,16 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T> constraints.clone(), tracer, )), + + // Shortcut And & Or prover if it contains only one element to simplify proofs + Body::And(items) | Body::Or(items) if items.len() == 1 => Box::new(BodyProver::new( + module, + global_counter, + items[0].clone(), + constraints.clone(), + tracer, + )), + Body::And(items) => Box::new(AndProver::new( module, global_counter, @@ -182,6 +194,7 @@ impl AndProver<'_, T> AndProver { tracer: tracer.begin_proof(ProofType::And), + current_tracer: None, module, sub_proofs: vec![( global_counter.snapshot(), @@ -316,6 +329,35 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> } else { + // Pretty logging + self.current_tracer = Some(self.tracer.begin_proof(ProofType::And)); + self.current_tracer.as_ref().unwrap().print_step(format!( + "And. {} {} {} :", + "Proved".fg::(), + "Proving".fg::(), + "Left".fg::() + )); + let mut output = String::new(); + for (i, x) in self.bodies.iter().enumerate() + { + let mut color = Style::new(); + if i == self.sub_proofs.len() - 1 + { + color = color.fg::(); + } + else if i < self.sub_proofs.len() - 1 + { + color = color.fg::(); + } + else + { + color = color.fg::(); + } + let _ = output.write_str(&format!("{}, ", x.style(color))); + } + self.current_tracer.as_ref().unwrap().print_step(output); + + // End pretty logging self.sub_proofs.push((current_proof_snap, current_proof)); self.sub_proofs.push(( self.global_counter.snapshot(), diff --git a/src/tracing.rs b/src/tracing.rs new file mode 100644 index 0000000..e69de29