From 700ffb009610ec26345745f68da7b263c391f69e Mon Sep 17 00:00:00 2001 From: Mikolaj Wielgus Date: Sun, 29 Oct 2023 16:07:43 +0000 Subject: [PATCH] draw,layout: Move segbend construction to `Layout` The method to add loose dots is now private. --- src/draw.rs | 67 ++++++++++++--------------------------------------- src/layout.rs | 43 ++++++++++++++++++++++++++++++--- 2 files changed, 55 insertions(+), 55 deletions(-) diff --git a/src/draw.rs b/src/draw.rs index 889fbd2..1262fff 100644 --- a/src/draw.rs +++ b/src/draw.rs @@ -258,27 +258,23 @@ impl<'a> Draw<'a> { cw: bool, width: f64, ) -> Result { - let (seg, dot) = self.seg(head, to, width)?; let net = head.dot().primitive(&self.layout.graph).net(); - let bend_to = self - .layout - .add_loose_dot(self.layout.primitive(dot).weight()) - .map_err(|err| { - self.undo_seg(seg, dot); - err - })?; - - let bend = self - .layout - .add_loose_bend(dot, bend_to, around, LooseBendWeight { net, cw }) - .map_err(|err| { - self.layout.remove(bend_to.into()); - self.undo_seg(seg, dot); - err - })?; + let segbend = self.layout.add_segbend( + head.dot(), + around, + LooseDotWeight { + net, + circle: Circle { + pos: to, + r: width / 2.0, + }, + }, + LooseSegWeight { net }, + LooseBendWeight { net, cw }, + )?; Ok(SegbendHead { - dot: bend_to, - segbend: Segbend { seg, dot, bend }, + dot: self.layout.primitive(segbend.bend).other_end(segbend.dot), + segbend, }) } @@ -296,39 +292,6 @@ impl<'a> Draw<'a> { Some(self.head(prev_dot.into())) } - //#[debug_requires(width <= self.layout.primitive(head.dot()).weight().circle.r * 2.0)] - #[debug_ensures(ret.is_ok() -> self.layout.node_count() == old(self.layout.node_count() + 2))] - #[debug_ensures(ret.is_err() -> self.layout.node_count() == old(self.layout.node_count()))] - fn seg( - &mut self, - head: Head, - to: Point, - width: f64, - ) -> Result<(LooseSegIndex, LooseDotIndex), ()> { - let net = head.dot().primitive(&self.layout.graph).net(); - let to_index = self.layout.add_loose_dot(LooseDotWeight { - net, - circle: Circle { - pos: to, - r: width / 2.0, - }, - })?; - let seg = self - .layout - .add_loose_seg(head.dot(), to_index, LooseSegWeight { net }) - .map_err(|err| { - self.layout.remove(to_index.into()); - err - })?; - Ok((seg, to_index)) - } - - #[debug_ensures(self.layout.node_count() == old(self.layout.node_count() - 2))] - fn undo_seg(&mut self, seg: LooseSegIndex, dot: LooseDotIndex) { - self.layout.remove(seg.into()); - self.layout.remove(dot.into()); - } - fn head(&self, dot: DotIndex) -> Head { match dot { DotIndex::Fixed(loose) => BareHead { dot: loose }.into(), diff --git a/src/layout.rs b/src/layout.rs index 7204a80..f251eb3 100644 --- a/src/layout.rs +++ b/src/layout.rs @@ -75,11 +75,12 @@ impl Layout { #[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 1))] #[debug_ensures(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))] #[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))] - pub fn add_loose_dot(&mut self, weight: LooseDotWeight) -> Result { + fn add_loose_dot(&mut self, weight: LooseDotWeight) -> Result { self.add_dot(weight) } - #[debug_ensures(self.graph.node_count() == old(self.graph.node_count() + 1))] + #[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 1))] + #[debug_ensures(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))] fn add_dot(&mut self, weight: W) -> Result, ()> where GenericIndex: Into + Copy, @@ -105,6 +106,42 @@ impl Layout { self.add_seg(from, to, weight) } + #[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 4))] + #[debug_ensures(ret.is_ok() -> self.graph.edge_count() == old(self.graph.edge_count() + 5))] + #[debug_ensures(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))] + #[debug_ensures(ret.is_err() -> self.graph.edge_count() == old(self.graph.edge_count()))] + pub fn add_segbend( + &mut self, + from: DotIndex, + around: Index, + dot_weight: LooseDotWeight, + seg_weight: LooseSegWeight, + bend_weight: LooseBendWeight, + ) -> Result { + let seg_to = self.add_loose_dot(dot_weight)?; + let seg = self.add_loose_seg(from, seg_to, seg_weight).map_err(|_| { + self.remove(seg_to.into()); + })?; + + let bend_to = self.add_loose_dot(dot_weight).map_err(|_| { + self.remove(seg.into()); + self.remove(seg_to.into()); + })?; + let bend = self + .add_loose_bend(seg_to, bend_to, around, bend_weight) + .map_err(|_| { + self.remove(bend_to.into()); + self.remove(seg.into()); + self.remove(seg_to.into()); + })?; + + Ok(Segbend { + seg, + dot: seg_to, + bend, + }) + } + #[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 1))] #[debug_ensures(ret.is_ok() -> self.graph.edge_count() == old(self.graph.edge_count() + 2))] #[debug_ensures(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))] @@ -173,7 +210,7 @@ impl Layout { #[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 1))] #[debug_ensures(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))] - pub fn add_loose_bend( + fn add_loose_bend( &mut self, from: LooseDotIndex, to: LooseDotIndex,