module grid (BIT) is

-------------------------------------------------------------------------------
-- Definition of the puzzle grid (rectangle of MxN cells), with an initial
-- subset of cells free denoting the form of the puzzle grid (the initially
-- occupied cells are considered to be absent from the grid).
-- A cell has initially the value W (resp. Z) if it is free (resp. occupied).

type Grid_Line is
    array [1 ... 7] of Piece_Name
end type

type Grid_Array is
    array [1 ... 7] of Grid_Line
end type

-- M, N are the number of lines and columns of the grid
-- (use according to the array type definitions above)

type Grid is
    Grid (M, N:Nat, A:Grid_Array)
    with get, set
end type

-- Initial configuration of the grid

function Initial_Grid : Grid is
    return
	Grid (7, 7,
	    Grid_Array (
		Grid_Line (W, W, W, W, W, W, Z),
		Grid_Line (W, W, W, W, W, W, Z),
		Grid_Line (W, W, W, W, W, W, W),
		Grid_Line (W, W, W, W, W, W, W),
		Grid_Line (W, W, W, W, W, W, W),
		Grid_Line (W, W, W, W, W, W, W),
		Grid_Line (W, W, W, Z, Z, Z, Z)
	    )
	)
end function

-- Line and column of the cell denoting a month number

function Get_Month_Coordinates (MONTH:Nat, out Line, Coln:Nat) is
    assert (MONTH >= 1) and (MONTH <= 12);

    case MONTH in
	  1 -> Line := 1; Coln := 1
    |	  2 -> Line := 1; Coln := 2
    |	  3 -> Line := 1; Coln := 3
    |	  4 -> Line := 1; Coln := 4
    |	  5 -> Line := 1; Coln := 5
    |	  6 -> Line := 1; Coln := 6
    |	  7 -> Line := 2; Coln := 1
    |	  8 -> Line := 2; Coln := 2
    |	  9 -> Line := 2; Coln := 3
    |	 10 -> Line := 2; Coln := 4
    |	 11 -> Line := 2; Coln := 5
    |	 12 -> Line := 2; Coln := 6
    |	any -> Line := 0; Coln := 0 -- case never reached
    end case
end function

-- Line and column of the cell denoting a day number

function Get_Day_Coordinates (Day:Nat, out Line, Coln:Nat) is
    assert (Day >= 1) and (Day <= 31);

    case Day in
	  1 -> Line := 3; Coln := 1
    |	  2 -> Line := 3; Coln := 2
    |	  3 -> Line := 3; Coln := 3
    |	  4 -> Line := 3; Coln := 4
    |	  5 -> Line := 3; Coln := 5
    |	  6 -> Line := 3; Coln := 6
    |	  7 -> Line := 3; Coln := 7
    |	  8 -> Line := 4; Coln := 1
    |	  9 -> Line := 4; Coln := 2
    |	 10 -> Line := 4; Coln := 3
    |	 11 -> Line := 4; Coln := 4
    |	 12 -> Line := 4; Coln := 5
    |	 13 -> Line := 4; Coln := 6
    |	 14 -> Line := 4; Coln := 7
    |	 15 -> Line := 5; Coln := 1
    |	 16 -> Line := 5; Coln := 2
    |	 17 -> Line := 5; Coln := 3
    |	 18 -> Line := 5; Coln := 4
    |	 19 -> Line := 5; Coln := 5
    |	 20 -> Line := 5; Coln := 6
    |	 21 -> Line := 5; Coln := 7
    |	 22 -> Line := 6; Coln := 1
    |	 23 -> Line := 6; Coln := 2
    |	 24 -> Line := 6; Coln := 3
    |	 25 -> Line := 6; Coln := 4
    |	 26 -> Line := 6; Coln := 5
    |	 27 -> Line := 6; Coln := 6
    |	 28 -> Line := 6; Coln := 7
    |	 29 -> Line := 7; Coln := 1
    |	 30 -> Line := 7; Coln := 2
    |	 31 -> Line := 7; Coln := 3
    |	any -> Line := 0; Coln := 0 -- case never reached
    end case
end function

