def dfs2

minebender-game@1.0.0.0 · solver.bend:261

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

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