From b80077f3a7204283344f11d2dd40145aa44f9b16 Mon Sep 17 00:00:00 2001 From: Albin Chaboissier Date: Mon, 9 Feb 2026 10:56:15 +0100 Subject: [PATCH] Starting tracer --- 1 | 0 Cargo.lock | 115 +------------------------------------- Cargo.toml | 1 - src/main.rs | 18 +++--- src/prover.rs | 91 +++++++++++++++++++----------- src/prover/constraints.rs | 25 +++++++-- src/prover/trace.rs | 0 src/prover/tracing.rs | 28 ++++++---- src/prover/unification.rs | 8 +-- 9 files changed, 110 insertions(+), 176 deletions(-) delete mode 100644 1 delete mode 100644 src/prover/trace.rs diff --git a/1 b/1 deleted file mode 100644 index e69de29..0000000 diff --git a/Cargo.lock b/Cargo.lock index 3f473bf..3d771a3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -47,7 +47,7 @@ version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" dependencies = [ - "windows-sys 0.61.2", + "windows-sys", ] [[package]] @@ -58,40 +58,15 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" dependencies = [ "anstyle", "once_cell_polyfill", - "windows-sys 0.61.2", + "windows-sys", ] -[[package]] -name = "autocfg" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" - -[[package]] -name = "cfg-if" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" - [[package]] name = "colorchoice" version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75" -[[package]] -name = "corosensei" -version = "0.3.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b2b4c7e3e97730e6b0b8c5ff5ca82c663d1a645e4f630f4fa4c24e80626787e" -dependencies = [ - "autocfg", - "cfg-if", - "libc", - "scopeguard", - "windows-sys 0.59.0", -] - [[package]] name = "env_filter" version = "0.1.4" @@ -145,12 +120,6 @@ dependencies = [ "syn", ] -[[package]] -name = "libc" -version = "0.2.180" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc" - [[package]] name = "litemap" version = "0.8.1" @@ -179,7 +148,6 @@ checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe" name = "picolog" version = "0.1.0" dependencies = [ - "corosensei", "env_logger", "litemap", "log", @@ -248,12 +216,6 @@ version = "0.8.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a96887878f22d7bad8a3b6dc5b7440e0ada9a245242924394987b21cf2210a4c" -[[package]] -name = "scopeguard" -version = "1.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" - [[package]] name = "serde_core" version = "1.0.228" @@ -303,15 +265,6 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5" -[[package]] -name = "windows-sys" -version = "0.59.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets", -] - [[package]] name = "windows-sys" version = "0.61.2" @@ -321,70 +274,6 @@ dependencies = [ "windows-link", ] -[[package]] -name = "windows-targets" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" -dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", -] - -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" - -[[package]] -name = "windows_aarch64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" - -[[package]] -name = "windows_i686_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" - -[[package]] -name = "windows_i686_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" - -[[package]] -name = "windows_i686_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" - -[[package]] -name = "windows_x86_64_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" - -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" - -[[package]] -name = "windows_x86_64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" - [[package]] name = "winnow" version = "0.7.14" diff --git a/Cargo.toml b/Cargo.toml index 2570f5d..6952248 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,7 +4,6 @@ version = "0.1.0" edition = "2024" [dependencies] -corosensei = "0.3.2" env_logger = "0.11.8" litemap = "0.8.1" log = "0.4.29" diff --git a/src/main.rs b/src/main.rs index dbe291a..fbe6f14 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,3 +1,4 @@ +use log::info; use picolog::ast::Body; use picolog::ast::Module; use picolog::ast::Predicate; @@ -21,14 +22,15 @@ fn main() " .into(); - //let prop: Body = "integer(s(zero))".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:"); - // println!("{}", c.simplified()); - // let _ = std::io::stdin().read_line(&mut String::new()); - // } + //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:"); + println!("{}", c.simplified()); + let _ = std::io::stdin().read_line(&mut String::new()); + } + // let p: Predicate = "add(s(zero), zero, Y)".into(); // let p1: Predicate = "add(X, zero, X)".into(); // // let p: Predicate = "integer(s(zero))".into(); diff --git a/src/prover.rs b/src/prover.rs index 4e14557..f205bb6 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -1,9 +1,8 @@ pub mod constraints; -pub mod trace; +pub mod tracing; pub mod unification; use std::cell::Cell; -use std::collections::VecDeque; use std::rc::Rc; use litemap::LiteMap; @@ -14,6 +13,9 @@ use crate::ast::Clause; use crate::ast::Module; use crate::ast::Predicate; use crate::prover::constraints::Constraints; +use crate::prover::tracing::ProofType; +use crate::prover::tracing::SimpleTracer; +use crate::prover::tracing::Tracer; #[derive(Clone, Copy, Debug, Default)] pub struct Counter(usize); @@ -46,45 +48,56 @@ impl GlobalCounter } } -pub struct BodyProver<'a> +pub struct BodyProver<'a, T: Tracer + 'a> { module: &'a Module, constraints: Constraints, - + tracer: Option, prover: Box + 'a>, } -pub struct PredicateProver<'a> +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>, + sub_proof: Option>, } -pub struct AndProver<'a> +pub struct AndProver<'a, T: Tracer> { module: &'a Module, bodies: Vec, constraints: Constraints, + tracer: T, global_counter: GlobalCounter, - sub_proofs: VecDeque<(Counter, BodyProver<'a>)>, + sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, } -impl BodyProver<'_> +impl<'a, T: Tracer + 'a> BodyProver<'a, T> { - pub fn new<'a>( + pub fn new( module: &'a Module, global_counter: GlobalCounter, body: Body, constraints: Constraints, - ) -> BodyProver<'a> + tracer: &T, + ) -> BodyProver<'a, T> { + let body_tracer = if let Body::And(_) = body + { + Some(tracer.begin_proof(ProofType::Body, format!("Proving {}", body))) + } + else + { + None + }; let prover: Box> = match &body { Body::Term(predicate) => Box::new(PredicateProver::new( @@ -92,22 +105,26 @@ impl BodyProver<'_> global_counter, predicate.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, )), }; - info!(target: "BodyProver", "Proving {}", body); + //info!(target: "BodyProver", "Proving {}", body); BodyProver { + tracer: body_tracer, module, constraints, prover, @@ -115,18 +132,20 @@ impl BodyProver<'_> } } -impl PredicateProver<'_> +impl<'a, T: Tracer + 'a> PredicateProver<'a, T> { - pub fn new<'a>( + pub fn new( module: &'a Module, global_counter: GlobalCounter, predicate: Predicate, constraints: Constraints, - ) -> PredicateProver<'a> + tracer: &T, + ) -> PredicateProver<'a, T> { - info!(target: "PredicateProver", "Proving {}", predicate); + //info!(target: "PredicateProver", "Proving {}", predicate); PredicateProver { module, + tracer: tracer.begin_proof(ProofType::Predicate, format!("Proving {}", &predicate)), predicate, constraints, current_clause: 0, @@ -137,28 +156,33 @@ impl PredicateProver<'_> } } -impl AndProver<'_> +impl AndProver<'_, T> { pub fn new<'a>( module: &'a Module, global_counter: GlobalCounter, bodies: Vec, constraints: Constraints, - ) -> AndProver<'a> + tracer: &T, + ) -> AndProver<'a, T> + where + T: 'a, { assert!(!bodies.is_empty()); AndProver { + tracer: tracer.begin_proof(ProofType::And), module, - sub_proofs: VecDeque::from(vec![( + sub_proofs: vec![( global_counter.snapshot(), BodyProver::new( module, global_counter.clone(), bodies[0].clone(), constraints.clone(), + tracer, ), - )]), + )], bodies, constraints, global_counter, @@ -166,7 +190,7 @@ impl AndProver<'_> } } -impl Iterator for PredicateProver<'_> +impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> { type Item = Constraints; @@ -184,17 +208,17 @@ impl Iterator for PredicateProver<'_> { let clause = &self.module.clauses[self.current_clause] .make_unique(self.global_counter.clone()); - info!(target: "PredicateProver", "Unifying '{}' against '{}'", self.predicate, clause); + //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)); if let Some(c) = &full_constraints { - info!(target: "PredicateProver", " => {}", c); + //info!(target: "PredicateProver", " => {}", c); } else { - info!(target: "PredicateProver", " => (Can't unify)"); + //info!(target: "PredicateProver", " => (Can't unify)"); } match full_constraints { @@ -212,6 +236,7 @@ impl Iterator for PredicateProver<'_> self.global_counter.clone(), clause.body.clone().unwrap(), constraints, + &self.tracer, )); self.next() } @@ -241,7 +266,7 @@ impl Iterator for PredicateProver<'_> } } -impl Iterator for BodyProver<'_> +impl<'a, T: Tracer + 'a> Iterator for BodyProver<'a, T> { type Item = Constraints; fn next(&mut self) -> Option @@ -250,7 +275,7 @@ impl Iterator for BodyProver<'_> } } -impl Iterator for AndProver<'_> +impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T> { type Item = Constraints; @@ -261,7 +286,7 @@ impl Iterator for AndProver<'_> return None; } - let (current_proof_snap, mut current_proof) = self.sub_proofs.pop_back().unwrap(); + let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap(); match current_proof.next() { @@ -269,21 +294,20 @@ impl Iterator for AndProver<'_> { if self.sub_proofs.len() == self.bodies.len() - 1 { - self.sub_proofs - .push_back((current_proof_snap, current_proof)); + self.sub_proofs.push((current_proof_snap, current_proof)); Some(constraints) } else { - self.sub_proofs - .push_back((current_proof_snap, current_proof)); - self.sub_proofs.push_back(( + 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, + &self.tracer, ), )); self.next() @@ -300,13 +324,14 @@ impl Iterator for AndProver<'_> impl Module { - pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a> + pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, SimpleTracer> { BodyProver::new( self, GlobalCounter::new(), body.clone(), Constraints::none(), + &SimpleTracer::new(ProofType::Body), ) } } diff --git a/src/prover/constraints.rs b/src/prover/constraints.rs index ecc0927..a13eab2 100644 --- a/src/prover/constraints.rs +++ b/src/prover/constraints.rs @@ -2,6 +2,7 @@ use std::fmt::Display; use litemap::LiteMap; +use crate::ast::Body; use crate::ast::Predicate; use crate::ast::Variable; @@ -128,8 +129,7 @@ impl Predicate { if let Some(pred) = constraints.set.get(name) { - let max_sub = pred.substitute(constraints); - max_sub + pred.substitute(constraints) } else { @@ -151,10 +151,23 @@ impl Predicate match self { Predicate::Variable(var_name) => name == var_name, - Predicate::Fixed(_, predicates) => predicates - .iter() - .find(|x| x.contains_variable(name)) - .is_some(), + Predicate::Fixed(_, predicates) => predicates.iter().any(|x| x.contains_variable(name)), + } + } +} + +impl Body +{ + pub fn substitute(&self, constraints: &Constraints) -> Body + { + match self + { + Body::Term(predicate) => Body::Term(predicate.substitute(constraints)), + Body::And(items) => + { + Body::And(items.iter().map(|x| x.substitute(constraints)).collect()) + } + Body::Or(items) => Body::Or(items.iter().map(|x| x.substitute(constraints)).collect()), } } } diff --git a/src/prover/trace.rs b/src/prover/trace.rs deleted file mode 100644 index e69de29..0000000 diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index e3117f2..8ff9327 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,4 +1,4 @@ -use std::fmt::Display; +use std::{default, fmt::Display}; use log::info; @@ -25,9 +25,9 @@ impl Display for ProofType pub trait Tracer { - fn next_step(&mut self, proof_type: ProofType) -> Self; - fn milestone(&self, str: T); - fn explain(&self, str: T); + fn begin_proof(&self, proof_type: ProofType) -> Self; + fn print_step(&self, show: T); + fn end_proof(self); } pub struct SimpleTracer @@ -35,21 +35,29 @@ pub struct SimpleTracer proof_type: ProofType, } +impl SimpleTracer +{ + pub fn new(proof_type: ProofType) -> Self + { + Self { proof_type } + } +} + impl Tracer for SimpleTracer { - fn next_step(&mut self, proof_type: ProofType) -> Self + fn begin_proof(&self, proof_type: ProofType) -> Self { SimpleTracer { proof_type } } - fn explain(&self, str: T) + fn print_step(&self, show: T) { - let proof_str = format!("{}", self.proof_type); - info!(target: &proof_str, "{}", str); + let str = format!("{}", self.proof_type); + info!(target: &str, "{}", show); } - fn milestone(&self, str: T) + fn end_proof(self) { - self.explain(str); + todo!() } } diff --git a/src/prover/unification.rs b/src/prover/unification.rs index 811038a..747d458 100644 --- a/src/prover/unification.rs +++ b/src/prover/unification.rs @@ -1,5 +1,3 @@ -use std::process::Output; - use log::debug; use crate::ast::Predicate; @@ -17,7 +15,7 @@ impl Predicate { Predicate::Variable(variable) => { - debug!("Unifying var {} against {}", self, other); + //debug!("Unifying var {} against {}", self, other); // We are trying to see if X (any) matches the other Predicate. // This is always true if X = other_predicate Some(Constraints::with(variable.clone(), other.clone())) @@ -32,7 +30,7 @@ impl Predicate // We are trying to see if something like "predicate(..., ...)" matches X // (any) // This is always true - debug!("Unifying pred {} against var {}", self, other); + //debug!("Unifying pred {} against var {}", self, other); Some(Constraints::with(var.clone(), self.clone())) } // Match pred(X, Y, Z, ...) with pred(_X, _Y, _Z, ...) @@ -40,7 +38,7 @@ impl Predicate if other_name == name && other_arguments.len() == arguments.len() => { // If there is no arguments, no constraints - debug!("Unifying fixed {} against fixed {}", self, other); + //debug!("Unifying fixed {} against fixed {}", self, other); if arguments.is_empty() { return Some(Constraints::none());