use crate::core_shapes::{CoreDrawable, CoreShape, DefinedCoreDrawable, DefinedCoreShape};

use super::styles::*;
use super::text::*;
use super::types::{Bool, Float};

#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
pub struct VariableHandle(usize);

impl VariableHandle {
    pub fn new(id: usize) -> Self {
        Self(id)
    }

    pub fn id(&self) -> usize {
        self.0
    }
}

/*
pub trait VariableFloat<'a> {
    fn id(&self) -> usize;
    fn dyn_clone(&self) -> Box<dyn VariableFloat<'a> + 'a>;

    fn eq(&self, other: &dyn VariableFloat) -> Bool<'a>;
    fn neq(&self, other: &dyn VariableFloat) -> Bool<'a>;
    fn gt(&self, other: &dyn VariableFloat) -> Bool<'a>;
    fn ge(&self, other: &dyn VariableFloat) -> Bool<'a>;
    fn lt(&self, other: &dyn VariableFloat) -> Bool<'a>;
    fn le(&self, other: &dyn VariableFloat) -> Bool<'a>;

    fn add(&self, other: &dyn VariableFloat) -> Float<'a>;
    fn sub(&self, other: &dyn VariableFloat) -> Float<'a>;
    fn mul(&self, other: &dyn VariableFloat) -> Float<'a>;
    fn div(&self, other: &dyn VariableFloat) -> Float<'a>;

    fn neg(&self) -> Float<'a>;
}

pub trait VariableBool<'a> {
    fn id(&self) -> usize;
    fn dyn_clone(&self) -> Box<dyn VariableBool<'a> + 'a>;

    fn eq(&self, other: &dyn VariableBool) -> Bool<'a>;
    fn neq(&self, other: &dyn VariableBool) -> Bool<'a>;

    fn and(&self, other: &dyn VariableBool) -> Bool<'a>;
    fn or(&self, other: &dyn VariableBool) -> Bool<'a>;

    fn not(&self) -> Bool<'a>;
}
*/

pub trait SolverContext {
    fn solve<'a>(&'a self) -> Box<dyn SolverModel + 'a>;
    fn constrain(&mut self, assertion: Bool);

    // Floats

    fn new_free_float(&mut self) -> Float;
    fn new_fixed_float(&mut self, value: f64) -> Float;

    fn float_add(&mut self, values: &[Float]) -> Float;
    fn float_sub(&mut self, values: &[Float]) -> Float;
    fn float_mul(&mut self, values: &[Float]) -> Float;
    fn float_div(&mut self, lhs: Float, rhs: Float) -> Float;
    fn float_neg(&mut self, value: Float) -> Float;

    fn float_eq(&mut self, lhs: Float, rhs: Float) -> Bool;
    fn float_ne(&mut self, lhs: Float, rhs: Float) -> Bool;
    fn float_gt(&mut self, lhs: Float, rhs: Float) -> Bool;
    fn float_ge(&mut self, lhs: Float, rhs: Float) -> Bool;
    fn float_lt(&mut self, lhs: Float, rhs: Float) -> Bool;
    fn float_le(&mut self, lhs: Float, rhs: Float) -> Bool;

    fn float_max(&mut self, values: &[Float]) -> Float {
        let result = self.new_free_float();

        for (index, &candidate) in values.iter().enumerate() {
            let comparisons: Vec<_> = values
                .iter()
                .enumerate()
                .filter(|(other_index, _)| *other_index != index)
                .map(|(_, &other)| self.float_ge(candidate, other))
                .collect();

            let premise = self.bool_and(&comparisons);
            let conclusion = self.float_eq(candidate, result);
            let implication = self.bool_implies(premise, conclusion);
            self.constrain(implication);
        }

        result
    }

    fn float_min(&mut self, values: &[Float]) -> Float {
        let result = self.new_free_float();

        for (index, &candidate) in values.iter().enumerate() {
            let comparisons: Vec<_> = values
                .iter()
                .enumerate()
                .filter(|(other_index, _)| *other_index != index)
                .map(|(_, &other)| self.float_le(candidate, other))
                .collect();

            let premise = self.bool_and(&comparisons);
            let conclusion = self.float_eq(candidate, result);
            let implication = self.bool_implies(premise, conclusion);
            self.constrain(implication);
        }

        result
    }

    // Bools

    fn new_free_bool(&mut self) -> Bool;
    fn new_fixed_bool(&mut self, value: bool) -> Bool;

    fn bool_eq(&mut self, lhs: Bool, rhs: Bool) -> Bool;
    fn bool_ne(&mut self, lhs: Bool, rhs: Bool) -> Bool;

    fn bool_and(&mut self, values: &[Bool]) -> Bool;
    fn bool_or(&mut self, values: &[Bool]) -> Bool;
    fn bool_not(&mut self, value: Bool) -> Bool;

    fn bool_implies(&mut self, lhs: Bool, rhs: Bool) -> Bool;
}

