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
        }
    }
}