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

Ugly and print, and simplified body prover depth

Browse Source
This commit is contained in:
Albin Chaboissier
2026-02-09 18:08:13 +01:00
parent a151b772aa
commit 1ab7d7bf95
3 changed files with 46 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
src/main.rs
View File

@ -20,8 +20,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 = "integer(s(X))".into();
let prop: Body = "mult(X, s(s(s(zero))), s(s(s(s(s(s(s(s(s(zero))))))))))".into();
for c in module.prove(&prop)
{
println!("true:");

46
src/prover.rs
View File

@ -3,14 +3,15 @@ pub mod tracing;
pub mod unification;
use std::cell::Cell;
use std::fmt::Write;
use std::rc::Rc;
use litemap::LiteMap;
use log::info;
use owo_colors::OwoColorize;
use owo_colors::Style;
use owo_colors::colors::Green;
use owo_colors::colors::Red;
use owo_colors::colors::css::Gray;
use owo_colors::colors::Yellow;
use crate::ast::Body;
use crate::ast::Clause;
@ -79,6 +80,7 @@ pub struct AndProver<'a, T: Tracer>
bodies: Vec<Body>,
constraints: Constraints,
tracer: T,
current_tracer: Option<T>,
global_counter: GlobalCounter,
sub_proofs: Vec<(Counter, BodyProver<'a, T>)>,
@ -111,6 +113,16 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T>
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,
@ -182,6 +194,7 @@ impl<T: Tracer> AndProver<'_, T>
AndProver {
tracer: tracer.begin_proof(ProofType::And),
current_tracer: None,
module,
sub_proofs: vec![(
global_counter.snapshot(),
@ -316,6 +329,35 @@ 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();
for (i, x) in self.bodies.iter().enumerate()
{
let mut color = Style::new();
if i == self.sub_proofs.len() - 1
{
color = color.fg::<Yellow>();
}
else if i < self.sub_proofs.len() - 1
{
color = color.fg::<Green>();
}
else
{
color = color.fg::<Red>();
}
let _ = output.write_str(&format!("{}, ", x.style(color)));
}
self.current_tracer.as_ref().unwrap().print_step(output);
// End pretty logging
self.sub_proofs.push((current_proof_snap, current_proof));
self.sub_proofs.push((
self.global_counter.snapshot(),

0
src/tracing.rs Normal file
View File