ProofSolver.dfs_none.pick: def of minebender-game@1.0.0.0 Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver Lines 934-973 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=934&end_line=973 import Base import minebender-game@1.0.0.0/types.bend as T import minebender-game@1.0.0.0/board.bend as B import minebender-game@1.0.0.0/solver.bend as S import minebender-game@1.0.0.0/proof_lists.bend as PL import minebender-game@1.0.0.0/proof_cells.bend as PS def dfs_none.pick(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +layout: T.Grid(Bool), +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}, +cov: {covers(w, h, S.Todo{c, rel} <> rest, part) == True{} : Bool}, +comp: {completes(w, h, part, layout) == True{} : Bool}, +tot: {B.total_mines(layout) == n : Nat}, +rok: {S.items_ok(rel, layout) == True{} : Bool}, +ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool}, +bl: Bool, ble: {B.mine(layout, c) == bl : Bool}, e: {S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n), x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its})), y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n), z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its}))) == None{} : Maybe<&2, T.Grid(Bool)>}, k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} -> {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})) == True{} : Bool} -> {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), layout) == True{} : Bool} -> Empty, k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>} -> {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})) == True{} : Bool} -> {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), layout) == True{} : Bool} -> Empty) -> Empty: match bl: case False{}: +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}) +comp0 = comp_set(w, h, c, part, layout, False{}, shP, ble, B.cells(w, h), PS.cells_on(w, h), comp) +ok0 = open_ok_sound(w, h, n, p0, rel, layout, PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{False{}}, shP), shL, comp0, tot, rok, ron) +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx} k0(dfs_when_none(S.open_ok(p0, rel, n), x => S.dfs(rest, p0, ctx), dfs_or_none_l(S.dfs.when(S.open_ok(p0, rel, n), x => S.dfs(rest, p0, ctx)), y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n), z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)), e), ok0), covers_set(w, h, c, rel, rest, part, False{}, shP, B.cells(w, h), PS.cells_on(w, h), cov), comp0) case True{}: +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}) +comp1 = comp_set(w, h, c, part, layout, True{}, shP, ble, B.cells(w, h), PS.cells_on(w, h), comp) +ok1 = open_ok_sound(w, h, n, p1, rel, layout, PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{True{}}, shP), shL, comp1, tot, rok, ron) +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx} k1(dfs_when_none(S.open_ok(p1, rel, n), z => S.dfs(rest, p1, ctx), dfs_or_none_r(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n), x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)), y => S.dfs.when(S.open_ok(p1, rel, n), z => S.dfs(rest, p1, ctx)), e), ok1), covers_set(w, h, c, rel, rest, part, True{}, shP, B.cells(w, h), PS.cells_on(w, h), cov), comp1) Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty 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=minebender-game@1.0.0.0/board.bend&name=cells https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine 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/board.bend&name=shaped https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=total_mines https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=WH https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=cells_on https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=shaped_set https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=comp_set https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=completes https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=covers https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=covers_set https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=dfs_or_none_l https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=dfs_or_none_r https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=dfs_when_none https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=items_onb https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=open_ok_sound 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=Item 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=dfs 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=items_ok https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=open_ok https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen