def flood_fact.go

minebender-game@1.0.0.0 · proof_inv.bend:72

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_flood.bend as PF

72# The flood's one-cell closure fact: a revealed zero's neighbour is revealed.
73def flood_fact.go(+n: Nat, +work: List<&2, G.Work>, +hd: Bool, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
74  +shown: T.Grid(Bool), +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
75  +cl: {closed(w, h, layout, shown) == True{} : Bool}, +cnt: {n == B.count_false(shown) : Nat},
76  +he: {G.head_hidden(w, h, shown, work) == hd : Bool}, +q: T.Pos, on: {B.on_board(w, h, q) == True{} : Bool},
77  after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool},
78  +z: {B.zero(w, h, layout, q) == True{} : Bool}, +r: T.Pos,
79  +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool},
80  +s: Bool, se: {B.at(Bool, False{}, shown, q) == s : Bool}) ->
81  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), r) == True{} : Bool}:
82  match s:
83    case True{}:
84      PF.flood_mono(n, work, hd, w, h, layout, shown, r, closed_use(w, h, layout, shown, cl, q, on, se, z, r, rm))
85    case False{}:
86      PF.flood_zero(n, work, hd, w, h, layout, shown, sh, cnt, he, q, se, after, z, r, rm)