def dfs_none.pick

minebender-game@1.0.0.0 · proof_solver.bend:934

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

934def dfs_none.pick(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
935  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +layout: T.Grid(Bool),
936  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool},
937  +cov: {covers(w, h, S.Todo{c, rel} <> rest, part) == True{} : Bool},
938  +comp: {completes(w, h, part, layout) == True{} : Bool}, +tot: {B.total_mines(layout) == n : Nat},
939  +rok: {S.items_ok(rel, layout) == True{} : Bool}, +ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool},
940  +bl: Bool, ble: {B.mine(layout, c) == bl : Bool},
941  e: {S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n),
942       x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), S.Ctx{w, h, n, rows, its})),
943     y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n),
944       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)>},
945  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)>} ->
946    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})) == True{} : Bool} ->
947    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), layout) == True{} : Bool} -> Empty,
948  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)>} ->
949    {covers(w, h, rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})) == True{} : Bool} ->
950    {completes(w, h, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), layout) == True{} : Bool} -> Empty) -> Empty:
951  match bl:
952    case False{}:
953      +p0 = B.set_at(Maybe<&2, Bool>, part, c, Some{False{}})
954      +comp0 = comp_set(w, h, c, part, layout, False{}, shP, ble, B.cells(w, h), PS.cells_on(w, h), comp)
955      +ok0 = open_ok_sound(w, h, n, p0, rel, layout, PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{False{}}, shP),
956        shL, comp0, tot, rok, ron)
957      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
958      k0(dfs_when_none(S.open_ok(p0, rel, n), x => S.dfs(rest, p0, ctx),
959          dfs_or_none_l(S.dfs.when(S.open_ok(p0, rel, n), x => S.dfs(rest, p0, ctx)),
960            y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, n),
961              z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)), e), ok0),
962        covers_set(w, h, c, rel, rest, part, False{}, shP, B.cells(w, h), PS.cells_on(w, h), cov), comp0)
963    case True{}:
964      +p1 = B.set_at(Maybe<&2, Bool>, part, c, Some{True{}})
965      +comp1 = comp_set(w, h, c, part, layout, True{}, shP, ble, B.cells(w, h), PS.cells_on(w, h), comp)
966      +ok1 = open_ok_sound(w, h, n, p1, rel, layout, PL.shaped_set(Maybe<&2, Bool>, w, h, part, c, Some{True{}}, shP),
967        shL, comp1, tot, rok, ron)
968      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
969      k1(dfs_when_none(S.open_ok(p1, rel, n), z => S.dfs(rest, p1, ctx),
970          dfs_or_none_r(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, n),
971              x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)),
972            y => S.dfs.when(S.open_ok(p1, rel, n), z => S.dfs(rest, p1, ctx)), e), ok1),
973        covers_set(w, h, c, rel, rest, part, True{}, shP, B.cells(w, h), PS.cells_on(w, h), cov), comp1)