layout,math: create some error types

We need this for debugging, as we need some better way to display what
intersects what at what moment. Otherwise it takes a lot of effort to
figure out what is going on.

I had to create some type annotations that appear superfluous. Might be
interference from the `contracts` library. This should be investigated.
This commit is contained in:
Mikolaj Wielgus 2023-12-21 03:17:53 +00:00
parent 9a755059c0
commit 59024d5e74
5 changed files with 178 additions and 87 deletions

View File

@ -9,7 +9,7 @@ use crate::{
WraparoundableIndex,
},
guide::{Guide, Head, HeadTrait, SegbendHead},
layout::Layout,
layout::{Exception, Infringement, Layout},
math::Circle,
primitive::{GetOtherEnd, GetWeight},
rules::{Conditions, Rules},
@ -32,7 +32,12 @@ impl<'a> Draw<'a> {
#[debug_ensures(ret.is_ok() -> self.layout.node_count() == old(self.layout.node_count() + 1))]
#[debug_ensures(ret.is_err() -> self.layout.node_count() == old(self.layout.node_count()))]
pub fn finish_in_dot(&mut self, head: Head, into: FixedDotIndex, width: f64) -> Result<(), ()> {
pub fn finish_in_dot(
&mut self,
head: Head,
into: FixedDotIndex,
width: f64,
) -> Result<(), Exception> {
let tangent = self
.guide(&Default::default())
.head_into_dot_segment(&head, into, width)?;
@ -53,7 +58,7 @@ impl<'a> Draw<'a> {
)?;
}
}
Ok(())
Ok::<(), Exception>(())
}
#[debug_ensures(ret.is_ok() -> self.layout.node_count() == old(self.layout.node_count() + 1))]
@ -64,7 +69,7 @@ impl<'a> Draw<'a> {
into_bend: LooseBendIndex,
into: LooseDotIndex,
width: f64,
) -> Result<(), ()> {
) -> Result<(), Exception> {
let to_head = self.guide(&Default::default()).segbend_head(into);
let to_cw = self
.guide(&Default::default())
@ -86,7 +91,7 @@ impl<'a> Draw<'a> {
into.into(),
LooseSegWeight { band: head.band() },
)?;
Ok(())
Ok::<(), Exception>(())
}
#[debug_ensures(ret.is_ok() -> self.layout.node_count() == old(self.layout.node_count() + 4))]
@ -96,7 +101,7 @@ impl<'a> Draw<'a> {
head: Head,
around: FixedDotIndex,
width: f64,
) -> Result<SegbendHead, ()> {
) -> Result<SegbendHead, Exception> {
let mut tangents = self.guide(&Default::default()).head_around_dot_segments(
&head,
around.into(),
@ -123,7 +128,11 @@ impl<'a> Draw<'a> {
)
.ok()
})
.ok_or(())
// XXX: Use proper exceptions instead of this temporary.
.ok_or(Exception::Infringement(Infringement(
head.dot().into(),
head.dot().into(),
)))
}
#[debug_ensures(ret.is_ok() -> self.layout.node_count() == old(self.layout.node_count() + 4))]
@ -133,7 +142,7 @@ impl<'a> Draw<'a> {
head: Head,
around: BendIndex,
width: f64,
) -> Result<SegbendHead, ()> {
) -> Result<SegbendHead, Exception> {
let mut tangents = self.guide(&Default::default()).head_around_bend_segments(
&head,
around.into(),
@ -160,7 +169,11 @@ impl<'a> Draw<'a> {
)
.ok()
})
.ok_or(())
// XXX: Use proper exceptions instead of this temporary.
.ok_or(Exception::Infringement(Infringement(
head.dot().into(),
head.dot().into(),
)))
}
#[debug_ensures(ret.is_ok() -> self.layout.node_count() == old(self.layout.node_count() + 4))]
@ -173,13 +186,13 @@ impl<'a> Draw<'a> {
to: Point,
cw: bool,
width: f64,
) -> Result<SegbendHead, ()> {
) -> Result<SegbendHead, Exception> {
let head = self.extend_head(head, from)?;
self.segbend(head, around, to, cw, width)
}
#[debug_ensures(self.layout.node_count() == old(self.layout.node_count()))]
fn extend_head(&mut self, head: Head, to: Point) -> Result<Head, ()> {
fn extend_head(&mut self, head: Head, to: Point) -> Result<Head, Infringement> {
if let Head::Segbend(head) = head {
self.layout.move_dot(head.dot, to)?;
Ok(Head::Segbend(head))
@ -197,7 +210,7 @@ impl<'a> Draw<'a> {
to: Point,
cw: bool,
width: f64,
) -> Result<SegbendHead, ()> {
) -> Result<SegbendHead, Exception> {
let segbend = self.layout.insert_segbend(
head.dot(),
around,
@ -215,7 +228,7 @@ impl<'a> Draw<'a> {
cw,
},
)?;
Ok(SegbendHead {
Ok::<SegbendHead, Exception>(SegbendHead {
dot: self.layout.primitive(segbend.bend).other_end(segbend.dot),
segbend,
band: head.band(),

View File

@ -4,7 +4,7 @@ use geo::Line;
use crate::{
graph::{BendIndex, DotIndex, FixedDotIndex, GetBand, LooseDotIndex, MakePrimitive},
layout::Layout,
math::{self, Circle},
math::{self, Circle, NoTangent},
primitive::{GetCore, GetInnerOuter, GetOtherEnd, GetWeight, MakeShape},
rules::{Conditions, Rules},
segbend::Segbend,
@ -77,7 +77,7 @@ impl<'a, 'b> Guide<'a, 'b> {
head: &Head,
into: FixedDotIndex,
width: f64,
) -> Result<Line, ()> {
) -> Result<Line, NoTangent> {
let from_circle = self.head_circle(head, width);
let to_circle = Circle {
pos: self.layout.primitive(into).weight().circle.pos,
@ -93,7 +93,7 @@ impl<'a, 'b> Guide<'a, 'b> {
head: &Head,
around: DotIndex,
width: f64,
) -> Result<(Line, Line), ()> {
) -> Result<(Line, Line), NoTangent> {
let from_circle = self.head_circle(head, width);
let to_circle = self.dot_circle(around, width);
@ -109,7 +109,7 @@ impl<'a, 'b> Guide<'a, 'b> {
around: DotIndex,
cw: bool,
width: f64,
) -> Result<Line, ()> {
) -> Result<Line, NoTangent> {
let from_circle = self.head_circle(head, width);
let to_circle = self.dot_circle(around, width);
@ -122,7 +122,7 @@ impl<'a, 'b> Guide<'a, 'b> {
head: &Head,
around: BendIndex,
width: f64,
) -> Result<(Line, Line), ()> {
) -> Result<(Line, Line), NoTangent> {
let from_circle = self.head_circle(head, width);
let to_circle = self.bend_circle(around, width);
@ -138,7 +138,7 @@ impl<'a, 'b> Guide<'a, 'b> {
around: BendIndex,
cw: bool,
width: f64,
) -> Result<Line, ()> {
) -> Result<Line, NoTangent> {
let from_circle = self.head_circle(head, width);
let to_circle = self.bend_circle(around, width);

View File

@ -1,4 +1,5 @@
use contracts::debug_invariant;
use enum_dispatch::enum_dispatch;
use geo::Point;
use petgraph::stable_graph::StableDiGraph;
use petgraph::visit::EdgeRef;
@ -14,6 +15,7 @@ use crate::graph::{
Retag, SegWeight, Weight, WraparoundableIndex,
};
use crate::guide::Guide;
use crate::math::NoTangent;
use crate::primitive::{
GenericPrimitive, GetConnectable, GetCore, GetEnds, GetFirstRail, GetInnerOuter, GetInterior,
GetOtherEnd, GetWeight, GetWraparound, MakeShape,
@ -23,7 +25,49 @@ use crate::shape::{Shape, ShapeTrait};
pub type RTreeWrapper = GeomWithData<Shape, Index>;
#[derive(Debug)]
#[enum_dispatch]
#[derive(Debug, Clone, Copy)]
pub enum Exception {
NoTangent(NoTangent),
Infringement(Infringement),
Collision(Collision),
AreConnected(AreConnected),
}
impl From<NoTangent> for Exception {
fn from(err: NoTangent) -> Self {
Exception::NoTangent(err)
}
}
impl From<Infringement> for Exception {
fn from(err: Infringement) -> Self {
Exception::Infringement(err)
}
}
impl From<Collision> for Exception {
fn from(err: Collision) -> Self {
Exception::Collision(err)
}
}
impl From<AreConnected> for Exception {
fn from(err: AreConnected) -> Self {
Exception::AreConnected(err)
}
}
#[derive(Debug, Clone, Copy)]
pub struct Infringement(pub Index, pub Index);
#[derive(Debug, Clone, Copy)]
pub struct Collision(pub Index, pub Index);
#[derive(Debug, Clone, Copy)]
pub struct AreConnected(pub Weight, pub Index);
#[derive(Debug, Clone, Copy)]
pub struct Band {
pub net: i64,
pub width: f64,
@ -89,7 +133,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()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
pub fn add_fixed_dot(&mut self, weight: FixedDotWeight) -> Result<FixedDotIndex, ()> {
pub fn add_fixed_dot(&mut self, weight: FixedDotWeight) -> Result<FixedDotIndex, Infringement> {
self.add_dot_infringably(weight, &[])
}
@ -106,7 +150,7 @@ impl Layout {
&mut self,
weight: W,
infringables: &[Index],
) -> Result<GenericIndex<W>, ()>
) -> Result<GenericIndex<W>, Infringement>
where
GenericIndex<W>: Into<Index> + Copy,
{
@ -115,7 +159,7 @@ impl Layout {
self.insert_into_rtree(dot.into());
self.fail_and_remove_if_infringes_except(dot.into(), infringables)?;
Ok(dot)
Ok::<GenericIndex<W>, Infringement>(dot)
}
#[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 1))]
@ -127,7 +171,7 @@ impl Layout {
from: FixedDotIndex,
to: FixedDotIndex,
weight: FixedSegWeight,
) -> Result<FixedSegIndex, ()> {
) -> Result<FixedSegIndex, Infringement> {
self.add_seg_infringably(from, to, weight, &[])
}
@ -142,7 +186,7 @@ impl Layout {
dot_weight: LooseDotWeight,
seg_weight: LooseSegWeight,
bend_weight: LooseBendWeight,
) -> Result<Segbend, ()> {
) -> Result<Segbend, Exception> {
let maybe_wraparound = match around {
WraparoundableIndex::FixedDot(around) => self.primitive(around).wraparound(),
WraparoundableIndex::FixedBend(around) => self.primitive(around).wraparound(),
@ -173,14 +217,14 @@ impl Layout {
}
// Segs must not cross.
if let Some(..) = self.detect_collision(segbend.seg.into()) {
if let Some(collision) = self.detect_collision(segbend.seg.into()) {
let end = self.primitive(segbend.bend).other_end(segbend.dot);
self.remove_interior(&segbend);
self.remove(end.into());
return Err(());
return Err(collision.into());
}
Ok(segbend)
Ok::<Segbend, Exception>(segbend)
}
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
@ -326,7 +370,7 @@ impl Layout {
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
#[debug_ensures(self.graph.edge_count() == old(self.graph.edge_count()))]
fn update_this_and_outward_bows(&mut self, around: LooseBendIndex) -> Result<(), ()> {
fn update_this_and_outward_bows(&mut self, around: LooseBendIndex) -> Result<(), Exception> {
let mut maybe_rail = Some(around);
while let Some(rail) = maybe_rail {
@ -374,7 +418,7 @@ impl Layout {
maybe_rail = self.primitive(rail).outer();
}
Ok(())
Ok::<(), Exception>(())
}
#[debug_ensures(ret.is_ok() -> self.graph.node_count() == old(self.graph.node_count() + 4))]
@ -388,7 +432,7 @@ impl Layout {
dot_weight: LooseDotWeight,
seg_weight: LooseSegWeight,
bend_weight: LooseBendWeight,
) -> Result<Segbend, ()> {
) -> Result<Segbend, Exception> {
self.add_segbend_infringably(
from,
around,
@ -411,29 +455,34 @@ impl Layout {
seg_weight: LooseSegWeight,
bend_weight: LooseBendWeight,
infringables: &[Index],
) -> Result<Segbend, ()> {
) -> Result<Segbend, Exception> {
let seg_to = self.add_dot_infringably(dot_weight, infringables)?;
let seg = self
.add_seg_infringably(from, seg_to, seg_weight, infringables)
.map_err(|_| {
.map_err(|err| {
self.remove(seg_to.into());
})?;
err
})
.map_err(|err| Exception::Infringement(err))?;
let bend_to = self
.add_dot_infringably(dot_weight, infringables)
.map_err(|_| {
.map_err(|err| {
self.remove(seg.into());
self.remove(seg_to.into());
})?;
err
})
.map_err(|err| Exception::Infringement(err))?;
let bend = self
.add_loose_bend_infringably(seg_to, bend_to, around, bend_weight, infringables)
.map_err(|_| {
.map_err(|err| {
self.remove(bend_to.into());
self.remove(seg.into());
self.remove(seg_to.into());
err
})?;
Ok(Segbend {
Ok::<Segbend, Exception>(Segbend {
seg,
dot: seg_to,
bend,
@ -449,7 +498,7 @@ impl Layout {
from: DotIndex,
to: LooseDotIndex,
weight: LooseSegWeight,
) -> Result<LooseSegIndex, ()> {
) -> Result<LooseSegIndex, Infringement> {
self.add_seg_infringably(from, to, weight, &[])
}
@ -463,7 +512,7 @@ impl Layout {
to: impl GetNodeIndex,
weight: W,
infringables: &[Index],
) -> Result<GenericIndex<W>, ()>
) -> Result<GenericIndex<W>, Infringement>
where
GenericIndex<W>: Into<Index> + Copy,
{
@ -508,10 +557,13 @@ impl Layout {
around: WraparoundableIndex,
weight: LooseBendWeight,
infringables: &[Index],
) -> Result<LooseBendIndex, ()> {
) -> Result<LooseBendIndex, Exception> {
// It makes no sense to wrap something around or under one of its connectables.
if self.bands[weight.band].net == around.primitive(self).net() {
return Err(());
return Err(Exception::AreConnected(AreConnected(
weight.into(),
around.into(),
)));
}
//
if let Some(wraparound) = match around {
@ -520,20 +572,23 @@ impl Layout {
WraparoundableIndex::LooseBend(around) => self.primitive(around).wraparound(),
} {
if self.bands[weight.band].net == wraparound.primitive(self).net() {
return Err(());
return Err(Exception::AreConnected(AreConnected(
weight.into(),
wraparound.into(),
)));
}
}
match around {
WraparoundableIndex::FixedDot(core) => {
self.add_core_bend_infringably(from, to, core, weight, infringables)
}
WraparoundableIndex::FixedBend(around) => {
self.add_outer_bend_infringably(from, to, around, weight, infringables)
}
WraparoundableIndex::LooseBend(around) => {
self.add_outer_bend_infringably(from, to, around, weight, infringables)
}
WraparoundableIndex::FixedDot(core) => self
.add_core_bend_infringably(from, to, core, weight, infringables)
.map_err(Into::into),
WraparoundableIndex::FixedBend(around) => self
.add_outer_bend_infringably(from, to, around, weight, infringables)
.map_err(Into::into),
WraparoundableIndex::LooseBend(around) => self
.add_outer_bend_infringably(from, to, around, weight, infringables)
.map_err(Into::into),
}
}
@ -548,7 +603,7 @@ impl Layout {
core: FixedDotIndex,
weight: W,
infringables: &[Index],
) -> Result<LooseBendIndex, ()>
) -> Result<LooseBendIndex, Infringement>
where
GenericIndex<W>: Into<Index> + Copy,
{
@ -577,7 +632,7 @@ impl Layout {
inner: impl GetNodeIndex,
weight: W,
infringables: &[Index],
) -> Result<LooseBendIndex, ()> {
) -> Result<LooseBendIndex, Infringement> {
let core = *self
.graph
.neighbors(inner.node_index())
@ -607,7 +662,7 @@ impl Layout {
self.insert_into_rtree(bend.into());
self.fail_and_remove_if_infringes_except(bend.into(), infringables)?;
Ok(bend)
Ok::<LooseBendIndex, Infringement>(bend)
}
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]
@ -639,10 +694,10 @@ impl Layout {
&mut self,
index: Index,
except: &[Index],
) -> Result<(), ()> {
if let Some(..) = self.detect_infringement_except(index, except) {
) -> Result<(), Infringement> {
if let Some(infringement) = self.detect_infringement_except(index, except) {
self.remove(index);
return Err(());
return Err(infringement);
}
Ok(())
}
@ -671,7 +726,7 @@ impl Layout {
#[debug_invariant(self.test_envelopes())]
impl Layout {
pub fn move_dot(&mut self, dot: LooseDotIndex, to: Point) -> Result<(), ()> {
pub fn move_dot(&mut self, dot: LooseDotIndex, to: Point) -> Result<(), Infringement> {
self.move_dot_infringably(
dot,
to,
@ -695,7 +750,7 @@ impl Layout {
dot: LooseDotIndex,
to: Point,
infringables: &[Index],
) -> Result<(), ()> {
) -> Result<(), Infringement> {
self.primitive(dot)
.seg()
.map(|seg| self.remove_from_rtree(seg.into()));
@ -733,7 +788,7 @@ impl Layout {
GenericPrimitive::new(index, self)
}
fn detect_infringement_except(&self, index: Index, except: &[Index]) -> Option<Index> {
fn detect_infringement_except(&self, index: Index, except: &[Index]) -> Option<Infringement> {
let shape = index.primitive(self).shape();
self.rtree
@ -746,10 +801,11 @@ impl Layout {
.filter(|wrapper| shape.intersects(wrapper.geom()))
.map(|wrapper| wrapper.data)
.next()
.and_then(|infringee| Some(Infringement(index, infringee)))
}
// TODO: Collision and infringement are the same for now. Change this.
fn detect_collision(&self, index: Index) -> Option<Index> {
fn detect_collision(&self, index: Index) -> Option<Collision> {
let shape = index.primitive(self).shape();
self.rtree
@ -761,6 +817,7 @@ impl Layout {
.filter(|wrapper| shape.intersects(wrapper.geom()))
.map(|wrapper| wrapper.data)
.next()
.and_then(|collidee| Some(Collision(index, collidee)))
}
#[debug_ensures(self.graph.node_count() == old(self.graph.node_count()))]

View File

@ -1,6 +1,9 @@
use geo::{geometry::Point, point, EuclideanDistance, Line};
use std::ops::Sub;
#[derive(Debug, Clone, Copy, PartialEq)]
pub struct NoTangent(pub Circle, pub Circle);
#[derive(Debug, Clone, Copy, PartialEq)]
pub struct CanonicalLine {
pub a: f64,
@ -69,8 +72,8 @@ fn cast_point_to_canonical_line(pt: Point, line: CanonicalLine) -> Point {
.into();
}
fn tangent_point_pairs(circle1: Circle, circle2: Circle) -> Result<[(Point, Point); 4], ()> {
let tgs = _tangents(circle1, circle2)?;
fn tangent_point_pairs(circle1: Circle, circle2: Circle) -> Result<[(Point, Point); 4], NoTangent> {
let tgs = _tangents(circle1, circle2).map_err(|_| NoTangent(circle1, circle2))?;
Ok([
(
@ -97,7 +100,7 @@ pub fn tangent_segments(
cw1: Option<bool>,
circle2: Circle,
cw2: Option<bool>,
) -> Result<impl Iterator<Item = Line>, ()> {
) -> Result<impl Iterator<Item = Line>, NoTangent> {
Ok(tangent_point_pairs(circle1, circle2)?
.into_iter()
.filter_map(move |tangent_point_pair| {
@ -128,7 +131,7 @@ pub fn tangent_segment(
cw1: Option<bool>,
circle2: Circle,
cw2: Option<bool>,
) -> Result<Line, ()> {
) -> Result<Line, NoTangent> {
Ok(tangent_segments(circle1, cw1, circle2, cw2)?
.next()
.unwrap())

View File

@ -4,7 +4,7 @@ use crate::{
draw::Draw,
graph::{FixedDotIndex, GetNet, LooseBendIndex},
guide::{BareHead, Head, SegbendHead},
layout::{Band, Layout},
layout::{Band, Exception, Layout},
mesh::{Mesh, VertexIndex},
primitive::{GetInnerOuter, GetWraparound},
rules::Rules,
@ -42,7 +42,12 @@ impl<'a> Tracer<'a> {
}
}
pub fn finish(&mut self, trace: &mut Trace, into: FixedDotIndex, width: f64) -> Result<(), ()> {
pub fn finish(
&mut self,
trace: &mut Trace,
into: FixedDotIndex,
width: f64,
) -> Result<(), Exception> {
self.draw().finish_in_dot(trace.head, into, width)
}
@ -52,7 +57,7 @@ impl<'a> Tracer<'a> {
trace: &mut Trace,
path: &[VertexIndex],
width: f64,
) -> Result<(), ()> {
) -> Result<(), Exception> {
let prefix_length = trace
.path
.iter()
@ -61,39 +66,54 @@ impl<'a> Tracer<'a> {
.count();
let length = trace.path.len();
self.undo_path(trace, length - prefix_length)?;
self.undo_path(trace, length - prefix_length);
self.path(trace, &path[prefix_length..], width)
}
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() + path.len()))]
pub fn path(&mut self, trace: &mut Trace, path: &[VertexIndex], width: f64) -> Result<(), ()> {
pub fn path(
&mut self,
trace: &mut Trace,
path: &[VertexIndex],
width: f64,
) -> Result<(), Exception> {
for (i, vertex) in path.iter().enumerate() {
if let Err(err) = self.step(trace, *vertex, width) {
self.undo_path(trace, i)?;
self.undo_path(trace, i);
return Err(err);
}
}
Ok(())
}
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() - step_count))]
pub fn undo_path(&mut self, trace: &mut Trace, step_count: usize) -> Result<(), ()> {
#[debug_ensures(trace.path.len() == old(trace.path.len() - step_count))]
pub fn undo_path(&mut self, trace: &mut Trace, step_count: usize) {
for _ in 0..step_count {
self.undo_step(trace)?;
self.undo_step(trace);
}
Ok(())
}
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() + 1))]
#[debug_ensures(ret.is_err() -> trace.path.len() == old(trace.path.len()))]
pub fn step(&mut self, trace: &mut Trace, to: VertexIndex, width: f64) -> Result<(), ()> {
pub fn step(
&mut self,
trace: &mut Trace,
to: VertexIndex,
width: f64,
) -> Result<(), Exception> {
trace.head = self.wrap(trace.head, to, width)?.into();
trace.path.push(to);
Ok(())
Ok::<(), Exception>(())
}
fn wrap(&mut self, head: Head, around: VertexIndex, width: f64) -> Result<SegbendHead, ()> {
fn wrap(
&mut self,
head: Head,
around: VertexIndex,
width: f64,
) -> Result<SegbendHead, Exception> {
match around {
VertexIndex::FixedDot(dot) => self.wrap_around_fixed_dot(head, dot, width),
VertexIndex::FixedBend(_fixed_bend) => todo!(),
@ -108,7 +128,7 @@ impl<'a> Tracer<'a> {
head: Head,
around: FixedDotIndex,
width: f64,
) -> Result<SegbendHead, ()> {
) -> Result<SegbendHead, Exception> {
let head = self.draw().segbend_around_dot(head, around.into(), width)?;
Ok(head)
}
@ -118,7 +138,7 @@ impl<'a> Tracer<'a> {
head: Head,
around: LooseBendIndex,
width: f64,
) -> Result<SegbendHead, ()> {
) -> Result<SegbendHead, Exception> {
let head = self
.draw()
.segbend_around_bend(head, around.into(), width)?;
@ -126,17 +146,15 @@ impl<'a> Tracer<'a> {
Ok(head)
}
#[debug_ensures(ret.is_ok() -> trace.path.len() == old(trace.path.len() - 1))]
#[debug_ensures(ret.is_err() -> trace.path.len() == old(trace.path.len()))]
pub fn undo_step(&mut self, trace: &mut Trace) -> Result<(), ()> {
#[debug_ensures(trace.path.len() == old(trace.path.len() - 1))]
pub fn undo_step(&mut self, trace: &mut Trace) {
if let Head::Segbend(head) = trace.head {
trace.head = self.draw().undo_segbend(head).unwrap();
} else {
return Err(());
panic!();
}
trace.path.pop();
Ok(())
}
fn draw(&mut self) -> Draw {