#|
This specification helps the `undo' button on the ACL2 interface figure
out what can and cannot be undone.  Since we do not support defmacro,
the set of event forms is fixed.
|#
(module event-form mzscheme
  (require (lib "plt-match.ss"))
  (provide event-form?)
  
  ;; (union Syntax s-expr) -> Boolean
  (define (event-form? e)
    (event-form/se? (if (syntax? e) (syntax-object->datum e) e)))
  
  ;; event-form/se? : s-expr -> boolean
  ;; does the given s-expr represent an ACL2 event form?
  (define (event-form/se? e)
    (match e
      [`(with-prover-time-limit ,num ,body) (event-form/se? body)]
      [`(,form-name . ,_)
        (and (memq form-name 
                   '(defun defund defthm defconst defmacro defpun 
                      defaxiom defchoose defcong defequiv 
                      defexec defevaluator
                      deflabel deflist defalist
                      defrefinement
                      defstructure
                      defstobj defstub deftheory
                      defthmd
                      defun-sk
                      encapsulate 
                      in-theory include-book
                      local
                      mutual-recursion
                      set-compile-fns
                      set-state-ok
                      verify-guards verify-termination

                      ;; ;; World teachpack
                      ;; big-bang on-tick-event on-key-event on-mouse-event
                      ;; on-redraw

                      ;; Testing teachpack
                      check-expect check-within check-error

                      ;; DoubleCheck teachpack
                      defproperty defgenerator
                      ))
             #t)]
      [else #f])))