-
-## How build the demo executable target (MacOS only)
-
-The project comes with a demo executable target. To build and run this use the provided [justfile](./justfile).
-
-For now only macOS is supported.
-
-### Dependencies
-
-Raylean has several dependencies:
-
-* [Lean](https://lean-lang.org), which we use for development of games.
-* [Just](https://github.com/casey/just), as a replacement for Make.
-* XCode for macOS SDK frameworks like OpenGL.
-* [Rust](https://www.rust-lang.org/) for building resvg, which provides SVG support.
-
-You need to install all four to build Raylean. Below follows instructions for each.
-
-#### [Lean](https://lean-lang.org)
-
-Use the [official documentation](https://lean-lang.org/lean4/doc/quickstart.html) to setup Lean.
-
-#### [Just command runner](https://github.com/casey/just)
-
-Install using [Homebrew](https://brew.sh) with:
-
-``` sh
-brew install just
-```
-
-#### XCode Commandline Tools
-
-The macOS clang installation and macOS SDK frameworks like OpenGL are required when linking the executable.
-
-Install by running:
-
-``` sh
-xcode-select --install
-```
-
-#### [Rust](https://www.rust-lang.org/)
-
-```sh
-curl https://sh.rustup.rs -sSf | sh
-```
-
-Or use the [official documentation](https://www.rust-lang.org/tools/install) to setup Rust.
-
-### Build and Run
-
-To build the raylib static library and the demo executable, run the following command in the project:
-
-``` sh
-just build
-```
-
-To run the demo, run the following command in the project:
-
-``` sh
-just run
-```
-
-### Assets
-
-Assets used by the demo application are stored in the [resources](./resources) directory.
-
-
-| Asset | Attribution |
-|--------------------------------------|----------------------------------------------------------|
-| [walter.png](./resources/walter.png) | [Liza Schulze](https://www.linkedin.com/in/lizaschulze/) |
-| [Asset.svg](./resources/Asset.svg) | [Liza Schulze](https://www.linkedin.com/in/lizaschulze/) |
+Proofs about Image Denotations including drawings via [raylean](https://github.com/funexists/raylean).
+This work is inspired by [Functional Images - Conal Elliott](http://conal.net/papers/functional-images/)
\ No newline at end of file
diff --git a/build/makeBundle b/build/makeBundle
new file mode 100755
index 0000000..84ad5d6
Binary files /dev/null and b/build/makeBundle differ
diff --git a/build/makeBundle.c b/build/makeBundle.c
new file mode 100644
index 0000000..69be3dc
--- /dev/null
+++ b/build/makeBundle.c
@@ -0,0 +1,2085 @@
+// Lean compiler output
+// Module: scripts.makeBundle
+// Imports: Init
+#include (path: &[Segment], kind: MarkerKind, mut draw_marker: P)
-where
- P: FnMut(tiny_skia_path::Point, usize),
-{
- match kind {
- MarkerKind::Start => {
- if let Some(Segment::MoveTo(p)) = path.first().cloned() {
- draw_marker(p, 0);
- }
- }
- MarkerKind::Middle => {
- let total = path.len() - 1;
- let mut i = 1;
- while i < total {
- let p = match path[i] {
- Segment::MoveTo(p) => p,
- Segment::LineTo(p) => p,
- Segment::CubicTo(_, _, p) => p,
- _ => {
- i += 1;
- continue;
- }
- };
-
- draw_marker(p, i);
-
- i += 1;
- }
- }
- MarkerKind::End => {
- let idx = path.len() - 1;
- match path.last().cloned() {
- Some(Segment::LineTo(p)) => {
- draw_marker(p, idx);
- }
- Some(Segment::CubicTo(_, _, p)) => {
- draw_marker(p, idx);
- }
- Some(Segment::Close) => {
- let p = get_subpath_start(path, idx);
- draw_marker(p, idx);
- }
- _ => {}
- }
- }
- }
-}
-
-fn calc_vertex_angle(path: &[Segment], idx: usize) -> f32 {
- if idx == 0 {
- // First segment.
-
- debug_assert!(path.len() > 1);
-
- let seg1 = path[0];
- let seg2 = path[1];
-
- match (seg1, seg2) {
- (Segment::MoveTo(pm), Segment::LineTo(p)) => calc_line_angle(pm.x, pm.y, p.x, p.y),
- (Segment::MoveTo(pm), Segment::CubicTo(p1, _, p)) => {
- if pm.x.approx_eq_ulps(&p1.x, 4) && pm.y.approx_eq_ulps(&p1.y, 4) {
- calc_line_angle(pm.x, pm.y, p.x, p.y)
- } else {
- calc_line_angle(pm.x, pm.y, p1.x, p1.y)
- }
- }
- _ => 0.0,
- }
- } else if idx == path.len() - 1 {
- // Last segment.
-
- let seg1 = path[idx - 1];
- let seg2 = path[idx];
-
- match (seg1, seg2) {
- (_, Segment::MoveTo(_)) => 0.0, // unreachable
- (_, Segment::LineTo(p)) => {
- let prev = get_prev_vertex(path, idx);
- calc_line_angle(prev.x, prev.y, p.x, p.y)
- }
- (_, Segment::CubicTo(p1, p2, p)) => {
- if p2.x.approx_eq_ulps(&p.x, 4) && p2.y.approx_eq_ulps(&p.y, 4) {
- calc_line_angle(p1.x, p1.y, p.x, p.y)
- } else {
- calc_line_angle(p2.x, p2.y, p.x, p.y)
- }
- }
- (Segment::LineTo(p), Segment::Close) => {
- let next = get_subpath_start(path, idx);
- calc_line_angle(p.x, p.y, next.x, next.y)
- }
- (Segment::CubicTo(_, p2, p), Segment::Close) => {
- let prev = get_prev_vertex(path, idx);
- let next = get_subpath_start(path, idx);
- calc_curves_angle(
- prev.x, prev.y, p2.x, p2.y, p.x, p.y, next.x, next.y, next.x, next.y,
- )
- }
- (_, Segment::Close) => 0.0,
- }
- } else {
- // Middle segments.
-
- let seg1 = path[idx];
- let seg2 = path[idx + 1];
-
- // TODO: Not sure if there is a better way.
- match (seg1, seg2) {
- (Segment::MoveTo(pm), Segment::LineTo(p)) => calc_line_angle(pm.x, pm.y, p.x, p.y),
- (Segment::MoveTo(pm), Segment::CubicTo(p1, _, _)) => {
- calc_line_angle(pm.x, pm.y, p1.x, p1.y)
- }
- (Segment::LineTo(p1), Segment::LineTo(p2)) => {
- let prev = get_prev_vertex(path, idx);
- calc_angle(prev.x, prev.y, p1.x, p1.y, p1.x, p1.y, p2.x, p2.y)
- }
- (Segment::CubicTo(_, c1_p2, c1_p), Segment::CubicTo(c2_p1, _, c2_p)) => {
- let prev = get_prev_vertex(path, idx);
- calc_curves_angle(
- prev.x, prev.y, c1_p2.x, c1_p2.y, c1_p.x, c1_p.y, c2_p1.x, c2_p1.y, c2_p.x,
- c2_p.y,
- )
- }
- (Segment::LineTo(pl), Segment::CubicTo(p1, _, p)) => {
- let prev = get_prev_vertex(path, idx);
- calc_curves_angle(
- prev.x, prev.y, prev.x, prev.y, pl.x, pl.y, p1.x, p1.y, p.x, p.y,
- )
- }
- (Segment::CubicTo(_, p2, p), Segment::LineTo(pl)) => {
- let prev = get_prev_vertex(path, idx);
- calc_curves_angle(prev.x, prev.y, p2.x, p2.y, p.x, p.y, pl.x, pl.y, pl.x, pl.y)
- }
- (Segment::LineTo(p), Segment::MoveTo(_)) => {
- let prev = get_prev_vertex(path, idx);
- calc_line_angle(prev.x, prev.y, p.x, p.y)
- }
- (Segment::CubicTo(_, p2, p), Segment::MoveTo(_)) => {
- if p.x.approx_eq_ulps(&p2.x, 4) && p.y.approx_eq_ulps(&p2.y, 4) {
- let prev = get_prev_vertex(path, idx);
- calc_line_angle(prev.x, prev.y, p.x, p.y)
- } else {
- calc_line_angle(p2.x, p2.y, p.x, p.y)
- }
- }
- (Segment::LineTo(p), Segment::Close) => {
- let prev = get_prev_vertex(path, idx);
- let next = get_subpath_start(path, idx);
- calc_angle(prev.x, prev.y, p.x, p.y, p.x, p.y, next.x, next.y)
- }
- (_, Segment::Close) => {
- let prev = get_prev_vertex(path, idx);
- let next = get_subpath_start(path, idx);
- calc_line_angle(prev.x, prev.y, next.x, next.y)
- }
- (_, Segment::MoveTo(_)) | (Segment::Close, _) => 0.0,
- }
- }
-}
-
-fn calc_line_angle(x1: f32, y1: f32, x2: f32, y2: f32) -> f32 {
- calc_angle(x1, y1, x2, y2, x1, y1, x2, y2)
-}
-
-fn calc_curves_angle(
- px: f32,
- py: f32, // previous vertex
- cx1: f32,
- cy1: f32, // previous control point
- x: f32,
- y: f32, // current vertex
- cx2: f32,
- cy2: f32, // next control point
- nx: f32,
- ny: f32, // next vertex
-) -> f32 {
- if cx1.approx_eq_ulps(&x, 4) && cy1.approx_eq_ulps(&y, 4) {
- calc_angle(px, py, x, y, x, y, cx2, cy2)
- } else if x.approx_eq_ulps(&cx2, 4) && y.approx_eq_ulps(&cy2, 4) {
- calc_angle(cx1, cy1, x, y, x, y, nx, ny)
- } else {
- calc_angle(cx1, cy1, x, y, x, y, cx2, cy2)
- }
-}
-
-fn calc_angle(x1: f32, y1: f32, x2: f32, y2: f32, x3: f32, y3: f32, x4: f32, y4: f32) -> f32 {
- use std::f32::consts::*;
-
- fn normalize(rad: f32) -> f32 {
- let v = rad % (PI * 2.0);
- if v < 0.0 {
- v + PI * 2.0
- } else {
- v
- }
- }
-
- fn vector_angle(vx: f32, vy: f32) -> f32 {
- let rad = vy.atan2(vx);
- if rad.is_nan() {
- 0.0
- } else {
- normalize(rad)
- }
- }
-
- let in_a = vector_angle(x2 - x1, y2 - y1);
- let out_a = vector_angle(x4 - x3, y4 - y3);
- let d = (out_a - in_a) * 0.5;
-
- let mut angle = in_a + d;
- if FRAC_PI_2 < d.abs() {
- angle -= PI;
- }
-
- normalize(angle).to_degrees()
-}
-
-fn get_subpath_start(segments: &[Segment], idx: usize) -> tiny_skia_path::Point {
- let offset = segments.len() - idx;
- for seg in segments.iter().rev().skip(offset) {
- if let Segment::MoveTo(p) = *seg {
- return p;
- }
- }
-
- tiny_skia_path::Point::zero()
-}
-
-fn get_prev_vertex(segments: &[Segment], idx: usize) -> tiny_skia_path::Point {
- match segments[idx - 1] {
- Segment::MoveTo(p) => p,
- Segment::LineTo(p) => p,
- Segment::CubicTo(_, _, p) => p,
- Segment::Close => get_subpath_start(segments, idx),
- }
-}
-
-fn convert_rect(node: SvgNode, state: &converter::State) -> Option