Finishes cache

src/main.rs

@@ -21,7 +21,7 @@ fn main()
     .into();
 
     //let prop: Body = "integer(s(X))".into();
-    let prop: Body = "mult(X, s(zero), s(zero))".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)

src/prover.rs

@@ -19,6 +19,7 @@ use crate::ast::Predicate;
 use crate::ast::Variable;
 use crate::prover::body::BodyProver;
 use crate::prover::constraints::Constraints;
+use crate::prover::tracing::EmptyTracer;
 use crate::prover::tracing::IndentedTracer;
 
 #[derive(Clone, Copy, Debug, Default)]
@@ -31,7 +32,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
@@ -61,6 +67,7 @@ impl Module
             GlobalCounter::new(),
             body.clone(),
             Constraints::none(),
+            //&mut EmptyTracer,
             &mut IndentedTracer::new(),
             //&SimpleTracer::new(ProofType::Body),
         )

src/prover/constraints.rs

@@ -8,7 +8,7 @@ use crate::ast::Variable;
 #[derive(Clone, Debug)]
 pub struct Constraints
 {
-    set: HashMap<Variable, Predicate>,
+    pub(crate) set: HashMap<Variable, Predicate>,
 }
 
 impl Constraints

src/prover/proof_cache.rs

@@ -1,15 +1,20 @@
-use std::{cell::RefCell, num::NonZero, rc::Rc};
+use std::cell::RefCell;
+use std::num::NonZero;
+use std::rc::Rc;
 
 use bimap::BiHashMap;
 use lru::LruCache;
 
-use crate::{
-    ast::{Body, Predicate, Variable},
-    prover::{
-        body::{self, BodyProver},
-        constraints::Constraints,
-    },
-};
+use crate::ast::Body;
+use crate::ast::Module;
+use crate::ast::Predicate;
+use crate::ast::Variable;
+use crate::prover::GlobalCounter;
+use crate::prover::body::BodyProver;
+use crate::prover::body::{self};
+use crate::prover::constraints;
+use crate::prover::constraints::Constraints;
+use crate::prover::tracing::EmptyTracer;
 
 pub struct PartialProof<T: Iterator<Item = Constraints>>
 {
@@ -19,9 +24,13 @@ pub struct PartialProof<T: Iterator<Item = Constraints>>
 
 pub struct CachedProver<'a>
 {
+    module: &'a Module,
     cache: Rc<RefCell<LruCache<Body, PartialProof<BodyProver<'a>>>>>,
-    body: Body,
+    normalized_body: Body,
+    normalized_counter: usize,
     mapping: VariableMap,
+    constraints: Constraints,
+
     proof_counter: usize,
 }
 
@@ -39,22 +48,68 @@ impl<'a> ProofCache<'a>
         }
     }
 
-    pub fn prove(&mut self, body: &Body) -> CachedProver<'a>
+    pub fn prove(
+        &mut self,
+        module: &'a Module,
+        constraints: &Constraints,
+        body: &Body,
+    ) -> CachedProver<'a>
     {
-        let (varmap, normalized) = body.normalized();
+        let (varmap, counter, normalized) = body.normalized();
+        CachedProver {
+            module,
+            cache: self.cache.clone(),
+            normalized_body: normalized,
+            normalized_counter: counter,
+            mapping: varmap,
+            proof_counter: 0,
+            constraints: constraints.clone(),
+        }
+    }
+}
 
