def solve_safe.go

minebender-game@1.0.0.0 · proof_solver.bend:2780

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

2780def solve_safe.go(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +c: T.Pos, +ok: Bool,
2781  oke: {B.shaped(T.Seen, w, h, rows) == ok : Bool},
2782  e: {S.solve.go(ok, S.hidden_cells(rows, B.cells(w, h)), w, h, n, rows) == Some{c} : Maybe<&2, T.Pos>}) ->
2783  L.ProvablySafe(T.Knowledge{w, h, n, rows}, c):
2784  match ok:
2785    case False{}:
2786      +hs = S.hidden_cells(rows, B.cells(w, h))
2787      safe_hidden(w, h, n, rows, c, hc_sound(rows, B.cells(w, h), c, head_some(hs, c, e)),
2788        layout => cons => safe_none(w, h, n, rows, oke, c, layout, cons))
2789    case True{}:
2790      +hs = S.hidden_cells(rows, B.cells(w, h))
2791      +its = S.items(w, h, rows, B.cells(w, h))
2792      ls = loop_some(hs, Nil{}, S.plan(w, h, S.todos(its, hs)), S.start(rows), S.Ctx{w, h, n, rows, its}, c, e)
2793      solve_safe.k(w, h, n, rows, c, oke, ls)