def flood_complete_c.go

minebender-game@1.0.0.0 · proof_laws.bend:752

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/LAWS.bend as L
import minebender-game@1.0.0.0/proof_flood.bend as PF
import minebender-game@1.0.0.0/proof_inv.bend as PI

752def flood_complete_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
753  +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}, +cl: {PI.closed(w, h, layout, s) == True{} : Bool},
754  +p: T.Pos, +on: {B.on_board(w, h, p) == True{} : Bool}, +q: T.Pos, +onq: {B.on_board(w, h, q) == True{} : Bool},
755  +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
756  +c: Bool, ce: {G.unrevealed(w, h, s, p) == c : Bool}, +m: Bool, me: {B.mine(layout, p) == m : Bool}) ->
757  {L.revealed(G.knowledge(G.open.go(c, m, G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}:
758  match c m:
759    case False{} _:
760      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q), B.at(Bool, False{}, s, q),
761        know_revealed(w, h, layout, s, f, T.Playing{}, q, onq)) : {_ == True{} : Bool}
762      path_closed(path, w, h, layout, s, cl, p, q, PF.unrev_shown(w, h, s, p, ce, on), wk)
763    case True{} True{}:
764      +s2 = B.set_at(Bool, s, p, True{})
765      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s2, f, T.Lost{T.Exploded{p}}}), q), B.at(Bool, False{}, s2, q),
766        know_revealed(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, q, onq)) : {_ == True{} : Bool}
767      path_closed(path, w, h, layout, s2, PI.closed_explode(w, h, layout, s, p, me, cl), p, q,
768        PF.at_set_on(w, h, s, p, shS, on), wk)
769    case True{} False{}:
770      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
771      +cf = B.count_false(s)
772      +hh = G.head_hidden(w, h, s, start)
773      +fl = G.flood(cf, start, hh, w, h, layout, s)
774      +st = G.won_or_playing(G.all_safe(w, h, layout, fl))
775      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, fl, f, st}), q), B.at(Bool, False{}, fl, q),
776        know_revealed(w, h, layout, fl, f, st, q, onq)) : {_ == True{} : Bool}
777      path_closed(path, w, h, layout, fl, PI.closed_flood(cf, start, hh, w, h, layout, s, shS, cl, {==}, {==}), p, q,
778        PF.flood_work(cf, start, hh, w, h, layout, s, shS, {==}, {==}, p, on, start_has(p)), wk)