theorem
Hex.GraphIso.Nauty.Sparse.count_neighbors
{n : Nat}
(G : SparseGraph n)
(lab ptn starts ends marks hits : Array Nat)
(level stamp first last : Nat)
(hp : lab.toList.Perm (List.range n))
(hs : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hi : Index.Valid n lab ptn level starts ends)
(hm : Scratch.Marks n stamp marks)
(hh : hits.size = n)
(hf : first ≤ last)
(hb : last ≤ n)
:
have r :=
(have marks := marks;
have hits := hits;
have touched := #[];
do
let __s ←
forIn [first:last] (marks, hits, touched) fun (i : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have vertex := lab[i]!;
do
let __s ←
forIn [G.offsets[vertex]!:G.offsets[vertex + 1]!] (marks, hits, touched)
fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have j := (Graph.ofGraph G).neighbor e;
have k := starts[j]!;
if (k != n) = true then
have __do_jp := fun (__r : Unit) (marks hits touched : Array Nat) =>
have hits := hits.set! j (hits[j]! + 1);
pure (ForInStep.yield (marks, hits, touched));
if (marks[k]! != stamp + 1) = true then
have marks := marks.set! k (stamp + 1);
have touched := touched.push k;
do
let __s ←
forIn [k:ends[k]! + 1] hits fun (l : Nat) (__s : Array Nat) =>
have hits := __s;
have hits := hits.set! lab[l]! 0;
pure (ForInStep.yield hits)
have hits : Array Nat := __s
__do_jp () marks hits touched
else __do_jp () marks hits touched
else pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (marks, sortCells touched, hits)).run;
CountScan n stamp marks r.fst r.snd.fst starts r.snd.snd
(List.flatMap (fun (q : Nat) => (Graph.ofGraph G).row lab[q]!) (List.range' first (last - first)))
The nontrivial splitter's executed neighbour loops maintain exact counts on all touched cells, including the first-touch clearing loop.