#lang scribble/doc
@(require scribble/manual scribble/eval "evaluator.ss"
          (for-label "../language/dracula.scm"))

@title[#:tag "events"]{Events and Definitions}

ACL2 events are special terms which define new functions or logical rules.
Defined names are in scope within their own definition and below; forward
references are not allowed.  Use the @scheme[mutual-recursion] event for
mutually recursive functions.

@defform[(assert$ test form)]{
Raises an error if the given test fails.
@examples[
#:eval the-evaluator
(assert$ (< 0 1) t)
(assert$ (< 1 0) t)
]
}

@defform[(defaxiom name term :rule-classes rule-classes :doc doc-string)]{
Defines an axiom. Using @scheme[defaxiom] is not recommended.
@examples[
#:eval the-evaluator
(defaxiom sbar (equal t nil)
          :rule-classes nil
          :doc ":Doc-Section ...")
]
}

@defform[(deflabel name :doc doc-string)]{
Defines a label, for adding a landmark and/or adding a documentation topic.
@examples[
#:eval the-evaluator
(deflabel interp-section
          :doc ":Doc-Section ...")
]
}

@defform[(defstub name args-sig => output-sig :doc doc-string)]{
}

@defform[(deftheory name term :doc doc-string)]{
Defines a theory (to enable or disable a set of rules)
@examples[
#:eval the-evaluator
(deftheory interp-theory
           (set-difference-theories
             (universal-theory :here)
             (universal-theory 'interp-section)))
]
}

@defform[(defthm name term
        :rule-classes rule-classes
        :instructions instructions
        :hints        hints
        :otf-flg      otf-flg
        :doc          doc-string)
]{
Defines a theorem to be proved and named.
@examples[
#:eval the-evaluator
(defthm x+x=2x (= (+ x x) (* 2 x)))
]
}

@defform[(in-theory term :doc doc-string)]{
@examples[
#:eval the-evaluator
(in-theory (set-difference-theories
             (universal-theory :here)
             '(flatten (:executable-counterpart flatten))))
]
}

@specform[(include-book file options ...)]{
Imports reusable definitions to the current program.
See the section on @secref["include-book"] for details on @scheme[include-book]
in Dracula.
}

@defform[(mutual-recursion def1 ... defn)]{
For defining mutually-recursive functions.
@examples[
#:eval the-evaluator
(mutual-recursion
 (defun evenlp (x)
   (if (consp x) (oddlp (cdr x)) t))
 (defun oddlp (x)
   (if (consp x) (evenlp (cdr x)) nil)))
]
}

@defform[(theory-invariant term :key key :error t/nil)]{}

@defform[(defconst name val)]{
Defines a constant value. The name must begin and end with asterisks.
@examples[
#:eval the-evaluator
(defconst *PI* 22/7)
(* 2 *PI*)
]
}

@defform[(defun name (args) (declare decl ...) ... body)]{
Defines a function.
@examples[
#:eval the-evaluator
(defun absolute-value (x)
     (cond 
       ((< x 0) (* -1 x))
       (t x)))
(absolute-value 5)
(absolute-value -5)
]
}

@defform[(declare d ...)]{
Used in @scheme[defun] to give ACL2 extra information about a function.
}