Solver.dfs2: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/solver.bend as Solver
Lines 261-277 of minebender-game@1.0.0.0/solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/solver.bend&start_line=261&end_line=277

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B

# The same search, carrying the mines t and unassigned cells f of the partial
# layout instead of recounting the whole grid at every step. PROOF.bend
# shows it answers exactly as dfs.
def dfs2(todo: List<&2, Todo>, +part: T.Grid(Maybe<&2, Bool>), +t: Nat, +f: Nat, +ctx: Ctx) ->
  Maybe<&2, T.Grid(Bool)>:
  match todo:
    case Nil{}:
      leaf(ctx, fill(part))
    case Todo{+c, +rel} <> +rest:
      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
      +n = ctx_n(ctx)
      +f1 = Nat.sub(f, 1n)
      dfs.free(is_none(look(part, c)),
        u => dfs2(rest, part, t, f, ctx),
        v => dfs.or(dfs.when(between(t, f1, n) && items_open(p0, rel), x => dfs2(rest, p0, t, f1, ctx)),
          y => dfs.when(between(1n+t, f1, n) && items_open(p1, rel), z => dfs2(rest, p1, 1n+t, f1, ctx))))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Ctx
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Todo
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=between
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=ctx_n
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.free
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.or
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.when
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=fill
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=is_none
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items_open
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=leaf
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=look
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid