def loop_none.found

minebender-game@1.0.0.0 · proof_solver.bend:2316

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

2316def loop_none.found(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2317  +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>,
2318  +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool},
2319  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, on0: {B.on_board(w, h, c0) == True{} : Bool},
2320  +c: T.Pos, mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2321  ex: Exists(T.Grid(Bool), l => {S.search(c0, todo, part, S.Ctx{w, h, n, rows, its}) == Some{l} : Maybe<&2, T.Grid(Bool)>} &
2322    {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>}),
2323  ih: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
2324    {all_valid(S.Ctx{w, h, n, rows, its}, l <> found) == True{} : Bool} -> {B.contains(t, c) == True{} : Bool} ->
2325    Witness(S.Ctx{w, h, n, rows, its}, c)) ->
2326  Witness(S.Ctx{w, h, n, rows, its}, c):
2327  match ex:
2328    case (+l, pr):
2329      match pr:
2330        case (+sl, ln):
2331          +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2332          +p1 = B.set_at(Maybe<&2, Bool>, part, c0, Some{True{}})
2333          +vl = dfs2_some_check(S.plan_todo(c0, todo, ctx), p1, S.part_true(p1), S.part_none(p1), ctx, l, sl)
2334          +ml = dfs2_some_keep(S.plan_todo(c0, todo, ctx), p1, S.part_true(p1), S.part_none(p1), ctx, l, sl, c0, True{},
2335            set_look(w, h, part, c0, Some{True{}}, shP, on0))
2336          loop_none.pick(ctx, c0, t, c, l, vl, ml, mr,
2337            mt => ih(l, ln, %Equal.sym(Bool, S.check(ctx, l), True{}, vl) : {Bool.and(_, all_valid(ctx, found)) == True{} : Bool}; val, mt))