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

Somewhat indented trace + Or prover

Browse Source
This commit is contained in:
Albin Chaboissier
2026-02-09 22:32:01 +01:00
parent 1ab7d7bf95
commit 5b9df71704
4 changed files with 273 additions and 48 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
src/main.rs
View File

@ -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:");

232
src/prover.rs
View File

@ -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<Body>,
constraints: Constraints,
tracer: T,
current_tracer: Option<T>,
current_tracer: T,
global_counter: GlobalCounter,
sub_proofs: Vec<(Counter, BodyProver<'a, T>)>,
}
pub struct OrProver<'a, T: Tracer>
{
module: &'a Module,
bodies: Vec<Body>,
constraints: Constraints,
tracer: T,
current_tracer: T,
current_proving: usize,
global_counter: GlobalCounter,
counter_snapshot: Counter,
sub_proof: Option<BodyProver<'a, T>>,
}
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::<Green>(),
@ -185,16 +200,42 @@ impl<T: Tracer> AndProver<'_, T>
global_counter: GlobalCounter,
bodies: Vec<Body>,
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::<Green>(),));
current_tracer.print_step(format!("{} : {}", "Proving".fg::<Yellow>(), bodies[0]));
current_tracer.print_step(format!("{} : {}", "Next".fg::<Red>(), 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<T: Tracer> AndProver<'_, T>
global_counter.clone(),
bodies[0].clone(),
constraints.clone(),
tracer,
&mut current_tracer,
),
)],
current_tracer,
bodies,
constraints,
global_counter,
}
}
}
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 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::<Green>(), c));
}
else
{
self.tracer
.print_step(format!("🭧 ↳ {}", "Contradictory".fg::<Red>()));
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() =>
@ -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::<Green>(),
"Proving".fg::<Yellow>(),
"Left".fg::<Red>()
));
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::<Yellow>();
dest = &mut proving;
}
else if i < self.sub_proofs.len() - 1
else if i < self.sub_proofs.len() + 1
{
color = color.fg::<Green>();
dest = &mut proved;
}
else
{
color = color.fg::<Red>();
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::<Green>(),
proved
));
self.current_tracer.print_step(format!(
"{} : {}",
"Proving".fg::<Yellow>(),
proving
));
self.current_tracer
.print_step(format!("{} : {}", "Next".fg::<Red>(), 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<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.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),
)
}
}

86
src/prover/tracing.rs
View File

@ -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<T: Display>(&self, show: T);
fn begin_proof(&mut self, proof_type: ProofType) -> Self;
fn print_step<T: Display>(&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<T: Display>(&self, show: T)
fn print_step<T: Display>(&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<T: Display>(&mut self, show: T)
{
for i in 0..self.depth
{
let style = if i % 2 == 0
{
Style::new().fg::<Gray>()
}
else
{
Style::new().fg::<DarkGray>()
};
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;

0
src/tracing.rs
View File