diff --git a/src/main.rs b/src/main.rs index d120503..d80f084 100644 --- a/src/main.rs +++ b/src/main.rs @@ -21,7 +21,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 = "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 fd52146..0f3187e 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -18,6 +18,7 @@ use crate::ast::Clause; use crate::ast::Module; use crate::ast::Predicate; use crate::prover::constraints::Constraints; +use crate::prover::tracing::IndentedTracer; use crate::prover::tracing::ProofType; use crate::prover::tracing::SimpleTracer; use crate::prover::tracing::Tracer; @@ -80,12 +81,26 @@ pub struct AndProver<'a, T: Tracer> bodies: Vec, constraints: Constraints, tracer: T, - current_tracer: Option, + current_tracer: T, global_counter: GlobalCounter, sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, } +pub struct OrProver<'a, T: Tracer> +{ + module: &'a Module, + bodies: Vec, + constraints: Constraints, + tracer: T, + current_tracer: T, + + current_proving: usize, + global_counter: GlobalCounter, + counter_snapshot: Counter, + sub_proof: Option>, +} + impl<'a, T: Tracer + 'a> BodyProver<'a, T> { pub fn new( @@ -93,7 +108,7 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T> global_counter: GlobalCounter, body: Body, constraints: Constraints, - tracer: &T, + tracer: &mut T, ) -> BodyProver<'a, T> { let body_tracer = if let Body::And(_) = body @@ -155,11 +170,11 @@ impl<'a, T: Tracer + 'a> PredicateProver<'a, T> global_counter: GlobalCounter, predicate: Predicate, constraints: Constraints, - tracer: &T, + tracer: &mut T, ) -> PredicateProver<'a, T> { //info!(target: "PredicateProver", "Proving {}", predicate); - let predicate_prover = tracer.begin_proof(ProofType::Predicate); + let mut predicate_prover = tracer.begin_proof(ProofType::Predicate); predicate_prover.print_step(format!( "{} '{}'", "Proving predicate".fg::(), @@ -185,16 +200,42 @@ impl AndProver<'_, T> global_counter: GlobalCounter, bodies: Vec, constraints: Constraints, - tracer: &T, + tracer: &mut T, ) -> AndProver<'a, T> where T: 'a, { 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 next = String::new(); + for x in bodies.iter().skip(1) + { + let _ = next.write_str(&format!("{}, ", x)); + } + + let mut conjuction = String::new(); + let len = bodies.len(); + for (i, x) in bodies.iter().enumerate() + { + let _ = conjuction.write_str(&format!("{}", x)); + if i != len - 1 + { + let _ = conjuction.write_str(" ∧ "); + } + } + + 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())); + // End pretty logging + AndProver { - tracer: tracer.begin_proof(ProofType::And), - current_tracer: None, + tracer: whole_trace, module, sub_proofs: vec![( global_counter.snapshot(), @@ -203,9 +244,67 @@ impl AndProver<'_, T> global_counter.clone(), bodies[0].clone(), constraints.clone(), - tracer, + &mut current_tracer, ), )], + current_tracer, + bodies, + constraints, + global_counter, + } + } +} + +impl OrProver<'_, T> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + bodies: Vec, + constraints: Constraints, + tracer: &mut T, + ) -> OrProver<'a, T> + where + T: 'a, + { + 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 next = String::new(); + for x in bodies.iter().skip(1) + { + let _ = next.write_str(&format!("{}, ", x)); + } + + let mut disjunction = String::new(); + let len = bodies.len(); + for (i, x) in bodies.iter().enumerate() + { + let _ = disjunction.write_str(&format!("{}", x)); + if i != len - 1 + { + let _ = disjunction.write_str(" ∨ "); + } + } + + // 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, + )), + current_proving: 0, + counter_snapshot: global_counter.snapshot(), + current_tracer, bodies, constraints, global_counter, @@ -232,24 +331,22 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> let clause = &self.module.clauses[self.current_clause] .make_unique(self.global_counter.clone()); //info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause); - self.tracer.print_step(format!( - "🭆 Unifying '{}' aginst '{}'", - self.predicate, clause - )); let uni = self.predicate.matches(&clause.head); let full_constraints = uni.and_then(|x| x.and(&self.constraints)); if let Some(c) = &full_constraints { - //info!(target: "PredicateProver", " => {}", c); - self.tracer - .print_step(format!("🭧 ↳ {}: {}", "Matches".fg::(), c)); - } - else - { - self.tracer - .print_step(format!("🭧 ↳ {}", "Contradictory".fg::())); + self.tracer.print_step(format!( + "Unifying '{}' aginst '{}'", + self.predicate, clause + )); + self.tracer.print_step(format!( + "↳ {}: {}", + "Matches".fg::(), + c.simplified() + )); } + match full_constraints { Some(constraints) if clause.body.is_none() => @@ -266,12 +363,13 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> self.global_counter.clone(), clause.body.clone().unwrap(), constraints, - &self.tracer, + &mut self.tracer, )); self.next() } None => { + self.global_counter.restore(self.counter_snapshot); self.current_clause += 1; self.next() } @@ -330,34 +428,41 @@ 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(); + self.current_tracer = self.tracer.begin_proof(ProofType::And); + let mut proved = String::new(); + let mut proving = String::new(); + let mut next = String::new(); for (i, x) in self.bodies.iter().enumerate() { - let mut color = Style::new(); - if i == self.sub_proofs.len() - 1 + let dest; + if i == self.sub_proofs.len() + 1 { - color = color.fg::(); + dest = &mut proving; } - else if i < self.sub_proofs.len() - 1 + else if i < self.sub_proofs.len() + 1 { - color = color.fg::(); + dest = &mut proved; } else { - color = color.fg::(); + dest = &mut next; } - let _ = output.write_str(&format!("{}, ", x.style(color))); + let _ = dest.write_str(&format!("{}, ", x)); } - self.current_tracer.as_ref().unwrap().print_step(output); - + self.current_tracer.print_step(format!( + "{} : {}", + "Proved".fg::(), + proved + )); + self.current_tracer.print_step(format!( + "{} : {}", + "Proving".fg::(), + proving + )); + self.current_tracer + .print_step(format!("{} : {}", "Next".fg::(), next)); // End pretty logging + self.sub_proofs.push((current_proof_snap, current_proof)); self.sub_proofs.push(( self.global_counter.snapshot(), @@ -366,7 +471,7 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> self.global_counter.clone(), self.bodies[self.sub_proofs.len()].clone(), constraints, - &self.tracer, + &mut self.current_tracer, ), )); self.next() @@ -381,16 +486,61 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> } } +impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + let proof = match &mut self.sub_proof + { + Some(sub_proof) => sub_proof.next(), + None => + { + return None; + } + }; + + match proof + { + Some(x) => Some(x), + None => + { + // Advance to next possibility + if self.current_proving == self.bodies.len() - 1 + { + self.sub_proof = None; + None + } + else + { + self.current_proving += 1; + self.global_counter.restore(self.counter_snapshot); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.current_proving].clone(), + self.constraints.clone(), + &mut self.current_tracer, + )); + self.next() + } + } + } + } +} + impl Module { - pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, SimpleTracer> + pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, impl Tracer> { BodyProver::new( self, GlobalCounter::new(), body.clone(), Constraints::none(), - &SimpleTracer::new(ProofType::Body), + &mut IndentedTracer::new(), + //&SimpleTracer::new(ProofType::Body), ) } } diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 47ccfbf..6e7c6d0 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,7 +1,10 @@ -use std::{default, fmt::Display}; +use std::{cell::RefCell, default, fmt::Display, rc::Rc}; use log::info; -use owo_colors::{OwoColorize, colors::css::Gray}; +use owo_colors::{ + OwoColorize, Style, + colors::css::{DarkGray, Gray}, +}; use crate::ast::Variable; @@ -28,8 +31,8 @@ impl Display for ProofType pub trait Tracer { - fn begin_proof(&self, proof_type: ProofType) -> Self; - fn print_step(&self, show: T); + fn begin_proof(&mut self, proof_type: ProofType) -> Self; + fn print_step(&mut self, show: T); fn end_proof(self); } @@ -48,12 +51,12 @@ impl SimpleTracer impl Tracer for SimpleTracer { - fn begin_proof(&self, proof_type: ProofType) -> Self + fn begin_proof(&mut self, proof_type: ProofType) -> Self { SimpleTracer { proof_type } } - fn print_step(&self, show: T) + fn print_step(&mut self, show: T) { let str = format!("{}", self.proof_type); info!(target: &str, "{}", show); @@ -65,6 +68,77 @@ impl Tracer for SimpleTracer } } +pub struct IndentedTracer +{ + first: bool, + depth: usize, +} + +impl IndentedTracer +{ + pub fn new() -> IndentedTracer + { + IndentedTracer { + first: true, + depth: 0, + } + } +} + +impl Tracer for IndentedTracer +{ + fn begin_proof(&mut self, _proof_type: ProofType) -> Self + { + IndentedTracer { + first: true, + depth: self.depth + 1, + } + } + + fn print_step(&mut self, show: T) + { + for i in 0..self.depth + { + let style = if i % 2 == 0 + { + Style::new().fg::() + } + else + { + Style::new().fg::() + }; + if i == self.depth - 1 && self.first + { + print!("{}", "🭋".style(style)); + } + else + { + print!("{}", "▐".style(style)); + } + } + self.first = false; + println!("{}", show); + } + + fn end_proof(self) + { + drop(self); + } +} + +impl Drop for IndentedTracer +{ + fn drop(&mut self) {} +} + +impl Default for IndentedTracer +{ + fn default() -> Self + { + Self::new() + } +} + pub fn colored_var(var: &Variable) -> String { let mut idx = None; diff --git a/src/tracing.rs b/src/tracing.rs deleted file mode 100644 index e69de29..0000000