#|$ACL2s-Preamble$;
#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "ccg" :uncertified-okp nil :dir :acl2s :ttags ((ccg)) :load-compiled-file :comp)
(include-book "ordinals/lexicographic-ordering" :dir :system)
(set-well-founded-relation l<)
(set-guard-checking :none)
;$ACL2s-SMode$;ACL2s
(begin-book t :ttags :all);$ACL2s-Preamble$|#


(in-package "ACL2")

(include-book "graphics" :dir :acl2s :ttags :all)

(defconst *empty-row*
  '(nil nil nil nil nil nil nil nil))
  
(defconst *initial-config*
  (list "" ; status bar text
        *empty-row* *empty-row* *empty-row*
        '(nil nil nil 1 0 nil nil nil)
        '(nil nil nil 0 1 nil nil nil)
        *empty-row* *empty-row* *empty-row*))

(defun present-row (rowidx colidx row pres)
  (cond ((endp row) ; no more elts
         pres)
        (t
         (let ((nextpres
                (cond ((= (first row) 0)
                       (fill-oval (/ colidx 8) (/ rowidx 8) 1/8 1/8 'white pres))
                      ((= (first row) 1)
                       (fill-oval (/ colidx 8) (/ rowidx 8) 1/8 1/8 'black pres))
                      (t
                       pres))))
           (present-row rowidx (+ 1 colidx) (rest row) nextpres)))))

(defun present-rows (rowidx config pres)
  (cond ((endp config) ; no more rows
         pres)
        (t
         (let ((nextpres (present-row rowidx 0 (first config) pres)))
           (present-rows (+ 1 rowidx) (rest config) nextpres)))))

(defun presenter (config pres)
  (let* ((pres (fill-rect 0 0 1 1 'gray pres))
         (pres (draw-line 0 1/8 1 1/8 'black pres))
         (pres (draw-line 0 2/8 1 2/8 'black pres))
         (pres (draw-line 0 3/8 1 3/8 'black pres))
         (pres (draw-line 0 4/8 1 4/8 'black pres))
         (pres (draw-line 0 5/8 1 5/8 'black pres))
         (pres (draw-line 0 6/8 1 6/8 'black pres))
         (pres (draw-line 0 7/8 1 7/8 'black pres))
         (pres (draw-line 1/8 0 1/8 1 'black pres))
         (pres (draw-line 2/8 0 2/8 1 'black pres))
         (pres (draw-line 3/8 0 3/8 1 'black pres))
         (pres (draw-line 4/8 0 4/8 1 'black pres))
         (pres (draw-line 5/8 0 5/8 1 'black pres))
         (pres (draw-line 6/8 0 6/8 1 'black pres))
         (pres (draw-line 7/8 0 7/8 1 'black pres))
         (pres (set-status-bar  (car config) pres)))
    (present-rows 0 (cdr config) pres)))

(defun flipper (button x y config)
  (declare (ignore button))
  (let* ((row (floor (* 8 y) 1))
         (col (floor (* 8 x) 1))
         (oldval (nth col (nth (1+ row) config)))
         (newval (cond ((= oldval 0)
                        1)
                       ((= oldval 1)
                        nil)
                       (t
                        0))))
    (update-nth (1+ row) (update-nth col newval (nth (1+ row) config)) config)))  

(set-initial-configuration *initial-config*)
(set-configuration-presenter 'presenter)
(add-click-handler 'flipper)


; and some misc. stuff to test the status bar, key typing & timers

(defun type-to-status-bar (char config)
  (cons (cond ((equal char #\Space)
               "")
              (t
               (coerce (append (coerce (car config) 'list)
                        (list char))
                'string)))
        (cdr config)))

(add-key-handler 'type-to-status-bar)

(defun remove-first-from-status-bar (config)
  (cond ((equal (car config) "")
         config)
        (t
         (cons (coerce (cdr (coerce (car config) 'list))
                       'string)
               (cdr config)))))

(add-timer-handler 1000 remove-first-from-status-bar)#|ACL2s-ToDo-Line|#



;; to run it:
;(big-bang)