% aknakereso -- dp big homework
% specification: "http://dp.iit.bme.hu/dp-current/dp06a-nhf.html"
% Zsbán Ambrus <ambrus@math.bme.hu>


% In order to understand this code, please observe the following
% conventions used.
% 
% The predicates I define follow a rigid structure.  All predicates
% have an output parameter, which is always the last parameter of
% the predicate.  This parameter must always be a variable when you
% call the predicate.  All other parameters of the predicate are
% input parameters.  All predicates succeed exactly once when called
% -- or throw an exception.  The values expected as input parameters
% and output in the output parameters are typically ground terms,
% but there is an exception covered in the next paragraph.  Naturally,
% the predicates required in the specification of the task are exempt
% from these conventions.
% 
% The head `fun' is for anonymous function objects.  Such a function
% object has the outline `fun(In_1, ..., In_n, Out, Body)', where
% Body is a callable term that, when evaluated, unifies the output
% parameter Out with the result of the function call.  To use such a
% function object, you unify the input parameters `In_1, ..., In_n'
% with the respective arguments of the function call, then call Body
% as a goal, then `Out' will be the output of the call.  You must,
% however, make a renamed copy (with `copy_term') of the function
% object before each call, both because of the input and output
% variables, and the bound variables in body.  The function objects
% use similar conventions to the named predicates: eg. when called,
% they succeed exactly once (or throw an exception).
% 
% The atom `rec' is used as the head of various (non-polymorphic)
% structure types that were not notable enough for an individual name.
% The functors `some/1' and `none/0' were used for anonymous polymorph
% types the same way.


% list_pump(+Lst, +Til, +N, -List_pump):
% Attempts to remove N elements from the head of Lst and
% prepend them in reverse order to Til.  On success, List_pump is
% list_pump_done(L, T) where L is the N-th tail of Lst, and
% T is the list Til with the N dropped elements prepended to it.
% If N is greater than the length of Lst, List_pump is list_pump_end(K,
% T) where K is N minus the length of Lst, and T is Til with all
% elements of Lst prepended to it.
list_pump(Lst, Til, N, List_pump) :- 
    N =< 0, !, List_pump = list_pump_done(Lst, Til).
list_pump(Lst, Til, N, List_pump) :- 
    ([A| D] = Lst -> 
    Diff is N - 1, list_pump(D, [A| Til], Diff, List_pump); 
    X = Lst, List_pump = list_pump_end(N, Til)).

% A tape represents a list of values which can be seeked to any
% position and is faster to access near that position.
% 
% Implementation: $tape(N, A, B) represents a tape whose first
% N elements are in the list B in reverse order and the elements
% starting from N are in the list A in forward order.  The current
% element of the tape is the first element of A.

% tape_make(+Lst, -Tape_make):
% Tape_make is a newly created tape with elements from a list Lst.
tape_make(Lst, Tape_make) :- 
    Tape_make = tape(0, Lst, []).

% tape_seek(+Tap, +N, -Tape_seek):
% Seek the tape Tap to (zero-based) position N
% Tape_seek is the new seeked tape, invalidating the old tape.
tape_seek(Tap, N, Tape_seek) :- 
    tape(Pos, Ahead, Back) = Tap, (N < Pos -> 
    Diff is Pos - N, list_pump(Back, Ahead, Diff, List_pump), 
    (list_pump_done(B, A) = List_pump -> 
    Tape_seek = tape(N, A, B); 
    list_pump_end(K, A1) = List_pump, 
    Tape_seek = tape(0, A1, [])); 
    Diff1 is N - Pos, list_pump(Ahead, Back, Diff1, List_pump1), 
    (list_pump_done(A2, B1) = List_pump1 -> 
    Tape_seek = tape(N, A2, B1); 
    list_pump_end(K1, B2) = List_pump1, Diff2 is N - K1, 
    Tape_seek = tape(Diff2, [], B2))).

% tape_ref(+Tap, +N, -Tape_ref):
% Retreives an element from index N of tape Tap.
% 
% Tape_ref is a pair rec(E, T).  E is some of the element at
% (zero-based) index N from tape Tap.  If N is less that zero or
% greater-equal to the size of Tap, E is none (N must still be
% an integer).  T is the new tape (seeked to n).  The old tape is
% invalidated (that is, you must not use it in any way).
tape_ref(Tap, N, Tape_ref) :- 
    tape_seek(Tap, N, Tape_seek), T = Tape_seek, 
    (tape(K, [A0| A1], B) = T -> 
    (N =:= K -> Cond = some(A0); Cond = none), 
    Tape_ref = rec(Cond, T); 
    E = T, Tape_ref = rec(none, T)).

% tape_amend(+Tap, +N, +Elt, -Tape_amend):
% Change the element at (zero-based) index N in tape Tap to Elt.
% N must be a valid index.  Tape_amend is the new tape.  Invalidates
% the old tape (as the operation might either be implemented with a
% destructive mutation of the tape or by copying the neccessary parts
% of the tape).
tape_amend(Tap, N, Elt, Tape_amend) :- 
    tape_seek(Tap, N, Tape_seek), 
    (tape(K, [A0| A1], B) = Tape_seek -> 
    (N =:= K -> Tape_amend = tape(K, [Elt| A1], B); 
    abort, Tape_amend = rec); 
    E = Tape_seek, abort, Tape_amend = rec).

% tapetape_ref(+Ttap, +M, +N, -Tapetape_ref):
% Retrieves an element from index M:N of tape of tapes Ttap.
% 
% Returns the pair rec(E, TT).  Here, if the element of index
% M of Ttap has an element X at index N, then E is some(X).
% If it doesn't, or Ttap doesn't have an element of index M,
% then E is none.  Regargless, TT is the updated tape of tapes.
% The original tape and its member tapes are invalidated.
tapetape_ref(Ttap, M, N, Tapetape_ref) :- 
    tape_ref(Ttap, M, Tape_ref), 
    (rec(some(T1), Tt1) = Tape_ref -> 
    tape_ref(T1, N, Tape_ref1), rec(X, T2) = Tape_ref1, 
    tape_amend(Tt1, M, T2, Tape_amend), 
    Tapetape_ref = rec(X, Tape_amend); 
    rec(E, Tt1_1) = Tape_ref, Tapetape_ref = rec(none, Tt1_1)).

% tapetape_amend(+Ttap, +M, +N, +Elt, -Tapetape_amend):
% Change the element at index N:M in tape of tapes Ttap.  M must
% be a valid index of Ttap, and N must be a valid index of element
% M of Ttap.  Tapetape_amend is the new tape.  The old tape and its 
% members are invalidated.
tapetape_amend(Ttap, M, N, Elt, Tapetape_amend) :- 
    tape_ref(Ttap, M, Tape_ref), 
    (rec(some(T1), Tt1) = Tape_ref -> 
    tape_amend(T1, N, Elt, Tape_amend), T2 = Tape_amend, 
    tape_amend(Tt1, M, T2, Tapetape_amend); 
    E = Tape_ref, abort, Tapetape_amend = rec).

% tapetape_clone(+Ttap, -Tapetape_clone):
% Returns a record of two copies of the tape of tapes Ttap.
% The two copies can be used and modified independently, as well as
% their subtapes.  The original tape, however, is invalidated.
tapetape_clone(Ttap, Tapetape_clone) :- 
    Tapetape_clone = rec(Ttap, Ttap).

% A square on the board is represented by a $field(M, N) structure.
% Here, M is one of $yesmine, $unmine, or $nomine meaning that the
% field is marked as a sure mine, its state is unknown, or is marked
% as a safe non-mine field.  N is either $nofieldnum if there's no
% number on the field, or $fieldnum(Danger, Safety) if, out of the
% eight neigbours of the field, Danger + Safety are currently marked
% as $unmine, and Danger of these should be marked as $yesmine and
% Safety of these $nomine, only we don't yet know which ones.

% We represent a partially solved minesweeper field by a structure
% $board($rec(Height, Width), Queen, Tapetape).  Here, Height and
% Width is the number of rows and columns of the board resp, Queen is
% a $fieldnum showing the number the mines and nonmines to be found
% yet, and Tapetape is a tape of tape of squares.

% initboard_emptyrow(+W, +T, -Initboard_emptyrow):
% Initboard_emptyrow is a list of W empty fields, prepended to 
% the list T.
initboard_emptyrow(W, T, Initboard_emptyrow) :- 
    0 =:= W, !, Initboard_emptyrow = T.
initboard_emptyrow(W, T, Initboard_emptyrow) :- 
    Diff is W - 1, initboard_emptyrow(
    Diff, [field(unmine, nofieldnum)| T], Initboard_emptyrow).

% initboard_empty(+H, +W, +T, -Initboard_empty):
% Initboard_empty is a list of H rows (tapes) of W empty fields, 
% prepended to the list T.
initboard_empty(H, W, T, Initboard_empty) :- 
    0 =:= H, !, Initboard_empty = T.
initboard_empty(H, W, T, Initboard_empty) :- 
    Diff is H - 1, initboard_emptyrow(W, [], Initboard_emptyrow), 
    tape_make(Initboard_emptyrow, Tape_make), 
    initboard_empty(Diff, W, [Tape_make| T], Initboard_empty).

% neighbours_fold(+R, +C, +Func, +Init, -Neighbours_fold):
% Calls the function object func for each of the eight neighbouring
% cells of cell R:C.
% 
% The function is called with three input parameters: the first one
% starts with Init and is folded through the calls (the return value
% of the previous call of Func is used as the first parameter in
% the next call).  The second and third one are the row and column
% coordinates of the neighbour cell.  The function is called eight
% times: once for each of the eight neigbours of the cell of row
% R and column C.  The order of the neighbours is undetermined.
% The functions are called even for cells that are out of the
% boundaries of the board.  Neighbours_fold is the folded value.
neighbours_fold(R, C, Func, Init, Neighbours_fold) :- 
    Diff is R - 1, Sum is R + 1, Diff1 is C - 1, Sum1 is C + 1, 
    Ru = Diff, Ro = Sum, Cu = Diff1, Co = Sum1, 
    copy_term(Func, fun(Init, Ru, Cu, Call, Body)), 
    Body, 
    copy_term(Func, fun(Call, Ru, C, Call1, Body1)), 
    Body1, 
    copy_term(Func, fun(Call1, Ru, Co, Call2, Body2)), 
    Body2, 
    copy_term(Func, fun(Call2, R, Cu, Call3, Body3)), 
    Body3, 
    copy_term(Func, fun(Call3, R, Co, Call4, Body4)), 
    Body4, 
    copy_term(Func, fun(Call4, Ro, Cu, Call5, Body5)), 
    Body5, 
    copy_term(Func, fun(Call5, Ro, C, Call6, Body6)), 
    Body6, 
    copy_term(Func, fun(Call6, Ro, Co, Neighbours_fold, Body7)), 
    Body7.

% count_unmines_around(+Ttap, +R, +C, -Count_unmines_around):
% Count_unmines_around is a tuple of the number of neighbours of 
% the cell R:C in table of tables Ttap which are not marked as 
% either mine or non-mine.
count_unmines_around(Ttap, R, C, Count_unmines_around) :- 
    neighbours_fold(R, C, fun(M, Rr, Cc, Case1, 
    (rec(K, Tt0) = M, tapetape_ref(Tt0, Rr, Cc, Tapetape_ref), 
    rec(Ofd, Tt1) = Tapetape_ref, 
    (some(field(unmine, E)) = Ofd -> Case = 1; 
    E1 = Ofd, Case = 0), 
    Sum is K + Case, 
    Case1 = rec(Sum, Tt1))), 
    rec(0, Ttap), 
    Count_unmines_around).

% paradox(-R):
% Signals a paradox state of the board, that is, that there is no
% solution to the current problem.  Never returns.
paradox(R) :-
	throw(lightning_bolt).

% whatif(+Thunk, -Ret)
% Calls the function object Thunk with no input arguments
% hypothetically.  If no paradox results from the hypothesis, Ret is
% some(Val) where Val is the output of the function call.  If the
% hypothesis is proven to be contradictory (and signals this with
% the paradox function), Ret is none.
whatif(Thunk, Ret) :-
	copy_term(Thunk, fun(Val, Body)), 
	catch((Body, Ret = some(Val)), lightning_bolt, Ret = none).

% list_length(+Lst, -List_length):
% List_length is the length of the list Lst.
list_length(Lst, List_length) :- 
    [A| D] = Lst, !, list_length(D, List_length1), 
    List_length is 1 + List_length1.
list_length(Lst, List_length) :- 
    E = Lst, List_length = 0.

% mark_safe(+Ttap, +R, +C, -Mark_safe):
% Marks the field R:C of a board as non-mine.
% 
% Ttap is the tape of tapes of squares.  It is modified in two ways:
% firstly the fieldmine part of the square R:C is changed to nomine
% from unmine, secondly in all neighbouring cells which (are inside
% the board and) have a fieldnum part, the safety count in the
% fieldnum is decreased by one.  If the safety count would have to
% be decreased below zero, paradox is called.  It is an error if
% the field R:C lies outside the board or if its fieldmine part
% contains nomine or yesmine.  Mark_safe is the new tape of tapes,
% invalidating the old one.
mark_safe(Ttap, R, C, Mark_safe) :- 
    tapetape_ref(Ttap, R, C, Tapetape_ref), 
    (rec(some(field(unmine, N)), Ttap1) = Tapetape_ref -> 
    tapetape_amend(
    Ttap1, R, C, field(nomine, N), Tapetape_amend), 
    neighbours_fold(R, C, fun(Tt0, Rr, Cc, Let, 
    (tapetape_ref(Tt0, Rr, Cc, Tapetape_ref1), 
    (rec(some(field(M, fieldnum(Cd, Cs))), Tt1) = Tapetape_ref1
     -> 
    (Cs < 1 -> paradox(Let); Diff is Cs - 1, tapetape_amend(
    Tt1, Rr, Cc, field(M, fieldnum(Cd, Diff)), Let)); 
    rec(E, Tt1_1) = Tapetape_ref1, Let = Tt1_1))), 
    Tapetape_amend, 
    Mark_safe); 
    rec(E1, Ttap1_1) = Tapetape_ref, abort, Mark_safe = rec).

% mark_dangerous(+Ttap, +R, +C, -Mark_dangerous):
% Marks the field R:C of a board as a mine.
% 
% Ttap is the tape of tapes of squares.  It is modified in two
% ways: firstly the fieldmine part of the square R:C is changed
% to yesmine from unmine, secondly in all neighbouring cells which
% (are inside the board and) have a fieldnum part, the danger count
% in the fieldnum is decreased by one.  If the danger count would
% have to be decreased below zero, a paradox is signalled.  It is an
% error if the field R:C lies outside the board or if its fieldmine
% part contains nomine or yesmine.  Mark_dangerous is the new tape 
% of tapes, invalidating the old one.
mark_dangerous(Ttap, R, C, Mark_dangerous) :- 
    tapetape_ref(Ttap, R, C, Tapetape_ref), 
    (rec(some(field(unmine, N)), Ttap1) = Tapetape_ref -> 
    tapetape_amend(
    Ttap1, R, C, field(yesmine, N), Tapetape_amend), 
    neighbours_fold(R, C, fun(Tt0, Rr, Cc, Let, 
    (tapetape_ref(Tt0, Rr, Cc, Tapetape_ref1), 
    (rec(some(field(M, fieldnum(Cd, Cs))), Tt1) = Tapetape_ref1
     -> 
    (Cd < 1 -> paradox(Let); Diff is Cd - 1, tapetape_amend(
    Tt1, Rr, Cc, field(M, fieldnum(Diff, Cs)), Let)); 
    rec(E, Tt1_1) = Tapetape_ref1, Let = Tt1_1))), 
    Tapetape_amend, 
    Mark_dangerous); 
    rec(E1, Ttap1_1) = Tapetape_ref, abort, Mark_dangerous = rec).

% initboard_fill(+Ttap, +Lst, -Initboard_fill):
% Fills the tape_of_tapes part of a board with the numbered cells
% from the original problem.  Ttap is the empty or partially filled
% tape of tapes, Lst is a list of p(R, C, M) values,
% where R and C give the row and column (these are converted from
% one-based to zero-based), and M is the number of mines around.
initboard_fill(Ttap, Lst, Initboard_fill) :- 
    [p(R1, C1, M)| D] = Lst, !, Diff is R1 - 1, Diff1 is C1 - 1, 
    R = Diff, C = Diff1, 
    count_unmines_around(Ttap, R, C, Count_unmines_around), 
    rec(U, Ttap1) = Count_unmines_around, 
    Diff2 is U - M, 
    tapetape_amend(
    Ttap1, R, C, field(unmine, fieldnum(M, Diff2)), 
    Tapetape_amend), 
    mark_safe(Tapetape_amend, R, C, Let), 
    initboard_fill(Let, D, Initboard_fill).
initboard_fill(Ttap, Lst, Initboard_fill) :- 
    E = Lst, Initboard_fill = Ttap.

% initboard(+Aknain, -Initboard):
% Converts the problem Aknain to the board format from the format
% in the specification.  Initboard is the board.
initboard(Aknain, Initboard) :- 
    a(-(Height, Width), Totalmines, Lst) = Aknain, 
    list_length(Lst, List_length), 
    Diff is (Height * Width) - (List_length + Totalmines), 
    initboard_empty(Height, Width, [], Initboard_empty), 
    tape_make(Initboard_empty, Tape_make), 
    initboard_fill(Tape_make, Lst, Initboard_fill), 
    Initboard = 
    board(rec(Height, Width), fieldnum(Totalmines, Diff), 
    Initboard_fill).

% rectangle_fold_row(
%     +Height, +Width, +Func, +Init, -Rectangle_fold_row
% ):
% A helper function for rectangle_fold.  Folds a function through
% a single row.
rectangle_fold_row(
    Height, Width, Func, Init, Rectangle_fold_row
    ) :- 
    0 < Width, !, Diff is Width - 1, Diff1 is Width - 1, 
    copy_term(Func, fun(Init, Height, Diff1, Call, Body)), 
    Body, 
    rectangle_fold_row(
    Height, Diff, Func, Call, Rectangle_fold_row).
rectangle_fold_row(
    Height, Width, Func, Init, Rectangle_fold_row
    ) :- 
    Rectangle_fold_row = Init.

% rectangle_fold(+Height, +Width, +Func, +Init, -Rectangle_fold):
% Iterates on every coordinate in a rectangle of size Height
% times Width.
% 
% The function object Func is called repeatedly with three input
% arguments.  The second and third arguments are the coordinates, these
% take every pair of integers R:C in the range (0 <= R < Height),
% (0 <= C < Width) exactly once, in undetermined order.  The first
% argument is the folded accumulator variable: it starts from init
% and is replaced with the output of the call of Func every time.
% Rectangle_fold is the fold value.
rectangle_fold(Height, Width, Func, Init, Rectangle_fold) :- 
    0 < Height, !, Diff is Height - 1, Diff1 is Height - 1, 
    rectangle_fold_row(
    Diff1, Width, Func, Init, Rectangle_fold_row), 
    rectangle_fold(
    Diff, Width, Func, Rectangle_fold_row, Rectangle_fold).
rectangle_fold(Height, Width, Func, Init, Rectangle_fold) :- 
    Rectangle_fold = Init.

% board_mark_safe_1(
%     +Dims, +Qfnum, +Ttap, +R, +C, -Board_mark_safe_1
% ):
% Helper for board_mark_safe, called when the square was unmarked.
board_mark_safe_1(Dims, Qfnum, Ttap, R, C, Board_mark_safe_1) :- 
    fieldnum(Qdanger, Qsafety) = Qfnum, !, 
    (Qsafety < 1 -> paradox(Board_mark_safe_1); 
    Diff is Qsafety - 1, mark_safe(Ttap, R, C, Mark_safe), 
    Board_mark_safe_1 = 
    board(Dims, fieldnum(Qdanger, Diff), Mark_safe)).
board_mark_safe_1(Dims, Qfnum, Ttap, R, C, Board_mark_safe_1) :- 
    E = Qfnum, abort, Board_mark_safe_1 = rec.

% board_mark_safe(+Brd, +R, +C, -Board_mark_safe):
% Checks if the square R:C has an unknown fieldmine state.  If it
% does, marks the square as safe (a sure non-mine).  This involves
% changing the fieldmine part to nomine, decreasing the safety
% count of any neigbouring squares marked with a fieldnum, and
% decreasing the global safety count reigning the whole board.
% If any safe counts would be decreased below zero, signals paradox.
% If the square R:C is already known to be a mine or non-mine or
% is outside the board, nothing is changed.  Board_mark_safe is 
% the new board, invalidating the old one.
board_mark_safe(Brd, R, C, Board_mark_safe) :- 
    board(Dims, Qfnum, Ttap) = Brd, 
    tapetape_ref(Ttap, R, C, Tapetape_ref), 
    (rec(some(field(unmine, Fnum)), Ttap1) = Tapetape_ref -> 
    board_mark_safe_1(Dims, Qfnum, Ttap1, R, C, Board_mark_safe); 
    rec(E, Ttap1_1) = Tapetape_ref, 
    Board_mark_safe = board(Dims, Qfnum, Ttap1_1)).

% board_mark_dangerous_1(
%     +Dims, +Qfnum, +Ttap, +R, +C, -Board_mark_dangerous_1
% ):
% Helper for board_mark_dangerous, called when the square was unmarked.
board_mark_dangerous_1(
    Dims, Qfnum, Ttap, R, C, Board_mark_dangerous_1
    ) :- 
    fieldnum(Qdanger, Qsafety) = Qfnum, !, 
    (Qdanger < 1 -> paradox(Board_mark_dangerous_1); 
    Diff is Qdanger - 1, 
    mark_dangerous(Ttap, R, C, Mark_dangerous), 
    Board_mark_dangerous_1 = 
    board(Dims, fieldnum(Diff, Qsafety), Mark_dangerous)).
board_mark_dangerous_1(
    Dims, Qfnum, Ttap, R, C, Board_mark_dangerous_1
    ) :- 
    E = Qfnum, abort, Board_mark_dangerous_1 = rec.

% board_mark_dangerous(+Brd, +R, +C, -Board_mark_dangerous):
% Checks if the square R:C has an unknown fieldmine state.  If it
% does, marks the square as dangerous (a sure mine).  This involves
% changing the fieldmine part to yesmine, decreasing the safety
% count of any neigbouring squares marked with a fieldnum, and
% decreasing the global safety count reigning the whole board.
% If any safe counts would be decreased below zero, signals paradox.
% If the square R:C is already known to be a mine or non-mine or
% is outside the board, nothing is changed.  Board_mark_dangerous is 
% the new board, invalidating the old one.
board_mark_dangerous(Brd, R, C, Board_mark_dangerous) :- 
    board(Dims, Qfnum, Ttap) = Brd, 
    tapetape_ref(Ttap, R, C, Tapetape_ref), 
    (rec(some(field(unmine, Fnum)), Ttap1) = Tapetape_ref -> 
    board_mark_dangerous_1(
    Dims, Qfnum, Ttap1, R, C, Board_mark_dangerous); 
    rec(E, Ttap1_1) = Tapetape_ref, 
    Board_mark_dangerous = board(Dims, Qfnum, Ttap1_1)).

% rule_square(+Brd, +R, +C, -Rule_square):
% Tries to do the local transformations on the board Brd at the
% square R:C. Rule_square is the new board, invalidating the old one.
% 
% Specifically, this function does the following transformation:
% if the danger value of R:C is zero, then all unmarked squares
% around it are marked as safe, and the fieldnum is removed from the
% R:C square as it would always be fieldnum(0, 0) which doesn't
% give any information.
rule_square(Brd, R, C, Rule_square) :- 
    board(Dims, Queen, Ttap) = Brd, 
    tapetape_ref(Ttap, R, C, Tapetape_ref), 
    (rec(some(field(Mtp, fieldnum(Danger, Safety))), Ttap1) = 
    Tapetape_ref -> (Danger =< 0 -> 
    (Danger < 0 -> abort, Rule_square = rec; tapetape_amend(
    Ttap1, R, C, field(Mtp, nofieldnum), Tapetape_amend), 
    neighbours_fold(R, C, fun(Bd, Rr, Cc, Board_mark_safe, 
    (board_mark_safe(Bd, Rr, Cc, Board_mark_safe))), 
    board(Dims, Queen, Tapetape_amend), 
    Rule_square)); 
    Safety =< 0 -> 
    (Safety < 0 -> abort, Rule_square = rec; tapetape_amend(
    Ttap1, R, C, field(Mtp, nofieldnum), Tapetape_amend1), 
    neighbours_fold(
    R, C, fun(Bd1, Rr1, Cc1, Board_mark_dangerous, 
    (board_mark_dangerous(Bd1, Rr1, Cc1, Board_mark_dangerous))), 
    board(Dims, Queen, Tapetape_amend1), 
    Rule_square)); 
    Rule_square = board(Dims, Queen, Ttap1)); 
    rec(E, Ttap1_1) = Tapetape_ref, 
    Rule_square = board(Dims, Queen, Ttap1_1)).

% localrule_step(+Brd, -Localrule_step):
% Does one step of the local transformations on the board Brd to 
% fill some squares.  Localrule_step is the new board, invalidating 
% the old one.
localrule_step(Brd, Localrule_step) :- 
    board(rec(Height, Width), Queen, Ttbl) = Brd, 
    rectangle_fold(Height, Width, 
    fun(Bd, R, C, Rule_square, (rule_square(Bd, R, C, Rule_square))), 
    Brd, 
    Localrule_step).

% localrule_iterate(+Brd, -Localrule_iterate):
% Repeatedly does local transformations on the board trying to 
% fill more and more squares until no more can be done that way.
localrule_iterate(Brd, Localrule_iterate) :- 
    board(Dims0, Queen0, Ttbl0) = Brd, 
    localrule_step(Brd, Localrule_step), 
    Brd1 = Localrule_step, 
    board(Dims1, Queen1, Ttbl1) = Brd1, 
    (Queen0 == Queen1 -> Localrule_iterate = Brd1; 
    localrule_iterate(Brd1, Localrule_iterate)).

% list_union(+Lst, +Til, -List_union):
% Returns a list containing the elements of the two lists Lst and Til,
% in an undetermined order.
list_union(Lst, Til, List_union) :- 
    [A| D] = Lst, !, list_union(D, [A| Til], List_union).
list_union(Lst, Til, List_union) :- 
    E = Lst, List_union = Til.

% list_of_nonnomines(+Brd, -List_of_nonnomines):
% List_of_nonnomines is the list of coordinates of fields not marked as 
% non-mines. Destroys the board.  The coordinates are converted to 
% one-based.
list_of_nonnomines(Brd, List_of_nonnomines) :- 
    board(rec(Height, Width), Queen, Ttbl) = Brd, 
    rectangle_fold(Height, Width, fun(M, R, C, Case, 
    (rec(Ls, Tt) = M, tapetape_ref(Tt, R, C, Tapetape_ref), 
    (rec(some(field(yesmine, Fnum)), Tt1) = Tapetape_ref -> 
    Sum is R + 1, Sum1 is C + 1, 
    Case = rec([-(Sum, Sum1)| Ls], Tt1); 
    rec(some(field(unmine, Fnum1)), Tt1_1) = Tapetape_ref -> 
    Sum2 is R + 1, Sum3 is C + 1, 
    Case = rec([-(Sum2, Sum3)| Ls], Tt1_1); 
    rec(E, Tt1_2) = Tapetape_ref, Case = rec(Ls, Tt1_2)))), 
    rec([], Ttbl), 
    Rectangle_fold), 
    rec(Ls1, Ttbl1) = Rectangle_fold, 
    List_of_nonnomines = Ls1.

% list_of_yesmines(+Brd, -List_of_yesmines):
% List_of_yesmines is the list of coordinates of fields marked as mines.
% Destroys the board.  The coordinates are converted to one-based.
list_of_yesmines(Brd, List_of_yesmines) :- 
    board(rec(Height, Width), Queen, Ttbl) = Brd, 
    rectangle_fold(Height, Width, fun(M, R, C, Case, 
    (rec(Ls, Tt) = M, tapetape_ref(Tt, R, C, Tapetape_ref), 
    (rec(some(field(yesmine, Fnum)), Tt1) = Tapetape_ref -> 
    Sum is R + 1, Sum1 is C + 1, 
    Case = rec([-(Sum, Sum1)| Ls], Tt1); 
    rec(E, Tt1_1) = Tapetape_ref, Case = rec(Ls, Tt1_1)))), 
    rec([], Ttbl), 
    Rectangle_fold), 
    rec(Ls1, Ttbl1) = Rectangle_fold, 
    List_of_yesmines = Ls1.

% extract_solution(+Brd, -Extract_solution):
% Checks whether we have filled out enough fileds on the board Brd
% that give a unique solution.  This can happen in two dual ways:
% either we've marked as many fields as mines as there are on the
% board (recall that the number of mines is given) or we've marked as
% many fields as non-mines that all the unmarked fields must be mines.
% If we've found a unique solution, Extract_solution is 
% unique_solution(L) where L is the solution in the format described
% in the specification, that is, a list of one-based coordinate
% pairs of mines -(Row, Col).  Otherwise Extract_solution is
% no_unique_solution(Board) where Board is the input board.
extract_solution(Brd, Extract_solution) :- 
    board(Dim, fieldnum(Danger, Safety), Ttbl) = Brd, !, 
    (Safety =< 0 -> 
    (Safety < 0 -> abort, Extract_solution = rec; 
    list_of_nonnomines(Brd, List_of_nonnomines), 
    Extract_solution = unique_solution(List_of_nonnomines)); 
    Danger =< 0 -> 
    (Danger < 0 -> abort, Extract_solution = rec; 
    list_of_yesmines(Brd, List_of_yesmines), 
    Extract_solution = unique_solution(List_of_yesmines)); 
    Extract_solution = no_unique_solution(Brd)).
extract_solution(Brd, Extract_solution) :- 
    E = Brd, abort, Extract_solution = rec.

% tense_field(+Brd, -Tense_field):
% Chooses a field from a board Brd by which the problem should be
% split to subproblems.  Tense_field is rec(Row, Col, B) where Row:Col
% is the coordinate of the field (which is always an unmarked field)
% and B is the new board.
tense_field(Brd, Tense_field) :- 
    board(rec(Height, Width), Queen, Ttbl) = Brd, 
    rectangle_fold(Height, Width, fun(M, R, C, Case, 
    (rec(Br, Bc, Tt) = M, tapetape_ref(Tt, R, C, Tapetape_ref), 
    (rec(some(field(unmine, Fnum)), Tt1) = Tapetape_ref -> 
    Case = rec(R, C, Tt1); 
    rec(E, Tt1_1) = Tapetape_ref, Case = rec(Br, Bc, Tt1_1)))), 
    rec(-1, 0, Ttbl), 
    Rectangle_fold), 
    rec(Tr, Tc, Ttbl1) = Rectangle_fold, 
    Tense_field = 
    rec(Tr, Tc, board(rec(Height, Width), Queen, Ttbl)).

% split(+Brd, -Split):
% Splits the problem to two subproblems by choosing an unmarked
% field and marking it as a non-mine in one subproblem and a mine in
% the other one.
% 
% Brd is a board representing the problem.  Split is rec(Brd_a,
% Brd_b) where Brd_a and Brd_b are the two boards representing the
% subproblems.
split(Brd, Split) :- 
    tense_field(Brd, Tense_field), rec(R, C, Brd1) = Tense_field, 
    board(Dims, Queen, Ttbl) = Brd1, 
    tapetape_clone(Ttbl, Tapetape_clone), 
    rec(Ttbl_a, Ttbl_b) = Tapetape_clone, 
    board_mark_dangerous(
    board(Dims, Queen, Ttbl_a), R, C, Board_mark_dangerous), 
    board_mark_safe(
    board(Dims, Queen, Ttbl_b), R, C, Board_mark_safe), 
    Split = rec(Board_mark_dangerous, Board_mark_safe).

% solve(+Brd, -Solve):
% Solve is the list of solutions for a problem Brd already in
% board form.  This is probably the single most important function
% in the program.
% 
% We do this by first applying local transformations to fill in the
% board as much as we can.  Then, three cases are possible.
% 
% 1.  We can prove that the problem has no solution.  (We signal this
% during the local transformations with an exception).  In this case,
% we return an empty list.
% 
% 2.  We find as much mines as there are or find as much non-mine
% fields that all other fields must be non-mines.  (We check for this
% only after the local transformations.)  In this case, we take the
% list of functions and return it.
% 
% 3. Neither of the above two happens.  In this case, we split
% the problem to two subproblems by finding a suitable field and
% marking it either a mine or a non-mine, solve both subproblems,
% and concatenate the two lists of solutions.
solve(Brd, Solve) :- 
    whatif(fun(Localrule_iterate, 
    (localrule_iterate(Brd, Localrule_iterate))), Whatif), 
    (some(Brd1) = Whatif -> 
    extract_solution(Brd1, Extract_solution), 
    (unique_solution(Sol) = Extract_solution -> Solve = [Sol]; 
    no_unique_solution(Brd2) = Extract_solution, 
    split(Brd2, Split), rec(Brd_a, Brd_b) = Split, 
    solve(Brd_a, Solve1), 
    solve(Brd_b, Solve2), 
    list_union(Solve1, Solve2, Solve)); 
    none = Whatif, Solve = []).

% aknakereso_list(+Aknain, -Aknakereso_list):
% Aknakereso_list is the list of solutions for the problem Aknain.
aknakereso_list(Aknain, Aknakereso_list) :- 
    initboard(Aknain, Initboard), 
    solve(Initboard, Aknakereso_list).

% my_member(?E, +L):
% Succeeds once for each member of the list L unifying E with the 
% member. 
my_member(R, [A| D]) :- R = A.
my_member(R, [A| D]) :- my_member(R, D).

% aknakereso(+Aknain, -Sol):
% Succeeds once for each solution of the aknakereso problem Aknain,
% unifying Sol with the solution.
aknakereso(Aknain, Sol) :- 
	aknakereso_list(Aknain, L), my_member(Sol, L).

