draw,layout: Move segbend construction to `Layout`

The method to add loose dots is now private.
This commit is contained in:
Mikolaj Wielgus 2023-10-29 16:07:43 +00:00
parent f0e2ba6e3a
commit 700ffb0096
2 changed files with 55 additions and 55 deletions

View File

@ -258,27 +258,23 @@ impl<'a> Draw<'a> {
cw: bool, cw: bool,
width: f64, width: f64,
) -> Result<SegbendHead, ()> { ) -> Result<SegbendHead, ()> {
let (seg, dot) = self.seg(head, to, width)?;
let net = head.dot().primitive(&self.layout.graph).net(); let net = head.dot().primitive(&self.layout.graph).net();
let bend_to = self let segbend = self.layout.add_segbend(
.layout head.dot(),
.add_loose_dot(self.layout.primitive(dot).weight()) around,
.map_err(|err| { LooseDotWeight {
self.undo_seg(seg, dot); net,
err circle: Circle {
})?; pos: to,
r: width / 2.0,
let bend = self },
.layout },
.add_loose_bend(dot, bend_to, around, LooseBendWeight { net, cw }) LooseSegWeight { net },
.map_err(|err| { LooseBendWeight { net, cw },
self.layout.remove(bend_to.into()); )?;
self.undo_seg(seg, dot);
err
})?;
Ok(SegbendHead { Ok(SegbendHead {
dot: bend_to, dot: self.layout.primitive(segbend.bend).other_end(segbend.dot),
segbend: Segbend { seg, dot, bend }, segbend,
}) })
} }
@ -296,39 +292,6 @@ impl<'a> Draw<'a> {
Some(self.head(prev_dot.into())) 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 { fn head(&self, dot: DotIndex) -> Head {
match dot { match dot {
DotIndex::Fixed(loose) => BareHead { dot: loose }.into(), DotIndex::Fixed(loose) => BareHead { dot: loose }.into(),

View File

@ -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_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(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))] #[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
pub fn add_loose_dot(&mut self, weight: LooseDotWeight) -> Result<LooseDotIndex, ()> { fn add_loose_dot(&mut self, weight: LooseDotWeight) -> Result<LooseDotIndex, ()> {
self.add_dot(weight) 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<W: DotWeight>(&mut self, weight: W) -> Result<GenericIndex<W>, ()> fn add_dot<W: DotWeight>(&mut self, weight: W) -> Result<GenericIndex<W>, ()>
where where
GenericIndex<W>: Into<Index> + Copy, GenericIndex<W>: Into<Index> + Copy,
@ -105,6 +106,42 @@ impl Layout {
self.add_seg(from, to, weight) 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<Segbend, ()> {
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.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_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()))] #[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_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(ret.is_err() -> self.graph.node_count() == old(self.graph.node_count()))]
pub fn add_loose_bend( fn add_loose_bend(
&mut self, &mut self,
from: LooseDotIndex, from: LooseDotIndex,
to: LooseDotIndex, to: LooseDotIndex,