2 files changed, 200 insertions, 0 deletions

diff --git a/cli/Cargo.toml b/cli/Cargo.toml
new file mode 100644
index 0000000..c02a484
--- /dev/null
+++ b/cli/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "diaphragm-cli"
+version = "0.1.0"
+authors = ["Minijackson <minijackson@riseup.net>"]
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+diaphragm-core = { path = "../core" }
+diaphragm-z3-solver = { path = "../z3-solver" }
+diaphragm-cairo-renderer = { path = "../cairo-renderer" }
diff --git a/cli/src/main.rs b/cli/src/main.rs
new file mode 100644
index 0000000..d2ec038
--- /dev/null
+++ b/cli/src/main.rs
@@ -0,0 +1,188 @@
+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,
+            },
+        }),
+    });
+}
+*/