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

Better looking indentation

Browse Source
This commit is contained in:
Albin Chaboissier
2026-02-09 22:49:26 +01:00
parent c920ef8d99
commit 3fd8414ba2
3 changed files with 20 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/main.rs
View File

@ -21,8 +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(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:");

49
src/prover.rs
View File

@ -75,7 +75,6 @@ pub struct AndProver<'a, T: Tracer>
module: &'a Module,
bodies: Vec<Body>,
tracer: T,
current_tracer: T,
global_counter: GlobalCounter,
sub_proofs: Vec<(Counter, BodyProver<'a>)>,
@ -87,7 +86,6 @@ pub struct OrProver<'a, T: Tracer>
bodies: Vec<Body>,
constraints: Constraints,
tracer: T,
current_tracer: T,
current_proving: usize,
global_counter: GlobalCounter,
@ -189,8 +187,7 @@ impl<T: Tracer> AndProver<'_, T>
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 tracer = tracer.begin_proof(ProofType::And);
let mut next = String::new();
for x in bodies.iter().skip(1)
{
@ -208,15 +205,14 @@ impl<T: Tracer> AndProver<'_, T>
}
}
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()));
tracer.print_step(format!("Proving conjuction {}", conjuction));
tracer.print_step(format!("{} :", "Proved".fg::<Green>(),));
tracer.print_step(format!("{} : {}", "Proving".fg::<Yellow>(), bodies[0]));
tracer.print_step(format!("{} : {}", "Next".fg::<Red>(), next));
tracer.print_step(format!("With constraints : {}", constraints.simplified()));
// End pretty logging
AndProver {
tracer: whole_trace,
module,
sub_proofs: vec![(
global_counter.snapshot(),
@ -225,10 +221,10 @@ impl<T: Tracer> AndProver<'_, T>
global_counter.clone(),
bodies[0].clone(),
constraints.clone(),
&mut current_tracer,
&mut tracer,
),
)],
current_tracer,
tracer,
bodies,
global_counter,
}
@ -250,8 +246,7 @@ impl<T: Tracer> OrProver<'_, T>
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 tracer = tracer.begin_proof(ProofType::And);
let mut next = String::new();
for x in bodies.iter().skip(1)
@ -273,18 +268,17 @@ impl<T: Tracer> OrProver<'_, T>
// 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,
&mut tracer,
)),
tracer,
current_proving: 0,
counter_snapshot: global_counter.snapshot(),
current_tracer,
bodies,
constraints,
global_counter,
@ -407,7 +401,6 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
else
{
// Pretty logging
self.current_tracer = self.tracer.begin_proof(ProofType::And);
let mut proved = String::new();
let mut proving = String::new();
let mut next = String::new();
@ -428,17 +421,11 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
}
let _ = dest.write_str(&format!("{}, ", x));
}
self.current_tracer.print_step(format!(
"{} : {}",
"Proved".fg::<Green>(),
proved
));
self.current_tracer.print_step(format!(
"{} : {}",
"Proving".fg::<Yellow>(),
proving
));
self.current_tracer
self.tracer
.print_step(format!("{} : {}", "Proved".fg::<Green>(), proved));
self.tracer
.print_step(format!("{} : {}", "Proving".fg::<Yellow>(), proving));
self.tracer
.print_step(format!("{} : {}", "Next".fg::<Red>(), next));
// End pretty logging
@ -450,7 +437,7 @@ impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
self.global_counter.clone(),
self.bodies[self.sub_proofs.len()].clone(),
constraints,
&mut self.current_tracer,
&mut self.tracer,
),
));
self.next()
@ -502,7 +489,7 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T>
self.global_counter.clone(),
self.bodies[self.current_proving].clone(),
self.constraints.clone(),
&mut self.current_tracer,
&mut self.tracer,
));
self.next()
}

9
src/prover/tracing.rs
View File

@ -106,14 +106,7 @@ impl Tracer for IndentedTracer
{
Style::new().fg::<DarkGray>()
};
if i == self.depth - 1 && self.first
{
print!("{}", "🭋".style(style));
}
else
{
print!("{}", "▐".style(style));
}
print!("{}", "│".style(style));
}
self.first = false;
println!("{}", show);