def solve_stuck.go

minebender-game@1.0.0.0 · proof_solver.bend:2821

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/LAWS.bend as L
import minebender-game@1.0.0.0/proof_cells.bend as PS

2821def solve_stuck.go(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +ok: Bool,
2822  oke: {B.shaped(T.Seen, w, h, rows) == ok : Bool},
2823  e: {S.solve.go(ok, S.hidden_cells(rows, B.cells(w, h)), w, h, n, rows) == None{} : Maybe<&2, T.Pos>},
2824  +p: T.Pos, ps: L.ProvablySafe(T.Knowledge{w, h, n, rows}, p)) -> Empty:
2825  match ok:
2826    case False{}:
2827      match ps:
2828        case (+hid, H):
2829          head_none(S.hidden_cells(rows, B.cells(w, h)), p, e,
2830            hc_member(rows, B.cells(w, h), p, PS.cells_member(w, h, p, hid_on(w, h, n, rows, p, hid)), hid_hp(w, h, n, rows, p, hid)))
2831    case True{}:
2832      match ps:
2833        case (+hid, H):
2834          +hs = S.hidden_cells(rows, B.cells(w, h))
2835          +its = S.items(w, h, rows, B.cells(w, h))
2836          +shS = Equal.trans(Bool, B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)), B.shaped(T.Seen, w, h, rows), True{},
2837            start_shaped(w, h, rows), oke)
2838          +mp = hc_member(rows, B.cells(w, h), p, PS.cells_member(w, h, p, hid_on(w, h, n, rows, p, hid)), hid_hp(w, h, n, rows, p, hid))
2839          stuck_wit(w, h, n, rows, p, H,
2840            loop_none(hs, Nil{}, S.plan(w, h, S.todos(its, hs)), S.start(rows), w, h, n, rows, its, e, {==}, shS,
2841              hc_on(rows, w, h, B.cells(w, h), PS.cells_on(w, h)), p, mp))