#|
Bug:  this teachpack provides procedures that
      do not check for 1st-order usage.
|#
(module world scheme
  (require (lib "unit.ss")
           (only-in (lib "htdp-beginner.ss" "lang") [image? universe:image?])
           ;(lib "world.ss" "htdp")
           (prefix-in universe: "universe.ss")
           ;(prefix-in world: (lib "world.ss" "htdp"))
           (prefix-in posn: (lib "posn.ss" "lang"))
           (for-syntax "../proof/wrapper.ss")
           (file "posn.ss"))

  (define (acl2->boolean v)
    (not (or (equal? v 'nil)
             (equal? v '()))))

  (define (boolean->acl2 v) (if v 't '()))

  (define (acl2? f) (lambda args (boolean->acl2 (apply f args))))

  (define-signature teachpack^
    [empty-scene place-image add-line
     ;(struct color (red green blue))
     make-color color-red color-green color-blue color?
     font-size?
     image-color? mode?
     image?
     rectangle circle text triangle star line
     image-width image-height overlay overlay/xy
     put-pinhole move-pinhole pinhole-x pinhole-y
     bytep
     image-inside? find-image image->color-list color-list->image

     make-posn posn? weak-posn? posn-x posn-y

     mouse-eventp key-eventp

     packet packet-world packet-message packet-p
     *localhost*
     
     (define-syntaxes ( on-tick-event
                        on-key-event
                        on-redraw
                        stop-when
                        on-mouse-event
                        on-receive-event
                        register
                        universe
                        big-bang )
       (values 
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:on-tick-event (lambda (w) (cb-name w))) 't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:on-key-event (lambda (k w) (cb-name k w)))
                       't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:on-redraw (lambda (w) (cb-name w))) 't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:stop-when
                        (lambda (w)
                          (acl2->boolean (cb-name w))))
                       't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:on-mouse-event 
                        (lambda (w x y evt) 
                          (cb-name w x y evt)))
                       't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:on-receive-event
                        (lambda (w s)
                          (cb-name w s)))
                       't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ host name)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:register host name)
                       't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ initial process)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:universe
                        (lambda (p1 p2)
                          (initial p1 p2))
                        (lambda (state player message)
                          (process state player message)))
                       't)))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ width height freq w0)
             (dracula-event
              (quasisyntax/loc stx
                (begin (universe:big-bang width height freq w0) 't)))]
            [_ (raise-syntax-error
                #f
                "big-bang is a procedure that expects 4 arguments"
                stx)]))))])
  
  ;(define-unit-from-context teachpack@ teachpack^)
  (provide acl2->boolean teachpack^ teachpack@)
  (define-unit teachpack@
    (import)
    (export teachpack^)
    ;; these need to be syntax that check for 1st order use.
    (define empty-scene universe:empty-scene)
    (define place-image universe:place-image)
    (define add-line universe:add-line)
    (define make-color universe:make-color)
    (define color-red universe:color-red)
    (define color-green universe:color-green)
    (define color-blue universe:color-blue)
    (define rectangle universe:nw:rectangle)
    (define circle universe:circle)
    (define text universe:text)
    (define image-width universe:image-width)
    (define image-height universe:image-height)
    (define overlay universe:overlay)
    (define overlay/xy universe:overlay/xy)
    (define color-list->image universe:color-list->image)
    (define image->color-list universe:image->color-list)
    (define triangle universe:triangle)
    (define star universe:star)
    (define line universe:line)
    (define put-pinhole universe:put-pinhole)
    (define move-pinhole universe:move-pinhole)
    (define pinhole-x universe:pinhole-x)
    (define pinhole-y universe:pinhole-y)

    (define image-inside? (acl2? universe:image-inside?))
    (define bytep (acl2? byte?))
    (define color? (acl2? universe:color?))
    (define image-color? (acl2? universe:image-color?))
    (define mode? (acl2? (lambda (x) (or (eq? x 'solid) (eq? x 'outline)))))
    (define image? (acl2? (lambda (x) (universe:image? x))))

    (define (make-posn x y)
      `(make-posn ,x ,y))

    (define (find-image a b)
      (let* ([p (universe:find-image a b)])
        (make-posn (posn:posn-x p) (posn:posn-y p))))

    (define (posn? v)
      (if (and (list? v)
               (= (length v) 3)
               (eq? (car v) 'make-posn)
               (integer? (cadr v))
               (integer? (caddr v)))
          't
          '()))

    (define (weak-posn? v)
      (if (and (list? v)
               (= (length v) 3)
               (eq? (car v) 'make-posn))
          't
          '()))

    (define (posn-x p)
      (cadr p))

    (define (posn-y p)
      (caddr p))

    (define (mouse-eventp v)
      (boolean->acl2 (memv v '(button-down button-up drag move enter leave))))

    (define (key-eventp v)
      (boolean->acl2 (or (symbol? v) (char? v))))

    (define (font-size? v)
      (boolean->acl2 (and (integer? v) (<= 1 v 255))))

    (define (packet world message)
      (universe:make-package world message))

    (define (packet-p x)
      (universe:package? x))
    
    (define (packet-world packet)
      (universe:package-world packet))

    (define (packet-message packet)
      (universe:package-message packet))
    
    (define *localhost* universe:LOCALHOST)
   
    )
  
  #|
  (require (only (lib "htdp-beginner.ss" "lang")
                 image?)
           (lib "world.ss" "htdp")
           (file "posn.ss")) ;; posns are in here.
  
  (provide (all-from-except (lib "world.ss" "htdp")
                            shrink-tl shrink-tr
                            shrink-bl shrink-br
                            shrink
                            rectangle 
                            nw:rectangle
                            image->alpha-color-list
                            alpha-color-list->image
                            make-alpha-color
                            alpha-color?
                            alpha-color-alpha
                            alpha-color-red
                            alpha-color-green
                            alpha-color-blue
                            
                            ;; These produce #t; we want T instead
                            on-tick-event
                            on-key-event
                            on-mouse-event
                            big-bang
                            on-redraw)
           (all-from (file "posn.ss")))
  
  (provide (rename acl2:image? image?)
           (rename nw:rectangle rectangle)
           (rename acl2:on-tick-event on-tick-event)
           (rename acl2:on-key-event on-key-event)
           (rename acl2:on-mouse-event on-mouse-event)
           (rename acl2:on-redraw on-redraw)
           (rename acl2:big-bang big-bang))

  (define (acl2:image? x)
    (if (image? x) 't '()))
  
  (define-syntax (acl2:on-tick-event stx)
    (syntax-case stx ()
      [(_ cb-name) #'(begin (on-tick-event (lambda (w) (cb-name w))) 't)]))
  
  (define-syntax (acl2:on-key-event stx)
    (syntax-case stx ()
      [(_ cb-name) #'(begin (on-key-event (lambda (k w) (cb-name k w))) 't)]))
  
  (define-syntax (acl2:on-mouse-event stx)
    (syntax-case stx ()
      [(_ cb-name) #'(begin (on-mouse-event (lambda (w x y evt) 
                                              (cb-name w x y evt))) 't)]))
  
  (define-syntax (acl2:on-redraw stx)
    (syntax-case stx ()
      [(_ cb-name) #'(begin (on-redraw (lambda (w) (cb-name w))) 't)]))
  
  (define-syntax (acl2:big-bang stx)
    (syntax-case stx ()
      [(_ width height freq w0)
       #'(begin (big-bang width height freq w0)
                't)]
      [_ (raise-syntax-error #f "big-bang is a procedure that expects 4 arguments" stx)]))
  |#
  #;
  (define (acl2:big-bang width height freq w0) 
    (big-bang width height freq w0)
    't)
  
  )