Module Utils.Odometer

Mixed-radix counter (odometer) for enumerating sequences.

An odometer of length n over a domain of size k represents a base-k number stored as an integer array. next increments it in the usual right-to-left carry-propagation order. sequence domain n produces the lazy Sequence of all length-n lists drawn from domain, in lexicographic order.

Used by the teacher's BFS enumeration of Σ* to generate candidate counterexamples.

val next : radix:Base.int -> Base.int Base.array -> Base.int Base.array Base.option

next ~radix idx returns the successor index array in base radix, or None if idx is already at the maximum (all digits = radix - 1).

val materialise : 'a Base.array -> Base.int Base.array -> 'a Base.list

materialise dom idx converts an index array into a list of domain elements.

val sequence : 'a Base.list -> Base.int -> 'a Base.list Base.Sequence.t

sequence domain n lazily enumerates all length-n lists over domain in lexicographic order. Returns an empty sequence if n = 0 and a singleton [] for n = 0, or the empty sequence if domain is empty.