def first_safe.go2

minebender-game@1.0.0.0 · proof_assist.bend:52

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/game.bend as G
import minebender-game@1.0.0.0/proof_grid.bend as PG
import minebender-game@1.0.0.0/proof_solver.bend as PV

52def first_safe.go2(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>, +hit: Bool,
53  he: {Bool.and(Bool.not(B.mine(layout, q)), Bool.not(B.at(Bool, False{}, shown, q))) == hit : Bool},
54  e: {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) == False{} : Bool},
55  ih: {G.all_safe.go(layout, shown, t) == False{} : Bool} -> SafeAt(layout, shown, t)) ->
56  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
57    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
58     {B.contains(q <> t, p) == True{} : Bool})):
59  match hit:
60    case True{}:
61      (q, ({==}, (he, PV.or_l(B.same(q, q), B.contains(t, q), PG.same_refl(q)))))
62    case False{}:
63      first_safe.lift(layout, shown, q, t,
64        ih(%not_and_false(B.mine(layout, q), B.at(Bool, False{}, shown, q), he) :
65            {Bool.and(_, G.all_safe.go(layout, shown, t)) == False{} : Bool}; e),
66        False{}, {==})