-------------------------------------------------------------------------------
-- Definition of the pieces of the puzzle (rectangles of cells), with the
-- occupied cells denoting the form of the piece.
-- Note: each side of the rectangle must be touched by an occupied cell
-- of the piece.
-- Each piece has a list of possible configurations (turns and flip,
-- if relevant) that will be tested when attempting to fit the piece
-- into the free area of the puzzle grid.
-- A cell has value 1 (resp. 0) if it is present in (resp. absent from)
-- the piece.

-- Piece identifiers

type Piece_Name is
    A, B, C, D, E, F, G, H, -- names of the puzzle pieces
    W,  -- free cell
    X,  -- month cell occupied
    Y,  -- day cell occupied
    Z   -- cell initially occupied
    with ==, !=
end type

type Bit_List is
    list of Bit
    with !=, ==, head, tail
end type

type Config is
    Config (M, N:Nat, A:Bit_List)
    with ==, !=, get
end type

type Config_Array_2 is
    array [1 ... 2] of Config
    with ==, !=
end type

type Config_Array_4 is
    array [1 ... 4] of Config
    with ==, !=
end type

type Config_Array_8 is
    array [1 ... 8] of Config
    with ==, !=
end type

type Piece is
    Piece_2 (P:Piece_Name, Q:Nat, C2:Config_Array_2),
    Piece_4 (P:Piece_Name, Q:Nat, C4:Config_Array_4),
    Piece_8 (P:Piece_Name, Q:Nat, C8:Config_Array_8)
    with ==, !=, get
end type

type Piece_List is
    list of Piece
    with ==, !=, head, tail
end type

-- Piece A --------------------------------------------------------------------

function Piece_A : Piece is
    return 
	Piece_2 (A, 2,
	    Config_Array_2 (
		Config (2, 3, {
		    1, 1, 1,
		    1, 1, 1
		}),
		Config (3, 2, {
		    1, 1,
		    1, 1,
		    1, 1
		})
	    )
	)
end function

-- Piece B --------------------------------------------------------------------

function Piece_B : Piece is
    return 
	Piece_4 (B, 4,
	    Config_Array_4 (
		Config (2, 3, {
		    1, 0, 1,
		    1, 1, 1
		}),
		Config (3, 2, {
		    1, 1,
		    1, 0,
		    1, 1
		}),
		Config (2, 3, {
		    1, 1, 1,
		    1, 0, 1
		}),
		Config (3, 2, {
		    1, 1,
		    0, 1,
		    1, 1
		})
	    )
	)
end function

-- Piece C --------------------------------------------------------------------

function Piece_C : Piece is
    return 
	Piece_8 (C, 8,
	    Config_Array_8 (
		Config (2, 4, {
		    0, 0, 1, 0,
		    1, 1, 1, 1
		}),
		Config (4, 2, {
		    1, 0,
		    1, 0,
		    1, 1,
		    1, 0
		}),
		Config (2, 4, {
		    1, 1, 1, 1,
		    0, 1, 0, 0
		}),
		Config (4, 2, {
		    0, 1,
		    1, 1,
		    0, 1,
		    0, 1
		}),
		Config (2, 4, {
		    0, 1, 0, 0,
		    1, 1, 1, 1
		}),
		Config (4, 2, {
		    1, 0,
		    1, 1,
		    1, 0,
		    1, 0
		}),
		Config (2, 4, {
		    1, 1, 1, 1,
		    0, 0, 1, 0
		}),
		Config (4, 2, {
		    0, 1,
		    0, 1,
		    1, 1,
		    0, 1
		})
	    )
	)
end function

-- Piece D --------------------------------------------------------------------

function Piece_D : Piece is
    return 
	Piece_4 (D, 4,
	    Config_Array_4 (
		Config (3, 3, {
		    1, 1, 0,
		    0, 1, 0,
		    0, 1, 1
		}),
		Config (3, 3, {
		    0, 0, 1,
		    1, 1, 1,
		    1, 0, 0
		}),
		Config (3, 3, {
		    0, 1, 1,
		    0, 1, 0,
		    1, 1, 0
		}),
		Config (3, 3, {
		    1, 0, 0,
		    1, 1, 1,
		    0, 0, 1
		})
	    )
	)
end function

-- Piece E --------------------------------------------------------------------

