use diaphragm_cairo_renderer::CairoRenderer;
use diaphragm_core::{styles::*, types::*, *};
use diaphragm_z3_solver::{z3, Z3Context};

// drawing::{cairo::CairoEngine, Engine},
// z3::{self, ast::Ast},

fn main() {
    let z3_cfg = z3::Config::new();
    let z3_ctx = z3::Context::new(&z3_cfg);
    let ctx = Z3Context::new(&z3_ctx);

    let cairo_renderer = CairoRenderer::new();

    let mut runtime = Runtime::new(Box::new(ctx), Box::new(cairo_renderer));

    let ctx = runtime.solver_ctx();

    let rect1_height = ctx.new_free_float();
    let rect1_width = ctx.new_free_float();

    let rect1_ctx = ShapeContext {
        bounds: Bounds {
            top: ctx.new_fixed_float(10.),
            left: ctx.new_fixed_float(10.),
            height: rect1_height,
            width: rect1_width,
        },
        fill: FillStyle::default(),
        stroke: StrokeStyle::default(),
    };

    let text_bounds = rect1_ctx.bounds.clone();

    let rect1 = core_shapes::Rectangle {};

    let rect2_top = ctx.new_free_float();
    let rect2_left = ctx.new_free_float();

    let rect2_ctx = ShapeContext {
        bounds: Bounds {
            top: rect2_top,
            left: rect2_left,
            height: rect1_width,
            width: rect1_height,
        },
        fill: FillStyle::default(),
        stroke: StrokeStyle::default(),
    };

    let rect2 = core_shapes::Rectangle {};

    let _2 = ctx.new_fixed_float(2.);
    let double_height = ctx.float_mul(&[rect1_height, _2]);
    let width_constraint = ctx.float_eq(rect1_width, double_height);
    ctx.constrain(width_constraint);

    let _42 = ctx.new_fixed_float(42.);
    let width_constraint2 = ctx.float_eq(rect1_width, _42);
    ctx.constrain(width_constraint2);

    let _10 = ctx.new_fixed_float(10.);
    let top_constraint = ctx.float_eq(rect2_top, _10);
    ctx.constrain(top_constraint);

    let bigger_width = ctx.float_add(&[rect1_width, _10]);
    let left_constraint = ctx.float_eq(rect2_left, bigger_width);
    ctx.constrain(left_constraint);

    let text = core_shapes::Text {
        content: String::from("Hello, World!"),
        font: text::FontDescription {
            family: String::from("mono"),
            style: Default::default(),
            weight: Default::default(),
            size: rect1_height,
        },
    };

    let text_ctx = ShapeContext {
        bounds: text_bounds,
        fill: FillStyle::default(),
        stroke: StrokeStyle::default(),
    };

    runtime.add_shape(rect1, rect1_ctx);
    runtime.add_shape(rect2, rect2_ctx);
    runtime.add_shape(text, text_ctx);

    runtime.render();
}

/*
fn main() {
    // simple_test()

    let z3_cfg = z3::Config::new();
    let z3_ctx = z3::Context::new(&z3_cfg);

    let mut ctx = Context::new();

    let rect1_height = z3::ast::Real::new_const(&z3_ctx, "rect1_height");
    let rect1_width = z3::ast::Real::new_const(&z3_ctx, "rect1_width");

    let rect1_bounds = Bounds {
        top: Float::Defined(10.),
        left: Float::Defined(10.),
        height: Float::Constrained(rect1_height.clone()),
        width: Float::Constrained(rect1_width.clone()),
    };

    let rect1 = Bounded::<Box<dyn Drawable>> {
        bounds: rect1_bounds,
        shape: Box::new(Shape::Rectangle(Rectangle {})),
    };

    let rect2_top = z3::ast::Real::new_const(&z3_ctx, "rect2_top");
    let rect2_left = z3::ast::Real::new_const(&z3_ctx, "rect2_left");

    let rect2_bounds = Bounds {
        top: Float::Constrained(rect2_top.clone()),
        left: Float::Constrained(rect2_left.clone()),
        height: Float::Constrained(rect1_width.clone()),
        width: Float::Constrained(rect1_height.clone()),
    };

    let rect2 = Bounded::<Box<dyn Drawable>> {
        bounds: rect2_bounds,
        shape: Box::new(Shape::Rectangle(Rectangle {})),
    };

    let solver = z3::Solver::new(&z3_ctx);

    solver.assert(&rect1_width._eq(&(rect1_height * z3::ast::Real::from_real(&z3_ctx, 2, 1))));
    solver.assert(&rect1_width._eq(&z3::ast::Real::from_real(&z3_ctx, 42, 1)));

    solver.assert(&rect2_top._eq(&z3::ast::Real::from_real(&z3_ctx, 10, 1)));
    solver.assert(&rect2_left._eq(&(rect1_width + z3::ast::Real::from_real(&z3_ctx, 10, 1))));

    ctx.add_shape(rect1);
    ctx.add_shape(rect2);
    ctx.set_constraints(&z3_ctx, &solver);

    solver.check();
    let model = solver.get_model().expect("Failed to get model");

    let shapes = ctx.draw(&model);

    let mut cairo = CairoEngine::new();

    for shape in shapes {
        cairo.draw(&shape);
    }
}

#[allow(dead_code)]
fn simple_test() {
    let mut cairo = CairoEngine::new();

    cairo.draw(&DefinitelyBounded {
        bounds: DefinedBounds {
            top: 10.,
            left: 10.,
            height: 40.,
            width: 40.,
        },
        shape: Shape::Rectangle(Rectangle {}),
    });

    cairo.draw(&DefinitelyBounded {
        bounds: DefinedBounds {
            top: 20.,
            left: 20.,
            height: 40.,
            width: 40.,
        },
        shape: Shape::Text(Text {
            content: String::from("Hello, World!"),
            font: FontDescription {
                family: String::from("Fira Code"),
                size: 21,
                style: FontStyle::Normal,
                weight: FontWeight::Normal,
            },
        }),
    });
}
*/