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

Merge remote-tracking branch 'origin/main' into operators

Browse Source
This commit is contained in:
Julien THILLARD
2026-02-10 22:23:52 +01:00
parent c82384764c 54724c2f4c
commit 27af8c9263
15 changed files with 827 additions and 331 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
1.pl
View File

@ -1,9 +1,22 @@
:- use_module(library(clpfd)).
entier(zero).
entier(s(X)) :- entier(X).
add(X, zero, X).
add(X, s(Y), Z) :- add(s(X), Y, Z).
inf(zero, X) :- entier(X).
inf(s(X), s(Y)) :- inf(X, Y).
mult(zero, X, zero).
mult(s(Y), X, Z) :- mult(Y, X, W), add(W, X, Z).
div(A, B) :- inf(A, B), inf(X, B), mult(X, A, B).
div_w(X, Y) :- inf(s(X), Y), inf(s(s(zero)), X), div(X, Y).
prime(X) :- entier(X), \+ div_w(_, X).
peano(X, zero) :- X #= 0.
peano(X, s(P)) :- X #> 0, X #= Y + 1, peano(Y, P).

60
Cargo.lock generated
View File

@ -11,6 +11,12 @@ dependencies = [
"memchr",
]
[[package]]
name = "allocator-api2"
version = "0.2.21"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923"
[[package]]
name = "anstream"
version = "0.6.21"
@ -61,6 +67,12 @@ dependencies = [
"windows-sys",
]
[[package]]
name = "bimap"
version = "0.6.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "230c5f1ca6a325a32553f8640d31ac9b49f2411e901e427570154868b46da4f7"
[[package]]
name = "colorchoice"
version = "1.0.4"
@ -90,6 +102,29 @@ dependencies = [
"log",
]
[[package]]
name = "equivalent"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
[[package]]
name = "foldhash"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb"
[[package]]
name = "hashbrown"
version = "0.16.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100"
dependencies = [
"allocator-api2",
"equivalent",
"foldhash",
]
[[package]]
name = "is_terminal_polyfill"
version = "1.70.2"
@ -120,18 +155,21 @@ dependencies = [
"syn",
]
[[package]]
name = "litemap"
version = "0.8.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77"
[[package]]
name = "log"
version = "0.4.29"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5e5032e24019045c762d3c0f28f5b6b8bbf38563a65908389bf7978758920897"
[[package]]
name = "lru"
version = "0.16.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a1dc47f592c06f33f8e3aea9591776ec7c9f9e4124778ff8a3c3b87159f7e593"
dependencies = [
"hashbrown",
]
[[package]]
name = "memchr"
version = "2.8.0"
@ -144,13 +182,21 @@ version = "1.70.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe"
[[package]]
name = "owo-colors"
version = "4.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9c6901729fa79e91a0913333229e9ca5dc725089d1c363b2f4b4760709dc4a52"
[[package]]
name = "picolog"
version = "0.1.0"
dependencies = [
"bimap",
"env_logger",
"litemap",
"log",
"lru",
"owo-colors",
"winnow",
]

4
Cargo.toml
View File

@ -4,7 +4,9 @@ version = "0.1.0"
edition = "2024"
[dependencies]
bimap = "0.6.3"
env_logger = "0.11.8"
litemap = "0.8.1"
log = "0.4.29"
winnow = { version = "0.7.14", path = "./winnow" }
lru = "0.16.3"
owo-colors = "4.2.3"

26
src/ast.rs
View File