pub trait SolverModel {
    fn eval_float(&self, f: Float) -> Option<f64>;
    fn eval_bool(&self, b: Bool) -> Option<bool>;
}

/*
pub trait Solver {
    fn constrain(&mut self, assertion: &Bool);
    fn solve(&self) -> Box<dyn SolverModel>;
}
*/

use super::types::*;

pub trait Constrainable {
    type Fixated;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated>;
}

impl Constrainable for CoreShape {
    type Fixated = DefinedCoreShape;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        match self {
            CoreShape::Rectangle(r) => Some(DefinedCoreShape::Rectangle(*r)),
            CoreShape::Text(t) => t.fixate(model).map(DefinedCoreShape::Text),
        }
    }
}

impl Constrainable for Float {
    type Fixated = f64;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        model.eval_float(*self)
    }

    /*
    fn fixate(&self, model: &Model) -> Self::Fixated {
        match self {
            Float::Defined(float) => *float,
            Float::Constrained(variable) => {
                let (num, den) = model
                    .eval::<z3::ast::Real>(variable)
                    .expect("Couldn't eval variable")
                    .as_real()
                    .expect("Couldn't get value from variable");

                num as f64 / den as f64
            }
            Float::Undefined => panic!("Undefined float"),
        }
    }
    */
}

impl Constrainable for Bounds {
    type Fixated = DefinedBounds;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedBounds {
            top: self.top.fixate(model)?,
            left: self.left.fixate(model)?,
            width: self.width.fixate(model)?,
            height: self.height.fixate(model)?,
        })
    }
}

impl Constrainable for StrokeStyle {
    type Fixated = DefinedStrokeStyle;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        let dash = match &self.dash {
            Some(dash) => Some(dash.fixate(model)?),
            None => None,
        };

        Some(DefinedStrokeStyle {
            pattern: self.pattern,
            dash,
            line_width: self.line_width.fixate(model)?,
        })
    }
}

impl Constrainable for DashStyle {
    type Fixated = DefinedDashStyle;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedDashStyle {
            dashes: self
                .dashes
                .iter()
                .map(|value| value.fixate(model))
                .collect::<Option<_>>()?,
            offset: self.offset.fixate(model)?,
        })
    }
}

impl Constrainable for CoreDrawable {
    type Fixated = DefinedCoreDrawable;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedCoreDrawable {
            shape: self.shape.fixate(model)?,
            context: self.context.fixate(model)?,
        })
    }
}

impl Constrainable for CoreShapeContext {
    type Fixated = DefinedCoreShapeContext;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedCoreShapeContext {
            bounds: self.bounds.fixate(model)?,
            fill: self.fill.clone(),
            stroke: self.stroke.fixate(model)?,
        })
    }
}

impl Constrainable for Point2D {
    type Fixated = DefinedPoint2D;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedPoint2D {
            x: self.x.fixate(model)?,
            y: self.y.fixate(model)?,
        })
    }
}

impl Constrainable for FontDescription {
    type Fixated = DefinedFontDescription;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedFontDescription {
            family: self.family.clone(),
            style: self.style,
            weight: self.weight,
            size: self.size.fixate(model)?,
        })
    }
}

impl Constrainable for Text {
    type Fixated = DefinedText;

    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
        Some(DefinedText {
            content: self.content.clone(),
            font: self.font.fixate(model)?,
        })
    }
}

// impl Constrainable for StraightPath {
//     type Fixated = DefinedStraightPath;
//
//     fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
//         let points: Option<_> = self
//             .points
//             .iter()
//             .map(|point| point.fixate(model))
//             .collect();
//         Some(DefinedStraightPath { points: points? })
//     }
// }