-        // Check if in cache ?
-        match self.cache.borrow().get(&normalized)
+impl<'a> Iterator for CachedProver<'a>
+{
+    type Item = Constraints;
+
+    fn next(&mut self) -> Option<Self::Item>
+    {
+        let constraints;
         {
-            Some() => todo!(),
-            None => todo!(),
+            let mut cache_borrow = self.cache.borrow_mut();
+            let partial_proof =
+                cache_borrow.get_or_insert_mut(self.normalized_body.clone(), || PartialProof {
+                    proved: vec![],
+                    prover: BodyProver::new(
+                        self.module,
+                        GlobalCounter::with(self.normalized_counter),
+                        self.normalized_body.clone(),
+                        Constraints::none(),
+                        &mut EmptyTracer,
+                    ),
+                });
+
+            while partial_proof.proved.len() <= self.proof_counter
+            {
+                let constraints = partial_proof.prover.next();
+                match constraints
+                {
+                    Some(constraints) => partial_proof.proved.push(constraints),
+                    None => return None,
+                }
+            }
+            self.proof_counter += 1;
+            let normalized_proof = partial_proof.proved[self.proof_counter]
+                .clone()
+                .contextualized(&self.mapping);
+            // Check if we can get a match
+            constraints = self.constraints.and(&normalized_proof);
         }
 
-        CachedProver {
-            cache: self.cache.clone(),
-            body: normalized,
-            mapping: todo!(),
-            proof_counter: todo!(),
+        match constraints
+        {
+            Some(c) => Some(c),
+            None => self.next(),
         }
     }
 }
@@ -65,13 +120,13 @@ pub struct VariableMap(BiHashMap<Variable, Variable>);
 
 pub trait Normalizable: Sized
 {
-    fn normalized(&self) -> (VariableMap, Self)
+    fn normalized(&self) -> (VariableMap, usize, Self)
     {
         let mut bimap = BiHashMap::new();
         let mut counter = 0;
         let normalized = self.normalized_with(&mut counter, &mut bimap);
 
-        (VariableMap(bimap), normalized)
+        (VariableMap(bimap), counter, normalized)
     }
 
     fn normalized_with(&self, counter: &mut usize, map: &mut BiHashMap<Variable, Variable>)
@@ -133,7 +188,7 @@ impl Normalizable for Variable
         map: &mut BiHashMap<Variable, Variable>,
     ) -> Variable
     {
-        match map.get_by_left(&self)
+        match map.get_by_left(self)
         {
             Some(normalized) => normalized.clone(),
             None =>
@@ -148,3 +203,37 @@ impl Normalizable for Variable
         }
     }
 }
+
+impl Predicate
+{
+    fn contextualized(&self, map: &VariableMap) -> Predicate
+    {
+        match self
+        {
+            Predicate::Variable(variable) =>
+            {
+                Predicate::Variable(map.0.get_by_right(variable).unwrap().clone())
+            }
+            Predicate::Fixed(name, predicates) => Predicate::Fixed(
+                name.clone(),
+                predicates.iter().map(|p| p.contextualized(map)).collect(),
+            ),
+        }
+    }
+}
+
+impl Constraints
+{
+    pub fn contextualized(&self, map: &VariableMap) -> Constraints
+    {
+        let mut new = Constraints::none();
+        for (var, pred) in self.set.iter()
+        {
+            let ctx_var = map.0.get_by_right(var).unwrap();
+            let ctx_pred = pred.contextualized(map);
+            new.set.insert(ctx_var.clone(), ctx_pred);
+        }
+
+        new
+    }
+}

src/prover/tracing.rs

@@ -1,8 +1,8 @@
 use log::info;
-use owo_colors::{
-    OwoColorize, Style,
-    colors::css::{DarkGray, Gray},
-};
+use owo_colors::OwoColorize;
+use owo_colors::Style;
+use owo_colors::colors::css::DarkGray;
+use owo_colors::colors::css::Gray;
 use std::fmt::Display;
 
 use crate::ast::Variable;
@@ -110,8 +110,8 @@ impl Tracer for IndentedTracer
         }
         self.first = false;
         println!("{}", show);
-        let _ = std::io::stdin().read_line(&mut String::new());
-        println!("\x1b[2A");
+        // let _ = std::io::stdin().read_line(&mut String::new());
+        // println!("\x1b[2A");
     }
 
     fn end_proof(self)
@@ -132,3 +132,17 @@ impl Default for IndentedTracer
         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) {}
+}