function Piece_E : Piece is
    return 
	Piece_8 (E, 8,
	    Config_Array_8 (
		Config (2, 4, {
		    1, 1, 1, 0,
		    0, 0, 1, 1
		}),
		Config (4, 2, {
		    0, 1,
		    0, 1,
		    1, 1,
		    1, 0
		}),
		Config (2, 4, {
		    1, 1, 0, 0,
		    0, 1, 1, 1
		}),
		Config (4, 2, {
		    0, 1,
		    1, 1,
		    1, 0,
		    1, 0
		}),
		Config (2, 4, {
		    0, 0, 1, 1,
		    1, 1, 1, 0
		}),
		Config (4, 2, {
		    1, 0,
		    1, 0,
		    1, 1,
		    0, 1
		}),
		Config (2, 4, {
		    0, 1, 1, 1,
		    1, 1, 0, 0
		}),
		Config (4, 2, {
		    1, 0,
		    1, 1,
		    0, 1,
		    0, 1
		})
	    )
	)
end function

-- Piece F --------------------------------------------------------------------

function Piece_F : Piece is
    return 
	Piece_8 (F, 8,
	    Config_Array_8 (
		Config (2, 4, {
		    1, 1, 1, 1,
		    0, 0, 0, 1
		}),
		Config (4, 2, {
		    0, 1,
		    0, 1,
		    0, 1,
		    1, 1
		}),
		Config (2, 4, {
		    1, 0, 0, 0,
		    1, 1, 1, 1
		}),
		Config (4, 2, {
		    1, 1,
		    1, 0,
		    1, 0,
		    1, 0
		}),
		Config (2, 4, {
		    0, 0, 0, 1,
		    1, 1, 1, 1
		}),
		Config (4, 2, {
		    1, 0,
		    1, 0,
		    1, 0,
		    1, 1
		}),
		Config (2, 4, {
		    1, 1, 1, 1,
		    1, 0, 0, 0
		}),
		Config (4, 2, {
		    1, 1,
		    0, 1,
		    0, 1,
		    0, 1
		})
	    )
	)
end function

-- Piece G --------------------------------------------------------------------

function Piece_G : Piece is
    return 
	Piece_4 (G, 4,
	    Config_Array_4 (
		Config (3, 3, {
		    1, 0, 0,
		    1, 0, 0,
		    1, 1, 1
		}),
		Config (3, 3, {
		    1, 1, 1,
		    1, 0, 0,
		    1, 0, 0
		}),
		Config (3, 3, {
		    1, 1, 1,
		    0, 0, 1,
		    0, 0, 1
		}),
		Config (3, 3, {
		    0, 0, 1,
		    0, 0, 1,
		    1, 1, 1
		})
	    )
	)
end function

-- Piece H --------------------------------------------------------------------

function Piece_H : Piece is
    return 
	Piece_8 (H, 8,
	    Config_Array_8 (
		Config (2, 3, {
		    1, 1, 0,
		    1, 1, 1
		}),
		Config (3, 2, {
		    1, 1,
		    1, 1,
		    1, 0
		}),
		Config (2, 3, {
		    1, 1, 1,
		    0, 1, 1
		}),
		Config (3, 2, {
		    0, 1,
		    1, 1,
		    1, 1
		}),
		Config (2, 3, {
		    0, 1, 1,
		    1, 1, 1
		}),
		Config (3, 2, {
		    1, 0,
		    1, 1,
		    1, 1
		}),
		Config (2, 3, {
		    1, 1, 1,
		    1, 1, 0
		}),
		Config (3, 2, {
		    1, 1,
		    1, 1,
		    0, 1
		})
	    )
	)
end function

-- Selection of the configuration of index J of piece P

function Get_Config (P:Piece, J:Nat) : Config is
    var C2:Config_Array_2,
	C4:Config_Array_4,
	C8:Config_Array_8
    in
	case P in
	    Piece_2 (any Piece_Name, any Nat, C2) -> return C2[J]
	|   Piece_4 (any Piece_Name, any Nat, C4) -> return C4[J]
	|   Piece_8 (any Piece_Name, any Nat, C8) -> return C8[J]
	end case
    end var
end function

-- List of all puzzle pieces, ordered to facilitate the exploration of grid
-- configurations: first the 6-cell piece, then the other 5-cell pieces

function Puzzle_Pieces : Piece_List is
    return {
	Piece_A,
	Piece_B,
	Piece_C,
	Piece_D,
	Piece_E,
	Piece_F,
	Piece_G,
	Piece_H
    }
end function

