#|
January 31 2006:  Decided to suspend formalization of images.
It's not on the critical path, and we can still reason about video games
via world-next and world-change.  The original code is toward the end
of this file.
|#

;; We'll just inform ACL2 that the image functions exist
;; but that we know nothing about them.

(in-package "ACL2")
(include-book "data-structures/structures" :dir :system)

;; Don't export bytep, but enable the prover to rewrite it away in
;; case it gets introduced by the theorems below.
(defun bytep (x) (integer-range-p 0 256 x)) ;; 0 <= x < 256
(defthm bytep-x=>0<=x<256
  (equal (bytep X) (integer-range-p 0 256 X)))
(in-theory (disable bytep))

(defstructure make-posn
   (x (:assert (integerp x)))
   (y (:assert (integerp y)))
   (:options (:keyword-constructor nil)
             (:keyword-updater nil)
             (:conc-name posn-)
             (:weak-predicate weak-posn?)
             (:predicate posn?)))

(encapsulate (((mode? *) => *)
              
              ((color? *) => *)
              ((image-color? *) => *)
              ((make-color * * *) => *)
              ((color-red *) => *)
              ((color-green *) => *)
              ((color-blue *) => *)
              
              ((image? *) => *)
              ((circle * * *) => *)
              ((rectangle * * * *) => *)
              ((triangle * * *) => *)
              ((line * * *) => *)
              ((add-line * * * * * *) => *)
              ((text * * *) => *)
              ((overlay * *) => *)
              ((overlay/xy * * * *) => *)
              
              ((image-width *) => *)
              ((image-height *) => *)
              
              ((pinhole-x *) => *)
              ((pinhole-y *) => *)
              ((move-pinhole * * *) => *)
              ((put-pinhole * * *) => *)
              
              ((image-inside? * *) => *)
              ((find-image * *) => *)
              
              ((image->color-list *) => *)
              ((color-list->image * * * * *) => *))
 (local (defun mode? (x) 
          (and (symbolp x)
               (or (eq x 'solid) (eq x 'outline)))))
 
 (local (defun color? (x) (eq (car x) 'color)))
 (local (defun image-color? (x) (or (symbolp x) (color? x))))
 (local (defun make-color (r g b) (list 'color r g b)))
 (local (defun color-red (c) (declare (ignore c)) 0))
 (local (defun color-green (c) (declare (ignore c)) 0))
 (local (defun color-blue (c) (declare (ignore c)) 0))
 

 ;; Image witnesses
 (local (defun image? (x) 
          (case-match x
	    (('circle r m c) (and (posp r) (mode? m) (image-color? c)))
	    (('rectangle w h m c)
	     (and (posp w) (posp h) (mode? m) (image-color? c)))
	    (('triangle lng m c)
	     (and (posp lng) (mode? m) (image-color? c)))
	    (('overlay im1 im2)
	     (and (image? im1) (image? im2)))
	    (('overlay/xy im1 x y im2)
	     (and (image? im1) (image? im2)
		  (integerp x) (integerp y)))
	    (('place-image im x y scene)
	     (and (image? im) (image? scene)
		  (integerp x) (integerp y)))
	    (('line x y c)
	     (and (integerp x) (integerp y) (image-color? c)))
	    (('add-line im x0 y0 x1 y1 c)
	     (and (image? im) (image-color? c) 
		  (integerp x0) (integerp y0)
		  (integerp x1) (integerp y1)))
	    (('text str sz c)
	     (and (stringp str) (posp sz) (image-color? c)))
	    )
	    
	    
	  ;(and (member-eq (car x) 
          ;                '(circle rectangle triangle overlay overlay/xy
          ;                         line add-line text color-list-image))
          ;     t)
	  ))
 (local (defun circle (radius mode color) 
          (list 'circle radius mode color)))
 (local (defun rectangle (width height mode color) 
          (list 'rectangle width height mode color)))
 (local (defun triangle (side-length mode color)
          (list 'triangle side-length mode color)))
 (local (defun overlay (image-1 image-2) (list 'overlay image-1 image-2)))
 (local (defun overlay/xy (tgt-img x y src-img)
          (list 'overlay/xy tgt-img x y src-img)))
 (local (defun place-image (img x y scene)
          (list 'place-image img x y scene)))
 (local (defun line (x y color)
          (list 'line x y color)))
 (local (defun add-line (img x0 y0 x1 y1 color)
          (list 'add-line img x0 y0 x1 y1 color)))
 (local (defun text (str size color)
          (list 'text str size color)))
 
 (local (defun image-width (x) (1+ (nfix x))))
 (local (defun image-height (x) (1+ (nfix x))))
 
 (local (defun pinhole-x (i) (nfix i)))
 (local (defun pinhole-y (i) (nfix i)))
 
 (local (defun move-pinhole (i x y) (declare (ignore x y)) i))
 (local (defun put-pinhole (i x y) (declare (ignore x y)) i))
 
 (local (defun image-inside? (i1 i2) (equal i1 i2)))
 (local (defun find-image (i1 i2)
          (declare (ignore i1 i2))
          (make-posn 0 0)))
 
 (local (defun image->color-list (img)
          (list img)))
 (local (defun color-list->image (lo-color width height x y)
          (list 'color-list-image lo-color width height x y)))
 
 ;; Drawing mode spec
 (defthm mode?<=>outline-or-solid
   (iff (mode? x) (or (eq x 'solid) (eq x 'outline))))
 
 ;; Color specification
 (defthm color?@any->bool (booleanp (color? X)))
 (defthm image-color?@any->bool (booleanp (image-color? X)))
 (defthm image-color?-defn
     (iff (image-color? x) (or (symbolp x) (color? x))))
 (defthm color?=>image-color?
   (implies (color? C) (image-color? C)))
 (defthm make-color@byte*byte*byte->color?
   (implies (and (bytep r) (bytep g) (bytep b))
            (color? (make-color r g b))))
 (defthm color-red@color?->byte
   (implies (color? c) (bytep (color-red c))))
 (defthm color-green@color?->byte
   (implies (color? c) (bytep (color-green c))))
 (defthm color-blue@color?->byte
   (implies (color? c) (bytep (color-blue c))))
 
 ;; Image spec
 (defthm image?@any->bool (booleanp (image? X)))
 ;(defthm image?-circle=true
 ;  (implies (and (posp radius) (mode? mode) (image-color? color))
 ;           (image? (circle radius mode color))))
 (defthm image?-circle
     (iff (image? (circle radius mode color))
          (and (posp radius) (mode? mode) (image-color? color))))
 (defthm image?-rectangle=true
   (implies (and (posp width) (posp height) (mode? mode) (image-color? color))
            (image? (rectangle width height mode color))))
 (defthm image?-triangle=true
   (implies (and (posp size) (mode? mode) (image-color? color))
            (image? (triangle size mode color))))
 (defthm image?-overlay=true
   (implies (and (image? I) (image? J)) (image? (overlay I J))))
 (defthm image?-overlay/xy=true
   (implies (and (image? src) (image? tgt) (integerp x) (integerp y))
            (image? (overlay/xy tgt x y src))))
 
 
 (defthm image-width@image?->posp
   (implies (image? I) (posp (image-width I))))
 (defthm image-height@image?->posp
   (implies (image? I) (posp (image-height I))))
 
 (defthm pinhole-x@image?->natp
   (implies (image? I) (natp (pinhole-x I))))
 (defthm pinhole-y@image?->natp
   (implies (image? I) (natp (pinhole-y I))))
 
 (defthm move-pinhole@image?*integerp*integerp->image?
   (implies (and (image? I) (integerp X) (integerp Y))
            (image? (move-pinhole I X Y))))
 (defthm put-pinhole@imag?*natp*natp->image?
   (implies (and (image? I) (natp X) (natp Y))
            (image? (put-pinhole I X Y))))
 
 (defthm image-inside?@image?*image?->bool
   (implies (and (image? I) (image? J)) (booleanp (image-inside? I J))))
 
 (defthm find-image@image?*image?->posn?
   (implies (and (image? I) (image? J)) (posn? (find-image I J))))
 )

#| January 31 2006 code for representing images in ACL2
(include-book "data-structures/structures" :dir :system)
(include-book "data-structures/list-theory" :dir :system)

;; Need arithmetic-3 to admit draw-line/0<=slope<=1.
(include-book "arithmetic-3/bind-free/top" :dir :system)
(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp 
                                              hist pspv)))
;; (floor width 2) & (floor height 2) are used 
;; to find the center of an image
(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)

(defun bytep (x)
  (integer-range-p 0 256 x))

(defstructure color 
  (red (:assert (bytep red)))
  (green (:assert (bytep green)))
  (blue (:assert (bytep blue))))
(defun color? (x) (color-p x))

(deflist color-listp (l) color-p)

(defstructure image 
  (width (:assert (posp width)))
  (height (:assert (posp height)))
  (pinhole-x (:assert (integer-range-p 0 (1+ width) pinhole-x)))
  (pinhole-y (:assert (integer-range-p 0 (1+ height) pinhole-y)))
  (pixels (:assert (and (color-listp pixels)
                        (= (len pixels) (* width height))))))
(defun image? (x) (image-p x))
(defun image-size (i)
  (len (image-pixels i)))

(defun pinhole-x (img)
  (image-pinhole-x img))

(defun pinhole-y (img)
  (image-pinhole-y img))

(defun solid? (m)
  (or (equal m 'solid) (string-equal m "solid")))

(defun outline? (m)
  (or (equal m 'outline) (string-equal m "outline")))

(defun mode? (m)
  (or (solid? m) (outline? m)))

(defun rectangle (width height mode color)
  (and (posp width) (posp height) (mode? mode) (color? color)
       (cond
         ((solid? mode)
          (image width height 
                 0 0
                 (make-list (* width height) :initial-element color)))
         ;; FIX ME:  outline =/= solid
         ((outline? mode)
          (image width height 
                 0 0
                 (make-list (* width height) :initial-element color))))))


(defthm rectangle-type
  (implies (and (posp width) (posp height) (mode? mode) (color? color))
           (image? (rectangle width height mode color))))

(defthm rectangle-size
  (implies (and (posp width) (posp height) (mode? mode) (color? color))
           (equal (image-size (rectangle width height mode color)) 
		  (* width height))))

(defun in-circle-at-origin? (col row radius)
  (let ((x (- (- col radius) 1/2))
	(y (- (- row radius) 1/2)))
    (<= (+ (* x x) (* y y)) (* radius radius))))

(defconst *white* (color 255 255 255))

(defun circle-scan-line (col row radius color)
  (if (zp col) 
      nil
      (cons (if (in-circle-at-origin? col row radius) 
                color 
                *white*)
            (circle-scan-line (1- col) row radius color))))

(defun circle-scan-lines (col row radius color)
  (if (zp row)
      nil
      (append (circle-scan-line col row radius color)
              (circle-scan-lines col (1- row) radius color))))

(defun circle (radius mode color)
  (let ((diameter (+ radius radius)))
    (cond
      ((solid? mode)
       (image diameter diameter
              radius radius
              (let ((bottom-half (circle-scan-lines diameter radius radius color)))
                (append (reverse bottom-half) bottom-half))))
      ((outline? mode)
       (image diameter diameter
              radius radius
              (let ((bottom-half (circle-scan-lines diameter radius radius color)))
                (append (reverse bottom-half) bottom-half)))))))

(defun update-pixel (x y width pixels new-color)
  (update-nth (+ (* y width) x) new-color pixels))

;; Draw a line with slope between 0 and 1.
(defun draw-line/0<slope<=1 (count x y dx dy eps color pixels width)
  (if (zp count)
      pixels
      (let ((pixels (update-pixel x y width pixels color))
            (eps (+ eps dy))
            (x (1+ x)))
        (mv-let (y eps)
                (if (>= (ash eps 1) dx)
                    (mv (1+ y) (- eps dx))
                    (mv y eps))
                (draw-line/0<slope<=1 (1- count) x y dx dy eps color pixels width)))))

(defun draw-line/1<slope<infinity (count x y dx dy eps color pixels width)
  (if (zp count)
      pixels
      (let ((pixels (update-pixel x y width pixels color))
            (eps (+ eps dx))
            (y (1+ y)))
        (mv-let (x eps)
                (if (>= (ash eps 1) dy)
                    (mv (1+ x) (- eps dy))
                    (mv x eps))
                (draw-line/1<slope<infinity (1- count) x y dx dy eps color pixels width)))))
(defun draw-line/slope=0 (count x0 y0 color pixels width)
  (if (zp count)
      pixels
      (let ((pixels (update-pixel x0 y0 width pixels color)))
        (draw-line/slope=0 (1- count) (1+ x0) y0 color pixels width))))

(defun draw-line/slope=infinity (count x0 y0 color pixels width)
  (if (zp count)
      pixels
      (let ((pixels (update-pixel x0 y0 width pixels color)))
        (draw-line/slope=infinity (1- count) x0 (1+ y0) color pixels width))))

;; If the slope and either dx or dy differ in their sign,
;; then we swap (x0,y0) with (x1,y1) 
(defun maybe-swap-points (x0 x1 y0 y1 dx dy slope)
  (cond ((eq slope 'infinity) (mv x0 x1 (min y0 y1) (max y0 y1) 0 (abs dy)))
        ((zerop slope) (mv (min x0 x1) (max x0 x1) y0 y1 (abs dx) 0))
        ((and (plusp slope) (minusp dy)) (mv x1 x0 y1 y0 (abs dx) (abs dy)))
        ((and (minusp slope) (plusp dy)) (mv x1 x0 y1 y0 (abs dx) (abs dy)))
        (t (mv x0 x1 y0 y1 dx dy))))

(defun add-line (img x0 y0 x1 y1 color)
  (let ((pixels (image-pixels img))
        (width (image-width img))
        (pinhole-x (image-pinhole-x img))
        (pinhole-y (image-pinhole-y img))
        (dy (- y1 y0))
        (dx (- x1 x0)))
    (let ((slope (if (zerop dx) 'infinity (/ dy dx))))
      (mv-let (x0 x1 y0 y1 dx dy)
              (maybe-swap-points (+ x0 pinhole-x) (+ x1 pinhole-x) (+ y0 pinhole-y) (+ y1 pinhole-y) dx dy slope)
        (image width (image-height img)
               (image-pinhole-x img) (image-pinhole-y img)
               (cond 
                 ((eq slope 'infinity)
                  (draw-line/slope=infinity (1+ (abs dy)) x0 (min y0 y1) color pixels width))
                 ((zerop slope)
                  (draw-line/slope=0 (1+ (abs dx)) (min x0 x1) y0 color pixels width))
                 ((and (< 0 slope) (<= slope 1))
                  (draw-line/0<slope<=1 (1+ (abs dx)) x0 y0 dx dy 0 color pixels width))
                 ((< 1 slope)
                  (draw-line/1<slope<infinity (1+ (abs dy)) x0 y0 (abs dx) (abs dy) 0 color pixels width))
                 ((minusp slope) slope)
                 (t slope)))))))

(defun partition (lst width)
  (if (endp lst)
      nil
      (cons (take width lst) (partition (nthcdr width lst) width))))

(defun colors->bw (pixels)
  (cond ((endp pixels) nil)
        ((equal (car pixels) (color 255 255 255)) (cons 0 (colors->bw (cdr pixels))))
        (t (cons 1 (colors->bw (cdr pixels))))))
(defun stupid-render (img)
  (let ((pixels (image-pixels img))
        (width (image-width img)))
    (partition (colors->bw pixels) width)))
(defconst *bg* (rectangle 10 10 'solid *white*))

;; Need to do 'line' to help here.
;(defun triangle (size mode color)
;  (and (posp size) (mode? mode) (color? color)
;       (image size size
;              (triangle-scan-lines size size color))))
|#