modular/builtins.scm
(module builtins mzscheme

  (require (prefix world: "../teachpacks/world.scm")
           (prefix rand: "../teachpacks/rand.scm")
           (prefix mod: "expansion/forms.scm")
           (lib "unit.ss"))

  (provide random-ifc random-mod random-impl
           image-ifc image-mod image-impl
           game-ifc
           play-ifc play-mod play-impl)

  (define-values/invoke-unit world:teachpack@
    (import)
    (export world:teachpack^))

  (define-values/invoke-unit rand:teachpack@
    (import)
    (export rand:teachpack^))

  (define-syntax (define-builtins stx)
    (syntax-case stx ()
      [(db ifc mod impl tag
           [(f arg ...) ...]
           [(thm expr) ...])
       (syntax/loc stx
         (begin
           (mod:interface
            ifc
            (sig f (arg ...)) ...
            (con thm expr) ...)
           (mod:module/impl
            impl
            builtin
            mod
            (import)
            (export (tag : ifc))
            (sharing)
            (assign (tag (f <- f) ...)))))]))

  (define-builtins
    random-ifc random-mod random-impl RANDOM
    [(seedp v)
     (initial-seed)
     (next-seed s)
     (rand n s)]
    [(initial-seed/seedp
      (seedp (initial-seed)))
     (next-seed/seedp
      (implies (seedp s)
               (seedp (next-seed s))))
     (rand/integerp
      (implies (and (seedp s) (integerp n) (< 0 n))
               (and (integerp (rand n s))
                    (<= 0 (rand n s))
                    (< (rand n s) n))))])

  (define-builtins
    image-ifc image-mod image-impl IMAGE
    [(make-posn x y) (posn-x p) (posn-y p) (posn? v) (weak-posn? v)
     (color? v) (image-color? v) (make-color r g b)
     (color-red c) (color-green c) (color-blue c)
     (bytep v) (mode? v) (image? v)
     (circle r m c) (rectangle w h m c) (triangle l m c)
     (line x y c) (add-line img x0 y0 x1 y1 c) (text str sz c)
     (overlay a b) (overlay/xy a x y b) (image-width i) (image-height i)
     (pinhole-x i) (pinhole-y i) (move-pinhole i x y) (put-pinhole i x y)
     (image-inside? a b) (find-image a b)
     (image->color-list i) (color-list->image lo w h x y)
     (empty-scene w h) (place-image i x y s)]
    [])

  (mod:interface
   game-ifc
   (sig gamep (v))
   (sig live-gamep (v))
   (sig initial-game ())
   (sig game-tick (g))
   (sig game-key (g k))
   (sig game-mouse (g x y m))
   (sig game-draw (g))
   (sig game-width ())
   (sig game-height ())
   (sig game-time ())
   (con live-gamep/gamep (implies (live-gamep g) (gamep g)))
   (con initial-game/live-gamep (live-gamep (initial-game)))
   (con game-tick/gamep (implies (live-gamep g) (gamep (game-tick g))))
   (con game-key/gamep
    (implies (and (live-gamep g) (stringp k)) (gamep (game-key g k))))
   (con game-mouse/gamep
    (implies
     (and (live-gamep g) (stringp m) (integerp x) (integerp y))
     (gamep (game-mouse g x y m)))))

  (mod:interface play-ifc (sig play ()))

  (mod:module/impl
   play-impl
   builtin
   play-mod
   (import (GAME : game-ifc))
   (export (PLAY : play-ifc))
   (sharing)

   (define (truep v)
     (not (or (equal? v 'nil) (equal? v '()))))

   (define (notp v)
     (if (truep v) '() 't))

   (define (event->string e)
     (string-downcase
      (cond
       [(char? e) (string e)]
       [(symbol? e) (symbol->string e)]
       [(string? e) e]
       [else (format "~a" e)])))

   (define (do-key g k)
     (GAME.game-key g (event->string k)))

   (define (do-mouse g x y m)
     (GAME.game-mouse g x y (event->string m)))

   (define (game-over? g)
     (notp (GAME.live-gamep g)))

   (define (play)
     (big-bang (GAME.game-width) (GAME.game-height)
               (GAME.game-time) (GAME.initial-game))
     (on-redraw GAME.game-draw)
     (stop-when game-over?)
     (on-tick-event GAME.game-tick)
     (on-key-event do-key)
     (on-mouse-event do-mouse))

   (assign (PLAY (play <- play))))

  )