def dfs_some_check.node

minebender-game@1.0.0.0 · proof_solver.bend:1138

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

1138def dfs_some_check.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
1139  +ctx: S.Ctx, +l: T.Grid(Bool), +fr: Bool,
1140  e: {S.dfs.free(fr, u => S.dfs(rest, part, ctx),
1141      v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
1142        x => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx)),
1143      y => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)),
1144        z => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1145  kp: {S.dfs(rest, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {S.check(ctx, l) == True{} : Bool},
1146  k0: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1147    {S.check(ctx, l) == True{} : Bool},
1148  k1: {S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1149    {S.check(ctx, l) == True{} : Bool}) -> {S.check(ctx, l) == True{} : Bool}:
1150  match fr:
1151    case False{}:
1152      kp(e)
1153    case True{}:
1154      dfs_some_check.br(l, ctx, S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx),
1155        S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx),
1156        dfs_branch_some(S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel, S.ctx_n(ctx)),
1157          S.open_ok(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel, S.ctx_n(ctx)),
1158          S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), ctx),
1159          S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), ctx), l, e), k0, k1)