diff --git a/src/main.rs b/src/main.rs index d80f084..0034206 100644 --- a/src/main.rs +++ b/src/main.rs @@ -21,8 +21,8 @@ fn main() .into(); //let prop: Body = "integer(s(X))".into(); - //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); + //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); for c in module.prove(&prop) { println!("true:"); diff --git a/src/prover.rs b/src/prover.rs index 8c95c4f..5aff903 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -75,7 +75,6 @@ pub struct AndProver<'a, T: Tracer> module: &'a Module, bodies: Vec, tracer: T, - current_tracer: T, global_counter: GlobalCounter, sub_proofs: Vec<(Counter, BodyProver<'a>)>, @@ -87,7 +86,6 @@ pub struct OrProver<'a, T: Tracer> bodies: Vec, constraints: Constraints, tracer: T, - current_tracer: T, current_proving: usize, global_counter: GlobalCounter, @@ -189,8 +187,7 @@ impl AndProver<'_, T> assert!(!bodies.is_empty()); // Pretty logging - let mut whole_trace = tracer.begin_proof(ProofType::And); - let mut current_tracer = whole_trace.begin_proof(ProofType::And); + let mut tracer = tracer.begin_proof(ProofType::And); let mut next = String::new(); for x in bodies.iter().skip(1) { @@ -208,15 +205,14 @@ impl AndProver<'_, T> } } - current_tracer.print_step(format!("Proving conjuction {}", conjuction)); - current_tracer.print_step(format!("{} :", "Proved".fg::(),)); - current_tracer.print_step(format!("{} : {}", "Proving".fg::(), bodies[0])); - current_tracer.print_step(format!("{} : {}", "Next".fg::(), next)); - current_tracer.print_step(format!("With constraints : {}", constraints.simplified())); + tracer.print_step(format!("Proving conjuction {}", conjuction)); + tracer.print_step(format!("{} :", "Proved".fg::(),)); + tracer.print_step(format!("{} : {}", "Proving".fg::(), bodies[0])); + tracer.print_step(format!("{} : {}", "Next".fg::(), next)); + tracer.print_step(format!("With constraints : {}", constraints.simplified())); // End pretty logging AndProver { - tracer: whole_trace, module, sub_proofs: vec![( global_counter.snapshot(), @@ -225,10 +221,10 @@ impl AndProver<'_, T> global_counter.clone(), bodies[0].clone(), constraints.clone(), - &mut current_tracer, + &mut tracer, ), )], - current_tracer, + tracer, bodies, global_counter, } @@ -250,8 +246,7 @@ impl OrProver<'_, T> assert!(!bodies.is_empty()); // Pretty logging - let mut whole_trace = tracer.begin_proof(ProofType::And); - let mut current_tracer = whole_trace.begin_proof(ProofType::And); + let mut tracer = tracer.begin_proof(ProofType::And); let mut next = String::new(); for x in bodies.iter().skip(1) @@ -273,18 +268,17 @@ impl OrProver<'_, T> // End pretty logging OrProver { - tracer: whole_trace, module, sub_proof: Some(BodyProver::new( module, global_counter.clone(), bodies[0].clone(), constraints.clone(), - &mut current_tracer, + &mut tracer, )), + tracer, current_proving: 0, counter_snapshot: global_counter.snapshot(), - current_tracer, bodies, constraints, global_counter, @@ -407,7 +401,6 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> else { // Pretty logging - self.current_tracer = self.tracer.begin_proof(ProofType::And); let mut proved = String::new(); let mut proving = String::new(); let mut next = String::new(); @@ -428,17 +421,11 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> } let _ = dest.write_str(&format!("{}, ", x)); } - self.current_tracer.print_step(format!( - "{} : {}", - "Proved".fg::(), - proved - )); - self.current_tracer.print_step(format!( - "{} : {}", - "Proving".fg::(), - proving - )); - self.current_tracer + self.tracer + .print_step(format!("{} : {}", "Proved".fg::(), proved)); + self.tracer + .print_step(format!("{} : {}", "Proving".fg::(), proving)); + self.tracer .print_step(format!("{} : {}", "Next".fg::(), next)); // End pretty logging @@ -450,7 +437,7 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> self.global_counter.clone(), self.bodies[self.sub_proofs.len()].clone(), constraints, - &mut self.current_tracer, + &mut self.tracer, ), )); self.next() @@ -502,7 +489,7 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> self.global_counter.clone(), self.bodies[self.current_proving].clone(), self.constraints.clone(), - &mut self.current_tracer, + &mut self.tracer, )); self.next() } diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 60ea6f5..51d90ca 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -106,14 +106,7 @@ impl Tracer for IndentedTracer { Style::new().fg::() }; - if i == self.depth - 1 && self.first - { - print!("{}", "🭋".style(style)); - } - else - { - print!("{}", "▐".style(style)); - } + print!("{}", "│".style(style)); } self.first = false; println!("{}", show);