def start_cover.cell

minebender-game@1.0.0.0 · proof_solver.bend:2130

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_grid.bend as PG
import minebender-game@1.0.0.0/proof_lists.bend as PL

2130def start_cover.cell(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +c: T.Pos, +q: T.Pos,
2131  +shP: {B.shaped(Maybe<&2, Bool>, w, h, S.start(rows)) == True{} : Bool},
2132  on: {B.on_board(w, h, q) == True{} : Bool}, +b: Bool, be: {B.same(c, q) == b : Bool}) ->
2133  {cv_f(CV{S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h)))), B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}})}, q)
2134    == True{} : Bool}:
2135  match b:
2136    case True{}:
2137      +todo = S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h))))
2138      %Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) :
2139        {Bool.or(Bool.not(S.is_none(S.look(B.set_at(Maybe<&2, Bool>, S.start(rows), _, Some{True{}}), q))), tcontains(todo, q)) == True{} : Bool}
2140      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, S.start(rows), q, Some{True{}}), q), Some{True{}},
2141        set_look(w, h, S.start(rows), q, Some{True{}}, shP, on)) :
2142        {Bool.or(Bool.not(S.is_none(_)), tcontains(todo, q)) == True{} : Bool}
2143      {==}
2144    case False{}:
2145      +todo = S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h))))
2146      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, S.start(rows), c, Some{True{}}), q), S.look(S.start(rows), q),
2147        PL.at_set_ne(Maybe<&2, Bool>, S.start(rows), c, q, Some{True{}}, None{}, be)) :
2148        {Bool.or(Bool.not(S.is_none(_)), tcontains(todo, q)) == True{} : Bool}
2149      %Equal.sym(Maybe<&2, Bool>, S.look(S.start(rows), q), S.start.cell(B.at(T.Seen, T.Hidden{}, rows, q)), start_at(rows, q)) :
2150        {Bool.or(Bool.not(S.is_none(_)), tcontains(todo, q)) == True{} : Bool}
2151      start_cover.seen(w, h, rows, its, q, on, B.at(T.Seen, T.Hidden{}, rows, q), {==})