@ -1,6 +1,9 @@
use owo_colors::{OwoColorize, colors::css::Gray};
use std::fmt::Display;
pub type Variable = String;
#[derive(Clone, PartialEq, Eq, Debug, Hash)]
pub struct Variable(pub String, pub Option<usize>);
#[derive(Clone, Debug)]
pub struct Module
@ -15,7 +18,7 @@ pub struct Clause
pub body: Option<Body>,
}
#[derive(Clone, Debug)]
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Body
{
Term(Predicate),
@ -23,21 +26,21 @@ pub enum Body
Or(Vec<Body>),
}
#[derive(Clone, Debug, PartialEq)]
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
pub enum Predicate
{
Variable(Variable), // Upercase variable like X
Fixed(Functor, Vec<Predicate>),
}
#[derive(Clone, Debug, PartialEq)]
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Functor
{
Operator(Operator),
Functor(String),
}
#[derive(Clone, Debug, PartialEq)]
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct Operator
{
pub op: String,
@ -90,6 +93,19 @@ impl Display for Body
}
}
impl Display for Variable
{
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
{
write!(f, "{}", self.0)?;
if let Some(num) = self.1
{
write!(f, "{}", format!("[{}]", num).fg::<Gray>())?;
}
Ok(())
}
}
impl Display for Predicate
{
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result

7
src/main.rs
View File

@ -33,9 +33,12 @@ fn main()
"
.into();
println!("{}", module);
let prop: Body = "integer(s(X))".into();
// println!("{}", module);
// 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(zero)), s(s(s(s(zero)))))".into();
//let prop: Body = "mult(X, Y, Z)".into();
//let prop: Body = "mult(s(s(zero)), s(s(zero)), X)".into();
for c in module.prove(&prop)
{
println!("true:");

3
src/parsing.rs
View File

@ -16,6 +16,7 @@ use crate::ast::Module;
use crate::ast::Operator;
use crate::ast::Predicate;
use crate::ast::{Body, OperatorType};
use crate::ast::Variable;
impl Operator
{
@ -203,7 +204,7 @@ pub fn predicate_parse_variable_or_functor(input: &mut Stream) -> Result<Predica
// Check if output is a variable
if ident.chars().next().is_some_and(|char| char.is_uppercase())
{
Ok(Predicate::Variable(String::from(ident)))
Ok(Predicate::Variable(Variable(String::from(ident), None)))
}
else
{

337
src/prover.rs
View File

@ -1,20 +1,24 @@
pub mod and;
pub mod body;
pub mod constraints;
pub mod not;
pub mod or;
pub mod predicate;
pub mod tracing;
pub mod unification;
use std::cell::Cell;
use std::collections::HashMap;
use std::rc::Rc;
use litemap::LiteMap;
use crate::ast::Body;
use crate::ast::Clause;
use crate::ast::Module;
use crate::ast::Predicate;
use crate::ast::Variable;
use crate::prover::body::BodyProver;
use crate::prover::constraints::Constraints;
use crate::prover::tracing::ProofType;
use crate::prover::tracing::SimpleTracer;
use crate::prover::tracing::Tracer;
use crate::prover::tracing::IndentedTracer;
#[derive(Clone, Copy, Debug, Default)]
pub struct Counter(usize);
@ -26,7 +30,12 @@ impl GlobalCounter
{
pub fn new() -> GlobalCounter
{
GlobalCounter(Rc::new(Cell::new(0)))
Self::with(0)
}
pub fn with(n: usize) -> GlobalCounter
{
GlobalCounter(Rc::new(Cell::new(n)))
}
pub fn get(&self) -> usize
@ -47,290 +56,18 @@ impl GlobalCounter
}
}
pub struct BodyProver<'a, T: Tracer + 'a>
{
module: &'a Module,
constraints: Constraints,
tracer: Option<T>,
prover: Box<dyn Iterator<Item = Constraints> + '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<BodyProver<'a, T>>,
}
pub struct AndProver<'a, T: Tracer>
{
module: &'a Module,
bodies: Vec<Body>,
constraints: Constraints,
tracer: T,
global_counter: GlobalCounter,
sub_proofs: Vec<(Counter, BodyProver<'a, T>)>,
}
impl<'a, T: Tracer + 'a> BodyProver<'a, T>
{
pub fn new(
module: &'a Module,
global_counter: GlobalCounter,
body: Body,
constraints: Constraints,
tracer: &T,
) -> BodyProver<'a, T>
{
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(
module,
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);
BodyProver {
tracer: body_tracer,
module,
constraints,
prover,
}
}
}
impl<'a, T: Tracer + 'a> PredicateProver<'a, T>
{
pub fn new(
module: &'a Module,
global_counter: GlobalCounter,
predicate: Predicate,
constraints: Constraints,
tracer: &T,
) -> PredicateProver<'a, T>
{
//info!(target: "PredicateProver", "Proving {}", predicate);
PredicateProver {
module,
tracer: tracer.begin_proof(ProofType::Predicate),
predicate,
constraints,
current_clause: 0,
sub_proof: None,
counter_snapshot: global_counter.snapshot(),
global_counter,
}
}
}
impl<T: Tracer> AndProver<'_, T>
{
pub fn new<'a>(
module: &'a Module,
global_counter: GlobalCounter,
bodies: Vec<Body>,
constraints: Constraints,
tracer: &T,
) -> AndProver<'a, T>
where
T: 'a,
{
assert!(!bodies.is_empty());
AndProver {
tracer: tracer.begin_proof(ProofType::And),
module,
sub_proofs: vec![(
global_counter.snapshot(),
BodyProver::new(
module,
global_counter.clone(),
bodies[0].clone(),
constraints.clone(),
tracer,
),
)],
bodies,
constraints,
global_counter,
}
}
}
impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
{
type Item = Constraints;
fn next(&mut self) -> Option<Self::Item>
{
match self.sub_proof.as_mut()
{
None =>
{
if self.current_clause == self.module.clauses.len()
{
None
}
else
{
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));
if let Some(c) = &full_constraints
{
//info!(target: "PredicateProver", " => {}", c);
}
else
{
//info!(target: "PredicateProver", " => (Can't unify)");
}
match full_constraints
{
Some(constraints) if clause.body.is_none() =>
{
self.current_clause += 1;
Some(constraints)
}
Some(constraints) =>
{
self.current_clause += 1;
self.counter_snapshot = self.global_counter.snapshot();
self.sub_proof = Some(BodyProver::new(
self.module,
self.global_counter.clone(),
clause.body.clone().unwrap(),
constraints,
&self.tracer,
));
self.next()
}
None =>
{
self.current_clause += 1;
self.next()
}
}
}
}
Some(prover) =>
{
let next = prover.next();
match next
{
Some(constraints) => Some(constraints),
None =>
{
self.global_counter.restore(self.counter_snapshot);
self.sub_proof = None;
self.next()
}
}
}
}
}
}
impl<'a, T: Tracer + 'a> Iterator for BodyProver<'a, T>
{
type Item = Constraints;
fn next(&mut self) -> Option<Constraints>
{
self.prover.next()
}
}
impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
{
type Item = Constraints;
fn next(&mut self) -> Option<Self::Item>
{
if self.sub_proofs.is_empty()
{
return None;
}
let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap();
match current_proof.next()
{
Some(constraints) =>
{
if self.sub_proofs.len() == self.bodies.len() - 1
{
self.sub_proofs.push((current_proof_snap, current_proof));
Some(constraints)
}
else
{
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()
}
}
None =>
{
self.global_counter.restore(current_proof_snap);
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>
{
BodyProver::new(
self,
GlobalCounter::new(),
body.clone(),
Constraints::none(),
&SimpleTracer::new(ProofType::Body),
//&mut EmptyTracer,
&mut IndentedTracer::new(),
//&SimpleTracer::new(ProofType::Body),
)
}
}
@ -339,7 +76,7 @@ impl Clause
{
pub fn make_unique(&self, counter: GlobalCounter) -> Clause
{
let mut unique_map = LiteMap::new();
let mut unique_map = HashMap::new();
Clause {
head: self.head.make_unique(counter.clone(), &mut unique_map),
body: self
@ -355,7 +92,7 @@ impl Body
pub fn make_unique(
&self,
counter: GlobalCounter,
unique_map: &mut LiteMap<String, usize>,
unique_map: &mut HashMap<Variable, usize>,
) -> Body
{
match self
@ -382,18 +119,15 @@ impl Predicate
pub fn make_unique(
&self,
counter: GlobalCounter,
unique_map: &mut LiteMap<String, usize>,
unique_map: &mut HashMap<Variable, usize>,
) -> Self
{
match self
{
Predicate::Variable(name) => Predicate::Variable(format!(
"_{}[{}]",
name,
unique_map
.entry(name.clone())
.or_insert_with(|| counter.get())
)),
Predicate::Variable(var) =>
{
Predicate::Variable(var.make_unique(counter.clone(), unique_map))
}
Predicate::Fixed(name, predicates) => Predicate::Fixed(
name.clone(),
predicates
@ -404,3 +138,22 @@ impl Predicate
}
}
}
impl Variable
{
pub fn make_unique(
&self,
counter: GlobalCounter,
unique_map: &mut HashMap<Variable, usize>,
) -> Self
{
Variable(
self.0.clone(),
Some(
*unique_map
.entry(self.clone())
.or_insert_with(|| counter.get()),
),
)
}
}

172
src/prover/and.rs Normal file
View File

@ -0,0 +1,172 @@
use std::fmt::Write;
use owo_colors::OwoColorize;
use crate::ast::Body;
use crate::ast::Module;
use crate::prover::Counter;
use crate::prover::GlobalCounter;
use crate::prover::body::BodyProver;
use crate::prover::constraints::Constraints;
use crate::prover::tracing::ProofType;
use crate::prover::tracing::Tracer;
pub struct AndProver<'a, T: Tracer>
{
module: &'a Module,
bodies: Vec<Body>,
tracer: T,
global_counter: GlobalCounter,
sub_proofs: Vec<(Counter, BodyProver<'a>)>,
}
impl<T: Tracer> AndProver<'_, T>
{
pub fn new<'a>(
module: &'a Module,
global_counter: GlobalCounter,
bodies: Vec<Body>,
constraints: Constraints,
tracer: &mut T,
) -> AndProver<'a, T>
where
T: 'a,
{
assert!(!bodies.is_empty());
// Pretty logging
let mut tracer = tracer.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(" ∧ ");
}
}
tracer.print_step(format!("Proving conjuction {}", conjuction));
tracer.print_step(format!("{} :", "Proved".fg::<owo_colors::colors::Green>(),));
tracer.print_step(format!(
"{} : {}",
"Proving".fg::<owo_colors::colors::Yellow>(),
bodies[0]
));
tracer.print_step(format!(
"{} : {}",
"Next".fg::<owo_colors::colors::Red>(),
next
));
tracer.print_step(format!("With constraints : {}", constraints.simplified()));
// End pretty logging
AndProver {
module,
sub_proofs: vec![(
global_counter.snapshot(),
BodyProver::new(
module,
global_counter.clone(),
bodies[0].clone(),
constraints.clone(),
&mut tracer,
),
)],
tracer,
bodies,
global_counter,
}
}
}
impl<'a, T: Tracer + 'a> Iterator for AndProver<'a, T>
{
type Item = Constraints;
fn next(&mut self) -> Option<Self::Item>
{
if self.sub_proofs.is_empty()
{
return None;
}
let (current_proof_snap, mut current_proof) = self.sub_proofs.pop().unwrap();
match current_proof.next()
{
Some(constraints) =>
{
if self.sub_proofs.len() == self.bodies.len() - 1
{
self.sub_proofs.push((current_proof_snap, current_proof));
Some(constraints)
}
else
{
// Pretty logging
let mut proved = String::new();
let mut proving = String::new();
let mut next = String::new();
for (i, x) in self.bodies.iter().enumerate()
{
let dest;
if i == self.sub_proofs.len() + 1
{
dest = &mut proving;
}
else if i < self.sub_proofs.len() + 1
{
dest = &mut proved;
}
else
{
dest = &mut next;
}
let _ = dest.write_str(&format!("{}, ", x));
}
self.tracer.print_step(format!(
"{} : {}",
"Proved".fg::<owo_colors::colors::Green>(),
proved
));
self.tracer.print_step(format!(
"{} : {}",
"Proving".fg::<owo_colors::colors::Yellow>(),
proving
));
self.tracer.print_step(format!(
"{} : {}",
"Next".fg::<owo_colors::colors::Red>(),
next
));
// End pretty logging
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,
&mut self.tracer,
),
));
self.next()
}
}
None =>
{
self.global_counter.restore(current_proof_snap);
self.next()
}
}
}
}

70
src/prover/body.rs Normal file
View File

@ -0,0 +1,70 @@
use crate::ast::Body;
use crate::ast::Module;
use crate::prover::GlobalCounter;
use crate::prover::and::AndProver;
use crate::prover::constraints::Constraints;
use crate::prover::predicate::PredicateProver;
use crate::prover::tracing::Tracer;
pub struct BodyProver<'a>
{
prover: Box<dyn Iterator<Item = Constraints> + 'a>,
}
impl<'a> BodyProver<'a>
{
pub fn new<T: Tracer + 'a>(
module: &'a Module,
global_counter: GlobalCounter,
body: Body,
constraints: Constraints,
tracer: &mut T,
) -> BodyProver<'a>
{
let prover: Box<dyn Iterator<Item = Constraints>> = match &body
{
Body::Term(predicate) => Box::new(PredicateProver::new(
module,
global_counter,
predicate.clone(),
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,
items.clone(),
constraints.clone(),
tracer,
)),
Body::Or(items) => Box::new(BodyProver::new(
module,
global_counter,
items[0].clone(),
constraints.clone(),
tracer,
)),
};
BodyProver { prover }
}
}
impl<'a> Iterator for BodyProver<'a>
{
type Item = Constraints;
fn next(&mut self) -> Option<Constraints>
{
self.prover.next()
}
}

11
src/prover/constraints.rs
View File

@ -1,7 +1,6 @@
use std::collections::HashMap;
use std::fmt::Display;
use litemap::LiteMap;
use crate::ast::Body;
use crate::ast::Predicate;
use crate::ast::Variable;
@ -9,7 +8,7 @@ use crate::ast::Variable;
#[derive(Clone, Debug)]
pub struct Constraints
{
set: LiteMap<Variable, Predicate>,
pub(crate) set: HashMap<Variable, Predicate>,
}
impl Constraints
@ -17,7 +16,7 @@ impl Constraints
pub fn none() -> Self
{
Constraints {
set: LiteMap::new(),
set: HashMap::new(),
}
}
@ -102,7 +101,7 @@ impl Constraints
let mut stripped = max_sub.clone();
'outer: for (var, _) in max_sub.set.iter()
{
if var.chars().next().is_some_and(|x| x == '_')
if var.0.chars().next().is_some_and(|x| x == '_') || var.1.is_some()
{
for (_, other_pred) in max_sub.set.iter()
{
@ -146,7 +145,7 @@ impl Predicate
}
}
pub fn contains_variable(&self, name: &String) -> bool
pub fn contains_variable(&self, name: &Variable) -> bool
{
match self
{

71
src/prover/not.rs Normal file
View File

@ -0,0 +1,71 @@
use crate::ast::Body;
use crate::ast::Module;
use crate::prover::GlobalCounter;
use crate::prover::body::BodyProver;
use crate::prover::constraints::Constraints;
use crate::prover::tracing::ProofType;
use crate::prover::tracing::Tracer;
pub struct NotProver<'a, T: Tracer + 'a>
{
prover: Option<BodyProver<'a>>,
constraints: Constraints,
tracer: T,
}
impl<'a, T: Tracer + 'a> NotProver<'a, T>
{
pub fn new(
module: &'a Module,
global_counter: GlobalCounter,
body: Body,
constraints: Constraints,
tracer: &mut T,
) -> NotProver<'a, T>
{
let mut not_tracer = tracer.begin_proof(ProofType::Body);
NotProver {
prover: Some(BodyProver::new(
module,
global_counter,
body,
constraints.clone(),
&mut not_tracer,
)),
tracer: not_tracer,
constraints: constraints.clone(),
}
}
}
impl<'a, T: Tracer + 'a> Iterator for NotProver<'a, T>
{
type Item = Constraints;
fn next(&mut self) -> Option<Constraints>
{
if let Some(x) = self.prover.as_mut()
{
match &mut x.next()
{
Some(_) =>
{
// The prover showed that the proof is true.
// Thus the negation is never true
self.prover = None;
None
}
None =>
{
// The prover did not find any proof
// Thus the negation is true
self.prover = None;
Some(self.constraints.clone())
}
}
}
else
{
None
}
}
}

124
src/prover/or.rs Normal file
View File

@ -0,0 +1,124 @@
use std::fmt::Write;
use crate::ast::Body;
use crate::ast::Module;
use crate::prover::Counter;
use crate::prover::GlobalCounter;
use crate::prover::body::BodyProver;
use crate::prover::constraints::Constraints;
use crate::prover::tracing::ProofType;
use crate::prover::tracing::Tracer;
pub struct OrProver<'a, T: Tracer>
{
module: &'a Module,
bodies: Vec<Body>,
constraints: Constraints,
tracer: T,
current_proving: usize,
global_counter: GlobalCounter,
counter_snapshot: Counter,
sub_proof: Option<BodyProver<'a>>,
}
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 tracer = tracer.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 {
module,
sub_proof: Some(BodyProver::new(
module,
global_counter.clone(),
bodies[0].clone(),
constraints.clone(),
&mut tracer,
)),
tracer,
current_proving: 0,
counter_snapshot: global_counter.snapshot(),
bodies,
constraints,
global_counter,
}
}
}
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.tracer
.print_step(format!("Tring with {}", self.bodies[self.current_proving]));
self.sub_proof = Some(BodyProver::new(
self.module,
self.global_counter.clone(),
self.bodies[self.current_proving].clone(),
self.constraints.clone(),
&mut self.tracer,
));
self.next()
}
}
}
}
}

