diff options
author | Minijackson <minijackson@riseup.net> | 2022-12-22 12:19:59 +0100 |
---|---|---|
committer | Minijackson <minijackson@riseup.net> | 2022-12-22 12:19:59 +0100 |
commit | 92a02c34628343153b33602eae00cef46e28d191 (patch) | |
tree | 8622ec528d24e456be22d984d93aa9bcafc97399 /cli | |
download | diaphragm-92a02c34628343153b33602eae00cef46e28d191.tar.gz diaphragm-92a02c34628343153b33602eae00cef46e28d191.zip |
WIP
Diffstat (limited to 'cli')
-rw-r--r-- | cli/Cargo.toml | 12 | ||||
-rw-r--r-- | cli/src/main.rs | 188 |
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 @@ | |||
1 | [package] | ||
2 | name = "diaphragm-cli" | ||
3 | version = "0.1.0" | ||
4 | authors = ["Minijackson <minijackson@riseup.net>"] | ||
5 | edition = "2021" | ||
6 | |||
7 | # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | ||
8 | |||
9 | [dependencies] | ||
10 | diaphragm-core = { path = "../core" } | ||
11 | diaphragm-z3-solver = { path = "../z3-solver" } | ||
12 | 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 @@ | |||
1 | use diaphragm_cairo_renderer::CairoRenderer; | ||
2 | use diaphragm_core::{styles::*, types::*, *}; | ||
3 | use diaphragm_z3_solver::{z3, Z3Context}; | ||
4 | |||
5 | // drawing::{cairo::CairoEngine, Engine}, | ||
6 | // z3::{self, ast::Ast}, | ||
7 | |||
8 | fn main() { | ||
9 | let z3_cfg = z3::Config::new(); | ||
10 | let z3_ctx = z3::Context::new(&z3_cfg); | ||
11 | let ctx = Z3Context::new(&z3_ctx); | ||
12 | |||
13 | let cairo_renderer = CairoRenderer::new(); | ||
14 | |||
15 | let mut runtime = Runtime::new(Box::new(ctx), Box::new(cairo_renderer)); | ||
16 | |||
17 | let ctx = runtime.solver_ctx(); | ||
18 | |||
19 | let rect1_height = ctx.new_free_float(); | ||
20 | let rect1_width = ctx.new_free_float(); | ||
21 | |||
22 | let rect1_ctx = ShapeContext { | ||
23 | bounds: Bounds { | ||
24 | top: ctx.new_fixed_float(10.), | ||
25 | left: ctx.new_fixed_float(10.), | ||
26 | height: rect1_height, | ||
27 | width: rect1_width, | ||
28 | }, | ||
29 | fill: FillStyle::default(), | ||
30 | stroke: StrokeStyle::default(), | ||
31 | }; | ||
32 | |||
33 | let text_bounds = rect1_ctx.bounds.clone(); | ||
34 | |||
35 | let rect1 = core_shapes::Rectangle {}; | ||
36 | |||
37 | let rect2_top = ctx.new_free_float(); | ||
38 | let rect2_left = ctx.new_free_float(); | ||
39 | |||
40 | let rect2_ctx = ShapeContext { | ||
41 | bounds: Bounds { | ||
42 | top: rect2_top, | ||
43 | left: rect2_left, | ||
44 | height: rect1_width, | ||
45 | width: rect1_height, | ||
46 | }, | ||
47 | fill: FillStyle::default(), | ||
48 | stroke: StrokeStyle::default(), | ||
49 | }; | ||
50 | |||
51 | let rect2 = core_shapes::Rectangle {}; | ||
52 | |||
53 | let _2 = ctx.new_fixed_float(2.); | ||
54 | let double_height = ctx.float_mul(&[rect1_height, _2]); | ||
55 | let width_constraint = ctx.float_eq(rect1_width, double_height); | ||
56 | ctx.constrain(width_constraint); | ||
57 | |||
58 | let _42 = ctx.new_fixed_float(42.); | ||
59 | let width_constraint2 = ctx.float_eq(rect1_width, _42); | ||
60 | ctx.constrain(width_constraint2); | ||
61 | |||
62 | let _10 = ctx.new_fixed_float(10.); | ||
63 | let top_constraint = ctx.float_eq(rect2_top, _10); | ||
64 | ctx.constrain(top_constraint); | ||
65 | |||
66 | let bigger_width = ctx.float_add(&[rect1_width, _10]); | ||
67 | let left_constraint = ctx.float_eq(rect2_left, bigger_width); | ||
68 | ctx.constrain(left_constraint); | ||
69 | |||
70 | let text = core_shapes::Text { | ||
71 | content: String::from("Hello, World!"), | ||
72 | font: text::FontDescription { | ||
73 | family: String::from("mono"), | ||
74 | style: Default::default(), | ||
75 | weight: Default::default(), | ||
76 | size: rect1_height, | ||
77 | }, | ||
78 | }; | ||
79 | |||
80 | let text_ctx = ShapeContext { | ||
81 | bounds: text_bounds, | ||
82 | fill: FillStyle::default(), | ||
83 | stroke: StrokeStyle::default(), | ||
84 | }; | ||
85 | |||
86 | runtime.add_shape(rect1, rect1_ctx); | ||
87 | runtime.add_shape(rect2, rect2_ctx); | ||
88 | runtime.add_shape(text, text_ctx); | ||
89 | |||
90 | runtime.render(); | ||
91 | } | ||
92 | |||
93 | /* | ||
94 | fn main() { | ||
95 | // simple_test() | ||
96 | |||
97 | let z3_cfg = z3::Config::new(); | ||
98 | let z3_ctx = z3::Context::new(&z3_cfg); | ||
99 | |||
100 | let mut ctx = Context::new(); | ||
101 | |||
102 | let rect1_height = z3::ast::Real::new_const(&z3_ctx, "rect1_height"); | ||
103 | let rect1_width = z3::ast::Real::new_const(&z3_ctx, "rect1_width"); | ||
104 | |||
105 | let rect1_bounds = Bounds { | ||
106 | top: Float::Defined(10.), | ||
107 | left: Float::Defined(10.), | ||
108 | height: Float::Constrained(rect1_height.clone()), | ||
109 | width: Float::Constrained(rect1_width.clone()), | ||
110 | }; | ||
111 | |||
112 | let rect1 = Bounded::<Box<dyn Drawable>> { | ||
113 | bounds: rect1_bounds, | ||
114 | shape: Box::new(Shape::Rectangle(Rectangle {})), | ||
115 | }; | ||
116 | |||
117 | let rect2_top = z3::ast::Real::new_const(&z3_ctx, "rect2_top"); | ||
118 | let rect2_left = z3::ast::Real::new_const(&z3_ctx, "rect2_left"); | ||
119 | |||
120 | let rect2_bounds = Bounds { | ||
121 | top: Float::Constrained(rect2_top.clone()), | ||
122 | left: Float::Constrained(rect2_left.clone()), | ||
123 | height: Float::Constrained(rect1_width.clone()), | ||
124 | width: Float::Constrained(rect1_height.clone()), | ||
125 | }; | ||
126 | |||
127 | let rect2 = Bounded::<Box<dyn Drawable>> { | ||
128 | bounds: rect2_bounds, | ||
129 | shape: Box::new(Shape::Rectangle(Rectangle {})), | ||
130 | }; | ||
131 | |||
132 | let solver = z3::Solver::new(&z3_ctx); | ||
133 | |||
134 | solver.assert(&rect1_width._eq(&(rect1_height * z3::ast::Real::from_real(&z3_ctx, 2, 1)))); | ||
135 | solver.assert(&rect1_width._eq(&z3::ast::Real::from_real(&z3_ctx, 42, 1))); | ||
136 | |||
137 | solver.assert(&rect2_top._eq(&z3::ast::Real::from_real(&z3_ctx, 10, 1))); | ||
138 | solver.assert(&rect2_left._eq(&(rect1_width + z3::ast::Real::from_real(&z3_ctx, 10, 1)))); | ||
139 | |||
140 | ctx.add_shape(rect1); | ||
141 | ctx.add_shape(rect2); | ||
142 | ctx.set_constraints(&z3_ctx, &solver); | ||
143 | |||
144 | solver.check(); | ||
145 | let model = solver.get_model().expect("Failed to get model"); | ||
146 | |||
147 | let shapes = ctx.draw(&model); | ||
148 | |||
149 | let mut cairo = CairoEngine::new(); | ||
150 | |||
151 | for shape in shapes { | ||
152 | cairo.draw(&shape); | ||
153 | } | ||
154 | } | ||
155 | |||
156 | #[allow(dead_code)] | ||
157 | fn simple_test() { | ||
158 | let mut cairo = CairoEngine::new(); | ||
159 | |||
160 | cairo.draw(&DefinitelyBounded { | ||
161 | bounds: DefinedBounds { | ||
162 | top: 10., | ||
163 | left: 10., | ||
164 | height: 40., | ||
165 | width: 40., | ||
166 | }, | ||
167 | shape: Shape::Rectangle(Rectangle {}), | ||
168 | }); | ||
169 | |||
170 | cairo.draw(&DefinitelyBounded { | ||
171 | bounds: DefinedBounds { | ||
172 | top: 20., | ||
173 | left: 20., | ||
174 | height: 40., | ||
175 | width: 40., | ||
176 | }, | ||
177 | shape: Shape::Text(Text { | ||
178 | content: String::from("Hello, World!"), | ||
179 | font: FontDescription { | ||
180 | family: String::from("Fira Code"), | ||
181 | size: 21, | ||
182 | style: FontStyle::Normal, | ||
183 | weight: FontWeight::Normal, | ||
184 | }, | ||
185 | }), | ||
186 | }); | ||
187 | } | ||
188 | */ | ||