		Search-engine friendly clone of the ACL2 documentation.

Defgrammar-event-generation

Defgrammar-gen-everything

Generate all the events.

Signature
(defgrammar-gen-everything name file untranslate well-formed closed parents short long other-events call state) → (mv erp event state)
Arguments: name — Guard (common-lisp::symbolp name).; file — Guard (common-lisp::stringp file).; untranslate — Guard (booleanp untranslate).; well-formed — Guard (booleanp well-formed).; closed — Guard (booleanp closed).; other-events — Guard (true-listp other-events).; call — Guard (pseudo-event-formp call).
Returns: event — Type (pseudo-event-formp event), given (true-listp other-events).

Definitions and Theorems

Function: defgrammar-gen-everything

(defun defgrammar-gen-everything
       (name file
             untranslate well-formed closed parents
             short long other-events call state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (common-lisp::symbolp name)
                             (common-lisp::stringp file)
                             (booleanp untranslate)
                             (booleanp well-formed)
                             (booleanp closed)
                             (true-listp other-events)
                             (pseudo-event-formp call))))
 (let ((__function__ 'defgrammar-gen-everything))
  (declare (ignorable __function__))
  (b*
   (((mv cstree state)
     (parse-grammar-from-file file state))
    ((unless (treep cstree))
     (value
          (prog2$ (raise "Internal error: no concrete syntax tree.")
                  '(_))))
    (astree (abstract-rulelist cstree))
    (defconst-event
         (cons 'defconst
               (cons name
                     (cons (cons 'quote (cons astree 'nil))
                           'nil))))
    (untranslate-event?
         (and untranslate
              (list (cons 'add-const-to-untranslate-preprocess
                          (cons name 'nil)))))
    (well-formed-event?
     (and
      well-formed
      (list
       (cons
        'defthm
        (cons
         (packn-pos (list 'rulelist-wfp-of- name)
                    name)
         (cons
          (cons 'rulelist-wfp (cons name 'nil))
          '(:hints (("Goal" :in-theory '((:e rulelist-wfp)))))))))))
    (closed-event?
     (and
      closed
      (list
       (cons
        'defthm
        (cons
         (packn-pos (list 'rulelist-closedp-of- name)
                    name)
         (cons
          (cons 'rulelist-closedp
                (cons name 'nil))
          '(:hints
               (("Goal" :in-theory '((:e rulelist-closedp)))))))))))
    (table-event (defgrammar-table-add call))
    (event
     (cons
      'progn
      (cons
       (cons
        'defsection
        (cons
         name
         (append
          (and (not (eq parents :absent))
               (list :parents parents))
          (append
           (and (not (eq short :absent))
                (list :short short))
           (append
            (and (not (eq long :absent))
                 (list :long long))
            (cons
             defconst-event
             (append
                 untranslate-event?
                 (append well-formed-event?
                         (append closed-event? other-events)))))))))
       (cons table-event 'nil)))))
   (value event))))

Theorem: pseudo-event-formp-of-defgrammar-gen-everything.event

(defthm pseudo-event-formp-of-defgrammar-gen-everything.event
  (implies (true-listp other-events)
           (b* (((mv acl2::?erp acl2::?event acl2::?state)
                 (defgrammar-gen-everything
                      name file
                      untranslate well-formed closed parents
                      short long other-events call state)))
             (pseudo-event-formp event)))
  :rule-classes :rewrite)