132
src/prover/predicate.rs Normal file
View File

@ -0,0 +1,132 @@
use owo_colors::OwoColorize;
use owo_colors::colors::Green;
use crate::ast::{Module, Predicate};
use crate::prover::body::BodyProver;
use crate::prover::constraints::Constraints;
use crate::prover::tracing::{ProofType, Tracer};
use crate::prover::{Counter, GlobalCounter};
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<BodyProver<'a>>,
}
impl<'a, T: Tracer + 'a> PredicateProver<'a, T>
{
pub fn new(
module: &'a Module,
global_counter: GlobalCounter,
predicate: Predicate,
constraints: Constraints,
tracer: &mut T,
) -> PredicateProver<'a, T>
{
//info!(target: "PredicateProver", "Proving {}", predicate);
let mut predicate_prover = tracer.begin_proof(ProofType::Predicate);
predicate_prover.print_step(format!(
"{} '{}'",
"Proving predicate".fg::<Green>(),
predicate
));
PredicateProver {
module,
tracer: predicate_prover,
predicate,
constraints,
current_clause: 0,
sub_proof: None,
counter_snapshot: global_counter.snapshot(),
global_counter,
}
}
}
impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T>
{
type Item = Constraints;
fn next(&mut self) -> Option<Self::Item>
{
match self.sub_proof.as_mut()
{
None =>
{
if self.current_clause == self.module.clauses.len()
{
None
}
else
{
let clause = &self.module.clauses[self.current_clause]
.make_unique(self.global_counter.clone());
let uni = self.predicate.matches(&clause.head);
let full_constraints = uni.and_then(|x| x.and(&self.constraints));
if let Some(c) = &full_constraints
{
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() =>
{
self.current_clause += 1;
Some(constraints)
}
Some(constraints) =>
{
self.current_clause += 1;
self.counter_snapshot = self.global_counter.snapshot();
self.sub_proof = Some(BodyProver::new(
self.module,
self.global_counter.clone(),
clause.body.clone().unwrap(),
constraints,
&mut self.tracer,
));
self.next()
}
None =>
{
self.global_counter.restore(self.counter_snapshot);
self.current_clause += 1;
self.next()
}
}
}
}
Some(prover) =>
{
let next = prover.next();
match next
{
Some(constraints) => Some(constraints),
None =>
{
self.global_counter.restore(self.counter_snapshot);
self.sub_proof = None;
self.next()
}
}
}
}
}
}

