From 92a02c34628343153b33602eae00cef46e28d191 Mon Sep 17 00:00:00 2001 From: Minijackson Date: Thu, 22 Dec 2022 12:19:59 +0100 Subject: WIP --- .envrc | 1 + .gitignore | 1 + .luarc.json | 4 + Cargo.lock | 759 ++++++++++++++++++++++++ Cargo.toml | 10 + TODO.md | 4 + cairo-renderer/Cargo.toml | 14 + cairo-renderer/src/drawing/cairo/mod.rs | 35 ++ cairo-renderer/src/drawing/mod.rs | 8 + cairo-renderer/src/lib.rs | 111 ++++ cli/Cargo.toml | 12 + cli/src/main.rs | 188 ++++++ core/Cargo.toml | 10 + core/src/colors.rs | 34 ++ core/src/complex_shapes.rs | 285 +++++++++ core/src/core_shapes.rs | 86 +++ core/src/lib.rs | 19 + core/src/mod.rs | 90 +++ core/src/rendering.rs | 86 +++ core/src/runtime.rs | 95 +++ core/src/solving.rs | 279 +++++++++ core/src/styles.rs | 161 +++++ core/src/text.rs | 81 +++ core/src/types.rs | 316 ++++++++++ examples/lib-dfscq-log/Cargo.toml | 15 + examples/lib-dfscq-log/dfscq-log.lua | 124 ++++ examples/lib-dfscq-log/src/block_list.rs | 183 ++++++ examples/lib-dfscq-log/src/blocks.rs | 72 +++ examples/lib-dfscq-log/src/bracket.rs | 42 ++ examples/lib-dfscq-log/src/explode.rs | 86 +++ examples/lib-dfscq-log/src/labeled.rs | 64 ++ examples/lib-dfscq-log/src/labeled_delimiter.rs | 121 ++++ examples/lib-dfscq-log/src/layer.rs | 169 ++++++ examples/lib-dfscq-log/src/main.rs | 642 ++++++++++++++++++++ examples/lib-dfscq-log/src/main2.rs | 61 ++ examples/lib-dfscq-log/src/spacer.rs | 133 +++++ flake.lock | 27 + flake.nix | 22 + lua-bindings/Cargo.toml | 15 + lua-bindings/src/lib.rs | 116 ++++ result | 1 + shell.nix | 10 + test.svg | 377 ++++++++++++ z3-solver/Cargo.toml | 12 + z3-solver/src/lib.rs | 691 +++++++++++++++++++++ z3-solver/src/solving/mod.rs | 9 + z3-solver/src/solving/z3/mod.rs | 44 ++ 47 files changed, 5725 insertions(+) create mode 100644 .envrc create mode 100644 .gitignore create mode 100644 .luarc.json create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 TODO.md create mode 100644 cairo-renderer/Cargo.toml create mode 100644 cairo-renderer/src/drawing/cairo/mod.rs create mode 100644 cairo-renderer/src/drawing/mod.rs create mode 100644 cairo-renderer/src/lib.rs create mode 100644 cli/Cargo.toml create mode 100644 cli/src/main.rs create mode 100644 core/Cargo.toml create mode 100644 core/src/colors.rs create mode 100644 core/src/complex_shapes.rs create mode 100644 core/src/core_shapes.rs create mode 100644 core/src/lib.rs create mode 100644 core/src/mod.rs create mode 100644 core/src/rendering.rs create mode 100644 core/src/runtime.rs create mode 100644 core/src/solving.rs create mode 100644 core/src/styles.rs create mode 100644 core/src/text.rs create mode 100644 core/src/types.rs create mode 100644 examples/lib-dfscq-log/Cargo.toml create mode 100644 examples/lib-dfscq-log/dfscq-log.lua create mode 100644 examples/lib-dfscq-log/src/block_list.rs create mode 100644 examples/lib-dfscq-log/src/blocks.rs create mode 100644 examples/lib-dfscq-log/src/bracket.rs create mode 100644 examples/lib-dfscq-log/src/explode.rs create mode 100644 examples/lib-dfscq-log/src/labeled.rs create mode 100644 examples/lib-dfscq-log/src/labeled_delimiter.rs create mode 100644 examples/lib-dfscq-log/src/layer.rs create mode 100644 examples/lib-dfscq-log/src/main.rs create mode 100644 examples/lib-dfscq-log/src/main2.rs create mode 100644 examples/lib-dfscq-log/src/spacer.rs create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 lua-bindings/Cargo.toml create mode 100644 lua-bindings/src/lib.rs create mode 120000 result create mode 100644 shell.nix create mode 100644 test.svg create mode 100644 z3-solver/Cargo.toml create mode 100644 z3-solver/src/lib.rs create mode 100644 z3-solver/src/solving/mod.rs create mode 100644 z3-solver/src/solving/z3/mod.rs diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..051d09d --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +eval "$(lorri direnv)" diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/target diff --git a/.luarc.json b/.luarc.json new file mode 100644 index 0000000..e1b9d70 --- /dev/null +++ b/.luarc.json @@ -0,0 +1,4 @@ +{ + "$schema": "https://raw.githubusercontent.com/sumneko/vscode-lua/master/setting/schema.json", + "Lua.workspace.checkThirdParty": false +} \ No newline at end of file diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..f39c0de --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,759 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "anyhow" +version = "1.0.36" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68803225a7b13e47191bab76f2687382b60d259e8cf37f6e1893658b84bb9479" + +[[package]] +name = "approx" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0e60b75072ecd4168020818c0107f2857bb6c4e64252d8d3983f6263b40a5c3" +dependencies = [ + "num-traits", +] + +[[package]] +name = "autocfg" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cdb031dd78e28731d87d56cc8ffef4a8f36ca26c38fe2de700543e627f8a464a" + +[[package]] +name = "bitflags" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693" + +[[package]] +name = "bstr" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ba3569f383e8f1598449f1a423e72e99569137b47740b1da11ef19af3d5c3223" +dependencies = [ + "memchr", +] + +[[package]] +name = "cairo-rs" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c5c0f2e047e8ca53d0ff249c54ae047931d7a6ebe05d00af73e0ffeb6e34bdb8" +dependencies = [ + "bitflags", + "cairo-sys-rs", + "glib", + "glib-sys", + "gobject-sys", + "libc", + "thiserror", +] + +[[package]] +name = "cairo-sys-rs" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2ed2639b9ad5f1d6efa76de95558e11339e7318426d84ac4890b86c03e828ca7" +dependencies = [ + "glib-sys", + "libc", + "system-deps", +] + +[[package]] +name = "cc" +version = "1.0.77" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9f73505338f7d905b19d18738976aae232eb46b8efc15554ffc56deb5d9ebe4" + +[[package]] +name = "cfg-if" +version = "0.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822" + +[[package]] +name = "diaphragm-cairo-renderer" +version = "0.1.0" +dependencies = [ + "cairo-rs", + "diaphragm-core", + "pango", + "pangocairo", +] + +[[package]] +name = "diaphragm-core" +version = "0.1.0" +dependencies = [ + "palette", +] + +[[package]] +name = "diaphragm-examples-lib-dfscq-log" +version = "0.1.0" +dependencies = [ + "diaphragm-cairo-renderer", + "diaphragm-core", + "diaphragm-z3-solver", +] + +[[package]] +name = "diaphragm-lua-bindings" +version = "0.1.0" +dependencies = [ + "diaphragm-cairo-renderer", + "diaphragm-core", + "diaphragm-z3-solver", + "mlua", +] + +[[package]] +name = "diaphragm-z3-solver" +version = "0.1.0" +dependencies = [ + "diaphragm-core", + "z3", +] + +[[package]] +name = "either" +version = "1.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e78d4f1cc4ae33bbfc157ed5d5a5ef3bc29227303d595861deb238fcec4e9457" + +[[package]] +name = "futures-channel" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4b7109687aa4e177ef6fe84553af6280ef2778bdb7783ba44c9dc3399110fe64" +dependencies = [ + "futures-core", +] + +[[package]] +name = "futures-core" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "847ce131b72ffb13b6109a221da9ad97a64cbe48feb1028356b836b47b8f1748" + +[[package]] +name = "futures-executor" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4caa2b2b68b880003057c1dd49f1ed937e38f22fcf6c212188a121f08cf40a65" +dependencies = [ + "futures-core", + "futures-task", + "futures-util", +] + +[[package]] +name = "futures-macro" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77408a692f1f97bcc61dc001d752e00643408fbc922e4d634c655df50d595556" +dependencies = [ + "proc-macro-hack", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "futures-task" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c554eb5bf48b2426c4771ab68c6b14468b6e76cc90996f528c3338d761a4d0d" +dependencies = [ + "once_cell", +] + +[[package]] +name = "futures-util" +version = "0.3.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d304cff4a7b99cfb7986f7d43fbe93d175e72e704a8860787cc95e9ffd85cbd2" +dependencies = [ + "futures-core", + "futures-macro", + "futures-task", + "pin-project", + "pin-utils", + "proc-macro-hack", + "proc-macro-nested", + "slab", +] + +[[package]] +name = "getrandom" +version = "0.1.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fc587bc0ec293155d5bfa6b9891ec18a1e330c234f896ea47fbada4cadbe47e6" +dependencies = [ + "cfg-if", + "libc", + "wasi", +] + +[[package]] +name = "glib" +version = "0.10.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c685013b7515e668f1b57a165b009d4d28cb139a8a989bbd699c10dad29d0c5" +dependencies = [ + "bitflags", + "futures-channel", + "futures-core", + "futures-executor", + "futures-task", + "futures-util", + "glib-macros", + "glib-sys", + "gobject-sys", + "libc", + "once_cell", +] + +[[package]] +name = "glib-macros" +version = "0.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41486a26d1366a8032b160b59065a59fb528530a46a49f627e7048fb8c064039" +dependencies = [ + "anyhow", + "heck", + "itertools", + "proc-macro-crate", + "proc-macro-error", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "glib-sys" +version = "0.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c7e9b997a66e9a23d073f2b1abb4dbfc3925e0b8952f67efd8d9b6e168e4cdc1" +dependencies = [ + "libc", + "system-deps", +] + +[[package]] +name = "gobject-sys" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "952133b60c318a62bf82ee75b93acc7e84028a093e06b9e27981c2b6fe68218c" +dependencies = [ + "glib-sys", + "libc", + "system-deps", +] + +[[package]] +name = "heck" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87cbf45460356b7deeb5e3415b5563308c0a9b057c85e12b06ad551f98d0a6ac" +dependencies = [ + "unicode-segmentation", +] + +[[package]] +name = "itertools" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "284f18f85651fe11e8a991b2adb42cb078325c996ed026d994719efcfca1d54b" +dependencies = [ + "either", +] + +[[package]] +name = "lazy_static" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" + +[[package]] +name = "libc" +version = "0.2.81" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1482821306169ec4d07f6aca392a4681f66c75c9918aa49641a2595db64053cb" + +[[package]] +name = "log" +version = "0.4.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fabed175da42fed1fa0746b0ea71f412aa9d35e76e95e59b192c64b9dc2bf8b" +dependencies = [ + "cfg-if", +] + +[[package]] +name = "memchr" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" + +[[package]] +name = "mlua" +version = "0.8.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4351dbcc863fb6249c81b3bd0c8001214e9d4d44d22cabda17026353a77fe612" +dependencies = [ + "bstr", + "cc", + "mlua_derive", + "num-traits", + "once_cell", + "pkg-config", + "rustc-hash", +] + +[[package]] +name = "mlua_derive" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9214e60d3cf1643013b107330fcd374ccec1e4ba1eef76e7e5da5e8202e71c0" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "num-traits" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a64b1ec5cda2586e284722486d802acf1f7dbdc623e2bfc57e65ca1cd099290" +dependencies = [ + "autocfg", +] + +[[package]] +name = "once_cell" +version = "1.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "13bd41f508810a131401606d54ac32a467c97172d74ba7662562ebba5ad07fa0" + +[[package]] +name = "palette" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a05c0334468e62a4dfbda34b29110aa7d70d58c7fdb2c9857b5874dd9827cc59" +dependencies = [ + "approx", + "num-traits", + "palette_derive", + "phf", + "phf_codegen", +] + +[[package]] +name = "palette_derive" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b4b5f600e60dd3a147fb57b4547033d382d1979eb087af310e91cb45a63b1f4" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "pango" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9937068580bebd8ced19975938573803273ccbcbd598c58d4906efd4ac87c438" +dependencies = [ + "bitflags", + "glib", + "glib-sys", + "gobject-sys", + "libc", + "once_cell", + "pango-sys", +] + +[[package]] +name = "pango-sys" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24d2650c8b62d116c020abd0cea26a4ed96526afda89b1c4ea567131fdefc890" +dependencies = [ + "glib-sys", + "gobject-sys", + "libc", + "system-deps", +] + +[[package]] +name = "pangocairo" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "00f5ae67a05a5e023f09f64e9a71c845274d4b82dedee237b70425811885e883" +dependencies = [ + "bitflags", + "cairo-rs", + "cairo-sys-rs", + "glib", + "glib-sys", + "gobject-sys", + "libc", + "pango", + "pango-sys", + "pangocairo-sys", +] + +[[package]] +name = "pangocairo-sys" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "94ccc97f698c2f0233b84e5ca676893a1e676785b60eec700b9c0e6dcd0feb98" +dependencies = [ + "cairo-sys-rs", + "glib-sys", + "libc", + "pango-sys", + "system-deps", +] + +[[package]] +name = "phf" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3dfb61232e34fcb633f43d12c58f83c1df82962dcdfa565a4e866ffc17dafe12" +dependencies = [ + "phf_shared", +] + +[[package]] +name = "phf_codegen" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cbffee61585b0411840d3ece935cce9cb6321f01c45477d30066498cd5e1a815" +dependencies = [ + "phf_generator", + "phf_shared", +] + +[[package]] +name = "phf_generator" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "17367f0cc86f2d25802b2c26ee58a7b23faeccf78a396094c13dced0d0182526" +dependencies = [ + "phf_shared", + "rand", +] + +[[package]] +name = "phf_shared" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c00cf8b9eafe68dde5e9eaa2cef8ee84a9336a47d566ec55ca16589633b65af7" +dependencies = [ + "siphasher", +] + +[[package]] +name = "pin-project" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ccc2237c2c489783abd8c4c80e5450fc0e98644555b1364da68cc29aa151ca7" +dependencies = [ + "pin-project-internal", +] + +[[package]] +name = "pin-project-internal" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8e8d2bf0b23038a4424865103a4df472855692821aab4e4f5c3312d461d9e5f" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "pin-utils" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8b870d8c151b6f2fb93e84a13146138f05d02ed11c7e7c54f8826aaaf7c9f184" + +[[package]] +name = "pkg-config" +version = "0.3.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3831453b3449ceb48b6d9c7ad7c96d5ea673e9b470a1dc578c2ce6521230884c" + +[[package]] +name = "ppv-lite86" +version = "0.2.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac74c624d6b2d21f425f752262f42188365d7b8ff1aff74c82e45136510a4857" + +[[package]] +name = "proc-macro-crate" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1d6ea3c4595b96363c13943497db34af4460fb474a95c43f4446ad341b8c9785" +dependencies = [ + "toml", +] + +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro-hack" +version = "0.5.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dbf0c48bc1d91375ae5c3cd81e3722dff1abcf81a30960240640d223f59fe0e5" + +[[package]] +name = "proc-macro-nested" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eba180dafb9038b050a4c280019bbedf9f2467b61e5d892dcad585bb57aadc5a" + +[[package]] +name = "proc-macro2" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e0704ee1a7e00d7bb417d0770ea303c1bccbabf0ef1667dae92b5967f5f8a71" +dependencies = [ + "unicode-xid", +] + +[[package]] +name = "quote" +version = "1.0.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "991431c3519a3f36861882da93630ce66b52918dcf1b8e2fd66b397fc96f28df" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rand" +version = "0.7.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a6b1679d49b24bbfe0c803429aa1874472f50d9b363131f0e89fc356b544d03" +dependencies = [ + "getrandom", + "libc", + "rand_chacha", + "rand_core", + "rand_hc", + "rand_pcg", +] + +[[package]] +name = "rand_chacha" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f4c8ed856279c9737206bf725bf36935d8666ead7aa69b52be55af369d193402" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19" +dependencies = [ + "getrandom", +] + +[[package]] +name = "rand_hc" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ca3129af7b92a17112d59ad498c6f81eaf463253766b90396d39ea7a39d6613c" +dependencies = [ + "rand_core", +] + +[[package]] +name = "rand_pcg" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16abd0c1b639e9eb4d7c50c0b8100b0d0f849be2349829c740fe8e6eb4816429" +dependencies = [ + "rand_core", +] + +[[package]] +name = "rustc-hash" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" + +[[package]] +name = "serde" +version = "1.0.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06c64263859d87aa2eb554587e2d23183398d617427327cf2b3d0ed8c69e4800" + +[[package]] +name = "siphasher" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fa8f3741c7372e75519bd9346068370c9cdaabcc1f9599cbcf2a2719352286b7" + +[[package]] +name = "slab" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c111b5bd5695e56cffe5129854aa230b39c93a305372fdbb2668ca2394eea9f8" + +[[package]] +name = "strum" +version = "0.18.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57bd81eb48f4c437cadc685403cad539345bf703d78e63707418431cecd4522b" + +[[package]] +name = "strum_macros" +version = "0.18.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87c85aa3f8ea653bfd3ddf25f7ee357ee4d204731f6aa9ad04002306f6e2774c" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "syn" +version = "1.0.55" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a571a711dddd09019ccc628e1b17fe87c59b09d513c06c026877aa708334f37a" +dependencies = [ + "proc-macro2", + "quote", + "unicode-xid", +] + +[[package]] +name = "system-deps" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0f3ecc17269a19353b3558b313bba738b25d82993e30d62a18406a24aba4649b" +dependencies = [ + "heck", + "pkg-config", + "strum", + "strum_macros", + "thiserror", + "toml", + "version-compare", +] + +[[package]] +name = "thiserror" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e9ae34b84616eedaaf1e9dd6026dbe00dcafa92aa0c8077cb69df1fcfe5e53e" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ba20f23e85b10754cd195504aebf6a27e2e6cbe28c17778a0c930724628dd56" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "toml" +version = "0.5.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a31142970826733df8241ef35dc040ef98c679ab14d7c3e54d827099b3acecaa" +dependencies = [ + "serde", +] + +[[package]] +name = "unicode-segmentation" +version = "1.7.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb0d2e7be6ae3a5fa87eed5fb451aff96f2573d2694942e40543ae0bbe19c796" + +[[package]] +name = "unicode-xid" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f7fe0bb3479651439c9112f72b6c505038574c9fbb575ed1bf3b797fa39dd564" + +[[package]] +name = "version-compare" +version = "0.0.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d63556a25bae6ea31b52e640d7c41d1ab27faba4ccb600013837a3d0b3994ca1" + +[[package]] +name = "version_check" +version = "0.9.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5a972e5669d67ba988ce3dc826706fb0a8b01471c088cb0b6110b805cc36aed" + +[[package]] +name = "wasi" +version = "0.9.0+wasi-snapshot-preview1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cccddf32554fecc6acb585f82a32a72e28b48f8c4c1883ddfeeeaa96f7d8e519" + +[[package]] +name = "z3" +version = "0.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c5bdc8c9e19d1b983c5584cd4baf6fbd71f3ca5c83283b9d46ad7780d67bd3b" +dependencies = [ + "lazy_static", + "log", + "z3-sys", +] + +[[package]] +name = "z3-sys" +version = "0.6.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "afa18ba5fbd4933e41ffb440c3fd91f91fe9cdb7310cce3ddfb6648563811de0" diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..91eae68 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,10 @@ +[workspace] +members = [ + "cairo-renderer", + # "cli", + "core", + "lua-bindings", + "z3-solver", + + "examples/lib-dfscq-log", +] diff --git a/TODO.md b/TODO.md new file mode 100644 index 0000000..da8c9b4 --- /dev/null +++ b/TODO.md @@ -0,0 +1,4 @@ +- Add the diaphragm language +- Add a piet-based renderer +- Add a web-based renderer? (maybe piet) +- Add a live renderer (maybe druid) diff --git a/cairo-renderer/Cargo.toml b/cairo-renderer/Cargo.toml new file mode 100644 index 0000000..9d7d818 --- /dev/null +++ b/cairo-renderer/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "diaphragm-cairo-renderer" +version = "0.1.0" +authors = ["Minijackson "] +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +diaphragm-core = { path = "../core" } + +cairo-rs = { version = "0.9", features = ["svg", "png"] } +pango = "0.9" +pangocairo = "0.10" diff --git a/cairo-renderer/src/drawing/cairo/mod.rs b/cairo-renderer/src/drawing/cairo/mod.rs new file mode 100644 index 0000000..09baa9c --- /dev/null +++ b/cairo-renderer/src/drawing/cairo/mod.rs @@ -0,0 +1,35 @@ +use super::Engine; +use crate::core::{shapes::Shape as CoreShape, types::DefinitelyBounded}; + +use cairo::Context; + +pub struct CairoEngine { + ctx: Context, +} + +impl Engine for CairoEngine { + fn new() -> Self { + let surface = cairo::SvgSurface::for_stream(200., 100., std::io::stdout()).unwrap(); + let ctx = cairo::Context::new(&surface); + + CairoEngine { ctx } + } + + fn draw(&mut self, shape: &DefinitelyBounded) { + let bounds = &shape.bounds; + + self.ctx.move_to(bounds.left, bounds.top); + + match &shape.shape { + CoreShape::Rectangle(_rectangle) => { + self.ctx + .rectangle(bounds.left, bounds.top, bounds.width, bounds.height); + self.ctx.stroke(); + } + CoreShape::Text(text) => { + // TODO: properly shape it, with font, etc. + self.ctx.show_text(&text.content); + } + } + } +} diff --git a/cairo-renderer/src/drawing/mod.rs b/cairo-renderer/src/drawing/mod.rs new file mode 100644 index 0000000..1c32fb1 --- /dev/null +++ b/cairo-renderer/src/drawing/mod.rs @@ -0,0 +1,8 @@ +pub mod cairo; + +use crate::core::{shapes::Shape as CoreShape, types::DefinitelyBounded}; + +pub trait Engine { + fn new() -> Self; + fn draw(&mut self, shape: &DefinitelyBounded); +} diff --git a/cairo-renderer/src/lib.rs b/cairo-renderer/src/lib.rs new file mode 100644 index 0000000..26ca089 --- /dev/null +++ b/cairo-renderer/src/lib.rs @@ -0,0 +1,111 @@ +use diaphragm_core::{ + styles::{Pattern, DefinedDashStyle}, + text::{DefinedFontDescription, FontDescription}, + Renderer, +}; + +pub struct CairoRenderer { + ctx: cairo::Context, +} + +impl CairoRenderer { + pub fn new() -> Self { + // TODO: properly + let surface = cairo::SvgSurface::for_stream(1920., 1080., std::io::stdout()).unwrap(); + let ctx = cairo::Context::new(&surface); + + Self { ctx } + } +} + +impl Renderer for CairoRenderer { + fn move_to(&mut self, x: f64, y: f64) { + self.ctx.move_to(x, y) + } + + fn stroke(&mut self) { + self.ctx.stroke(); + } + + fn fill(&mut self) { + self.ctx.fill(); + } + + fn fill_preserve(&mut self) { + self.ctx.fill_preserve(); + } + + fn set_pattern(&mut self, pattern: &Pattern) { + match pattern { + Pattern::Solid(color) => { + let (red, green, blue, alpha) = color.rgba(); + self.ctx.set_source_rgba(red, green, blue, alpha) + } + Pattern::None => {} + _ => panic!("Unhandled pattern"), + } + } + + fn set_dash(&mut self, dash: &DefinedDashStyle) { + self.ctx.set_dash(&dash.dashes(), dash.offset()); + } + + fn clear_dash(&mut self) { + self.ctx.set_dash(&[], 0.); + } + + fn set_line_width(&mut self, width: f64) { + self.ctx.set_line_width(width); + } + + fn line_to(&mut self, x: f64, y: f64) { + self.ctx.line_to(x, y) + } + + fn rectangle(&mut self, x: f64, y: f64, width: f64, height: f64) { + self.ctx.rectangle(x, y, width, height); + } + + fn text_extents(&self, text: &str, font: &FontDescription) -> (f64, f64) { + let layout = pangocairo::create_layout(&self.ctx).expect("Couldn't create layout"); + let font_desc = pango::FontDescription::from_string(&font.family); + layout.set_font_description(Some(&font_desc)); + layout.set_markup(text); + + //let (extents, _) = layout.get_pixel_extents(); + //(extents.width as f64, extents.height as f64) + + // TODO: get height from the baseline + let mut layout_iter = layout.get_iter().unwrap(); + let _height = loop { + if layout_iter.at_last_line() { + break layout_iter.get_baseline(); + } + + layout_iter.next_line(); + }; + + // TODO: Probably should use the logical extents, but it has weird width + let (_, extents) = layout.get_pixel_extents(); + //let (extents, _) = layout.get_pixel_extents(); + (extents.width as f64, extents.height as f64) + + //let (width, height) = layout.get_pixel_size(); + //(width as f64, height as f64) + } + + fn show_text(&mut self, text: &str, font: &DefinedFontDescription) { + let layout = pangocairo::create_layout(&self.ctx).expect("Couldn't create layout"); + let mut font_desc = pango::FontDescription::from_string(&font.family); + + // TODO: I have no fucking idea why + font_desc.set_size((font.size * 600.) as _); + //font_desc.set_size((font.size * 700.) as _); + //font_desc.set_absolute_size(font.size * 800.); + layout.set_font_description(Some(&font_desc)); + layout.set_markup(text); + + //self.ctx.set_font_size(dbg!(font.size)); + pangocairo::show_layout(&self.ctx, &layout); + } +} 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 "] +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::> { + 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::> { + 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, + }, + }), + }); +} +*/ diff --git a/core/Cargo.toml b/core/Cargo.toml new file mode 100644 index 0000000..37fb207 --- /dev/null +++ b/core/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "diaphragm-core" +version = "0.1.0" +authors = ["Minijackson "] +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +palette = "0.5" 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; + +#[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; +} + +impl DynClone for T { + fn dyn_clone(&self) -> Box { + Box::new(self.clone()) + } +} + +#[derive(Debug, Clone)] +pub struct Drawable { + pub(crate) context: ShapeContext, + pub(crate) shape: T, +} + +impl Drawable { + 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 + 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 { + context: ShapeContextBuilder, + shape: T, +} + +impl DrawableBuilder { + 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 { + Drawable { + shape: self.shape.clone(), + context: self.context.build(solver), + } + } +} + +pub struct DynDrawable { + pub(crate) context: ShapeContext, + pub(crate) shape: Box, +} + +// TODO: copy paste is bad? +impl DynDrawable { + pub fn new(shape: T, context: ShapeContext) -> Self { + Self { + context, + shape: Box::new(shape), + } + } + + pub fn new_dyn(shape: Box, context: ShapeContext) -> Self { + Self { context, shape } + } + + pub fn from_shape(shape: T, solver: &mut dyn SolverContext) -> Self { + Self { + context: ShapeContext::builder().build(solver), + shape: Box::new(shape), + } + } + + pub fn from_dyn(shape: Box, 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 From> for DynDrawable { + fn from(drawable: Drawable) -> Self { + DynDrawable { + context: drawable.context, + shape: Box::new(drawable.shape), + } + } +} + +pub struct DrawResult { + pub(crate) subshapes: Vec, + pub(crate) waiting_on: Vec<()>, +} + +impl DrawResult { + pub fn new() -> Self { + Self { + subshapes: Vec::new(), + waiting_on: Vec::new(), + } + } + + /* + pub fn push_shape(&mut self, shape: T, context: ShapeContext) { + self.subshapes.push(DynDrawable { + context, + shape: Box::new(shape), + }) + } + + pub fn push_boxed_shape(&mut self, shape: Box, context: ShapeContext) { + self.subshapes.push(DynDrawable { context, shape }) + } + */ + + pub fn push(&mut self, drawable: Drawable) { + 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 { + 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>, + Vec>>, + ) { + // TODO: clone, really? + ( + vec![Bounded:: { + bounds: bounds.clone(), + shape: self.clone(), + }], + vec![], + ) + } + + fn constraints(&self, _bounds: &Bounds, _z3_ctx: &z3::Context) -> Vec { + vec![] + } +} + +/* +impl<'a, T: Drawable> Drawable for Vec> { + fn draw<'z3>( + &self, + _bounds: &Bounds<'z3>, + as_render Vec>, + Vec>>, + ) { + 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 { + 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>; +} + +impl 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> { + 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> { + self.fixate(model) + .map(|path| -> Box { Box::new(path) }) + } +} + +#[derive(Clone, Debug, Default)] +pub struct StraightPath { + pub(crate) points: Vec, +} + +impl StraightPath { + pub fn new(points: Vec) -> Self { + Self { points } + } +} + +pub struct DefinedStraightPath { + pub(crate) points: Vec, +} + +impl CoreShape for StraightPath { + fn to_render(&self, model: &dyn SolverModel) -> Option> { + self.fixate(model) + .map(|path| -> Box { 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>>, +} + +impl<'z3> Context<'z3> { + pub fn new() -> Self { + Self { drawables: vec![] } + } + + pub fn add_shape(&mut self, shape: Bounded<'z3, Box>) { + 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> { + 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, + renderer: Box, + drawables: Vec, +} + +impl<'a> Runtime<'a> { + pub fn new(solver_ctx: Box, renderer: Box) -> Self { + Self { + solver_ctx, + renderer, + drawables: Vec::new(), + } + } + + pub fn add_drawable(&mut self, drawable: Drawable) { + 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 + '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 + '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; + 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; + fn eval_bool(&self, b: Bool) -> Option; +} + +/* +pub trait Solver { + fn constrain(&mut self, assertion: &Bool); + fn solve(&self) -> Box; +} +*/ + +use super::types::*; + +pub trait Constrainable { + type Fixated; + + fn fixate(&self, model: &dyn SolverModel) -> Option; +} + +impl Constrainable for Float { + type Fixated = f64; + + fn fixate(&self, model: &dyn SolverModel) -> Option { + 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::(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 { + 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 { + 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 { + Some(DefinedDashStyle { + dashes: self + .dashes + .iter() + .map(|value| value.fixate(model)) + .collect::>()?, + offset: self.offset.fixate(model)?, + }) + } +} + +impl Constrainable for ShapeContext { + type Fixated = DefinedShapeContext; + + fn fixate(&self, model: &dyn SolverModel) -> Option { + 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 { + 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 { + 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 { + 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 { + 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, + 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, + dash: Option, + line_width: Option, +} + +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, + pub(crate) offset: Float, +} + +impl DashStyle { + pub fn new(dashes: Vec, offset: Float) -> Self { + Self { dashes, offset } + } + + pub fn dashes(&self) -> &[Float] { + &self.dashes + } + + pub fn dashes_mut(&mut self) -> &mut Vec { + &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, + pub(crate) line_width: f64, +} + +#[derive(Clone, PartialEq, Debug, Default)] +pub struct DefinedDashStyle { + pub(crate) dashes: Vec, + 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 { + match self { + Float::Fixed(_) => None, + Float::Variable(handle) => Some(handle), + } + } + */ +} + +#[derive(Clone, Default)] +struct FloatBuilder(Option); + +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| 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 { + 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 { + 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, + fill: Option, + stroke: Option, +} + +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, +} diff --git a/examples/lib-dfscq-log/Cargo.toml b/examples/lib-dfscq-log/Cargo.toml new file mode 100644 index 0000000..8146aa4 --- /dev/null +++ b/examples/lib-dfscq-log/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "diaphragm-examples-lib-dfscq-log" +version = "0.1.0" +authors = ["Minijackson "] +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[package.metadata.riff] +runtime-inputs = ["z3", "cairo"] + +[dependencies] +diaphragm-core = { path = "../../core" } +diaphragm-z3-solver = { path = "../../z3-solver" } +diaphragm-cairo-renderer = { path = "../../cairo-renderer" } diff --git a/examples/lib-dfscq-log/dfscq-log.lua b/examples/lib-dfscq-log/dfscq-log.lua new file mode 100644 index 0000000..c54e4f2 --- /dev/null +++ b/examples/lib-dfscq-log/dfscq-log.lua @@ -0,0 +1,124 @@ +local diaphragm = require("diaphragm") + +-- TODO: anyone can use metatable? + +local Blocks = diaphragm.Drawable:new() +Blocks.elements = {} +Blocks.unit_width = diaphragm.float() + +function Blocks:draw() + local len = #self.elements + assert(len >= 1, "Blocks must have at least 1 element") + + local total_grow = 0 + for el in self.elements do + total_grow = el.grow or 1 + end + + diaphragm.constrain(self.width == self.unit_width * total_grow) + + local param = self.elements[0] + + -- TODO: this would be written with layout.hstack + + local block = diaphragm.shape.Rectangle:new() + block.fill(param.color) + diaphragm.constrain(block.left() == self.left()) + diaphragm.constrain(block.top() == self.top()) + diaphragm.constrain(block.bottom() == self.bottom()) + diaphragm.constrain(block.width() == (param.grow or 1) * self.unit_width) + + block.draw() + + local previous_right = block.right() + + for i = 2, len do + param = self.elements[i] + + block = diaphragm.shape.Rectangle:new() + block.fill(param.color) + + diaphragm.constrain(block.left() == previous_right) + diaphragm.constrain(block.top() == self.top()) + diaphragm.constrain(block.bottom() == self.bottom()) + diaphragm.constrain(block.width() == (param.grow or 1) * self.unit_width) + + block.draw() + + previous_right = block.right() + end +end + +-- Library +---------- + +local function block(color) + local res = diaphragm.shape.Rectangle:new() + res.fill(color) + return res +end + +local function blocks_by_len(count, color) + local res = {} + for i = 1, count do + res[i] = block(color) + end + + -- TODO: rename cons? Misleading + diaphragm.cons.same_size(res) + return diaphragm.layout.hstack(res) +end + +local function layer(config) + local name = config.name or "" + local entries = config.entries or {} + + -- TODO: how to do it without box? + -- TODO: implement union or combine + -- probably combine because + -- union could remove some + -- strokes + return diaphragm.layout.box({}) +end + +-- Parameters +------------- + +local blue = diaphragm.color.from_rgb(0.35, 0.35, 1.) + +local active_txn_count = 5 + +-- Log API +---------- + +local log_api = layer({ + name = "LogAPI", + entries = { + { + name = "activeTxn", + content = blocks_by_len(active_txn_count, blue), + }, + }, +}) + +-- Group Commit +--------------- + +-- local group_commit = nil + +-- Disk Log +----------- + +-- local disk_log = nil + +-- Applier +---------- + +-- local applier = nil + +diaphragm.draw(diaphragm.layout.vstack({ + log_api, + -- group_commit, + -- disk_log, + -- applier, +})) diff --git a/examples/lib-dfscq-log/src/block_list.rs b/examples/lib-dfscq-log/src/block_list.rs new file mode 100644 index 0000000..be0eee0 --- /dev/null +++ b/examples/lib-dfscq-log/src/block_list.rs @@ -0,0 +1,183 @@ +use super::blocks::Blocks; +use super::bracket::*; + +use diaphragm_core::{ + core_shapes::Text, + text::FontDescription, + types::{Bounds, Float, ShapeContext}, + ComplexShape, DrawResult, Drawable, SolverContext, +}; + +#[derive(Clone)] +pub struct BlockList { + pub block_list: Vec>, + pub block_unit_width: Float, + pub bracket_width: Float, + pub blocks_vert_padding: Float, +} + +impl ComplexShape for BlockList { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let bounds = context.bounds(); + + // Left bracket + let opening_bracket_left = { + let bracket = Drawable::builder(Bracket { + r#type: BracketType::Opening, + }) + .bounds( + Bounds::builder() + .top(bounds.top(solver)) + .left(bounds.left(solver)) + .width(self.bracket_width) + .height(bounds.height(solver)) + .build(solver), + ) + .stroke(context.stroke().clone()) + .build(solver); + + let bracket_left = bracket.bounds().left(solver); + + result.push(bracket); + + bracket_left + }; + + let bounds_left = bounds.left(solver); + let mut x_acc = solver.float_add(&[bounds_left, self.bracket_width]); + + // Block list + + let bounds_top = bounds.top(solver); + let bounds_height = bounds.height(solver); + let wanted_blocks_top = solver.float_add(&[bounds_top, self.blocks_vert_padding]); + let wanted_blocks_height = solver.float_sub(&[ + bounds_height, + self.blocks_vert_padding, + self.blocks_vert_padding, + ]); + + let mut block_list_iter = self.block_list.iter(); + + // First blocks + if let Some(first_blocks) = block_list_iter.next() { + // TODO: waaay too verbose + + let blocks_top = first_blocks.bounds().top(solver); + let blocks_top_constraint = solver.float_eq(blocks_top, wanted_blocks_top); + solver.constrain(blocks_top_constraint); + + let blocks_left = first_blocks.bounds().left(solver); + let blocks_left_constraint = solver.float_eq(blocks_left, x_acc); + solver.constrain(blocks_left_constraint); + + let blocks_height = first_blocks.bounds().height(solver); + let blocks_height_constraint = solver.float_eq(blocks_height, wanted_blocks_height); + solver.constrain(blocks_height_constraint); + + let block_unit_width_constraint = + solver.float_eq(first_blocks.shape().unit_width, self.block_unit_width); + solver.constrain(block_unit_width_constraint); + + result.push(first_blocks.clone()); + + let blocks_width = first_blocks.bounds().width(solver); + x_acc = solver.float_add(&[x_acc, blocks_width]); + } + + // Rest of the blocks + for blocks in block_list_iter { + // Comma + let comma = Drawable::builder(Text { + content: String::from(", "), + font: FontDescription { + family: String::from("mono"), + style: Default::default(), + weight: Default::default(), + size: wanted_blocks_height, + }, + }) + .bounds( + Bounds::builder() + .top(wanted_blocks_top) + .left(x_acc) + .build(solver), + ) + .stroke(context.stroke().clone()) + .build(solver); + + let comma_width = comma.bounds().width(solver); + + x_acc = solver.float_add(&[x_acc, comma_width]); + + result.push(comma); + + // Blocks + /* + let blocks_context = ShapeContext { + bounds: Bounds { + top: blocks_top, + left: x_acc, + height: blocks_height, + width: blocks_width, + }, + fill: FillStyle::default(), + stroke: StrokeStyle::default(), + }; + */ + + let blocks_top = blocks.bounds().top(solver); + let blocks_top_constraint = solver.float_eq(blocks_top, wanted_blocks_top); + solver.constrain(blocks_top_constraint); + + let blocks_left = blocks.bounds().left(solver); + let blocks_left_constraint = solver.float_eq(blocks_left, x_acc); + solver.constrain(blocks_left_constraint); + + let blocks_height = blocks.bounds().height(solver); + let blocks_height_constraint = solver.float_eq(blocks_height, wanted_blocks_height); + solver.constrain(blocks_height_constraint); + + let block_unit_width_constraint = + solver.float_eq(blocks.shape().unit_width, self.block_unit_width); + solver.constrain(block_unit_width_constraint); + + result.push(blocks.clone()); + + let blocks_width = blocks.bounds().width(solver); + x_acc = solver.float_add(&[x_acc, blocks_width]); + } + + // Right bracket + let closing_bracket_right = { + let bracket = Drawable::builder(Bracket { + r#type: BracketType::Closing, + }) + .bounds( + Bounds::builder() + .top(bounds.top(solver)) + .left(x_acc) + .width(self.bracket_width) + .height(bounds.height(solver)) + .build(solver), + ) + .stroke(context.stroke().clone()) + .build(solver); + + let bracket_right = bracket.bounds().right(solver); + + result.push(bracket); + + bracket_right + }; + + let this_width = solver.float_sub(&[closing_bracket_right, opening_bracket_left]); + let bounds_width = bounds.width(solver); + let bounds_width_constraint = solver.float_eq(bounds_width, this_width); + solver.constrain(bounds_width_constraint); + + result + } +} diff --git a/examples/lib-dfscq-log/src/blocks.rs b/examples/lib-dfscq-log/src/blocks.rs new file mode 100644 index 0000000..0576b7d --- /dev/null +++ b/examples/lib-dfscq-log/src/blocks.rs @@ -0,0 +1,72 @@ +use diaphragm_core::{ + core_shapes::Rectangle, + types::{Float, ShapeContext}, + ComplexShape, DrawResult, Drawable, SolverContext, +}; + +#[derive(Debug, Clone)] +pub struct Block { + pub grow: u8, +} + +impl ComplexShape for Block { + fn draw(&self, context: &ShapeContext, _solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + // Grow is handled at the upper level + let block = Drawable::new(Rectangle {}, context.clone()); + + result.push(block); + + result + } +} + +#[derive(Debug, Clone)] +pub struct Blocks { + pub blocks: Vec>, + pub unit_width: Float, +} + +impl ComplexShape for Blocks { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let sum: u8 = self.blocks.iter().map(|block| block.shape().grow).sum(); + + let mut rect_left = context.bounds().left(solver); + let rect_top = context.bounds().top(solver); + let rect_height = context.bounds().height(solver); + + for block in &self.blocks { + let block_top = block.bounds().top(solver); + let rect_top_constraint = solver.float_eq(block_top, rect_top); + solver.constrain(rect_top_constraint); + + let block_left = block.bounds().left(solver); + let rect_left_constraint = solver.float_eq(block_left, rect_left); + solver.constrain(rect_left_constraint); + + let grow = Float::Fixed(block.shape().grow as f64); + let block_width = block.bounds().width(solver); + let rect_width = solver.float_mul(&[self.unit_width, grow]); + let rect_width_constraint = solver.float_eq(block_width, rect_width); + solver.constrain(rect_width_constraint); + + let block_height = block.bounds().height(solver); + let rect_height_constraint = solver.float_eq(block_height, rect_height); + solver.constrain(rect_height_constraint); + + result.push(block.clone()); + + rect_left = solver.float_add(&[rect_left, rect_width]); + } + + let this_width = solver.float_mul(&[self.unit_width, Float::Fixed(sum as f64)]); + let bounds_width = context.bounds().width(solver); + let bounds_width_constraint = solver.float_eq(bounds_width, this_width); + solver.constrain(bounds_width_constraint); + + result + } +} diff --git a/examples/lib-dfscq-log/src/bracket.rs b/examples/lib-dfscq-log/src/bracket.rs new file mode 100644 index 0000000..02bca8d --- /dev/null +++ b/examples/lib-dfscq-log/src/bracket.rs @@ -0,0 +1,42 @@ +use diaphragm_core::{ + core_shapes::StraightPath, types::ShapeContext, ComplexShape, DrawResult, Drawable, + SolverContext, +}; + +#[derive(Copy, Clone)] +pub enum BracketType { + Opening, + Closing, +} + +#[derive(Clone)] +pub struct Bracket { + pub r#type: BracketType, +} + +impl ComplexShape for Bracket { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let bounds = context.bounds(); + + let path = match self.r#type { + BracketType::Opening => StraightPath::new(vec![ + bounds.top_right(solver), + bounds.top_left(solver), + bounds.bottom_left(solver), + bounds.bottom_right(solver), + ]), + BracketType::Closing => StraightPath::new(vec![ + bounds.top_left(solver), + bounds.top_right(solver), + bounds.bottom_right(solver), + bounds.bottom_left(solver), + ]), + }; + + result.push(Drawable::new(path, context.clone())); + + result + } +} diff --git a/examples/lib-dfscq-log/src/explode.rs b/examples/lib-dfscq-log/src/explode.rs new file mode 100644 index 0000000..aeb85bd --- /dev/null +++ b/examples/lib-dfscq-log/src/explode.rs @@ -0,0 +1,86 @@ +use diaphragm_core::{ + core_shapes::StraightPath, + types::{Float, Point2D, ShapeContext}, + ComplexShape, DrawResult, Drawable, SolverContext, +}; + +#[derive(Clone)] +pub struct Explode { + pub top_left: Point2D, + pub top_right: Point2D, + pub bottom_left: Point2D, + pub bottom_right: Point2D, + + pub arm_length: Float, +} + +impl ComplexShape for Explode { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let wanted_top = solver.float_min(&[self.top_left.y(), self.top_right.y()]); + let wanted_left = solver.float_min(&[self.top_left.x(), self.bottom_left.x()]); + let wanted_bottom = solver.float_max(&[self.bottom_left.x(), self.bottom_right.x()]); + let wanted_right = solver.float_max(&[self.top_right.y(), self.bottom_right.y()]); + + let bounds_top = context.bounds().top(solver); + let bounds_left = context.bounds().left(solver); + let bounds_bottom = context.bounds().bottom(solver); + let bounds_right = context.bounds().right(solver); + + // TODO: add a facility to help this? + let bounds_top_constraint = solver.float_eq(bounds_top, wanted_top); + solver.constrain(bounds_top_constraint); + + let bounds_left_constraint = solver.float_eq(bounds_left, wanted_left); + solver.constrain(bounds_left_constraint); + + let bounds_bottom_constraint = solver.float_eq(bounds_bottom, wanted_bottom); + solver.constrain(bounds_bottom_constraint); + + let bounds_right_constraint = solver.float_eq(bounds_right, wanted_right); + solver.constrain(bounds_right_constraint); + + let top_left_arm_bottom = Point2D::new( + self.top_left.x(), + solver.float_add(&[self.top_left.y(), self.arm_length]), + ); + + let bottom_left_arm_top = Point2D::new( + self.bottom_left.x(), + solver.float_sub(&[self.bottom_left.y(), self.arm_length]), + ); + + result.push(Drawable::new( + StraightPath::new(vec![ + self.top_left.clone(), + top_left_arm_bottom, + bottom_left_arm_top, + self.bottom_left.clone(), + ]), + context.clone(), + )); + + let top_right_arm_bottom = Point2D::new( + self.top_right.x(), + solver.float_add(&[self.top_right.y(), self.arm_length]), + ); + + let bottom_right_arm_top = Point2D::new( + self.bottom_right.x(), + solver.float_sub(&[self.bottom_right.y(), self.arm_length]), + ); + + result.push(Drawable::new( + StraightPath::new(vec![ + self.top_right.clone(), + top_right_arm_bottom, + bottom_right_arm_top, + self.bottom_right.clone(), + ]), + context.clone(), + )); + + result + } +} diff --git a/examples/lib-dfscq-log/src/labeled.rs b/examples/lib-dfscq-log/src/labeled.rs new file mode 100644 index 0000000..20aebcd --- /dev/null +++ b/examples/lib-dfscq-log/src/labeled.rs @@ -0,0 +1,64 @@ +use diaphragm_core::{ + core_shapes::Text, + text::FontDescription, + types::{Bounds, Float, ShapeContext}, + ComplexShape, DrawResult, DynClone, SolverContext, +}; + +pub struct Labeled { + pub label: String, + pub label_font: FontDescription, + pub content: Box, + pub content_left: Float, +} + +impl ComplexShape for Labeled { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + // Label + + let label = Text { + content: self.label.clone(), + font: self.label_font.clone(), + }; + + let mut label_context = context.clone(); + // TODO: make the text constrain the width + label_context.bounds.width = solver.new_free_float(); + + let label_right = solver.float_add(&[context.bounds.left, label_context.bounds.width]); + let content_left_constrain = solver.float_eq(label_right, self.content_left); + solver.constrain(content_left_constrain); + + result.push_shape(label, label_context); + + // Content + + let content_context = ShapeContext { + bounds: Bounds { + top: context.bounds.top, + left: solver.float_add(&[context.bounds.left, self.content_left]), + height: context.bounds.height, + width: context.bounds.width, + }, + fill: context.fill.clone(), + stroke: context.stroke.clone(), + }; + + result.push_boxed_shape(self.content.dyn_clone(), content_context); + + result + } +} + +impl DynClone for Labeled { + fn dyn_clone(&self) -> Box { + Box::new(Labeled { + label: self.label.clone(), + label_font: self.label_font.clone(), + content: self.content.dyn_clone(), + content_left: self.content_left.clone(), + }) + } +} diff --git a/examples/lib-dfscq-log/src/labeled_delimiter.rs b/examples/lib-dfscq-log/src/labeled_delimiter.rs new file mode 100644 index 0000000..5a1c610 --- /dev/null +++ b/examples/lib-dfscq-log/src/labeled_delimiter.rs @@ -0,0 +1,121 @@ +use diaphragm_core::{ + core_shapes::{StraightPath, Text}, + types::{Bounds, Float, Point2D, ShapeContext}, + ComplexShape, DrawResult, Drawable, SolverContext, +}; + +#[derive(Debug, Clone)] +pub struct Delimiter { + pub width: Float, + pub label: Drawable, +} + +#[derive(Debug, Clone)] +pub struct LabeledDelimiter { + pub delimiters: Vec, + pub tick_height: Float, +} + +impl ComplexShape for LabeledDelimiter { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let bounds_left = context.bounds().left(solver); + let bounds_right = context.bounds().right(solver); + let bounds_bottom = context.bounds().bottom(solver); + let bounds_width = context.bounds().width(solver); + + let tick_top = context.bounds().top(solver); + let tick_bottom = solver.float_add(&[tick_top, self.tick_height]); + + let first_tick = Drawable::builder(StraightPath::new(vec![ + context.bounds().top_left(solver), + Point2D::new(bounds_left, tick_bottom), + ])) + .bounds( + Bounds::builder() + .top(tick_top) + .left(bounds_left) + .height(self.tick_height) + .width(Float::Fixed(0.)) + .build(solver), + ) + .stroke(context.stroke().clone()) + .build(solver); + + let baseline_y = first_tick.bounds().vert_center(solver); + + result.push(first_tick); + + // TODO: split everything into functions + + let baseline = Drawable::builder(StraightPath::new(vec![ + Point2D::new(bounds_left, baseline_y), + Point2D::new(bounds_right, baseline_y), + ])) + .bounds( + Bounds::builder() + .top(baseline_y) + .left(bounds_left) + .width(bounds_width) + .height(Float::Fixed(0.)) + .build(solver), + ) + .stroke(context.stroke().clone()) + .build(solver); + + result.push(baseline); + + let mut section_end = bounds_left; + let mut all_label_bottoms = vec![]; + + for &Delimiter { + width: section_width, + ref label, + } in &self.delimiters + { + let section_begin = section_end; + section_end = solver.float_add(&[section_end, section_width]); + + let section_half_width = solver.float_div(section_width, Float::Fixed(2.)); + let section_middle = solver.float_add(&[section_begin, section_half_width]); + + let tick = Drawable::builder(StraightPath::new(vec![ + Point2D::new(section_end, tick_top), + Point2D::new(section_end, tick_bottom), + ])) + .bounds( + Bounds::builder() + .top(tick_top) + .left(section_end) + .height(self.tick_height) + .width(Float::Fixed(0.)) + .build(solver), + ) + .stroke(context.stroke().clone()) + .build(solver); + + result.push(tick); + + let label_top = label.bounds().top(solver); + let label_bottom = label.bounds().bottom(solver); + let label_horiz_center = label.bounds().horiz_center(solver); + + let label_top_constraint = solver.float_eq(label_top, tick_bottom); + solver.constrain(label_top_constraint); + + let label_middle_constraint = solver.float_eq(label_horiz_center, section_middle); + solver.constrain(label_middle_constraint); + + result.push(label.clone()); + + all_label_bottoms.push(label_bottom); + } + + let wanted_bounds_bottom = solver.float_max(&all_label_bottoms); + let bounds_bottom_constraint = solver.float_eq(bounds_bottom, wanted_bounds_bottom); + solver.constrain(bounds_bottom_constraint); + + result + } +} diff --git a/examples/lib-dfscq-log/src/layer.rs b/examples/lib-dfscq-log/src/layer.rs new file mode 100644 index 0000000..45edb56 --- /dev/null +++ b/examples/lib-dfscq-log/src/layer.rs @@ -0,0 +1,169 @@ +use diaphragm_core::{ + core_shapes::Rectangle, + core_shapes::Text, + text::FontDescription, + types::{Bounds, Float, ShapeContext}, + ComplexShape, DrawResult, Drawable, DynDrawable, SolverContext, +}; + +#[derive(Clone)] +pub struct Entry { + // TODO: transform this to just Text + pub label: Option, + pub label_vert_center_offset: Option, + pub content: DynDrawable, +} + +#[derive(Clone)] +pub struct Layer { + // TODO: transform this to just Text + pub name: String, + pub name_font: FontDescription, + pub label_font: FontDescription, + pub padding: Float, + pub entries: Vec, + pub entries_width: Float, +} + +impl ComplexShape for Layer { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let bounds_top = context.bounds().top(solver); + let bounds_left = context.bounds().left(solver); + let bounds_right = context.bounds().right(solver); + let bounds_height = context.bounds().height(solver); + + let inner_top = solver.float_add(&[bounds_top, self.padding]); + let inner_right = solver.float_sub(&[bounds_right, self.padding]); + + // Outer box + + result.push(Drawable::new(Rectangle {}, context.clone())); + + // Layer name + + let layer_name = Drawable::builder(Text { + content: self.name.clone(), + font: self.name_font.clone(), + }) + .bounds( + Bounds::builder() + .top(inner_top) + .left(solver.float_add(&[bounds_left, self.padding])) + .build(solver), + ) + .stroke(context.stroke().clone()) + .fill(context.fill().clone()) + .build(solver); + + let layer_name_bottom = layer_name.bounds().bottom(solver); + + /* + let mut rect_context = layer_name_context.clone(); + rect_context.stroke = StrokeStyle::solid(Color::from_rgb(1., 0., 0.)); + result.push_shape(Rectangle {}, rect_context); + */ + + result.push(layer_name); + + // Entries + + let mut entry_y_acc = inner_top; + + for entry in &self.entries { + // Entry content + + /* + let content_context = ShapeContext { + bounds: Bounds { + top: solver.new_free_float(), + left: content_left, + width: entry.width, + height: entry.height, + }, + fill: Default::default(), + stroke: Default::default(), + }; + */ + + let content_vert_center = entry.content.bounds().vert_center(solver); + let content_top = entry.content.bounds().top(solver); + let content_left = entry.content.bounds().left(solver); + let content_bottom = entry.content.bounds().bottom(solver); + + // TODO: to replace with label offset + let content_half_height = solver.float_sub(&[content_vert_center, content_top]); + + result.push_dyn(entry.content.clone()); + + // Entry label + + if let Some(label_content) = entry.label.clone() { + let label_top = solver.new_free_float(); + let label_width = solver.new_free_float(); + let label_left = solver.float_sub(&[inner_right, self.entries_width, label_width]); + + let label = Drawable::builder(Text { + content: label_content, + font: self.label_font.clone(), + }) + .bounds( + Bounds::builder() + .top(label_top) + .left(label_left) + .width(label_width) + .build(solver), + ) + .build(solver); + + /* + let mut rect_context = label_context.clone(); + rect_context.stroke = StrokeStyle::solid(Color::from_rgb(1., 0., 0.)); + result.push_shape(Rectangle {}, rect_context); + */ + + // TODO + let label_vert_center = label.bounds().vert_center(solver); + let label_top = label.bounds().top(solver); + let label_right = label.bounds().right(solver); + + let label_vert_center_constraint = + solver.float_eq(label_vert_center, content_vert_center); + solver.constrain(label_vert_center_constraint); + + let label_half_height = solver.float_sub(&[label_vert_center, label_top]); + + let dumb_label_mid_placement = + solver.float_add(&[entry_y_acc, content_half_height]); + let safe_label_mid_placement = + solver.float_add(&[layer_name_bottom, label_half_height]); + let label_mid_placement = + solver.float_max(&[safe_label_mid_placement, dumb_label_mid_placement]); + let label_mid_placement_constraint = + solver.float_eq(label_vert_center, label_mid_placement); + solver.constrain(label_mid_placement_constraint); + + let label_right_constraint = solver.float_eq(label_right, content_left); + solver.constrain(label_right_constraint); + + result.push(label); + } else { + let content_top_constraint = solver.float_eq(content_top, entry_y_acc); + solver.constrain(content_top_constraint); + + let wanted_content_left = solver.float_sub(&[inner_right, self.entries_width]); + let content_left_constraint = solver.float_eq(content_left, wanted_content_left); + solver.constrain(content_left_constraint); + } + + entry_y_acc = solver.float_add(&[content_bottom, self.padding]); + } + + let wanted_bounds_height = solver.float_sub(&[entry_y_acc, bounds_top]); + let height_constraint = solver.float_eq(bounds_height, wanted_bounds_height); + solver.constrain(height_constraint); + + result + } +} diff --git a/examples/lib-dfscq-log/src/main.rs b/examples/lib-dfscq-log/src/main.rs new file mode 100644 index 0000000..fe5db9a --- /dev/null +++ b/examples/lib-dfscq-log/src/main.rs @@ -0,0 +1,642 @@ +mod block_list; +mod blocks; +mod bracket; +mod explode; +mod labeled_delimiter; +mod layer; +mod spacer; + +//mod labeled; +//use labeled::Labeled; + +use block_list::BlockList; +use blocks::*; +use explode::*; +use labeled_delimiter::*; +use layer::*; +use spacer::*; + +use diaphragm_cairo_renderer::CairoRenderer; +use diaphragm_core::{ + colors::Color, + core_shapes::{Text}, + styles::*, + text::FontDescription, + types::*, + *, +}; +use diaphragm_z3_solver::{z3, Z3Context}; + +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 solver = runtime.solver_ctx(); + + let blue = Color::from_rgb(0.35, 0.35, 1.); + let light_grey = Color::from_rgb(0.8, 0.8, 0.8); + let dark_grey = Color::from_rgb(0.5, 0.5, 0.5); + + // ----------------8<---------------- + + /* + let mut make_blocks = |grows: &[u8]| { + grows + .iter() + .map(|&grow| { + Drawable::builder(Block { grow }) + .fill(FillStyle::solid(blue)) + .build(solver) + }) + .collect() + }; + + let blocks = Drawable::builder(Blocks { + blocks: make_blocks(&[1, 2, 1, 1, 4, 1, 1]), + unit_width: solver.new_free_float(), + }) + .bounds( + Bounds::builder() + .top(Float::Fixed(20.)) + .left(Float::Fixed(20.)) + .width(Float::Fixed(150.)) + .height(Float::Fixed(50.)) + .build(solver), + ) + .build(solver); + + runtime.add_drawable(blocks); + */ + + // ----------------8<---------------- + + /* + let block_unit_width = solver.new_fixed_float(10.); + + fn color_block(grow: u8, color: Color, solver: &mut dyn SolverContext) -> Drawable { + Drawable::builder(Block { grow }) + .fill(FillStyle::solid(color)) + .build(solver) + }; + + fn blocks(block_descs: &[(u8, Color)], solver: &mut dyn SolverContext) -> Drawable { + let mut blocks = Vec::new(); + + for &(grow, color) in block_descs { + blocks.push(color_block(grow, color, solver)); + } + + Drawable::builder(Blocks { + blocks, + unit_width: solver.new_free_float(), + }) + .build(solver) + } + + let block_list = Drawable::builder(BlockList { + block_list: vec![ + blocks(&[(1, light_grey), (1, light_grey), (1, light_grey)], solver), + blocks( + &[ + (1, light_grey), + (2, blue), + (1, light_grey), + (1, light_grey), + (1, light_grey), + ], + solver, + ), + blocks(&[(3, light_grey), (2, blue)], solver), + ], + block_unit_width, + bracket_width: block_unit_width, + blocks_vert_padding: block_unit_width, + }) + .bounds( + Bounds::builder() + .top(Float::Fixed(10.)) + .left(Float::Fixed(10.)) + .height(Float::Fixed(40.)) + .build(solver), + ) + .build(solver); + + runtime.add_drawable(block_list); + */ + + // ----------------8<---------------- + + /* + let label_font = FontDescription { + family: String::from("mono"), + style: Default::default(), + weight: Default::default(), + size: Float::Fixed(15.), + }; + + let layer = Drawable::builder(Layer { + name: String::from("Hello"), + name_font: FontDescription { + family: Default::default(), + style: Default::default(), + weight: Default::default(), + size: Float::Fixed(10.), + }, + entries: vec![], + padding: Float::Fixed(5.), + entries_width: Float::Fixed(50.), + label_font, + }) + .bounds(Bounds::builder() + .top(Float::Fixed(10.)) + .left(Float::Fixed(10.)) + .width(Float::Fixed(100.)) + .height(Float::Fixed(40.)) + .build(solver)) + .build(solver); + + runtime.add_drawable(layer); + */ + + // ----------------8<---------------- + + let title_font = FontDescription { + family: String::from("Fanwood"), + style: Default::default(), + weight: Default::default(), + size: Float::Fixed(30.), + }; + + let label_font = FontDescription { + family: String::from("mono"), + style: Default::default(), + weight: Default::default(), + size: Float::Fixed(15.), + }; + + let layer_padding = Float::Fixed(15.); + let layer_margin = Float::Fixed(15.); + //let layer_height = Float::Fixed(40.); + let layer_left_content_padding = Float::Fixed(240.); + //let layer_width = solver.new_free_float(); + //let layer_width_constraint = solver.float_eq(layer_width, Float::Fixed(100.)); + //solver.constrain(layer_width_constraint); + + let mut layer_top = Float::Fixed(15.); + + let entries_width = solver.new_free_float(); + let mut all_entry_content_widths = vec![]; + + let layer_width = solver.float_add(&[ + layer_left_content_padding, + entries_width, + layer_padding, + layer_padding, + ]); + + let blocks_vert_padding = Float::Fixed(10.); + + let block_unit_width = Float::Fixed(20.); + + let blocks_height = Float::Fixed(26.); + let block_list_height = + solver.float_add(&[blocks_height, blocks_vert_padding, blocks_vert_padding]); + + let blue_transaction_len = 5; + + let blocks = |grows: &[u8], color, solver: &mut dyn SolverContext| { + let mut blocks = Vec::new(); + + for &grow in grows { + blocks.push( + Drawable::builder(Block { grow }) + .fill(FillStyle::solid(color)) + .build(solver), + ); + } + + Drawable::builder(Blocks { + blocks, + unit_width: block_unit_width, + }) + .bounds(Bounds::builder().height(blocks_height).build(solver)) + .build(solver) + }; + + let blocks_by_len = + |len, color, solver: &mut dyn SolverContext| blocks(&vec![1; len], color, solver); + + // Log API + { + let blocks = blocks_by_len(blue_transaction_len, blue, solver); + let blocks_width = blocks.bounds().width(solver); + + let layer = Drawable::builder(Layer { + name: String::from("LogAPI"), + name_font: title_font.clone(), + label_font: label_font.clone(), + padding: layer_padding, + entries: vec![Entry { + label: Some(String::from("activeTxn: ")), + label_vert_center_offset: None, + content: blocks.into(), + }], + entries_width, + }) + .bounds( + Bounds::builder() + // TODO: Replace that with a "distributeHorizontally" that applies to all layer + .top(layer_top) + .left(Float::Fixed(10.)) + .width(layer_width) + .build(solver), + ) + .build(solver); + + all_entry_content_widths.push(blocks_width); + + let layer_height = layer.bounds().height(solver); + layer_top = solver.float_add(&[layer_top, layer_height, layer_margin]); + + runtime.add_drawable(layer); + } + + let solver = runtime.solver_ctx(); + + let other_transactions = [2, 7, 4]; + + let group_commit_left; + let group_commit_right; + let group_commit_bottom; + + // Group Commit + { + let mut block_list = Vec::new(); + for &blocks_count in other_transactions.iter() { + block_list.push(blocks_by_len(blocks_count, dark_grey, solver)); + } + + block_list.push(blocks_by_len(blue_transaction_len, blue, solver)); + + let block_list = Drawable::builder(BlockList { + block_list, + block_unit_width, + blocks_vert_padding: Float::Fixed(10.), + bracket_width: Float::Fixed(10.), + }) + .bounds(Bounds::builder().height(block_list_height).build(solver)) + .build(solver); + + let content_width = block_list.bounds().width(solver); + + group_commit_left = block_list.bounds().left(solver); + group_commit_right = block_list.bounds().right(solver); + group_commit_bottom = block_list.bounds().bottom(solver); + + let layer = Drawable::builder(Layer { + name: String::from("GroupCommit"), + name_font: title_font.clone(), + label_font: label_font.clone(), + padding: layer_padding, + entries: vec![Entry { + label: Some(String::from("commitedTxns: ")), + label_vert_center_offset: None, + content: block_list.into(), + }], + entries_width, + }) + .bounds( + Bounds::builder() + .top(layer_top) + .left(Float::Fixed(10.)) + .width(layer_width) + .build(solver), + ) + .build(solver); + + all_entry_content_widths.push(content_width); + + let layer_height = layer.bounds().height(solver); + layer_top = solver.float_add(&[layer_top, layer_height, layer_margin]); + + runtime.add_drawable(layer); + } + + let solver = runtime.solver_ctx(); + + let commit_in_log_left; + let commit_in_log_right; + let commit_in_log_top; + let big_block_grow; + let small_block_unit_width; + let data_in_log_left; + let data_in_log_right; + let data_in_log_bottom; + + // Disk log + { + big_block_grow = (blue_transaction_len + other_transactions.iter().sum::()) as u8; + + let make_block = |grow, color, solver: &mut dyn SolverContext| { + Drawable::builder(Block { grow }) + .bounds(Bounds::builder().height(blocks_height).build(solver)) + .fill(FillStyle::solid(color)) + .build(solver) + }; + + let make_blocks = |block_descs: &[_], solver: &mut dyn SolverContext| { + let mut blocks = Vec::new(); + + for &(grow, color) in block_descs { + blocks.push(make_block(grow, color, solver)); + } + + blocks + }; + + let header_block = make_block(big_block_grow, Color::black(), solver); + let header_block_width = header_block.bounds().width(solver); + + let mut blocks = vec![header_block]; + + blocks.append(&mut make_blocks( + &[(big_block_grow, light_grey), (big_block_grow, light_grey)], + solver, + )); + + let sample_commit_start_id = blocks.len(); + + for &txn_block_count in other_transactions.iter() { + for _i in 0..txn_block_count { + blocks.push(make_block(1, dark_grey, solver)); + } + } + + for _ in 0..blue_transaction_len { + blocks.push(make_block(1, blue, solver)); + } + + let sample_commit_end_id = blocks.len() - 1; + + commit_in_log_left = blocks[sample_commit_start_id].bounds().left(solver); + commit_in_log_right = blocks[sample_commit_end_id].bounds().right(solver); + commit_in_log_top = blocks[sample_commit_end_id].bounds().top(solver); + + let log_data_blocks_widths: Vec<_> = blocks[1..] + .iter() + .map(|block| block.bounds().width(solver)) + .collect(); + let log_data_blocks_width = solver.float_add(&log_data_blocks_widths); + + let log_space_block = make_block(big_block_grow, Color::white(), solver); + let log_space_width = log_space_block.bounds().width(solver); + blocks.push(log_space_block); + + // Make it so that it takes as much space as the bigger one + small_block_unit_width = solver.new_free_float(); + + let disk_log_layout = Drawable::builder(Blocks { + blocks, + unit_width: small_block_unit_width, + }) + .bounds(Bounds::builder().width(entries_width).build(solver)) + .build(solver); + + let mut make_delimiter_label = |content| { + Drawable::builder(Text { + content: String::from(content), + font: FontDescription { + family: String::from("Fanwood"), + size: Float::Fixed(15.), + style: Default::default(), + weight: Default::default(), + }, + }) + .build(solver) + }; + + let delimiters = vec![ + Delimiter { + label: make_delimiter_label("header"), + width: header_block_width, + }, + Delimiter { + label: make_delimiter_label("data"), + width: log_data_blocks_width, + }, + Delimiter { + label: make_delimiter_label("available"), + width: log_space_width, + }, + ]; + + let disk_log_label = Drawable::builder(LabeledDelimiter { + delimiters, + tick_height: Float::Fixed(10.), + }) + .bounds(Bounds::builder().width(entries_width).build(solver)) + .build(solver); + + let label_left = disk_log_label.bounds().left(solver); + data_in_log_left = solver.float_add(&[label_left, header_block_width]); + data_in_log_right = solver.float_add(&[data_in_log_left, log_data_blocks_width]); + data_in_log_bottom = disk_log_label.bounds().bottom(solver); + + let layer = Drawable::builder(Layer { + name: String::from("DiskLog"), + name_font: title_font.clone(), + label_font: label_font.clone(), + padding: layer_padding, + entries: vec![ + Entry { + label: Some(String::from("disk log: ")), + label_vert_center_offset: None, + content: disk_log_layout.into(), + }, + Entry { + label: None, + label_vert_center_offset: None, + content: disk_log_label.into(), + }, + ], + entries_width, + }) + .bounds( + Bounds::builder() + .top(layer_top) + .left(Float::Fixed(10.)) + .width(layer_width) + .build(solver), + ) + .build(solver); + + let layer_height = layer.bounds().height(solver); + layer_top = solver.float_add(&[layer_top, layer_height, layer_margin]); + + runtime.add_drawable(layer); + } + + let solver = runtime.solver_ctx(); + + // Explode GroupLog -> DiskLog + { + let margin = Float::Fixed(6.); + let explode_top = solver.float_add(&[group_commit_bottom, margin]); + let explode_bottom = solver.float_sub(&[commit_in_log_top, margin]); + + let explode = Drawable::builder(Explode { + top_left: Point2D::new(group_commit_left, explode_top), + top_right: Point2D::new(group_commit_right, explode_top), + bottom_left: Point2D::new(commit_in_log_left, explode_bottom), + bottom_right: Point2D::new(commit_in_log_right, explode_bottom), + + arm_length: Float::Fixed(12.), + }) + .stroke( + StrokeStyle::builder() + .dash(DashStyle::new(vec![Float::Fixed(2.)], Float::Fixed(0.))) + .build(), + ) + .build(solver); + + runtime.add_drawable(explode); + } + + let solver = runtime.solver_ctx(); + + let data_in_applier_top; + let data_in_applier_left; + let data_in_applier_right; + + // Applier + { + // TODO: this is exactly the same as before... + let make_block = |grow, color, solver: &mut dyn SolverContext| { + Drawable::builder(Block { grow }) + .bounds(Bounds::builder().height(blocks_height).build(solver)) + .fill(FillStyle::solid(color)) + .build(solver) + }; + + let _make_blocks = |block_descs: &[_], solver: &mut dyn SolverContext| { + let mut blocks = Vec::new(); + + for &(grow, color) in block_descs { + blocks.push(make_block(grow, color, solver)); + } + + blocks + }; + + let mut blocks = vec![]; + + blocks.push(make_block(big_block_grow, light_grey, solver)); + for &txn_block_count in other_transactions.iter() { + for _i in 0..txn_block_count { + blocks.push(make_block(1, dark_grey, solver)); + } + } + + for _ in 0..blue_transaction_len { + blocks.push(make_block(1, blue, solver)); + } + + let blocks = Drawable::builder(Blocks { + blocks, + unit_width: small_block_unit_width, + }) + .build(solver); + + data_in_applier_top = blocks.bounds().top(solver); + data_in_applier_left = blocks.bounds().left(solver); + data_in_applier_right = blocks.bounds().right(solver); + + let spaced_data = Spacer::builder(blocks) + .horizontal_align_center(solver) + .vertical_align_center_with(Float::Fixed(10.)) + .build(solver); + + let spaced_data = Drawable::builder(spaced_data) + .bounds(Bounds::builder().width(entries_width).build(solver)) + .build(solver); + + let disk_data = Drawable::builder(Block { grow: 1 }) + .bounds( + Bounds::builder() + .height(blocks_height) + .width(entries_width) + .build(solver), + ) + .fill(FillStyle::solid(Color::white())) + .build(solver); + + let layer = Drawable::builder(Layer { + name: String::from("Applier"), + name_font: title_font.clone(), + label_font: label_font.clone(), + padding: layer_padding, + entries: vec![ + Entry { + label: None, + label_vert_center_offset: None, + content: spaced_data.into(), + }, + Entry { + label: Some(String::from("disk data:")), + label_vert_center_offset: None, + content: disk_data.into(), + }, + ], + entries_width, + }) + .bounds( + Bounds::builder() + .top(layer_top) + .left(Float::Fixed(10.)) + .width(layer_width) + .build(solver), + ) + .build(solver); + + runtime.add_drawable(layer); + } + + let solver = runtime.solver_ctx(); + + // Explode DiskLog -> Applier + { + let margin = Float::Fixed(6.); + let explode_top = solver.float_add(&[data_in_log_bottom, margin]); + let explode_bottom = solver.float_sub(&[data_in_applier_top, margin]); + + let explode = Drawable::builder(Explode { + top_left: Point2D::new(data_in_log_left, explode_top), + top_right: Point2D::new(data_in_log_right, explode_top), + bottom_left: Point2D::new(data_in_applier_left, explode_bottom), + bottom_right: Point2D::new(data_in_applier_right, explode_bottom), + + arm_length: Float::Fixed(12.), + }) + .stroke( + StrokeStyle::builder() + .dash(DashStyle::new(vec![Float::Fixed(2.)], Float::Fixed(0.))) + .build(), + ) + .build(solver); + + runtime.add_drawable(explode); + } + + let solver = runtime.solver_ctx(); + + let max_entry_content_width = solver.float_max(&all_entry_content_widths); + let entries_width_constraint = solver.float_eq(entries_width, max_entry_content_width); + solver.constrain(entries_width_constraint); + + runtime.render(); +} diff --git a/examples/lib-dfscq-log/src/main2.rs b/examples/lib-dfscq-log/src/main2.rs new file mode 100644 index 0000000..9db235d --- /dev/null +++ b/examples/lib-dfscq-log/src/main2.rs @@ -0,0 +1,61 @@ +fn main() { + let solver = Solver::new(); + let output = Output::new(); + + let blue_transaction_len = 5; + + let blue_block = Block::builder().color(blue); + let dark_gray_block = Block::builder().color(dark_gray); + + let log_layer = Layer::builder() + .name("LogAPI") + .push_entry( + Entry::builder() + .label("activeTxn: ") + .content( + Blocks::builder() + .push(blue_transaction_len, blue_block.build()) + .build(), + ) + .build(), + ) + .build(); + + let other_transactions = [2, 7, 4]; + + let group_commit_layer = Layer::builder() + .name("GroupCommit") + .push_entry( + Entry::builder() + .label("commitedTxn: ") + .content( + BlockList::builder() + .append( + other_transactions + .iter() + // TODO: need collect? + .map(|len| Blocks::builder().push(len, dark_gray_block.build())), + ) + .push(Blocks::builder().push(blue_transaction_len, blue_block.build())) + .build(), + ) + .build(), + ) + .build(); + + let disk_log_layer = todo!(); + + let applier_layer = todo!(); + + let layers = &[ + &log_layer, + &group_commit_layer, + &disk_log_layer, + &applier_layer, + ]; + constraints::distribute_vertically(solver, layers); + constraints::align_left(solver, layers); + + solver.solve(); + output.write_to_stdout(Output::Format::SVG); +} diff --git a/examples/lib-dfscq-log/src/spacer.rs b/examples/lib-dfscq-log/src/spacer.rs new file mode 100644 index 0000000..6878183 --- /dev/null +++ b/examples/lib-dfscq-log/src/spacer.rs @@ -0,0 +1,133 @@ +use diaphragm_core::{ + types::{Float, ShapeContext}, + ComplexShape, DrawResult, DynDrawable, SolverContext, +}; + +#[derive(Clone)] +pub struct Spacer { + pub margin_left: Float, + pub margin_right: Float, + pub margin_top: Float, + pub margin_bottom: Float, + pub content: DynDrawable, +} + +impl Spacer { + pub fn builder>(drawable: T) -> SpacerBuilder { + SpacerBuilder::new(drawable) + } +} + +impl ComplexShape for Spacer { + fn draw(&self, context: &ShapeContext, solver: &mut dyn SolverContext) -> DrawResult { + let mut result = DrawResult::new(); + + let bounds_left = context.bounds().left(solver); + let bounds_right = context.bounds().right(solver); + let bounds_top = context.bounds().top(solver); + let bounds_bottom = context.bounds().bottom(solver); + + let wanted_content_left = solver.float_add(&[bounds_left, self.margin_left]); + let content_left = self.content.bounds().left(solver); + let content_left_constraint = solver.float_eq(content_left, wanted_content_left); + solver.constrain(content_left_constraint); + + let wanted_content_right = solver.float_sub(&[bounds_right, self.margin_right]); + let content_right = self.content.bounds().right(solver); + let content_right_constraint = solver.float_eq(content_right, wanted_content_right); + solver.constrain(content_right_constraint); + + let wanted_content_top = solver.float_add(&[bounds_top, self.margin_top]); + let content_top = self.content.bounds().top(solver); + let content_top_constraint = solver.float_eq(content_top, wanted_content_top); + solver.constrain(content_top_constraint); + + let wanted_content_bottom = solver.float_sub(&[bounds_bottom, self.margin_bottom]); + let content_bottom = self.content.bounds().bottom(solver); + let content_bottom_constraint = solver.float_eq(content_bottom, wanted_content_bottom); + solver.constrain(content_bottom_constraint); + + result.push_dyn(self.content.clone()); + + result + } +} + +#[derive(Clone)] +pub struct SpacerBuilder { + pub margin_left: Option, + pub margin_right: Option, + pub margin_top: Option, + pub margin_bottom: Option, + pub content: DynDrawable, +} + +impl SpacerBuilder { + pub fn new>(drawable: T) -> Self { + SpacerBuilder { + margin_left: None, + margin_right: None, + margin_top: None, + margin_bottom: None, + content: drawable.into(), + } + } + + pub fn margin_left(&mut self, margin_left: Float) -> &mut Self { + self.margin_left = Some(margin_left); + self + } + + pub fn margin_right(&mut self, margin_right: Float) -> &mut Self { + self.margin_right = Some(margin_right); + self + } + + pub fn margin_top(&mut self, margin_top: Float) -> &mut Self { + self.margin_top = Some(margin_top); + self + } + + pub fn margin_bottom(&mut self, margin_bottom: Float) -> &mut Self { + self.margin_bottom = Some(margin_bottom); + self + } + + pub fn vertical_align_center(&mut self, solver: &mut dyn SolverContext) -> &mut Self { + let vertical_margin = solver.new_free_float(); + self.margin_top = Some(vertical_margin); + self.margin_bottom = Some(vertical_margin); + self + } + + pub fn vertical_align_center_with(&mut self, margin: Float) -> &mut Self { + self.margin_top = Some(margin); + self.margin_bottom = Some(margin); + self + } + + pub fn horizontal_align_center(&mut self, solver: &mut dyn SolverContext) -> &mut Self { + let horizontal_margin = solver.new_free_float(); + self.margin_left = Some(horizontal_margin); + self.margin_right = Some(horizontal_margin); + self + } + + pub fn horizontal_align_center_with(&mut self, margin: Float) -> &mut Self { + self.margin_left = Some(margin); + self.margin_right = Some(margin); + self + } + + pub fn build(&self, solver: &mut dyn SolverContext) -> Spacer { + Spacer { + margin_left: self.margin_left.unwrap_or_else(|| solver.new_free_float()), + margin_right: self.margin_right.unwrap_or_else(|| solver.new_free_float()), + margin_top: self.margin_top.unwrap_or_else(|| solver.new_free_float()), + margin_bottom: self + .margin_bottom + .unwrap_or_else(|| solver.new_free_float()), + content: self.content.clone(), + } + } +} diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..bcd2dca --- /dev/null +++ b/flake.lock @@ -0,0 +1,27 @@ +{ + "nodes": { + "nixpkgs": { + "locked": { + "lastModified": 1670461440, + "narHash": "sha256-jy1LB8HOMKGJEGXgzFRLDU1CBGL0/LlkolgnqIsF0D8=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "04a75b2eecc0acf6239acf9dd04485ff8d14f425", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-22.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..bbe2ab1 --- /dev/null +++ b/flake.nix @@ -0,0 +1,22 @@ +{ + inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-22.11"; + + outputs = { + self, + nixpkgs, + }: let + pkgs = nixpkgs.legacyPackages.x86_64-linux; + in { + devShell.x86_64-linux = pkgs.mkShell { + buildInputs = with pkgs; [ + pkgconfig + cairo + pango + z3 + + lua5_4 + stylua + ]; + }; + }; +} diff --git a/lua-bindings/Cargo.toml b/lua-bindings/Cargo.toml new file mode 100644 index 0000000..3859c4e --- /dev/null +++ b/lua-bindings/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "diaphragm-lua-bindings" +version = "0.1.0" +edition = "2021" + +[lib] +crate-type = ["cdylib"] +name = "diaphragm" + +[dependencies] +diaphragm-core = { path = "../core" } +diaphragm-z3-solver = { path = "../z3-solver" } +diaphragm-cairo-renderer = { path = "../cairo-renderer" } + +mlua = { version = "0.8", features = ["lua54", "module"] } diff --git a/lua-bindings/src/lib.rs b/lua-bindings/src/lib.rs new file mode 100644 index 0000000..6628ee2 --- /dev/null +++ b/lua-bindings/src/lib.rs @@ -0,0 +1,116 @@ +use std::sync::atomic::{AtomicUsize, Ordering}; + +use diaphragm_core::{ + solving::VariableHandle, + text::{FontDescription as CoreFontDescription, FontStyle, FontWeight, Text as CoreText}, + types::Float as CoreFloat, +}; +// use diaphragm_cairo_renderer::CairoRenderer; +// use diaphragm_core::Runtime; +// use diaphragm_z3_solver::{z3, Z3Context}; +use mlua::prelude::*; + +static MAX_ID: AtomicUsize = AtomicUsize::new(0); + +#[derive(Clone, Copy, Debug)] +struct Float(CoreFloat); + +impl Float { + fn new() -> Float { + Float(CoreFloat::Variable(VariableHandle::new( + MAX_ID.fetch_add(1, Ordering::SeqCst), + ))) + } +} +impl LuaUserData for Float {} + +fn float(_: &Lua, _: ()) -> LuaResult { + Ok(Float::new()) +} + +#[derive(Clone, Debug)] +struct FontDescription(CoreFontDescription); +impl LuaUserData for FontDescription {} + +const DEFAULT_FONT_FAMILY: &str = "serif"; + +impl Default for FontDescription { + fn default() -> Self { + Self(CoreFontDescription { + family: DEFAULT_FONT_FAMILY.to_string(), + style: FontStyle::Normal, + weight: FontWeight::Normal, + size: Float::new().0, + }) + } +} + +fn font(_: &Lua, params: LuaTable) -> LuaResult { + // TODO: better validation of the table + // What happens when I mistype a param? + // TODO: better error handling + + let family = params + .get::<_, Option<_>>("family")? + .unwrap_or_else(|| DEFAULT_FONT_FAMILY.to_string()); + + let style = match params.get::<_, Option>("style")?.as_deref() { + Some("normal") | None => FontStyle::Normal, + Some(_) => return Err(LuaError::RuntimeError("Unknown style".to_string())), + }; + + let weight = match params.get::<_, Option>("weight")?.as_deref() { + Some("normal") | None => FontWeight::Normal, + Some(_) => return Err(LuaError::RuntimeError("Unknown weight".to_string())), + }; + + let size = params + .get::<_, Option<_>>("size")? + .unwrap_or_else(Float::new); + + Ok(FontDescription(CoreFontDescription { + family, + style, + weight, + size: size.0, + })) +} + +#[derive(Clone, Debug)] +struct Text(CoreText); +impl LuaUserData for Text {} + +fn text(_: &Lua, params: LuaTable) -> LuaResult { + let content = params.get("content")?; + + let font = params + .get::<_, Option>("font")? + .unwrap_or_default(); + + Ok(Text(CoreText { + content, + font: font.0, + })) +} + +fn draw(_: &Lua, params: LuaTable) -> LuaResult<()> { + let content: LuaTable = params.get("content")?; + let output: LuaTable = params.get("output")?; + + dbg!(content, output); + + Ok(()) +} + +#[mlua::lua_module] +fn libdiaphragm(lua: &Lua) -> LuaResult { + // TODO: the solver as a mutable global solves so much problem (pun not intended) + let exports = lua.create_table()?; + exports.set("text", lua.create_function(text)?)?; + exports.set("font", lua.create_function(font)?)?; + exports.set("float", lua.create_function(float)?)?; + + exports.set("draw", lua.create_function(draw)?)?; + + Ok(exports) +} diff --git a/result b/result new file mode 120000 index 0000000..42743c9 --- /dev/null +++ b/result @@ -0,0 +1 @@ +/nix/store/wzmhg661jib969sj02hbf5991mq4had4-lua-5.4.4 \ No newline at end of file diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..2d25ec7 --- /dev/null +++ b/shell.nix @@ -0,0 +1,10 @@ +{ pkgs ? import {} }: + +pkgs.mkShell { + buildInputs = with pkgs; [ + pkgconfig cairo pango z3 + + # keep this line if you use bash + pkgs.bashInteractive + ]; +} diff --git a/test.svg b/test.svg new file mode 100644 index 0000000..bfef495 --- /dev/null +++ b/test.svg @@ -0,0 +1,377 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/z3-solver/Cargo.toml b/z3-solver/Cargo.toml new file mode 100644 index 0000000..6f63e1c --- /dev/null +++ b/z3-solver/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "diaphragm-z3-solver" +version = "0.1.0" +authors = ["Minijackson "] +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +diaphragm-core = { path = "../core" } + +z3 = "0.9" diff --git a/z3-solver/src/lib.rs b/z3-solver/src/lib.rs new file mode 100644 index 0000000..04d77eb --- /dev/null +++ b/z3-solver/src/lib.rs @@ -0,0 +1,691 @@ +pub use z3; + +use diaphragm_core::{ + solving::VariableHandle, + types::{Bool, Float}, + SolverContext, SolverModel, +}; + +use z3::ast::Ast; + +use std::collections::HashMap; + +#[derive(Debug)] +pub struct Z3Context<'z3> { + ctx: &'z3 z3::Context, + solver: z3::Solver<'z3>, + + floats: HashMap>, + max_float_id: u32, + + bools: HashMap>, + pub max_bool_id: u32, +} + +impl Drop for Z3Context<'_> { + fn drop(&mut self) { + eprintln!("bool: {}", self.max_bool_id); + eprintln!("float: {}", self.max_float_id); + } +} + +fn value_to_num_den(value: f64) -> (i32, i32) { + let fract = value.fract(); + let number_of_fract_digits = -fract.log10().floor(); + + if number_of_fract_digits >= 1. && !number_of_fract_digits.is_infinite() { + let den = 10f64.powf(number_of_fract_digits); + ((value * den) as i32, den as i32) + } else { + (value as i32, 1) + } +} + +impl<'z3> Z3Context<'z3> { + pub fn new(ctx: &'z3 z3::Context) -> Self { + Self { + ctx, + solver: z3::Solver::new(&ctx), + floats: HashMap::new(), + max_float_id: 0, + bools: HashMap::new(), + max_bool_id: 0, + } + } + + fn anon_float(&mut self, f: z3::ast::Real<'z3>) -> Float { + self.max_float_id += 1; + let id = self.max_float_id; + let handle = VariableHandle::new(id as usize); + self.floats.insert(handle, f); + Float::from_handle(handle) + } + + fn anon_bool(&mut self, f: z3::ast::Bool<'z3>) -> Bool { + self.max_bool_id += 1; + let id = self.max_bool_id; + let handle = VariableHandle::new(id as usize); + self.bools.insert(handle, dbg!(f)); + Bool::new(handle) + } + + /* + fn float_handle(&mut self, f: Float) -> VariableHandle { + match f { + Float::Fixed(value) => { + let new_float = self.new_fixed_float(value); + self.float_handle(new_float) + } + Float::Variable(handle) => handle, + } + } + */ + + fn float(&self, f: Float) -> z3::ast::Real<'z3> { + let handle = match f { + Float::Fixed(value) => { + let (num, den) = value_to_num_den(value); + return z3::ast::Real::from_real(&self.ctx, num, den); + } + Float::Variable(handle) => handle, + }; + + self.floats + .get(&handle) + .expect("Couldn't get float") + .clone() + } + + fn bool(&self, f: Bool) -> &z3::ast::Bool<'z3> { + self.bools.get(&f.handle()).expect("Couldn't get float") + } +} + +impl<'z3> SolverContext for Z3Context<'z3> { + fn solve<'a>(&'a self) -> Box { + match self.solver.check() { + z3::SatResult::Unsat | z3::SatResult::Unknown => panic!("Failed solving"), + z3::SatResult::Sat => {} + } + Box::new(Z3Model { + ctx: self, + model: self.solver.get_model().unwrap(), + }) + } + + fn constrain(&mut self, assertion: Bool) { + self.solver.assert( + self.bools + .get(&assertion.handle()) + .expect("Couldn't get bool"), + ); + } + + // Floats + + fn new_free_float(&mut self) -> Float { + self.max_float_id += 1; + let id = self.max_float_id; + let handle = VariableHandle::new(id as usize); + self.floats + .insert(handle, z3::ast::Real::new_const(&self.ctx, id)); + Float::from_handle(handle) + } + + fn new_fixed_float(&mut self, value: f64) -> Float { + self.max_float_id += 1; + let id = self.max_float_id; + let handle = VariableHandle::new(id as usize); + + let (num, den) = value_to_num_den(value); + + self.floats + .insert(handle, z3::ast::Real::from_real(&self.ctx, num, den)); + Float::from_handle(handle) + } + + // TODO: that's a lot of copying things + + fn float_add(&mut self, values: &[Float]) -> Float { + let values = values.iter().map(|f| self.float(*f)).collect::>(); + let result = z3::ast::Real::add( + self.ctx, + &values.iter().collect::>() + ); + + self.anon_float(result) + } + + fn float_sub(&mut self, values: &[Float]) -> Float { + let values = values.iter().map(|f| self.float(*f)).collect::>(); + let result = z3::ast::Real::sub( + self.ctx, + &values.iter().collect::>() + ); + + self.anon_float(result) + } + + fn float_mul(&mut self, values: &[Float]) -> Float { + let values = values.iter().map(|f| self.float(*f)).collect::>(); + let result = z3::ast::Real::mul( + self.ctx, + &values.iter().collect::>() + ); + + self.anon_float(result) + } + + fn float_div(&mut self, lhs: Float, rhs: Float) -> Float { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs.div(&rhs); + self.anon_float(result) + } + + fn float_neg(&mut self, value: Float) -> Float { + self.anon_float(self.float(value).unary_minus()) + } + + fn float_eq(&mut self, lhs: Float, rhs: Float) -> Bool { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs._eq(&rhs); + self.anon_bool(result) + } + + fn float_ne(&mut self, lhs: Float, rhs: Float) -> Bool { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs._eq(&rhs).not(); + self.anon_bool(result) + } + + fn float_gt(&mut self, lhs: Float, rhs: Float) -> Bool { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs.gt(&rhs); + self.anon_bool(result) + } + + fn float_ge(&mut self, lhs: Float, rhs: Float) -> Bool { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs.ge(&rhs); + self.anon_bool(result) + } + + fn float_lt(&mut self, lhs: Float, rhs: Float) -> Bool { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs.lt(&rhs); + self.anon_bool(result) + } + + fn float_le(&mut self, lhs: Float, rhs: Float) -> Bool { + let lhs = self.float(lhs); + let rhs = self.float(rhs); + let result = lhs.le(&rhs); + self.anon_bool(result) + } + + // Bools + + fn new_free_bool(&mut self) -> Bool { + self.max_bool_id += 1; + let id = self.max_bool_id; + let handle = VariableHandle::new(id as usize); + self.bools + .insert(handle, z3::ast::Bool::new_const(&self.ctx, id)); + Bool::new(handle) + } + + fn new_fixed_bool(&mut self, value: bool) -> Bool { + self.max_bool_id += 1; + let id = self.max_bool_id; + let handle = VariableHandle::new(id as usize); + + self.bools + .insert(handle, z3::ast::Bool::from_bool(&self.ctx, value)); + Bool::new(handle) + } + + fn bool_eq(&mut self, lhs: Bool, rhs: Bool) -> Bool { + let lhs = self.bool(lhs); + let rhs = self.bool(rhs); + let result = lhs._eq(&rhs); + self.anon_bool(result) + } + + fn bool_ne(&mut self, lhs: Bool, rhs: Bool) -> Bool { + let lhs = self.bool(lhs); + let rhs = self.bool(rhs); + let result = lhs._eq(&rhs).not(); + self.anon_bool(result) + } + + fn bool_and(&mut self, values: &[Bool]) -> Bool { + let result = z3::ast::Bool::and( + self.ctx, + &values.iter().map(|b| self.bool(*b)).collect::>(), + ); + + self.anon_bool(result) + } + + fn bool_or(&mut self, values: &[Bool]) -> Bool { + let result = z3::ast::Bool::or( + self.ctx, + &values.iter().map(|b| self.bool(*b)).collect::>(), + ); + + self.anon_bool(result) + } + + fn bool_not(&mut self, value: Bool) -> Bool { + self.anon_bool(self.bool(value).not()) + } + + fn bool_implies(&mut self, lhs: Bool, rhs: Bool) -> Bool { + let lhs = self.bool(lhs); + let rhs = self.bool(rhs); + let result = lhs.implies(rhs); + self.anon_bool(result) + } +} + +pub struct Z3Model<'z3> { + ctx: &'z3 Z3Context<'z3>, + model: z3::Model<'z3>, +} + +impl SolverModel for Z3Model<'_> { + fn eval_float(&self, f: Float) -> Option { + let handle = match f { + Float::Fixed(value) => return Some(value), + Float::Variable(handle) => handle, + }; + + let (num, den) = self + .model + .eval::(self.ctx.floats.get(&handle).expect("Couldn't find float")) + .unwrap() + .as_real() + .unwrap(); + // TODO: handle errors + Some(num as f64 / den as f64) + } + + fn eval_bool(&self, f: Bool) -> Option { + Some( + self.model + .eval::(&self.ctx.bool(f)) + .unwrap() + .as_bool() + .unwrap(), + ) + // TODO: handle errors + } +} + +/* +use std::cell::RefCell; +use std::collections::HashMap; +use std::rc::Rc; + +#[derive(Clone, Eq, PartialEq, Debug)] +pub struct Z3Float<'z3> { + id: u32, + real: z3::ast::Real<'z3>, + ctx: Z3Context<'z3>, +} + +// TODO: try to remove this clone? +fn get_real<'z3>(f: &dyn VariableFloat, ctx: &Z3Context<'z3>) -> z3::ast::Real<'z3> { + let id = f.id() as u32; + ctx.0 + .borrow() + .floats + .get(&id) + .expect("Couldn't find float") + .clone() +} + +impl<'z3> VariableFloat<'z3> for Z3Float<'z3> { + fn id(&self) -> usize { + self.id as usize + } + + fn dyn_clone(&self) -> Box + 'z3> { + Box::new(Z3Float { + id: self.id, + real: self.real.clone(), + ctx: self.ctx.clone(), + }) + } + + fn eq(&self, other: &dyn VariableFloat) -> Bool<'z3> { + let other = get_real(other, &self.ctx); + let result = self.real._eq(&other); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn neq(&self, other: &dyn VariableFloat) -> Bool<'z3> { + let other = get_real(other, &self.ctx); + let result = self.real._eq(&other).not(); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn gt(&self, other: &dyn VariableFloat) -> Bool<'z3> { + let other = get_real(other, &self.ctx); + let result = self.real.gt(&other); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn ge(&self, other: &dyn VariableFloat) -> Bool<'z3> { + let other = get_real(other, &self.ctx); + let result = self.real.ge(&other); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn lt(&self, other: &dyn VariableFloat) -> Bool<'z3> { + let other = get_real(other, &self.ctx); + let result = self.real.lt(&other); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn le(&self, other: &dyn VariableFloat) -> Bool<'z3> { + let other = get_real(other, &self.ctx); + let result = self.real.le(&other); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn add(&self, other: &dyn VariableFloat) -> Float<'z3> { + let other = get_real(other, &self.ctx); + let result = &self.real + &other; + let id = self.ctx.anon_float(&result); + + Float::new(Box::new(Z3Float { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn sub(&self, other: &dyn VariableFloat) -> Float<'z3> { + let other = get_real(other, &self.ctx); + let result = &self.real - &other; + let id = self.ctx.anon_float(&result); + + Float::new(Box::new(Z3Float { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn mul(&self, other: &dyn VariableFloat) -> Float<'z3> { + let other = get_real(other, &self.ctx); + let result = &self.real * &other; + let id = self.ctx.anon_float(&result); + + Float::new(Box::new(Z3Float { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn div(&self, other: &dyn VariableFloat) -> Float<'z3> { + let other = get_real(other, &self.ctx); + let result = &self.real / &other; + let id = self.ctx.anon_float(&result); + + Float::new(Box::new(Z3Float { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn neg(&self) -> Float<'z3> { + let result = self.real.unary_minus(); + let id = self.ctx.anon_float(&result); + + Float::new(Box::new(Z3Float { + id, + real: result, + ctx: self.ctx.clone(), + })) + } +} + +#[derive(Clone, Eq, PartialEq, Debug)] +pub struct Z3Bool<'z3> { + id: u32, + real: z3::ast::Bool<'z3>, + ctx: Z3Context<'z3>, +} + +// TODO: try to remove this clone? +fn get_bool<'z3>(f: &dyn VariableBool, ctx: &Z3Context<'z3>) -> z3::ast::Bool<'z3> { + let id = f.id() as u32; + ctx.0 + .borrow() + .bools + .get(&id) + .expect("Couldn't find bool") + .clone() +} + +impl<'z3> VariableBool<'z3> for Z3Bool<'z3> { + fn id(&self) -> usize { + self.id as usize + } + + fn dyn_clone(&self) -> Box + 'z3> { + Box::new(Z3Bool { + id: self.id, + real: self.real.clone(), + ctx: self.ctx.clone(), + }) + } + + fn eq(&self, other: &dyn VariableBool) -> Bool<'z3> { + let other = get_bool(other, &self.ctx); + let result = self.real._eq(&other); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn neq(&self, other: &dyn VariableBool) -> Bool<'z3> { + let other = get_bool(other, &self.ctx); + let result = self.real._eq(&other).not(); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn and(&self, other: &dyn VariableBool) -> Bool<'z3> { + let other = get_bool(other, &self.ctx); + let result = &self.real & &other; + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn or(&self, other: &dyn VariableBool) -> Bool<'z3> { + let other = get_bool(other, &self.ctx); + let result = &self.real | &other; + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } + + fn not(&self) -> Bool<'z3> { + let result = self.real.not(); + let id = self.ctx.anon_bool(&result); + + Bool::new(Box::new(Z3Bool { + id, + real: result, + ctx: self.ctx.clone(), + })) + } +} + +#[derive(Clone, Eq, PartialEq, Debug)] +pub struct Z3Context<'z3>(Rc>>); + +#[derive(Eq, PartialEq, Debug)] +pub struct Z3ContextImpl<'z3> { + ctx: z3::Context, + floats: HashMap>, + max_float_id: u32, + bools: HashMap>, + max_bool_id: u32, +} + +impl<'z3> Z3Context<'z3> { + pub fn new() -> Self { + let conf = z3::Config::new(); + let ctx = z3::Context::new(&conf); + Z3Context(Rc::new(RefCell::new(Z3ContextImpl { + ctx, + floats: HashMap::new(), + max_float_id: 0, + bools: HashMap::new(), + max_bool_id: 0, + }))) + } + + fn anon_float(&self, f: &z3::ast::Real<'z3>) -> u32 { + let mut ctx = self.0.borrow_mut(); + + ctx.max_float_id += 1; + let id = ctx.max_float_id; + ctx.floats.insert(id, f.clone()); + id + } + + fn anon_bool(&self, f: &z3::ast::Bool<'z3>) -> u32 { + let mut ctx = self.0.borrow_mut(); + + ctx.max_float_id += 1; + let id = ctx.max_float_id; + ctx.bools.insert(id, f.clone()); + id + } +} + +impl<'z3> SolverContext<'z3> for Z3Context<'z3> { + fn new_float(&'z3 mut self) -> Box + 'z3> { + let mut ctx: std::cell::RefMut<'z3, _> = self.0.borrow_mut(); + + ctx.max_float_id += 1; + let id = ctx.max_float_id; + // :( + // Should be safe since the z3 context inside the RefCell of self cannot be dropped while + // the Box is still alive + let f = z3::ast::Real::new_const(unsafe { std::mem::transmute(&ctx.ctx) }, id); + ctx.floats.insert(id, f.clone()); + Box::new(Z3Float { + id, + real: f, + ctx: self.clone(), + }) + } + + fn new_bool(&'z3 mut self) -> Box + 'z3> { + let mut ctx = self.0.borrow_mut(); + + ctx.max_bool_id += 1; + let id = ctx.max_float_id; + // :( + // Should be safe since the z3 context inside the RefCell of self cannot be dropped while + // the Box is still alive + let b = z3::ast::Bool::new_const(unsafe { std::mem::transmute(&ctx.ctx) }, id); + ctx.bools.insert(id, b.clone()); + Box::new(Z3Bool { + id: id, + real: b, + ctx: self.clone(), + }) + } +} + +pub struct Z3Solver<'z3>(z3::Solver<'z3>); + +impl<'z3> Z3Solver<'z3> { + pub fn new(ctx: &'z3 Z3Context) -> Self { + Self(z3::Solver::new(unsafe { + // :( + // again + std::mem::transmute(&ctx.0.borrow().ctx) + })) + } +} + +impl<'z3> Solver for Z3Solver<'z3> { + fn constrain(&mut self, assertion: &Bool) { + todo!() + } + + fn solve(&self) -> Box { + todo!() + } +} +*/ diff --git a/z3-solver/src/solving/mod.rs b/z3-solver/src/solving/mod.rs new file mode 100644 index 0000000..f3f6673 --- /dev/null +++ b/z3-solver/src/solving/mod.rs @@ -0,0 +1,9 @@ +pub mod z3; + +#[derive(Debug, Eq, PartialEq, Ord, PartialOrd, Hash, Clone, Copy)] +pub struct FloatHandle(u32); + +pub trait Solver { + // TODO: make handles generic? + fn new_float<'a>(&'a mut self, handles: &mut z3::Handles<'a>) -> FloatHandle; +} diff --git a/z3-solver/src/solving/z3/mod.rs b/z3-solver/src/solving/z3/mod.rs new file mode 100644 index 0000000..2f29073 --- /dev/null +++ b/z3-solver/src/solving/z3/mod.rs @@ -0,0 +1,44 @@ +use super::{Solver, FloatHandle}; + +use std::collections::HashMap; + +pub struct Z3Solver { + ctx: z3::Context, +} + +pub struct Handles<'a> { + float: HashMap>, + float_max_id: u32, +} + +impl<'a> Handles<'a> { + pub fn new() -> Self { + Self { + float: HashMap::new(), + float_max_id: 0, + } + } +} + +impl Z3Solver { + pub fn new<'a>() -> (Self, Handles<'a>) { + let config = z3::Config::new(); + + ( + Self { + ctx: z3::Context::new(&config), + }, + Handles::new(), + ) + } +} + +impl Solver for Z3Solver { + fn new_float<'a>(&'a mut self, handles: &mut Handles<'a>) -> FloatHandle { + let id = handles.float_max_id; + let float = z3::ast::Real::new_const(&self.ctx, id); + handles.float_max_id += 1; + handles.float.insert(id, float); + FloatHandle(id) + } +} -- cgit v1.2.3