WIP

11 files changed, 1532 insertions, 0 deletions

diff --git a/core/src/colors.rs b/core/src/colors.rs
new file mode 100644
index 0000000..ba78fa3
--- /dev/null
+++ b/core/src/colors.rs
@@ -0,0 +1,34 @@
+type Srgba = palette::Srgba<f64>;
+
+#[derive(Copy, Clone, PartialEq, Debug, Default)]
+pub struct Color(Srgba);
+
+impl Color {
+    pub fn transparent() -> Self {
+        Color(Srgba::new(0., 0., 0., 0.))
+    }
+
+    pub fn white() -> Self {
+        Color(Srgba::new(1., 1., 1., 1.))
+    }
+
+    pub fn black() -> Self {
+        Color(Srgba::new(0., 0., 0., 1.))
+    }
+
+    pub fn from_rgb(r: f64, g: f64, b: f64) -> Self {
+        Color(Srgba::new(r, g, b, 1.0))
+    }
+
+    pub fn from_rgba(r: f64, g: f64, b: f64, a: f64) -> Self {
+        Color(Srgba::new(r, g, b, a))
+    }
+
+    pub fn rgb(&self) -> (f64, f64, f64) {
+        (self.0.red, self.0.green, self.0.blue)
+    }
+
+    pub fn rgba(&self) -> (f64, f64, f64, f64) {
+        (self.0.red, self.0.green, self.0.blue, self.0.alpha)
+    }
+}
diff --git a/core/src/complex_shapes.rs b/core/src/complex_shapes.rs
new file mode 100644
index 0000000..e23881d
--- /dev/null
+++ b/core/src/complex_shapes.rs
@@ -0,0 +1,285 @@
+use super::core_shapes::CoreShape;
+use super::solving::SolverContext;
+use super::styles::{FillStyle, StrokeStyle};
+use super::types::{Bounds, ShapeContext, ShapeContextBuilder};
+
+pub trait ComplexShape: DynClone {
+    fn as_core_shape(&self) -> Option<&dyn CoreShape> {
+        None
+    }
+
+    fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult;
+}
+
+pub trait DynClone {
+    fn dyn_clone(&self) -> Box<dyn ComplexShape>;
+}
+
+impl<T: Clone + ComplexShape + 'static> DynClone for T {
+    fn dyn_clone(&self) -> Box<dyn ComplexShape> {
+        Box::new(self.clone())
+    }
+}
+
+#[derive(Debug, Clone)]
+pub struct Drawable<T: ComplexShape> {
+    pub(crate) context: ShapeContext,
+    pub(crate) shape: T,
+}
+
+impl<T: ComplexShape> Drawable<T> {
+    pub fn new(shape: T, context: ShapeContext) -> Self {
+        Self { context, shape }
+    }
+
+    pub fn from_shape(shape: T, solver: &mut dyn SolverContext) -> Self {
+        Self {
+            context: ShapeContext::builder().build(solver),
+            shape,
+        }
+    }
+
+    pub fn builder(shape: T) -> DrawableBuilder<T>
+    where
+        T: Clone,
+    {
+        DrawableBuilder::new(shape)
+    }
+
+    pub fn shape(&self) -> &T {
+        &self.shape
+    }
+
+    pub fn shape_mut(&mut self) -> &mut T {
+        &mut self.shape
+    }
+
+    pub fn bounds(&self) -> &Bounds {
+        &self.context.bounds
+    }
+
+    pub fn bounds_mut(&mut self) -> &mut Bounds {
+        &mut self.context.bounds
+    }
+
+    pub fn fill_style(&mut self) -> &mut FillStyle {
+        &mut self.context.fill
+    }
+
+    pub fn stroke_style(&mut self) -> &mut StrokeStyle {
+        &mut self.context.stroke
+    }
+}
+
+pub struct DrawableBuilder<T: ComplexShape> {
+    context: ShapeContextBuilder,
+    shape: T,
+}
+
+impl<T: ComplexShape + Clone> DrawableBuilder<T> {
+    pub fn new(shape: T) -> Self {
+        Self {
+            context: ShapeContext::builder(),
+            shape,
+        }
+    }
+
+    pub fn bounds(&mut self, bounds: Bounds) -> &mut Self {
+        self.context.bounds(bounds);
+        self
+    }
+
+    pub fn fill(&mut self, fill: FillStyle) -> &mut Self {
+        self.context.fill(fill);
+        self
+    }
+
+    pub fn stroke(&mut self, stroke: StrokeStyle) -> &mut Self {
+        self.context.stroke(stroke);
+        self
+    }
+
+    pub fn build(&self, solver: &mut dyn SolverContext) -> Drawable<T> {
+        Drawable {
+            shape: self.shape.clone(),
+            context: self.context.build(solver),
+        }
+    }
+}
+
+pub struct DynDrawable {
+    pub(crate) context: ShapeContext,
+    pub(crate) shape: Box<dyn ComplexShape>,
+}
+
+// TODO: copy paste is bad?
+impl DynDrawable {
+    pub fn new<T: ComplexShape + 'static>(shape: T, context: ShapeContext) -> Self {
+        Self {
+            context,
+            shape: Box::new(shape),
+        }
+    }
+
+    pub fn new_dyn(shape: Box<dyn ComplexShape>, context: ShapeContext) -> Self {
+        Self { context, shape }
+    }
+
+    pub fn from_shape<T: ComplexShape + 'static>(shape: T, solver: &mut dyn SolverContext) -> Self {
+        Self {
+            context: ShapeContext::builder().build(solver),
+            shape: Box::new(shape),
+        }
+    }
+
+    pub fn from_dyn(shape: Box<dyn ComplexShape>, solver: &mut dyn SolverContext) -> Self {
+        Self {
+            context: ShapeContext::builder().build(solver),
+            shape,
+        }
+    }
+
+    pub fn shape(&self) -> &dyn ComplexShape {
+        &*self.shape
+    }
+
+    pub fn shape_mut(&mut self) -> &mut dyn ComplexShape {
+        &mut *self.shape
+    }
+
+    pub fn bounds(&self) -> &Bounds {
+        &self.context.bounds
+    }
+
+    pub fn bounds_mut(&mut self) -> &mut Bounds {
+        &mut self.context.bounds
+    }
+
+    pub fn fill_style(&mut self) -> &mut FillStyle {
+        &mut self.context.fill
+    }
+
+    pub fn stroke_mut(&mut self) -> &mut StrokeStyle {
+        &mut self.context.stroke
+    }
+}
+
+impl Clone for DynDrawable {
+    fn clone(&self) -> Self {
+        DynDrawable {
+            context: self.context.clone(),
+            shape: self.shape.dyn_clone(),
+        }
+    }
+}
+
+impl<T: ComplexShape + 'static> From<Drawable<T>> for DynDrawable {
+    fn from(drawable: Drawable<T>) -> Self {
+        DynDrawable {
+            context: drawable.context,
+            shape: Box::new(drawable.shape),
+        }
+    }
+}
+
+pub struct DrawResult {
+    pub(crate) subshapes: Vec<DynDrawable>,
+    pub(crate) waiting_on: Vec<()>,
+}
+
+impl DrawResult {
+    pub fn new() -> Self {
+        Self {
+            subshapes: Vec::new(),
+            waiting_on: Vec::new(),
+        }
+    }
+
+    /*
+    pub fn push_shape<T: ComplexShape + 'static>(&mut self, shape: T, context: ShapeContext) {
+        self.subshapes.push(DynDrawable {
+            context,
+            shape: Box::new(shape),
+        })
+    }
+
+    pub fn push_boxed_shape(&mut self, shape: Box<dyn ComplexShape>, context: ShapeContext) {
+        self.subshapes.push(DynDrawable { context, shape })
+    }
+    */
+
+    pub fn push<T: ComplexShape + 'static>(&mut self, drawable: Drawable<T>) {
+        self.subshapes.push(drawable.into())
+    }
+
+    pub fn push_dyn(&mut self, drawable: DynDrawable) {
+        self.subshapes.push(drawable)
+    }
+}
+
+/*
+pub trait Drawable {
+    fn draw<'z3>(&self, bounds: &Bounds<'z3>, z3_ctx: &z3::Context) -> DrawResult;
+}
+
+/*
+impl Drawable for Box<dyn Drawable> {
+    fn draw<'z3>(&self, bounds: &Bounds<'z3>, z3_ctx: &z3::Context) -> DrawResult {
+        (**self).draw(bounds, z3_ctx)
+    }
+}
+*/
+
+impl Drawable for CoreShape {
+    fn draw<'z3>(
+        &self,
+        bounds: &Bounds<'z3>,
+    ) -> (
+        Vec<Bounded<'z3, CoreShape>>,
+        Vec<Bounded<'z3, Box<dyn Drawable>>>,
+    ) {
+        // TODO: clone, really?
+        (
+            vec![Bounded::<CoreShape> {
+                bounds: bounds.clone(),
+                shape: self.clone(),
+            }],
+            vec![],
+        )
+    }
+
+    fn constraints(&self, _bounds: &Bounds, _z3_ctx: &z3::Context) -> Vec<z3::ast::Bool> {
+        vec![]
+    }
+}
+
+/*
+impl<'a, T: Drawable> Drawable for Vec<Bounded<'a, T>> {
+    fn draw<'z3>(
+        &self,
+        _bounds: &Bounds<'z3>,
+  as_render        Vec<Bounded<'z3, CoreShape>>,
+        Vec<Bounded<'z3, Box<dyn Drawable>>>,
+    ) {
+        let mut core_shapes = Vec::new();
+        let mut complex_drawables = Vec::new();
+
+        for drawable in self.iter() {
+            let (mut inner_core_shapes, mut inner_complex_drawables) =
+                drawable.shape.draw(&drawable.bounds);
+
+            core_shapes.append(&mut inner_core_shapes);
+            complex_drawables.append(&mut inner_complex_drawables);
+        }
+
+        (core_shapes, complex_drawables)
+    }
+
+    fn constraints(&self, _bounds: &Bounds, z3_ctx: &z3::Context) -> Vec<z3::ast::Bool> {
+        self.iter()
+            .flat_map(|drawable| drawable.shape.constraints(&drawable.bounds, z3_ctx))
+            .collect()
+    }
+}
+*/
+*/
diff --git a/core/src/core_shapes.rs b/core/src/core_shapes.rs
new file mode 100644
index 0000000..c3d3cae
--- /dev/null
+++ b/core/src/core_shapes.rs
@@ -0,0 +1,86 @@
+use super::complex_shapes::{ComplexShape, DrawResult};
+use super::rendering::{Render, Renderer};
+use super::solving::{Constrainable, SolverContext, SolverModel};
+use super::types::*;
+
+pub trait CoreShape {
+    fn constrain(
+        &self,
+        _context: &ShapeContext,
+        _solver: &mut dyn SolverContext,
+        _renderer: &dyn Renderer,
+    ) {
+    }
+    fn to_render(&self, model: &dyn SolverModel) -> Option<Box<dyn Render>>;
+}
+
+impl<T: CoreShape + Clone + 'static> ComplexShape for T {
+    fn as_core_shape(&self) -> Option<&dyn CoreShape> {
+        Some(self)
+    }
+
+    fn draw(&self, _context: &ShapeContext, _solver: &mut dyn SolverContext) -> DrawResult {
+        panic!("Tried to decompose core shape")
+    }
+}
+
+// TODO: add default
+#[derive(Copy, Clone, Debug, Default)]
+pub struct Rectangle {}
+
+impl CoreShape for Rectangle {
+    fn to_render(&self, _model: &dyn SolverModel) -> Option<Box<dyn Render>> {
+        Some(Box::new(self.clone()))
+    }
+}
+
+pub use super::text::{DefinedText, Text};
+
+impl CoreShape for Text {
+    fn constrain(
+        &self,
+        context: &ShapeContext,
+        solver: &mut dyn SolverContext,
+        renderer: &dyn Renderer,
+    ) {
+        let height_constraint = solver.float_eq(context.bounds.height, self.font.size);
+        solver.constrain(height_constraint);
+
+        // TODO: handle multiline
+        let (width, height) = renderer.text_extents(&self.content, &self.font);
+        dbg!(height);
+
+        let scale = solver.float_div(self.font.size, Float::Fixed(height));
+
+        let calculated_width = solver.float_mul(&[Float::Fixed(width), scale]);
+        let width_constraint = solver.float_eq(context.bounds.width, calculated_width);
+        solver.constrain(width_constraint);
+    }
+
+    fn to_render(&self, model: &dyn SolverModel) -> Option<Box<dyn Render>> {
+        self.fixate(model)
+            .map(|path| -> Box<dyn Render> { Box::new(path) })
+    }
+}
+
+#[derive(Clone, Debug, Default)]
+pub struct StraightPath {
+    pub(crate) points: Vec<Point2D>,
+}
+
+impl StraightPath {
+    pub fn new(points: Vec<Point2D>) -> Self {
+        Self { points }
+    }
+}
+
+pub struct DefinedStraightPath {
+    pub(crate) points: Vec<DefinedPoint2D>,
+}
+
+impl CoreShape for StraightPath {
+    fn to_render(&self, model: &dyn SolverModel) -> Option<Box<dyn Render>> {
+        self.fixate(model)
+            .map(|path| -> Box<dyn Render> { Box::new(path) })
+    }
+}
diff --git a/core/src/lib.rs b/core/src/lib.rs
new file mode 100644
index 0000000..57e45df
--- /dev/null
+++ b/core/src/lib.rs
@@ -0,0 +1,19 @@
+#![warn(clippy::all)]
+#![deny(unsafe_code)]
+
+pub mod colors;
+mod complex_shapes;
+pub mod core_shapes;
+mod rendering;
+mod runtime;
+pub mod solving;
+pub mod styles;
+pub mod text;
+pub mod types;
+
+pub use complex_shapes::{
+    ComplexShape, DrawResult, Drawable, DrawableBuilder, DynClone, DynDrawable,
+};
+pub use rendering::Renderer;
+pub use runtime::Runtime;
+pub use solving::{SolverContext, SolverModel};
diff --git a/core/src/mod.rs b/core/src/mod.rs
new file mode 100644
index 0000000..40fe74f
--- /dev/null
+++ b/core/src/mod.rs
@@ -0,0 +1,90 @@
+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
+    }
+}
diff --git a/core/src/rendering.rs b/core/src/rendering.rs
new file mode 100644
index 0000000..f7a0189
--- /dev/null
+++ b/core/src/rendering.rs
@@ -0,0 +1,86 @@
+use super::core_shapes::*;
+use super::styles::{DefinedDashStyle, DefinedStrokeStyle, FillStyle, Pattern};
+use super::text::{DefinedFontDescription, FontDescription};
+use super::types::DefinedShapeContext;
+
+pub trait Renderer {
+    fn move_to(&mut self, x: f64, y: f64);
+    fn stroke(&mut self);
+    fn fill(&mut self);
+    fn fill_preserve(&mut self);
+    fn set_pattern(&mut self, pattern: &Pattern);
+    fn set_dash(&mut self, dash: &DefinedDashStyle);
+    fn clear_dash(&mut self);
+    fn set_line_width(&mut self, width: f64);
+    fn line_to(&mut self, x: f64, y: f64);
+    fn rectangle(&mut self, x: f64, y: f64, width: f64, height: f64);
+    // For a font of size 1.
+    fn text_extents(&self, text: &str, font: &FontDescription) -> (f64, f64);
+    fn show_text(&mut self, text: &str, font: &DefinedFontDescription);
+}
+
+pub trait Render {
+    fn render(&self, context: DefinedShapeContext, renderer: &mut dyn Renderer);
+}
+
+fn draw(fill: &FillStyle, stroke: &DefinedStrokeStyle, renderer: &mut dyn Renderer) {
+    let stroking = !stroke.pattern.is_none();
+
+    if !fill.pattern.is_none() {
+        renderer.set_pattern(&fill.pattern);
+        if stroking {
+            renderer.fill_preserve();
+        } else {
+            renderer.fill();
+        }
+    }
+
+    if !stroke.pattern.is_none() {
+        renderer.set_pattern(&stroke.pattern);
+        renderer.set_line_width(stroke.line_width);
+        if let Some(dash) = &stroke.dash {
+            renderer.set_dash(dash);
+        }
+        renderer.stroke();
+        renderer.clear_dash();
+    }
+}
+
+impl Render for Rectangle {
+    fn render(&self, context: DefinedShapeContext, renderer: &mut dyn Renderer) {
+        let bounds = &context.bounds;
+        renderer.rectangle(bounds.left, bounds.top, bounds.width, bounds.height);
+        draw(&context.fill, &context.stroke, renderer);
+    }
+}
+
+impl Render for DefinedText {
+    fn render(&self, context: DefinedShapeContext, renderer: &mut dyn Renderer) {
+        // TODO: select font, style, text shaping (renderer specific), etc.
+        let bounds = &context.bounds;
+        //renderer.move_to(bounds.left, bounds.top + self.font.size);
+        renderer.move_to(bounds.left, bounds.top);
+        // TODO: ???
+        //draw(&context.fill, &context.stroke, renderer);
+        renderer.show_text(&self.content, &self.font);
+    }
+}
+
+impl Render for DefinedStraightPath {
+    fn render(&self, context: DefinedShapeContext, renderer: &mut dyn Renderer) {
+        let mut iter = self.points.iter();
+
+        let first_point = match iter.next() {
+            Some(point) => point,
+            None => return,
+        };
+
+        renderer.move_to(first_point.x, first_point.y);
+
+        for point in iter {
+            renderer.line_to(point.x, point.y);
+        }
+
+        draw(&context.fill, &context.stroke, renderer);
+    }
+}
diff --git a/core/src/runtime.rs b/core/src/runtime.rs
new file mode 100644
index 0000000..bfb31fa
--- /dev/null
+++ b/core/src/runtime.rs
@@ -0,0 +1,95 @@
+use super::complex_shapes::{ComplexShape, Drawable, DynDrawable};
+use super::rendering::Renderer;
+use super::solving::{Constrainable, SolverContext};
+
+const RECURSION_LIMIT: u64 = 10_000;
+
+pub struct Runtime<'a> {
+    solver_ctx: Box<dyn SolverContext + 'a>,
+    renderer: Box<dyn Renderer>,
+    drawables: Vec<DynDrawable>,
+}
+
+impl<'a> Runtime<'a> {
+    pub fn new(solver_ctx: Box<dyn SolverContext + 'a>, renderer: Box<dyn Renderer>) -> Self {
+        Self {
+            solver_ctx,
+            renderer,
+            drawables: Vec::new(),
+        }
+    }
+
+    pub fn add_drawable<T: ComplexShape + 'static>(&mut self, drawable: Drawable<T>) {
+        self.drawables.push(drawable.into())
+    }
+
+    pub fn solver_ctx(&mut self) -> &mut (dyn SolverContext + 'a) {
+        &mut *self.solver_ctx
+    }
+
+    // TODO: preserve ordering of shapes
+    pub fn render(mut self) {
+        let mut drawables = self.drawables;
+        let mut waited_on_variables = Vec::new();
+        let mut core_shapes = Vec::new();
+
+        /*
+        for drawable in &self.shapes {
+            let bounds = &drawable.bounds;
+            let shape = &drawable.shape;
+
+            if let Some(core_shape) = shape.to_render() {
+                drawables.push((*drawable).clone());
+                continue;
+            }
+
+            let mut result = shape.draw(bounds);
+            drawables.append(&mut result.subshapes);
+            waited_on_variables.append(&mut result.waiting_on);
+        }
+        */
+
+        let mut recursion_count = 0;
+
+        while !drawables.is_empty() {
+            recursion_count += 1;
+
+            if recursion_count > RECURSION_LIMIT {
+                panic!("Recursion limit reached");
+            }
+
+            let mut tmp_drawables = Vec::new();
+
+            for drawable in drawables.drain(..) {
+                let shape_ctx = &drawable.context;
+                let shape = &drawable.shape;
+
+                if let Some(core_shape) = shape.as_core_shape() {
+                    core_shape.constrain(shape_ctx, &mut *self.solver_ctx, &*self.renderer);
+                    core_shapes.push((shape.dyn_clone(), shape_ctx.clone())); // Better to Arc? Cow?
+                    continue;
+                }
+
+                let mut result = shape.draw(shape_ctx, &mut *self.solver_ctx);
+                tmp_drawables.append(&mut result.subshapes);
+                waited_on_variables.append(&mut result.waiting_on);
+            }
+
+            drawables = tmp_drawables;
+        }
+
+        let model = self.solver_ctx.solve();
+
+        // Delay rendering core shapes until later to have all the constraints
+        for (core_shape, shape_ctx) in core_shapes {
+            let core_shape = core_shape.as_core_shape().unwrap();
+
+            match (core_shape.to_render(&*model), shape_ctx.fixate(&*model)) {
+                (Some(defined_shape), Some(shape_ctx)) => {
+                    defined_shape.render(shape_ctx, &mut *self.renderer)
+                }
+                _ => panic!("Failed to fixate core shape"),
+            }
+        }
+    }
+}
diff --git a/core/src/solving.rs b/core/src/solving.rs
new file mode 100644
index 0000000..c7e94ba
--- /dev/null
+++ b/core/src/solving.rs
@@ -0,0 +1,279 @@
+use super::core_shapes::*;
+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 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.clone(),
+            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 ShapeContext {
+    type Fixated = DefinedShapeContext;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedShapeContext {
+            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? })
+    }
+}
diff --git a/core/src/styles.rs b/core/src/styles.rs
new file mode 100644
index 0000000..c061c58
--- /dev/null
+++ b/core/src/styles.rs
@@ -0,0 +1,161 @@
+use super::colors::Color;
+use super::types::Float;
+
+#[derive(Copy, Clone, PartialEq, Debug)]
+#[non_exhaustive]
+pub enum Pattern {
+    Solid(Color),
+    None,
+}
+
+impl Pattern {
+    pub fn is_none(&self) -> bool {
+        match self {
+            Pattern::None => true,
+            _ => false,
+        }
+    }
+}
+
+impl Default for Pattern {
+    fn default() -> Self {
+        Pattern::Solid(Color::default())
+    }
+}
+
+#[derive(Clone, PartialEq, Debug)]
+pub struct FillStyle {
+    pub(crate) pattern: Pattern,
+}
+
+impl FillStyle {
+    pub fn solid(color: Color) -> Self {
+        FillStyle {
+            pattern: Pattern::Solid(color),
+        }
+    }
+}
+
+impl Default for FillStyle {
+    fn default() -> Self {
+        FillStyle {
+            pattern: Pattern::None,
+        }
+    }
+}
+
+// TODO: probably move Float into an enum with Defined(f64) and Variable(handle)
+#[derive(Clone, Debug)]
+pub struct StrokeStyle {
+    pub(crate) pattern: Pattern,
+    pub(crate) dash: Option<DashStyle>,
+    pub(crate) line_width: Float,
+}
+
+impl StrokeStyle {
+    pub fn solid(color: Color) -> Self {
+        StrokeStyle {
+            pattern: Pattern::Solid(color),
+            dash: None,
+            line_width: Float::Fixed(0.),
+        }
+    }
+
+    pub fn builder() -> StrokeStyleBuilder {
+        StrokeStyleBuilder::default()
+    }
+}
+
+impl Default for StrokeStyle {
+    fn default() -> Self {
+        Self::builder().build()
+    }
+}
+
+#[derive(Clone, Default)]
+pub struct StrokeStyleBuilder {
+    pattern: Option<Pattern>,
+    dash: Option<DashStyle>,
+    line_width: Option<Float>,
+}
+
+impl StrokeStyleBuilder {
+    pub fn pattern(&mut self, pattern: Pattern) -> &mut Self {
+        self.pattern = Some(pattern);
+        self
+    }
+
+    pub fn dash(&mut self, dash: DashStyle) -> &mut Self {
+        self.dash = Some(dash);
+        self
+    }
+
+    pub fn line_width(&mut self, width: Float) -> &mut Self {
+        self.line_width = Some(width);
+        self
+    }
+
+    pub fn build(&mut self) -> StrokeStyle {
+        StrokeStyle {
+            pattern: self.pattern.clone().unwrap_or_default(),
+            dash: self.dash.clone(),
+            line_width: self.line_width.unwrap_or(Float::Fixed(2.)),
+        }
+    }
+
+}
+
+
+
+
+#[derive(Clone, Debug, Default)]
+pub struct DashStyle {
+    pub(crate) dashes: Vec<Float>,
+    pub(crate) offset: Float,
+}
+
+impl DashStyle {
+    pub fn new(dashes: Vec<Float>, offset: Float) -> Self {
+        Self { dashes, offset }
+    }
+
+    pub fn dashes(&self) -> &[Float] {
+        &self.dashes
+    }
+
+    pub fn dashes_mut(&mut self) -> &mut Vec<Float> {
+        &mut self.dashes
+    }
+
+    pub fn offset(&self) -> Float {
+        self.offset
+    }
+
+    // TODO: does this makes sense?
+    pub fn offset_mut(&mut self) -> &mut Float {
+        &mut self.offset
+    }
+}
+
+#[derive(Clone, PartialEq, Debug, Default)]
+pub struct DefinedStrokeStyle {
+    pub(crate) pattern: Pattern,
+    pub(crate) dash: Option<DefinedDashStyle>,
+    pub(crate) line_width: f64,
+}
+
+#[derive(Clone, PartialEq, Debug, Default)]
+pub struct DefinedDashStyle {
+    pub(crate) dashes: Vec<f64>,
+    pub(crate) offset: f64,
+}
+
+impl DefinedDashStyle {
+    pub fn dashes(&self) -> &[f64] {
+        &self.dashes
+    }
+
+    pub fn offset(&self) -> f64 {
+        self.offset
+    }
+}
diff --git a/core/src/text.rs b/core/src/text.rs
new file mode 100644
index 0000000..3110030
--- /dev/null
+++ b/core/src/text.rs
@@ -0,0 +1,81 @@
+use super::types::Float;
+
+#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, Debug)]
+#[non_exhaustive]
+pub enum FontStyle {
+    Normal,
+    Oblique,
+    Italic,
+}
+
+impl Default for FontStyle {
+    fn default() -> Self {
+        Self::Normal
+    }
+}
+
+#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, Debug)]
+#[non_exhaustive]
+pub enum FontVariant {
+    Normal,
+    SmallCaps,
+}
+
+impl Default for FontVariant {
+    fn default() -> Self {
+        Self::Normal
+    }
+}
+
+#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, Debug)]
+#[non_exhaustive]
+pub enum FontWeight {
+    Thin,
+    Ultralight,
+    Light,
+    Semilight,
+    Book,
+    Normal,
+    Medium,
+    Semibold,
+    Bold,
+    Ultrabold,
+    Heavy,
+    Ultraheavy,
+}
+
+impl Default for FontWeight {
+    fn default() -> Self {
+        Self::Normal
+    }
+}
+
+#[derive(Clone, Debug)]
+pub struct FontDescription {
+    pub family: String,
+    pub style: FontStyle,
+    pub weight: FontWeight,
+    // TODO: handles weirdly with bounds that specifies both top and bottom
+    pub size: Float,
+}
+
+// TODO: automate creation of Defined* structs
+#[derive(Clone, Debug)]
+pub struct DefinedFontDescription {
+    pub family: String,
+    pub style: FontStyle,
+    pub weight: FontWeight,
+    pub size: f64,
+}
+
+#[derive(Clone, Debug)]
+pub struct Text {
+    pub content: String,
+    pub font: FontDescription,
+}
+
+#[derive(Clone, Debug)]
+pub struct DefinedText {
+    pub content: String,
+    pub font: DefinedFontDescription,
+}
diff --git a/core/src/types.rs b/core/src/types.rs
new file mode 100644
index 0000000..1b7623a
--- /dev/null
+++ b/core/src/types.rs
@@ -0,0 +1,316 @@
+use super::solving::{SolverContext, VariableHandle};
+use super::styles::{DefinedStrokeStyle, FillStyle, StrokeStyle};
+
+// TODO: if we're so dependent on lifetimes, it's probably better to remove Box, and use raw
+// references instead
+
+// Not Eq / Ord to prevent cofusion
+#[derive(Copy, Clone, Debug)]
+pub enum Float {
+    Fixed(f64),
+    Variable(VariableHandle),
+}
+
+impl Default for Float {
+    fn default() -> Self {
+        Float::Fixed(0.)
+    }
+}
+
+impl Float {
+    pub fn from_handle(handle: VariableHandle) -> Self {
+        Float::Variable(handle)
+    }
+
+    /*
+    pub fn handle(&self) -> Option<VariableHandle> {
+        match self {
+            Float::Fixed(_) => None,
+            Float::Variable(handle) => Some(handle),
+        }
+    }
+    */
+}
+
+#[derive(Clone, Default)]
+struct FloatBuilder(Option<Float>);
+
+impl FloatBuilder {
+    pub fn set(&mut self, value: Float) {
+        self.0 = Some(value);
+    }
+
+    pub fn build(&self, solver: &mut dyn SolverContext) -> Float {
+        self.0.unwrap_or_else(|| solver.new_free_float())
+    }
+}
+
+// Not Eq / Ord to prevent cofusion
+#[derive(Copy, Clone, Hash, Debug)]
+pub struct Bool(VariableHandle);
+
+impl Bool {
+    pub fn new(handle: VariableHandle) -> Self {
+        Bool(handle)
+    }
+
+    pub fn handle(&self) -> VariableHandle {
+        self.0
+    }
+}
+
+#[derive(Clone, Debug)]
+pub struct Point2D {
+    pub(crate) x: Float,
+    pub(crate) y: Float,
+}
+
+impl Point2D {
+    pub fn new(x: Float, y: Float) -> Self {
+        Point2D { x, y }
+    }
+
+    pub fn x(&self) -> Float {
+        self.x
+    }
+
+    pub fn y(&self) -> Float {
+        self.y
+    }
+}
+
+#[derive(Clone, PartialEq, PartialOrd, Debug)]
+pub struct DefinedPoint2D {
+    pub(crate) x: f64,
+    pub(crate) y: f64,
+}
+
+#[derive(Clone, Debug)]
+pub struct Bounds {
+    // TODO: really pub? That allows modification, when one might expect constraints
+    pub(crate) top: Float,
+    pub(crate) left: Float,
+    pub(crate) width: Float,
+    pub(crate) height: Float,
+}
+
+impl Bounds {
+    pub fn builder() -> BoundsBuilder {
+        BoundsBuilder::default()
+    }
+
+    pub fn top(&self, _ctx: &mut dyn SolverContext) -> Float {
+        self.top
+    }
+
+    pub fn left(&self, _ctx: &mut dyn SolverContext) -> Float {
+        self.left
+    }
+
+    pub fn width(&self, _ctx: &mut dyn SolverContext) -> Float {
+        self.width
+    }
+
+    pub fn height(&self, _ctx: &mut dyn SolverContext) -> Float {
+        self.height
+    }
+
+    pub fn right(&self, solver: &mut dyn SolverContext) -> Float {
+        solver.float_add(&[self.left, self.width])
+    }
+
+    pub fn bottom(&self, solver: &mut dyn SolverContext) -> Float {
+        solver.float_add(&[self.top, self.height])
+    }
+
+    pub fn vert_center(&self, solver: &mut dyn SolverContext) -> Float {
+        let half_height = solver.float_div(self.height, Float::Fixed(2.));
+        solver.float_add(&[self.top, half_height])
+    }
+
+    pub fn horiz_center(&self, solver: &mut dyn SolverContext) -> Float {
+        let half_width = solver.float_div(self.width, Float::Fixed(2.));
+        solver.float_add(&[self.left, half_width])
+    }
+
+    pub fn top_left(&self, _ctx: &mut dyn SolverContext) -> Point2D {
+        Point2D::new(self.left, self.top)
+    }
+
+    pub fn top_right(&self, solver: &mut dyn SolverContext) -> Point2D {
+        Point2D::new(self.right(solver), self.top)
+    }
+
+    pub fn bottom_left(&self, solver: &mut dyn SolverContext) -> Point2D {
+        Point2D::new(self.left, self.bottom(solver))
+    }
+
+    pub fn bottom_right(&self, solver: &mut dyn SolverContext) -> Point2D {
+        Point2D::new(self.right(solver), self.bottom(solver))
+    }
+
+    pub fn center(&self, solver: &mut dyn SolverContext) -> Point2D {
+        Point2D::new(self.horiz_center(solver), self.vert_center(solver))
+    }
+
+    pub fn with_margin(&self, margin: Float, solver: &mut dyn SolverContext) -> Self {
+        let neg_margin = solver.float_neg(margin);
+        Bounds {
+            top: solver.float_add(&[self.top, neg_margin]),
+            left: solver.float_add(&[self.top, neg_margin]),
+            height: solver.float_add(&[self.top, margin]),
+            width: solver.float_add(&[self.top, margin]),
+        }
+    }
+}
+
+#[derive(Clone, Default)]
+pub struct BoundsBuilder {
+    top: FloatBuilder,
+    left: FloatBuilder,
+    width: FloatBuilder,
+    height: FloatBuilder,
+}
+
+impl BoundsBuilder {
+    pub fn top(&mut self, top: Float) -> &mut Self {
+        self.top.set(top);
+        self
+    }
+
+    pub fn left(&mut self, left: Float) -> &mut Self {
+        self.left.set(left);
+        self
+    }
+
+    pub fn width(&mut self, width: Float) -> &mut Self {
+        self.width.set(width);
+        self
+    }
+
+    pub fn height(&mut self, height: Float) -> &mut Self {
+        self.height.set(height);
+        self
+    }
+
+    pub fn build(&self, solver: &mut dyn SolverContext) -> Bounds {
+        let _build_float =
+            |maybe_float: Option<Float>| maybe_float.unwrap_or_else(|| solver.new_free_float());
+
+        Bounds {
+            top: self.top.build(solver),
+            left: self.left.build(solver),
+            width: self.width.build(solver),
+            height: self.height.build(solver),
+        }
+    }
+}
+
+#[derive(Clone, Debug)]
+pub struct Bounded<Shape> {
+    pub bounds: Bounds,
+    pub shape: Shape,
+}
+
+#[derive(Clone, PartialEq, PartialOrd, Debug)]
+pub struct DefinedBounds {
+    pub top: f64,
+    pub left: f64,
+    pub width: f64,
+    pub height: f64,
+}
+
+#[derive(Clone, PartialEq, PartialOrd, Debug)]
+pub struct DefinitelyBounded<Shape> {
+    pub bounds: DefinedBounds,
+    pub shape: Shape,
+}
+
+#[derive(Clone, Debug)]
+pub struct ShapeContext {
+    pub(crate) bounds: Bounds,
+    pub(crate) fill: FillStyle,
+    pub(crate) stroke: StrokeStyle,
+}
+
+impl ShapeContext {
+    pub fn new(solver: &mut dyn SolverContext) -> Self {
+        Self {
+            bounds: Bounds {
+                top: solver.new_free_float(),
+                left: solver.new_free_float(),
+                width: solver.new_free_float(),
+                height: solver.new_free_float(),
+            },
+            fill: FillStyle::default(),
+            stroke: StrokeStyle::default(),
+        }
+    }
+
+    pub(crate) fn builder() -> ShapeContextBuilder {
+        ShapeContextBuilder::default()
+    }
+
+    pub fn bounds(&self) -> &Bounds {
+        &self.bounds
+    }
+
+    pub fn bounds_mut(&mut self) -> &mut Bounds {
+        &mut self.bounds
+    }
+
+    pub fn fill(&self) -> &FillStyle {
+        &self.fill
+    }
+
+    pub fn fill_mut(&mut self) -> &mut FillStyle {
+        &mut self.fill
+    }
+
+    pub fn stroke(&self) -> &StrokeStyle {
+        &self.stroke
+    }
+
+    pub fn stroke_mut(&mut self) -> &mut StrokeStyle {
+        &mut self.stroke
+    }
+}
+
+#[derive(Clone, Default)]
+pub(crate) struct ShapeContextBuilder {
+    bounds: Option<Bounds>,
+    fill: Option<FillStyle>,
+    stroke: Option<StrokeStyle>,
+}
+
+impl ShapeContextBuilder {
+    pub fn bounds(&mut self, bounds: Bounds) -> &mut Self {
+        self.bounds = Some(bounds);
+        self
+    }
+
+    pub fn fill(&mut self, fill: FillStyle) -> &mut Self {
+        self.fill = Some(fill);
+        self
+    }
+
+    pub fn stroke(&mut self, stroke: StrokeStyle) -> &mut Self {
+        self.stroke = Some(stroke);
+        self
+    }
+
+    pub fn build(&self, solver: &mut dyn SolverContext) -> ShapeContext {
+        ShapeContext {
+            bounds: self.bounds.clone().unwrap_or_else(|| Bounds::builder().build(solver)),
+            fill: self.fill.clone().unwrap_or_default(),
+            stroke: self.stroke.clone().unwrap_or_default(),
+        }
+    }
+}
+
+#[derive(Clone, Debug)]
+pub struct DefinedShapeContext {
+    pub bounds: DefinedBounds,
+    pub fill: FillStyle,
+    pub stroke: DefinedStrokeStyle,
+}