(in-package "ACL2")

(include-book "image")

(encapsulate 
 (((empty-scene * *) => *)
  ((place-image * * * *) => *)
  ((end-of-time *) => *))
 (local (defun empty-scene (x y) (rectangle x y 'solid 'white)))
 (local (defun place-image (img x y canvas-img)
          (overlay/xy canvas-img x y img)))
 (local (defun end-of-time (msg) 
          (declare (ignore msg))
          'final-world))
 (defthm image?-empty-scene=true
     (implies (and (posp x) (posp y))
              (image? (empty-scene x y))))

 ;; CCE: this was an iff in the other direction,
 ;; but image.lisp does not support that conclusion.
 (defthm image?-place-image=true
     (implies (and (image? img) (integerp x) (integerp y) (image? scene))
              (image? (place-image img x y scene))))

 )

(defmacro big-bang (width height frequency world0)
  ;(declare (ignore width height frequency world0))
  `(defconst *big-bang* (list ,width ,height ,frequency ,world0)))

(defmacro on-redraw (x) 
  `(defconst *on-redraw* (quote ,x)))
(defmacro on-tick-event (x)
  `(defconst *on-tick-event* (quote ,x)))
(defmacro on-key-event (x) 
  `(defconst *on-key-event* (quote ,x)))
(defmacro on-mouse-event (x)
  `(defconst *on-mouse-event* (quote ,x)))