#|
Bug:  this teachpack provides procedures that
      do not check for 1st-order usage.
|#
(module world mzscheme
  (require (lib "unit.ss")
           (rename (lib "htdp-beginner.ss" "lang") world:image? image?)
           ;(lib "world.ss" "htdp")
           (prefix world: (lib "world.ss" "htdp"))
           (prefix posn: (lib "posn.ss" "lang"))
           (file "posn.scm"))
  (require-for-syntax "../modular/expansion/proof-syntax.scm")

  (define (acl2? f) (lambda args (if (apply f args) 't '())))

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

  (define-signature teachpack^
    [empty-scene place-image add-line
     ;(struct color (red green blue))
     make-color color-red color-green color-blue color?
     image-color? mode?
     image?
     rectangle circle text triangle 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
     
     (define-syntaxes ( on-tick-event
                        on-key-event
                        on-redraw
                        stop-when
                        on-mouse-event
                        big-bang )
       (values 
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (make-event
              stx
              #'(begin (world:on-tick-event (lambda (w) (cb-name w))) 't))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (make-event
              stx
              #'(begin (world:on-key-event (lambda (k w) (cb-name k w))) 't))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (make-event
              stx
              #'(begin (world:on-redraw (lambda (w) (cb-name w))) 't))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (make-event
              stx
              #'(begin (world:stop-when
                        (lambda (w)
                          (acl2->boolean (cb-name w))))
                       't))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ cb-name)
             (make-event
              stx
              #'(begin (world:on-mouse-event 
                        (lambda (w x y evt) 
                          (cb-name w x y evt)))
                       't))]))
        (lambda (stx)
          (syntax-case stx ()
            [(_ width height freq w0)
             (make-event
              stx
              #'(begin (world: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 teachpack^ teachpack@)
  (define-unit teachpack@
    (import)
    (export teachpack^)
    ;; these need to be syntax that check for 1st order use.
    (define empty-scene world:empty-scene)
    (define place-image world:place-image)
    (define add-line world:add-line)
    (define make-color world:make-color)
    (define color-red world:color-red)
    (define color-green world:color-green)
    (define color-blue world:color-blue)
    (define rectangle world:nw:rectangle)
    (define circle world:circle)
    (define text world:text)
    (define image-width world:image-width)
    (define image-height world:image-height)
    (define overlay world:overlay)
    (define overlay/xy world:overlay/xy)
    (define color-list->image world:color-list->image)
    (define image->color-list world:image->color-list)
    (define triangle world:triangle)
    (define line world:line)
    (define put-pinhole world:put-pinhole)
    (define move-pinhole world:move-pinhole)
    (define pinhole-x world:pinhole-x)
    (define pinhole-y world:pinhole-y)

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

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

    (define (find-image a b)
      (let* ([p (world: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))
    
    )
  
  #|
  (require (only (lib "htdp-beginner.ss" "lang")
                 image?)
           (lib "world.ss" "htdp")
           (file "posn.scm")) ;; 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.scm")))
  
  (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)
  
  )