def open_mine.k

minebender-game@1.0.0.0 · proof_laws.bend:859

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_copy.bend as PC
import minebender-game@1.0.0.0/proof_inv.bend as PI

859def open_mine.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
860  shape: {L.shaped(Bool, w, h, layout) == True{} : Bool},
861  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, boom: {L.mine(layout, p) == True{} : Bool},
862  c: Canon(w, h, layout, g)) ->
863  {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
864  {L.seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}:
865  match c:
866    case (eg, facts):
867      match facts:
868        case (sh, f2):
869          match f2:
870            case (won, f3):
871              match f3:
872                case (cm, cl):
873                  +s = shown_of(g)
874                  +f = flags_of(g)
875                  %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
876                    {G.status(G.open(_, p)) == T.Lost{T.Exploded{p}} : T.Status} &
877                    {L.seen(G.knowledge(G.open(_, p)), p) == T.Boom{} : T.Seen}
878                  %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
879                    {G.status(G.open(G.Game{w, h, layout, s, f, _}, p)) == T.Lost{T.Exploded{p}} : T.Status} &
880                    {L.seen(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), p) == T.Boom{} : T.Seen}
881                  open_mine_c(w, h, layout, s, f,
882                    %Equal.sym(Bool, B.shaped(Bool, w, h, layout), L.shaped(Bool, w, h, layout), PC.shaped_eq(Bool, w, h, layout)) :
883                      {_ == True{} : Bool}; shape,
884                    sh,
885                    %playing : {PI.calm(_, w, h, layout, s) == True{} : Bool}; cm,
886                    p,
887                    %Equal.sym(Bool, B.mine(layout, p), L.mine(layout, p), PC.mine_eq(layout, p)) :
888                      {_ == True{} : Bool}; boom)