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

Fixes infinite loop

Browse Source
This commit is contained in:
Albin Chaboissier
2026-02-09 09:07:38 +01:00
parent 134ebc6dc6
commit 694a84fb00
7 changed files with 12589 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

0
1 Normal file
View File

12518
head Normal file
View File

File diff suppressed because it is too large Load Diff

2
src/ast.rs
View File

@ -23,7 +23,7 @@ pub enum Body
Or(Vec<Body>),
}
#[derive(Clone, Debug)]
#[derive(Clone, Debug, PartialEq)]
pub enum Predicate
{
Variable(Variable), // Upercase variable like X

15
src/main.rs
View File

@ -22,16 +22,17 @@ 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 = "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();
// // let p1: Predicate = "integer(s(X))".into();
// println!("{}", p.matches(&p1).unwrap());
//
}

6
src/prover/constraints.rs
View File

@ -1,11 +1,9 @@
use std::fmt::Display;
use litemap::LiteMap;
use winnow::Str;
use crate::ast::Predicate;
use crate::ast::Variable;
use crate::prover::constraints;
#[derive(Clone, Debug)]
pub struct Constraints
@ -33,6 +31,10 @@ impl Constraints
{
if let Some(other_predicate) = self.set.get(variable)
{
if predicate == other_predicate
{
return true;
}
// If variable is already contrained, we need to check if both contraints are
// contradictory

55
src/prover/tracing.rs Normal file
View File

@ -0,0 +1,55 @@
use std::fmt::Display;
use log::info;
#[derive(Clone, Copy)]
pub enum ProofType
{
Body,
And,
Predicate,
}
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"),
}
}
}
pub trait Tracer
{
fn next_step(&mut self, proof_type: ProofType) -> Self;
fn milestone<T: Display>(&self, str: T);
fn explain<T: Display>(&self, str: T);
}
pub struct SimpleTracer
{
proof_type: ProofType,
}
impl Tracer for SimpleTracer
{
fn next_step(&mut self, proof_type: ProofType) -> Self
{
SimpleTracer { proof_type }
}
fn explain<T: Display>(&self, str: T)
{
let proof_str = format!("{}", self.proof_type);
info!(target: &proof_str, "{}", str);
}
fn milestone<T: Display>(&self, str: T)
{
self.explain(str);
}
}

4
src/prover/unification.rs
View File

@ -13,11 +13,11 @@ impl Predicate
/// returns `None` if the predicate cannot be unified against the other
pub fn matches(&self, other: &Predicate) -> Option<Constraints>
{
debug!("Unifying {} against {}", self, other);
match self
{
Predicate::Variable(variable) =>
{
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,6 +32,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);
Some(Constraints::with(var.clone(), self.clone()))
}
// Match pred(X, Y, Z, ...) with pred(_X, _Y, _Z, ...)
@ -39,6 +40,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);
if arguments.is_empty()
{
return Some(Constraints::none());