(include-book "data-structures/structures" :dir :system)
(include-book "world" :dir :teachpacks)

(defconst *width* 400)
(defconst *height* 800)
(defconst *brick-dim* 20) ;; dimension of one brick

;; Block = (block Nat Nat)
;; For now, blocks are just a single brick.  No interesting shapes.
(defstructure brick x y)
(defun brick? (b)
  (and (brick-p b) (natp (brick-x b)) (natp (brick-y b))))

;; Block -> Block
;; Make the block fall a little bit.
(defun drop-brick-one-dim (b)
  (brick (brick-x b) (+ (brick-y b) *brick-dim*)))

;; World = (tetris-world Brick)
(defstructure tetris-world falling-brick)

;; World -> Boolean
;; Make sure w contains a brick.
(defun tetris-world? (w)
  (and (tetris-world-p w)
       (brick? (tetris-world-falling-brick w))))

;; -> Image
;; Produce the blank background.
(defun tetris-bg () (empty-scene *width* *height*))

;; Block Image -> Image
;; Draw the given block into scene.
(defun render-brick (b scene)
  (place-image (rectangle *brick-dim* *brick-dim* 'solid 'blue)
               (brick-x b) (brick-y b)
               scene))

;; World -> Image
;; Draw it.
(defun render-world (w)
  (render-brick (tetris-world-falling-brick w)
                (tetris-bg)))

;; World -> World
;; Drop the falling block by one quantum.
(defun tick (w)
  (tetris-world (drop-brick-one-dim (tetris-world-falling-brick w))))

#|  SPECIFICATIONS  |#
(defun brick-in-bounds? (b)
  (and (brick? b)
       (<= (brick-x b) *width*)
       (<= (brick-y b) *height*)))

(defun world-good? (w)
  (and (tetris-world? w)
       (brick-in-bounds? (tetris-world-falling-brick w))))

(defthm tick-preserves-world-good
  (implies (world-good? w)
           (world-good? (tick w))))

;; The initial world has a block in the top-middle.
(defconst *world0* (tetris-world (brick (/ *width* 2) 0)))
;; Run it:
(big-bang *width* *height* 1/5 *world0*)
(on-tick-event tick)
(on-redraw render-world)