def seek_bounds

bendtorch-core@0.1.0.0 · src/storage/api.bend:621

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

621def seek_bounds(+fuel: Nat, +n: Nat, +k: Nat, +c: Nat, done: Bool, +decided: {done == Nat.is_le(n, c) : Bool},
622  +sized: {c == Model.capacity(k) : Nat}, +left: {Nat.add(fuel, k) == 20n : Nat},
623  +limit: {Nat.is_le(n, Model.capacity(20n)) == True{} : Bool}, +positive: {Nat.is_lt(0n, n) == True{} : Bool}) ->
624  {Storage.bounds(Pair.fst(Nat, Nat, Storage.depth_seek(fuel, n, k, c, done)), n) == True{} : Bool}:
625  match fuel:
626    case 0n:
627      bounds_from(k, n, seek_depth(k, left), positive, seek_full(n, k, left, limit))
628    case 1n+p:
629      match done:
630        case True{}:
631          bounds_from(k, n, seek_room(1n+p, k, left), positive, seek_fit(n, k, c, decided, sized))
632        case False{}:
633          seek_bounds(p, n, 1n+k, Nat.add(c, c), Nat.is_le(n, Nat.add(c, c)), {==}, seek_double(k, c, sized),
634            seek_left(p, k, left), limit, positive)