diff --git a/1.pl b/1.pl index 4c0d8bc..29e751f 100644 --- a/1.pl +++ b/1.pl @@ -1,10 +1,22 @@ +:- use_module(library(clpfd)). + entier(zero). entier(s(X)) :- entier(X). add(X, zero, X). add(X, s(Y), Z) :- add(s(X), Y, Z). +inf(zero, X) :- entier(X). +inf(s(X), s(Y)) :- inf(X, Y). + mult(zero, X, zero). mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z). +div(A, B) :- inf(A, B), inf(X, B), mult(X, A, B). +div_w(X, Y) :- inf(s(X), Y), inf(s(s(zero)), X), div(X, Y). +prime(X) :- entier(X), \+ div_w(_, X). + +peano(X, zero) :- X #= 0. +peano(X, s(P)) :- X #> 0, X #= Y + 1, peano(Y, P). + diff --git a/src/prover.rs b/src/prover.rs index 4a4928e..70022f2 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -1,20 +1,16 @@ pub mod and; pub mod body; pub mod constraints; +pub mod not; pub mod or; pub mod predicate; pub mod tracing; pub mod unification; use std::cell::Cell; -use std::fmt::Write; use std::rc::Rc; use litemap::LiteMap; -use owo_colors::OwoColorize; -use owo_colors::colors::Green; -use owo_colors::colors::Red; -use owo_colors::colors::Yellow; use crate::ast::Body; use crate::ast::Clause; @@ -22,8 +18,6 @@ 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::Tracer; #[derive(Clone, Copy, Debug, Default)] pub struct Counter(usize); @@ -56,452 +50,6 @@ impl GlobalCounter } } -pub struct BodyProver<'a> -{ - prover: Box + 'a>, -} - -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>, -} - -pub struct AndProver<'a, T: Tracer> -{ - module: &'a Module, - bodies: Vec, - tracer: T, - - global_counter: GlobalCounter, - sub_proofs: Vec<(Counter, BodyProver<'a>)>, -} - -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<'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, 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 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 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 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() - } - } - } - } - } -} - -impl<'a> Iterator for BodyProver<'a> -{ - type Item = Constraints; - fn next(&mut self) -> Option - { - self.prover.next() - } -} - -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() - } - } - } -} - -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() - } - } - } - } -} - impl Module { pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a> diff --git a/src/prover/not.rs b/src/prover/not.rs new file mode 100644 index 0000000..8fa41ed --- /dev/null +++ b/src/prover/not.rs @@ -0,0 +1,71 @@ +use crate::ast::Body; +use crate::ast::Module; +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 NotProver<'a, T: Tracer + 'a> +{ + prover: Option>, + constraints: Constraints, + tracer: T, +} + +impl<'a, T: Tracer + 'a> NotProver<'a, T> +{ + pub fn new( + module: &'a Module, + global_counter: GlobalCounter, + body: Body, + constraints: Constraints, + tracer: &mut T, + ) -> NotProver<'a, T> + { + let mut not_tracer = tracer.begin_proof(ProofType::Body); + NotProver { + prover: Some(BodyProver::new( + module, + global_counter, + body, + constraints.clone(), + &mut not_tracer, + )), + tracer: not_tracer, + constraints: constraints.clone(), + } + } +} + +impl<'a, T: Tracer + 'a> Iterator for NotProver<'a, T> +{ + type Item = Constraints; + fn next(&mut self) -> Option + { + if let Some(x) = self.prover.as_mut() + { + match &mut x.next() + { + Some(_) => + { + // The prover showed that the proof is true. + // Thus the negation is never true + self.prover = None; + None + } + None => + { + // The prover did not find any proof + // Thus the negation is true + self.prover = None; + Some(self.constraints.clone()) + } + } + } + else + { + None + } + } +}