def loop_some.found

minebender-game@1.0.0.0 · proof_solver.bend:2236

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
import minebender-game@1.0.0.0/proof_grid.bend as PG

2236def loop_some.found(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2237  +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos,
2238  r: Or({c0 == c : T.Pos} & {S.search(c0, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>},
2239    Exists(T.Grid(Bool), l => {S.search(c0, todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} &
2240      {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>})),
2241  ih: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c)) ->
2242  LoopSome(c0 <> t, todo, part, ctx, c):
2243  match r:
2244    case Inl{pr}:
2245      match pr:
2246        case (cc, sn):
2247          %cc : {Bool.or(B.same(c0, _), B.contains(t, _)) == True{} : Bool} &
2248            {S.search(_, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>}
2249          (or_l(B.same(c0, c0), B.contains(t, c0), PG.same_refl(c0)), sn)
2250    case Inr{ex}:
2251      match ex:
2252        case (l, pr):
2253          match pr:
2254            case (sl, lp):
2255              loop_some.lift(c0, t, todo, part, ctx, c, ih(l, lp))