octagonal/picolog
1
1
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Removes all warnings

Browse Source
This commit is contained in:
Albin Chaboissier
2026-02-09 22:38:23 +01:00
parent 5b9df71704
commit c920ef8d99
4 changed files with 15 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

45
src/prover.rs
View File

@ -8,7 +8,6 @@ use std::rc::Rc;
use litemap::LiteMap;
use owo_colors::OwoColorize;
use owo_colors::Style;
use owo_colors::colors::Green;
use owo_colors::colors::Red;
use owo_colors::colors::Yellow;
@ -20,7 +19,6 @@ 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;
#[derive(Clone, Copy, Debug, Default)]
@ -54,11 +52,8 @@ impl GlobalCounter
}
}
pub struct BodyProver<'a, T: Tracer + 'a>
pub struct BodyProver<'a>
{
module: &'a Module,
constraints: Constraints,
tracer: Option<T>,
prover: Box<dyn Iterator<Item = Constraints> + 'a>,
}
@ -72,19 +67,18 @@ pub struct PredicateProver<'a, T: Tracer>
global_counter: GlobalCounter,
current_clause: usize,
sub_proof: Option<BodyProver<'a, T>>,
sub_proof: Option<BodyProver<'a>>,
}
pub struct AndProver<'a, T: Tracer>
{
module: &'a Module,
bodies: Vec<Body>,
constraints: Constraints,
tracer: T,
current_tracer: T,
global_counter: GlobalCounter,
sub_proofs: Vec<(Counter, BodyProver<'a, T>)>,
sub_proofs: Vec<(Counter, BodyProver<'a>)>,
}
pub struct OrProver<'a, T: Tracer>
@ -98,27 +92,19 @@ pub struct OrProver<'a, T: Tracer>
current_proving: usize,
global_counter: GlobalCounter,
counter_snapshot: Counter,
sub_proof: Option<BodyProver<'a, T>>,
sub_proof: Option<BodyProver<'a>>,
}
impl<'a, T: Tracer + 'a> BodyProver<'a, T>
impl<'a> BodyProver<'a>
{
pub fn new(
pub fn new<T: Tracer + 'a>(
module: &'a Module,
global_counter: GlobalCounter,
body: Body,
constraints: Constraints,
tracer: &mut T,
) -> BodyProver<'a, T>
) -> BodyProver<'a>
{
let body_tracer = if let Body::And(_) = body
{
Some(tracer.begin_proof(ProofType::Body))
}
else
{
None
};
let prover: Box<dyn Iterator<Item = Constraints>> = match &body
{
Body::Term(predicate) => Box::new(PredicateProver::new(
@ -153,13 +139,8 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T>
tracer,
)),
};
//info!(target: "BodyProver", "Proving {}", body);
BodyProver {
tracer: body_tracer,
module,
constraints,
prover,
}
BodyProver { prover }
}
}
@ -249,7 +230,6 @@ impl<T: Tracer> AndProver<'_, T>
)],
current_tracer,
bodies,
constraints,
global_counter,
}
}
@ -330,7 +310,6 @@ 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);
let uni = self.predicate.matches(&clause.head);
let full_constraints = uni.and_then(|x| x.and(&self.constraints));
@ -394,7 +373,7 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
}
}
impl<'a, T: Tracer + 'a> Iterator for BodyProver<'a, T>
impl<'a> Iterator for BodyProver<'a>
{
type Item = Constraints;
fn next(&mut self) -> Option<Constraints>
@ -516,6 +495,8 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T>
{
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(),
@ -532,7 +513,7 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T>
impl Module
{
pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, impl Tracer>
pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a>
{
BodyProver::new(
self,