Putting provers in separate files
This commit is contained in:
1
1.pl
1
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).
|
||||
|
||||
|
||||
|
||||
@ -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)
|
||||
{
|
||||
|
||||
@ -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;
|
||||
|
||||
|
||||
172
src/prover/and.rs
Normal file
172
src/prover/and.rs
Normal file
@ -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<Body>,
|
||||
tracer: T,
|
||||
|
||||
global_counter: GlobalCounter,
|
||||
sub_proofs: Vec<(Counter, BodyProver<'a>)>,
|
||||
}
|
||||
impl<T: Tracer> AndProver<'_, T>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
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::<owo_colors::colors::Green>(),));
|
||||
tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Proving".fg::<owo_colors::colors::Yellow>(),
|
||||
bodies[0]
|
||||
));
|
||||
tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Next".fg::<owo_colors::colors::Red>(),
|
||||
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<Self::Item>
|
||||
{
|
||||
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::<owo_colors::colors::Green>(),
|
||||
proved
|
||||
));
|
||||
self.tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Proving".fg::<owo_colors::colors::Yellow>(),
|
||||
proving
|
||||
));
|
||||
self.tracer.print_step(format!(
|
||||
"{} : {}",
|
||||
"Next".fg::<owo_colors::colors::Red>(),
|
||||
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()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
70
src/prover/body.rs
Normal file
70
src/prover/body.rs
Normal file
@ -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<dyn Iterator<Item = Constraints> + 'a>,
|
||||
}
|
||||
|
||||
impl<'a> BodyProver<'a>
|
||||
{
|
||||
pub fn new<T: Tracer + 'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
body: Body,
|
||||
constraints: Constraints,
|
||||
tracer: &mut T,
|
||||
) -> BodyProver<'a>
|
||||
{
|
||||
let prover: Box<dyn Iterator<Item = Constraints>> = 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<Constraints>
|
||||
{
|
||||
self.prover.next()
|
||||
}
|
||||
}
|
||||
124
src/prover/or.rs
Normal file
124
src/prover/or.rs
Normal file
@ -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<Body>,
|
||||
constraints: Constraints,
|
||||
tracer: T,
|
||||
|
||||
current_proving: usize,
|
||||
global_counter: GlobalCounter,
|
||||
counter_snapshot: Counter,
|
||||
sub_proof: Option<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
impl<T: Tracer> OrProver<'_, T>
|
||||
{
|
||||
pub fn new<'a>(
|
||||
module: &'a Module,
|
||||
global_counter: GlobalCounter,
|
||||
bodies: Vec<Body>,
|
||||
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<Self::Item>
|
||||
{
|
||||
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()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
132
src/prover/predicate.rs
Normal file
132
src/prover/predicate.rs
Normal file
@ -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<BodyProver<'a>>,
|
||||
}
|
||||
|
||||
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::<Green>(),
|
||||
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<Self::Item>
|
||||
{
|
||||
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::<Green>(),
|
||||
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()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -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)
|
||||
|
||||
Reference in New Issue
Block a user