From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 16 May 2022 02:08:23 +0000 (+0100)
Subject: spec loop detecton: Write down the rule
X-Git-Tag: otter-1.1.0~77
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=ecef994d8ae0b61fb0db170c4304f6b53eea3c3c;p=otter.git

spec loop detecton: Write down the rule

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
---

diff --git a/src/gamestate.rs b/src/gamestate.rs
index 62cd3b39..700fc1b0 100644
--- a/src/gamestate.rs
+++ b/src/gamestate.rs
@@ -412,6 +412,18 @@ impl SpecDepth {
 }
 
 impl<'a> PieceLoadArgs<'a> {
+  /// Call when recursing to not-strictly-weaker method
+  ///
+  /// Call this when your implementation of any PieceTrait method
+  /// calls another PieceTrait method from another object,
+  /// unless the call is *strictly* lower in the following hierarchy:
+  ///
+  ///  * `load`
+  ///  * `load_inert`
+  ///  * `count` with nonempty `PieceAliases`
+  ///  * `count` with empty `PieceAliases`
+  ///
+  /// If this rule is followed, recursion will be bounded.
   #[throws(SpE)]
   pub fn recursing(mut self) -> Self {
     self.depth = self.depth.increment()