-------------------------------------------------------------------------------
-- Check if a piece configuration C can be placed in the grid G starting at
-- the cell at Line and Coln

function Check_Placement (G:Grid, C:Config, Line, Coln:Nat) : Bool is
    var
	Line_C, Coln_C:Nat,
	BL:Bit_List,
	Fits:Bool
    in
	Line_C := 1;
	Coln_C := 1;

	if (Line + C.M - 1 > G.M) or (Coln + C.N - 1 > G.N) then
	    -- The configuration goes outside the grid:
	    -- no placement possible
	    Fits := false
	else
	    -- Scan the bits of the piece configuration from left to right
	    -- (i.e., the cells of the piece configuration rectangle from
	    -- left to right and top to bottom) and check whether the occupied
	    -- cells of the piece configuration can be placed in some free
	    -- cells of the grid

	    Fits := true;

	    for BL := C.A while BL != nil by BL := tail (BL) loop L in
		if (head (BL) == 0) or (G.A [Line + Line_C - 1][Coln + Coln_C - 1] == W) then
		    -- Current cell of the piece configuration (if occupied)
		    -- fits in the grid: move to the next cell in the piece
		    -- configuration rectangle

		    if (Coln_C mod C.N) == 0 then
			-- Move to the first cell of the next line

			Line_C := Line_C + 1;
			Coln_C := 1
		    else
			-- Move to the next cell in the same line

			Coln_C := Coln_C + 1
		    end if
		else
		    -- Current cell of the piece does not fit in the grid:
		    -- no placement possible

		    Fits := false;
		    break L
		end if
	    end loop
	end if;

	return Fits
    end var
end function

-------------------------------------------------------------------------------
-- Update the grid by placing (the configuration of) a piece

function Update_Grid (in var G:Grid, P:Piece_Name, Line, Coln:Nat,
	C:Config) : Grid
is
    var
	Line_C, Coln_C:Nat,
	BL:Bit_List,
	G_Line:Grid_Line,
	G_Array:Grid_Array
    in
	Line_C := 1;
	Coln_C := 1;

	for BL := C.A while BL != nil by BL := tail (BL) loop
	    if head (BL) == 1 then
		-- Update the grid with the current cell of the piece

		-- G.A[Line + Line_C - 1][Coln + Coln_C - 1] := P
		G_Line := G.A [Line + Line_C - 1];
		G_Line [Coln + Coln_C - 1] := P;
		G_Array := G.A;
		G_Array [Line + Line_C - 1] := G_Line;
		G := G.{A -> G_Array}
	    end if;

	    -- Move to the next cell in the piece configuration rectangle

	    if (Coln_C mod C.N) == 0 then
		-- Move to the first cell of the next line

		Line_C := Line_C + 1;
		Coln_C := 1
	    else
		-- Move to the next cell in the same line

		Coln_C := Coln_C + 1
	    end if
	end loop;

	return G
    end var
end function

-------------------------------------------------------------------------------
-- Check whether a grid is valid for continuing the placement of pieces
-- (i.e., all the free regions on the grid have a size multiple of 5)

type Cell is
    !implementedby "C:CELL"
    Cell (I, J: Nat)
	!implementedby "C:MAKE_CELL"
    with get
	!implementedby "C:GET_%s_CELL"
end type

type Cell_List is
    !implementedby "C:CELL_LIST"
    cons (C:Cell, L:Cell_List)
	!implementedby "C:CONS_CELL_LIST"
    ,
    nil
	!implementedby "C:NIL_CELL_LIST"
    with get
	!implementedby "C:GET_%s_CELL_LIST"
end type

-- List of free cells in a grid

function Free_Cells (G:Grid) : Cell_List is
    var L:Cell_List, I, J:Nat in
	L := nil;

	for I := 1 while I <= 7 by I := I + 1 loop
	    for J := 1 while J <= 7 by J := J + 1 loop
		if G.A[I][J] == W then
		   L := cons (Cell (I, J), L) 
		end if
	    end loop
	end loop;

	return L
    end var
end function

function Valid_Grid (L:Cell_List) : Bool is
    !implementedby "VALID_GRID"
    !external
end function

function Get_Current_Month () : Nat is
    !implementedby "GET_CURRENT_MONTH"
    !external
end function

function Get_Current_Day () : Nat is
    !implementedby "GET_CURRENT_DAY"
    !external
end function

end module