127
src/prover/tracing.rs
View File

@ -1,17 +1,24 @@
use log::info;
use owo_colors::colors::css::DarkGray;
use owo_colors::colors::css::Gray;
use owo_colors::OwoColorize;
use owo_colors::Style;
use std::fmt::Display;
use log::info;
#[derive(Clone, Copy)]
pub enum ProofType {
pub enum ProofType
{
Body,
And,
Predicate,
}
impl Display for ProofType {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
match self {
impl Display for ProofType
{
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result
{
match self
{
ProofType::Body => write!(f, "body_prover"),
ProofType::And => write!(f, "and_prover"),
ProofType::Predicate => write!(f, "predicate_prover"),
@ -19,33 +26,121 @@ impl Display for ProofType {
}
}
pub trait Tracer {
fn begin_proof(&self, proof_type: ProofType) -> Self;
fn print_step<T: Display>(&self, show: T);
pub trait Tracer
{
fn begin_proof(&mut self, proof_type: ProofType) -> Self;
fn print_step<T: Display>(&mut self, show: T);
fn end_proof(self);
}
pub struct SimpleTracer {
pub struct SimpleTracer
{
proof_type: ProofType,
}
impl SimpleTracer {
pub fn new(proof_type: ProofType) -> Self {
impl SimpleTracer
{
pub fn new(proof_type: ProofType) -> Self
{
Self { proof_type }
}
}
impl Tracer for SimpleTracer {
fn begin_proof(&self, proof_type: ProofType) -> Self {
impl Tracer for SimpleTracer
{
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);
}
fn end_proof(self) {
fn end_proof(self)
{
todo!()
}
}
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>()
};
print!("{}", "│".style(style));
}
self.first = false;
println!("{}", show);
// let _ = std::io::stdin().read_line(&mut String::new());
// println!("\x1b[2A");
}
fn end_proof(self)
{
drop(self);
}
}
impl Drop for IndentedTracer
{
fn drop(&mut self) {}
}
impl Default for IndentedTracer
{
fn default() -> Self
{
Self::new()
}
}
pub struct EmptyTracer;
impl Tracer for EmptyTracer
{
fn begin_proof(&mut self, _proof_type: ProofType) -> Self
{
EmptyTracer
}
fn print_step<T: Display>(&mut self, _show: T) {}
fn end_proof(self) {}
}

1
src/prover/unification.rs
View File

@ -1,4 +1,3 @@
use crate::ast::Predicate;
use crate::prover::constraints::Constraints;