1 files changed, 642 insertions, 0 deletions

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<Block> {
+        Drawable::builder(Block { grow })
+            .fill(FillStyle::solid(color))
+            .build(solver)
+    };
+
+    fn blocks(block_descs: &[(u8, Color)], solver: &mut dyn SolverContext) -> Drawable<Blocks> {
+        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::<usize>()) 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();
+}