		Search-engine friendly clone of the ACL2 documentation.

Defgrammar-implementation

Defgrammar-fn

Process the inputs and generate the events.

Signature
(defgrammar-fn args call ctx state) → (mv erp event state)
Arguments: args — Guard (true-listp args).; call — Guard (pseudo-event-formp call).; ctx — Guard (ctxp ctx).
Returns: event — Type (pseudo-event-formp event), given (true-listp args).

Definitions and Theorems

Function: defgrammar-fn

(defun defgrammar-fn (args call ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args)
                             (pseudo-event-formp call)
                             (ctxp ctx))))
 (let ((__function__ 'defgrammar-fn))
  (declare (ignorable __function__))
  (b* (((when (defgrammar-table-lookup call (w state)))
        (value '(value-triple :redundant)))
       ((er (list name file untranslate well-formed
                  closed parents short long other-events)
            :iferr '(_))
        (defgrammar-process-inputs args ctx state)))
   (defgrammar-gen-everything name file
                              untranslate well-formed closed parents
                              short long other-events call state))))

Theorem: pseudo-event-formp-of-defgrammar-fn.event

(defthm pseudo-event-formp-of-defgrammar-fn.event
  (implies (true-listp args)
           (b* (((mv acl2::?erp acl2::?event acl2::?state)
                 (defgrammar-fn args call ctx state)))
             (pseudo-event-formp event)))
  :rule-classes :rewrite)