theorem
Hex.GraphIso.Nauty.Sparse.Binary.binary_pass
{n : Nat}
(level stamp : Nat)
(cells : Array Nat)
(s : RefineSt n)
(hp : s.lab.toList.Perm (List.range n))
(hs : s.ptn.size = n)
(hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend)
(hn : cells.toList.Nodup)
(hc :
∀ (a : Nat), a ∈ cells.toList → IsCell s.ptn level a (s.cellend[a]! + 1 - a) ∧ a < s.cellend[a]! ∧ s.cellend[a]! < n)
:
Pass level stamp cells.toList s
(have s := s;
do
let __s ←
forIn cells s fun (first : Nat) (__s : RefineSt n) =>
have s := __s;
have s :=
(have s := s.hash first;
have last := s.cellend[first]! + 1;
have lab := s.lab;
have s :=
{ lab := #[], ptn := s.ptn, active := s.active, queue := s.queue, cellstart := s.cellstart,
cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks,
stamp := s.stamp, numcells := s.numcells, longcode := s.longcode };
have v2 := first;
have hit := #[];
do
let __s ←
forIn [first:last] (lab, v2, hit) fun (j : Nat) (__s : Array Nat × Nat × Array Nat) =>
have lab := __s.fst;
have __s := __s.snd;
have v2 := __s.fst;
have hit := __s.snd;
have v := lab[j]!;
if (s.vmarks[v]! == stamp) = true then
have hit := hit.push v;
pure (ForInStep.yield (lab, v2, hit))
else have lab := lab.set! v2 v;
have v2 := v2 + 1;
pure (ForInStep.yield (lab, v2, hit))
have lab : Array Nat := __s.fst
have __s : Nat × Array Nat := __s.snd
have v2 : Nat := __s.fst
have hit : Array Nat := __s.snd
have s : RefineSt n := s.hash hit.size
have starts : Array Nat := s.cellstart
have s : RefineSt n :=
{ lab := s.lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := #[],
cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks,
stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }
have v3 : Nat := v2
let __s ←
forIn [:hit.size] (lab, starts, v3) fun (t : Nat) (__s : Array Nat × Array Nat × Nat) =>
have lab := __s.fst;
have __s := __s.snd;
have starts := __s.fst;
have v3 := __s.snd;
have j := hit[hit.size - 1 - t]!;
have starts := starts.set! j v2;
have lab := lab.set! v3 j;
have v3 := v3 + 1;
pure (ForInStep.yield (lab, starts, v3))
have lab : Array Nat := __s.fst
have __s : Array Nat × Nat := __s.snd
have starts : Array Nat := __s.fst
have v3 : Nat := __s.snd
have __do_jp : Unit → RefineSt n → Array Nat → Id (RefineSt n) :=
fun (__r : Unit) (s : RefineSt n) (starts : Array Nat) =>
pure
{ lab := lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := starts,
cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks,
stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }
if (v2 != v3 && v2 != first) = true then
have __do_jp := fun (__r : Unit) (starts : Array Nat) =>
have __do_jp := fun (__r : Unit) (starts : Array Nat) =>
have s :=
{ lab := s.lab, ptn := s.ptn.set! (v2 - 1) level, active := s.active, queue := s.queue,
cellstart := s.cellstart, cellend := (s.cellend.set! first (v2 - 1)).set! v2 (v3 - 1),
indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp,
numcells := s.numcells + 1, longcode := s.longcode };
have s := s.hash v2;
if (decide (v2 - first ≤ v3 - v2) && !s.active.mem first) = true then
have s := s.push first;
__do_jp () s starts
else have s := s.push v2;
__do_jp () s starts;
if (v3 == v2 + 1) = true then
have starts := starts.set! lab[v2]! n;
__do_jp () starts
else __do_jp () starts;
if (v2 == first + 1) = true then
have starts := starts.set! lab[first]! n;
__do_jp () starts
else __do_jp () starts
else __do_jp () s starts).run;
pure (ForInStep.yield s)
have s : RefineSt n := __s
pure s).run
The actual singleton-cell iterator admits its complete cell trace. The cached endpoints of all not-yet-processed cells remain valid.