diff --git a/1.pl b/1.pl index 4363d7e..4c0d8bc 100644 --- a/1.pl +++ b/1.pl @@ -7,3 +7,4 @@ add(X, s(Y), Z) :- add(s(X), Y, Z). mult(zero, X, zero). mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z). + diff --git a/src/main.rs b/src/main.rs index 0034206..ef05226 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(s(s(zero)), s(s(zero)), X)".into(); + let prop: Body = "mult(X, s(zero), s(zero))".into(); + //let prop: Body = "mult(X, Y, Z)".into(); //let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into(); for c in module.prove(&prop) { diff --git a/src/prover.rs b/src/prover.rs index 5aff903..4a4928e 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -1,4 +1,8 @@ +pub mod and; +pub mod body; pub mod constraints; +pub mod or; +pub mod predicate; pub mod tracing; pub mod unification; diff --git a/src/prover/and.rs b/src/prover/and.rs new file mode 100644 index 0000000..a7c9125 --- /dev/null +++ b/src/prover/and.rs @@ -0,0 +1,172 @@ +use std::fmt::Write; + +use owo_colors::OwoColorize; + +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::Counter; +use crate::prover::GlobalCounter; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::ProofType; +use crate::prover::tracing::Tracer; + +pub struct AndProver<'a, T: Tracer> +{ + module: &'a Module, + bodies: Vec, + tracer: T, + + global_counter: GlobalCounter, + sub_proofs: Vec<(Counter, BodyProver<'a>)>, +} +impl AndProver<'_, T> +{ + pub fn new<'a>( + module: &'a Module, + global_counter: GlobalCounter, + bodies: Vec, + constraints: Constraints, + tracer: &mut T, + ) -> AndProver<'a, T> + where + T: 'a, + { + assert!(!bodies.is_empty()); + + // Pretty logging + let mut tracer = tracer.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(" ∧ "); + } + } + + 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 { + module, + sub_proofs: vec![( + global_counter.snapshot(), + BodyProver::new( + module, + global_counter.clone(), + bodies[0].clone(), + constraints.clone(), + &mut tracer, + ), + )], + tracer, + bodies, + global_counter, + } + } +} +impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + if self.sub_proofs.is_empty() + { + return None; + } + + let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap(); + + match current_proof.next() + { + Some(constraints) => + { + if self.sub_proofs.len() == self.bodies.len() - 1 + { + self.sub_proofs.push((current_proof_snap, current_proof)); + Some(constraints) + } + else + { + // Pretty logging + let mut proved = String::new(); + let mut proving = String::new(); + let mut next = String::new(); + for (i, x) in self.bodies.iter().enumerate() + { + let dest; + if i == self.sub_proofs.len() + 1 + { + dest = &mut proving; + } + else if i < self.sub_proofs.len() + 1 + { + dest = &mut proved; + } + else + { + dest = &mut next; + } + let _ = dest.write_str(&format!("{}, ", x)); + } + 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 + + self.sub_proofs.push((current_proof_snap, current_proof)); + self.sub_proofs.push(( + self.global_counter.snapshot(), + BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.sub_proofs.len()].clone(), + constraints, + &mut self.tracer, + ), + )); + self.next() + } + } + None => + { + self.global_counter.restore(current_proof_snap); + self.next() + } + } + } +} diff --git a/src/prover/body.rs b/src/prover/body.rs new file mode 100644 index 0000000..3388d19 --- /dev/null +++ b/src/prover/body.rs @@ -0,0 +1,70 @@ +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::GlobalCounter; +use crate::prover::and::AndProver; +use crate::prover::constraints::Constraints; +use crate::prover::predicate::PredicateProver; +use crate::prover::tracing::Tracer; + +pub struct BodyProver<'a> +{ + prover: Box + 'a>, +} + +impl<'a> BodyProver<'a> +{ + pub fn new( + module: &'a Module, + global_counter: GlobalCounter, + body: Body, + constraints: Constraints, + tracer: &mut T, + ) -> BodyProver<'a> + { + let prover: Box> = match &body + { + Body::Term(predicate) => Box::new(PredicateProver::new( + module, + global_counter, + predicate.clone(), + 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, + items.clone(), + constraints.clone(), + tracer, + )), + Body::Or(items) => Box::new(BodyProver::new( + module, + global_counter, + items[0].clone(), + constraints.clone(), + tracer, + )), + }; + + BodyProver { prover } + } +} + +impl<'a> Iterator for BodyProver<'a> +{ + type Item = Constraints; + fn next(&mut self) -> Option + { + self.prover.next() + } +} diff --git a/src/prover/or.rs b/src/prover/or.rs new file mode 100644 index 0000000..e12f35b --- /dev/null +++ b/src/prover/or.rs @@ -0,0 +1,124 @@ +use std::fmt::Write; + +use crate::ast::Body; +use crate::ast::Module; +use crate::prover::Counter; +use crate::prover::GlobalCounter; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::ProofType; +use crate::prover::tracing::Tracer; + +pub struct OrProver<'a, T: Tracer> +{ + module: &'a Module, + bodies: Vec, + constraints: Constraints, + tracer: T, + + current_proving: usize, + global_counter: GlobalCounter, + counter_snapshot: Counter, + sub_proof: Option>, +} + +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 tracer = tracer.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 { + module, + sub_proof: Some(BodyProver::new( + module, + global_counter.clone(), + bodies[0].clone(), + constraints.clone(), + &mut tracer, + )), + tracer, + current_proving: 0, + counter_snapshot: global_counter.snapshot(), + bodies, + constraints, + global_counter, + } + } +} + +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.tracer + .print_step(format!("Tring with {}", self.bodies[self.current_proving])); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + self.bodies[self.current_proving].clone(), + self.constraints.clone(), + &mut self.tracer, + )); + self.next() + } + } + } + } +} diff --git a/src/prover/predicate.rs b/src/prover/predicate.rs new file mode 100644 index 0000000..5ae7edb --- /dev/null +++ b/src/prover/predicate.rs @@ -0,0 +1,132 @@ +use owo_colors::OwoColorize; +use owo_colors::colors::Green; + +use crate::ast::{Module, Predicate}; +use crate::prover::body::BodyProver; +use crate::prover::constraints::Constraints; +use crate::prover::tracing::{ProofType, Tracer}; +use crate::prover::{Counter, GlobalCounter}; + +pub struct PredicateProver<'a, T: Tracer> +{ + module: &'a Module, + predicate: Predicate, + constraints: Constraints, + counter_snapshot: Counter, + tracer: T, + + global_counter: GlobalCounter, + current_clause: usize, + sub_proof: Option>, +} + +impl<'a, T: Tracer + 'a> PredicateProver<'a, T> +{ + pub fn new( + module: &'a Module, + global_counter: GlobalCounter, + predicate: Predicate, + constraints: Constraints, + tracer: &mut T, + ) -> PredicateProver<'a, T> + { + //info!(target: "PredicateProver", "Proving {}", predicate); + let mut predicate_prover = tracer.begin_proof(ProofType::Predicate); + predicate_prover.print_step(format!( + "{} '{}'", + "Proving predicate".fg::(), + predicate + )); + PredicateProver { + module, + tracer: predicate_prover, + predicate, + constraints, + current_clause: 0, + sub_proof: None, + counter_snapshot: global_counter.snapshot(), + global_counter, + } + } +} + +impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> +{ + type Item = Constraints; + + fn next(&mut self) -> Option + { + match self.sub_proof.as_mut() + { + None => + { + if self.current_clause == self.module.clauses.len() + { + None + } + else + { + let clause = &self.module.clauses[self.current_clause] + .make_unique(self.global_counter.clone()); + let uni = self.predicate.matches(&clause.head); + let full_constraints = uni.and_then(|x| x.and(&self.constraints)); + + if let Some(c) = &full_constraints + { + 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() => + { + self.current_clause += 1; + Some(constraints) + } + Some(constraints) => + { + self.current_clause += 1; + self.counter_snapshot = self.global_counter.snapshot(); + self.sub_proof = Some(BodyProver::new( + self.module, + self.global_counter.clone(), + clause.body.clone().unwrap(), + constraints, + &mut self.tracer, + )); + self.next() + } + None => + { + self.global_counter.restore(self.counter_snapshot); + self.current_clause += 1; + self.next() + } + } + } + } + Some(prover) => + { + let next = prover.next(); + match next + { + Some(constraints) => Some(constraints), + None => + { + self.global_counter.restore(self.counter_snapshot); + self.sub_proof = None; + self.next() + } + } + } + } + } +} diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 51d90ca..f97400e 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -110,6 +110,8 @@ impl Tracer for IndentedTracer } self.first = false; println!("{}", show); + let _ = std::io::stdin().read_line(&mut String::new()); + println!("\x1b[2A"); } fn end_proof(self)