pub mod constraints;
pub mod drawable;
pub mod shapes;
pub mod text;
pub mod types;

pub use self::drawable::Drawable;
pub use self::shapes::Shape as CoreShape;
pub use self::types::{Bounded, Bounds, DefinitelyBounded};

use self::constraints::Constrainable;

const RECURSION_LIMIT: u64 = 10_000;

pub struct Context<'z3> {
    drawables: Vec<Bounded<'z3, Box<dyn Drawable>>>,
}

impl<'z3> Context<'z3> {
    pub fn new() -> Self {
        Self { drawables: vec![] }
    }

    pub fn add_shape(&mut self, shape: Bounded<'z3, Box<dyn Drawable>>) {
        self.drawables.push(shape);
    }

    pub fn set_constraints(&self, z3_ctx: &z3::Context, solver: &z3::Solver) {
        for drawable in &self.drawables {
            for constraint in drawable.shape.constraints(&drawable.bounds, &z3_ctx) {
                solver.assert(&constraint);
            }
        }
    }

    // TODO: simplify until not possible?

    pub fn draw(&self, model: &z3::Model) -> Vec<DefinitelyBounded<CoreShape>> {
        let mut acc_core_drawables = Vec::new();
        let mut acc_complex_drawables = Vec::new();

        for drawable in &self.drawables {
            let bounds = &drawable.bounds;
            let shape = &drawable.shape;

            let (core_drawables, mut complex_drawables) = shape.draw(bounds);

            acc_core_drawables.extend(core_drawables.iter().map(|Bounded { bounds, shape }| {
                DefinitelyBounded {
                    bounds: bounds.fixate(model),
                    shape: shape.clone(),
                }
            }));

            acc_complex_drawables.append(&mut complex_drawables);
        }

        let mut recursion_count = 0;

        while !acc_complex_drawables.is_empty() {
            recursion_count += 1;

            let mut tmp_complex_drawables = Vec::new();

            for drawable in acc_complex_drawables.drain(..) {
                let bounds = drawable.bounds;
                let shape = drawable.shape;

                let (core_drawables, mut complex_drawables) = shape.draw(&bounds);

                acc_core_drawables.extend(core_drawables.into_iter().map(
                    |Bounded { bounds, shape }| DefinitelyBounded {
                        bounds: bounds.fixate(model),
                        shape,
                    },
                ));

                tmp_complex_drawables.append(&mut complex_drawables);
            }

            acc_complex_drawables = tmp_complex_drawables;

            if recursion_count > RECURSION_LIMIT {
                panic!("Recursion limit reached");
            }
        }

        acc_core_drawables
    }
}