// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  Sokoban (倉庫番, Japanese for "warehouse keeper") is a transport
//  puzzle in which the player pushes boxes around a maze, viewed
//  from above, and tries to put them in designated locations. Only
//  one box may be pushed at a time, not two, and boxes cannot be
//  pulled.
//
//  Sokoban was created in 1980 by Hiroyuki Imabayashi, and was
//  published in 1982 by Thinking Rabbit, a software house based in
//  Takarazuka, Japan.
//
//  It is known that Sokoban is PSPACE-complete. For references see
//  many resources in the web like http://en.wikipedia.org/wiki/Sokoban.
//
//  To use this Quartz description, you have to define static
//  constants "rows" and "cols" before including this file,
//  a further module "InitialField" to initialize the
//  field, and a specification "SokobanSpec" that defines the
//  fields where the boxes should be finally moved to.
//
// **************************************************************************

package Sokoban;

macro cols = 8;
macro rows = 8;

// objects that may occupy a field
macro EMPTY = 0b00;
macro WALL = 0b11;
macro BOX = 0b01;
macro ROBOT = 0b10;

// move instructions to the robot
macro UP = 0b00;
macro DOWN = 0b01;
macro LEFT = 0b10;
macro RIGHT = 0b11;

module Play(
    bv{2} ?mv,
    [cols][rows]bv{2} f,
    nat{cols} robot_x,
    nat{rows} robot_y
) {
    // InitialField(f);
    loop {
        case
            (mv==UP) do {
                if(robot_y<=rows-3 & f[robot_x][robot_y+1]==BOX & f[robot_x][robot_y+2]==EMPTY()) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x][robot_y+1]) = ROBOT;
                    next(f[robot_x][robot_y+2]) = BOX;
                    next(robot_y) = robot_y+1;
                }
                if(robot_y<=rows-2 & f[robot_x][robot_y+1]==EMPTY) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x][robot_y+1]) = ROBOT;
                    next(robot_y) = robot_y+1;
                }
            }
            (mv==DOWN) do {
                if(robot_y>=2 & f[robot_x][robot_y-1]==BOX & f[robot_x][robot_y-2]==EMPTY) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x][robot_y-1]) = ROBOT;
                    next(f[robot_x][robot_y-2]) = BOX;
                    next(robot_y) = robot_y-1;
                }
                if(robot_y>=1 & f[robot_x][robot_y-1]==EMPTY) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x][robot_y-1]) = ROBOT;
                    next(robot_y) = robot_y-1;
                }
            }
            (mv==LEFT) do {
                if(robot_x>=2 & f[robot_x-1][robot_y]==BOX & f[robot_x-2][robot_y]==EMPTY) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x-1][robot_y]) = ROBOT;
                    next(f[robot_x-2][robot_y]) = BOX;
                    next(robot_x) = robot_x-1;
                }
                if(robot_x>=1 & f[robot_x-1][robot_y]==EMPTY) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x-1][robot_y]) = ROBOT;
                    next(robot_x) = robot_x-1;
                }
            }
            (mv==RIGHT) do {
                if(robot_x<=cols-3 & f[robot_x+1][robot_y]==BOX & f[robot_x+2][robot_y]==EMPTY()) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x+1][robot_y]) = ROBOT;
                    next(f[robot_x+2][robot_y]) = BOX;
                    next(robot_x) = robot_x+1;
                }
                if(robot_x<=cols-2 & f[robot_x+1][robot_y]==EMPTY) {
                    next(f[robot_x][robot_y]) = EMPTY;
                    next(f[robot_x+1][robot_y]) = ROBOT;
                    next(robot_x) = robot_x+1;
                }
            }
            default nothing;
        pause;
    }
}