-- Automatic generation produced by ISE Eiffel --

class interface
     GAME

create

     make (no_cards: INTEGER)
                 -- Create the columns, cells and the cards
           require
                 maximum_number_of_cards: no_cards < 53
                 minimum_number_of_cards: no_cards > 0

feature -- Access

     card_from_home_cell (cell_number: INTEGER): INTEGER
                 -- The card from home_cell cell_number
           require
                 valid_cell_less: cell_number <= number_of_cells
                 valid_cell_greater: cell_number > 0

     card_from_top_of_column (column_number: INTEGER): INTEGER
                 -- The card from top of column column_number
           require
                 valid_column_less: column_number <= number_of_columns
                 valid_column_greater: column_number > 0
                 not_empty: not (columns @ column_number).is_empty

     card_from_xcell (cell_number: INTEGER): INTEGER
                 -- The card from xcell cell_number
           require
                 valid_cell_less: cell_number <= number_of_cells
                 valid_cell_greater: cell_number > 0

     card_in_xcell (a_card: CARD; a_xcell: INTEGER): BOOLEAN
                 -- Is a_card in xcell a_xcell?

     Card_offset: INTEGER is 3
                 -- The offset of a card_number and first_card
                 -- (from GAME_CONSTANTS)

     column_empty (column_number: INTEGER): BOOLEAN
                 -- Is the column corresponding to column_number empty?
           require
                 valid_column_less: column_number <= number_of_columns
                 valid_column_greater: column_number > 0

     column_from (column_number: INTEGER): LINKED_LIST [INTEGER]
                 -- A linear representation of the column
                 -- corresponding to column_number
           require
                 valid_column_less: column_number <= number_of_columns
                 valid_column_greater: column_number > 0
           ensure
                 result_not_void: Result /= void

     Column_offset: INTEGER is 4
                 -- A column is identified in the movement by its number + 4
                 -- (from GAME_CONSTANTS)

     columns: ARRAY [COLUMN [INTEGER]]
                 -- The columns in the game

     First_card: INTEGER is 4
                 -- The first card number in the game
                 -- (from GAME_CONSTANTS)

     home_cell_empty (cell_number: INTEGER): BOOLEAN
                 -- Is the home_cell corresponding to cell_number empty?
           require
                 valid_cell_less: cell_number <= number_of_cells
                 valid_cell_greater: cell_number > 0

     Home_cell_offset: INTEGER is 12
                 -- A home_cell is identified in the movement by its number + 12
                 -- (from GAME_CONSTANTS)

     Maximum_game_number: INTEGER is 65000
                 -- Maximum game number to play
                 -- (from GAME_CONSTANTS)

     Maximum_number_of_cards: INTEGER is 52
                 -- Maximum number of cards to play with
                 -- (from GAME_CONSTANTS)

     Most_left_x_position: INTEGER is 20
                 -- Defines the space between the cards
                 -- and the left border of the window
                 -- (from GAME_CONSTANTS)

     Most_top_y_position: INTEGER is 10
                 -- Most top y_position of a card.
                 -- This position is equal to the y_position
                 -- of the home_cells and the "xcells"
                 -- (from GAME_CONSTANTS)

     Number_of_cells: INTEGER is 4
                 -- Number of cells for each kind of cell
                 -- (from GAME_CONSTANTS)

     Number_of_columns: INTEGER is 8
                 -- Number of columns present in the game
                 -- (from GAME_CONSTANTS)

     one_from_top_in_column (a_column: INTEGER): INTEGER
                 -- The card number which is one from the top
                 -- in the column corresponding to a_column
           require
                 valid_column_less: a_column <= number_of_columns
                 valid_column_greater: a_column > 0

     Space_between_cards: INTEGER is 28
                 -- Vertical space between the cards in a column
                 -- (from GAME_CONSTANTS)

     Space_between_columns: INTEGER is 80
                 -- Horizontal space between the columns including the card width
                 -- (from GAME_CONSTANTS)

     Start_of_column_y_position: INTEGER is 130
                 -- The minimal y_position of a column
                 -- (from GAME_CONSTANTS)

     state_change: INTEGER
                 -- The change which is to be made if there
                 -- is a legal_candidate

     the_cards: ARRAY [CARD]
                 -- The cards in the game

     top_of_column (a_card: CARD; a_column: INTEGER): BOOLEAN
                 -- Is a_card top of column a_column
           require
                 valid_column_less: a_column <= number_of_columns
                 valid_column_greater: a_column > 0
                 not_empty: not (columns @ a_column).is_empty

     White_offset: INTEGER is 40
                 -- White space surrounding picture at start
                 -- of the game
                 -- (from GAME_CONSTANTS)

     xcell_empty (cell_number: INTEGER): BOOLEAN
                 -- Is the xcell corresponding to cell_number empty?
           require
                 valid_cell_less: cell_number <= number_of_cells
                 valid_cell_greater: cell_number > 0

     Xcell_offset: INTEGER is 0
                 -- A xcell is identified in the movement by its number + 0
                 -- (from GAME_CONSTANTS)
     
feature -- Status report

     goal_state: BOOLEAN
                 -- Is the game in the goal_state?

     legal_candidate: BOOLEAN
                 -- Are the current settings for destination
                 -- and source legal to make a move?
     
feature -- Element change

     change_state
                 -- Changes the state
           require
                 legal_argument: state_change /= 0 and state_change < 6
                 legal_candidate: legal_candidate
           ensure
                 did_a_change: state_change = 0

     deal_game
                 -- Deal the game

     remove_top_from_column (column_number: INTEGER)
                 -- Remove the top card number from column column_number

     set_go_from (move_from: INTEGER)
                 -- Set the source of the movement to be made.
           ensure
                 go_from_is_set: go_from = move_from

     set_go_to (to: INTEGER)
                 -- Set the destination of the movement to be made.

     shuffle_the_cards (game_number: INTEGER)
                 -- Shuffle the cards in the game with game_number as seed.
           require
                 game_number_greater_than_zero: game_number > 0
     
invariant

           -- from ANY
     reflexive_equality: standard_is_equal (Current)
     reflexive_conformance: conforms_to (Current)

end -- class GAME

-- Generated by ISE Eiffel --

-- For more details: www.eiffel.com --