diff --git a/src/ast.rs b/src/ast.rs index f07abbc..19f413a 100644 --- a/src/ast.rs +++ b/src/ast.rs @@ -1,8 +1,5 @@ -use std::fmt::Display; - -use owo_colors::{OwoColorize, colors::css::Gray}; - use crate::prover::tracing::colored_var; +use std::fmt::Display; pub type Variable = String; diff --git a/src/prover.rs b/src/prover.rs index 0f3187e..8c95c4f 100644 --- a/src/prover.rs +++ b/src/prover.rs @@ -8,7 +8,6 @@ use std::rc::Rc; use litemap::LiteMap; use owo_colors::OwoColorize; -use owo_colors::Style; use owo_colors::colors::Green; use owo_colors::colors::Red; use owo_colors::colors::Yellow; @@ -20,7 +19,6 @@ use crate::ast::Predicate; use crate::prover::constraints::Constraints; use crate::prover::tracing::IndentedTracer; use crate::prover::tracing::ProofType; -use crate::prover::tracing::SimpleTracer; use crate::prover::tracing::Tracer; #[derive(Clone, Copy, Debug, Default)] @@ -54,11 +52,8 @@ impl GlobalCounter } } -pub struct BodyProver<'a, T: Tracer + 'a> +pub struct BodyProver<'a> { - module: &'a Module, - constraints: Constraints, - tracer: Option, prover: Box + 'a>, } @@ -72,19 +67,18 @@ pub struct PredicateProver<'a, T: Tracer> global_counter: GlobalCounter, current_clause: usize, - sub_proof: Option>, + sub_proof: Option>, } pub struct AndProver<'a, T: Tracer> { module: &'a Module, bodies: Vec, - constraints: Constraints, tracer: T, current_tracer: T, global_counter: GlobalCounter, - sub_proofs: Vec<(Counter, BodyProver<'a, T>)>, + sub_proofs: Vec<(Counter, BodyProver<'a>)>, } pub struct OrProver<'a, T: Tracer> @@ -98,27 +92,19 @@ pub struct OrProver<'a, T: Tracer> current_proving: usize, global_counter: GlobalCounter, counter_snapshot: Counter, - sub_proof: Option>, + sub_proof: Option>, } -impl<'a, T: Tracer + 'a> BodyProver<'a, T> +impl<'a> BodyProver<'a> { - pub fn new( + pub fn new( module: &'a Module, global_counter: GlobalCounter, body: Body, constraints: Constraints, tracer: &mut T, - ) -> BodyProver<'a, T> + ) -> BodyProver<'a> { - let body_tracer = if let Body::And(_) = body - { - Some(tracer.begin_proof(ProofType::Body)) - } - else - { - None - }; let prover: Box> = match &body { Body::Term(predicate) => Box::new(PredicateProver::new( @@ -153,13 +139,8 @@ impl<'a, T: Tracer + 'a> BodyProver<'a, T> tracer, )), }; - //info!(target: "BodyProver", "Proving {}", body); - BodyProver { - tracer: body_tracer, - module, - constraints, - prover, - } + + BodyProver { prover } } } @@ -249,7 +230,6 @@ impl AndProver<'_, T> )], current_tracer, bodies, - constraints, global_counter, } } @@ -330,7 +310,6 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> { 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)); @@ -394,7 +373,7 @@ impl<'a, T: Tracer + 'a> Iterator for PredicateProver<'a, T> } } -impl<'a, T: Tracer + 'a> Iterator for BodyProver<'a, T> +impl<'a> Iterator for BodyProver<'a> { type Item = Constraints; fn next(&mut self) -> Option @@ -516,6 +495,8 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> { 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(), @@ -532,7 +513,7 @@ impl<'a, T: Tracer + 'a> Iterator for OrProver<'a, T> impl Module { - pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a, impl Tracer> + pub fn prove<'a>(&'a self, body: &'a Body) -> BodyProver<'a> { BodyProver::new( self, diff --git a/src/prover/tracing.rs b/src/prover/tracing.rs index 6e7c6d0..60ea6f5 100644 --- a/src/prover/tracing.rs +++ b/src/prover/tracing.rs @@ -1,10 +1,9 @@ -use std::{cell::RefCell, default, fmt::Display, rc::Rc}; - use log::info; use owo_colors::{ OwoColorize, Style, colors::css::{DarkGray, Gray}, }; +use std::fmt::Display; use crate::ast::Variable; diff --git a/src/prover/unification.rs b/src/prover/unification.rs index 747d458..d6d5042 100644 --- a/src/prover/unification.rs +++ b/src/prover/unification.rs @@ -1,5 +1,3 @@ -use log::debug; - use crate::ast::Predicate; use crate::prover::constraints::Constraints;