def bitseq.next

bend-osdev-algo@0.1.0.0 · bitmap.bend:21

import Base

21# the least i with start <= i < size whose bit is want, or size if there is
22# none (bits past the end of bs are clear)
23def bitseq.next(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>) -> Nat:
24  match size:
25    case 0n:
26      0n
27    case 1n+s:
28      match start want bs:
29        case 1n+st w Nil{}:
30          1n+bitseq.next(s, st, w, Nil{})
31        case 1n+st w Con{h, t}:
32          1n+bitseq.next(s, st, w, t)
33        case 0n False{} Nil{}:
34          0n
35        case 0n True{} Nil{}:
36          1n+s
37        case 0n True{} Con{True{}, t}:
38          0n
39        case 0n False{} Con{False{}, t}:
40          0n
41        case 0n True{} Con{False{}, t}:
42          1n+bitseq.next(s, 0n, True{}, t)
43        case 0n False{} Con{True{}, t}:
44          1n+bitseq.next(s, 0n, False{}, t)