• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
      • Deftreeops
      • Defdefparse
        • Defdefparse-implementation
          • Defdefparse-event-generation
            • Defdefparse-gen-function-for-rulename
            • Defdefparse-gen-code-for-alternation
            • Defdefparse-gen-code-for-repetition
            • Defdefparse-gen-function-for-group
            • Defdefparse-function-spec
            • Defdefparse-gen-code-for-element
            • Defdefparse-gen-*-group-macro
            • Defdefparse-gen-function-for-option
            • Defdefparse-gen-option-macro
            • Defdefparse-gen-group-macro
            • Defdefparse-gen-code-for-concatenation
            • Defdefparse-gen-function-for-repetition
            • Defdefparse-gen-*-rulename-macro
            • Defdefparse-gen-rulename-macro
            • Defdefparse-gen-repetition-alist
            • Defdefparse-gen-option-alist
            • Defdefparse-gen-group-alist
            • Defdefparse-gen-everything
            • Defdefparse-gen-repetition-table-macro
            • Defdefparse-gen-option-table-macro
            • Defdefparse-gen-group-table-macro
            • Defdefparse-gen-function-for-spec
            • Defdefparse-gen-repetition-table
            • Defdefparse-gen-option-table
            • Defdefparse-gen-group-table
            • Defdefparse-reorder-alternation
            • Defdefparse-order-permutationp
            • Defdefparse-gen-repetition-table-name
            • Defdefparse-gen-option-table-name
            • Defdefparse-gen-group-table-name
            • Defdefparse-alt-symbol-alist
            • Defdefparse-rep-symbol-alist
          • Defdefparse-fn
          • Defdefparse-input-processing
          • Defdefparse-table
          • Defdefparse-macro-definition
      • Defgrammar
      • Abnf-tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
      • Differences-with-paper
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defdefparse-event-generation

Defdefparse-gen-rulename-macro

Generate the defparse-name-rulename macro described in the defdefparse user documentation.

Signature

(defdefparse-gen-rulename-macro 
     name 
     pkg-wit grammar prefix group-table-name 
     option-table-name repetition-table-name) 
 
  → 
event

Arguments

name — Guard (common-lisp::symbolp name).

pkg-wit — Guard (common-lisp::symbolp pkg-wit).

grammar — Guard (common-lisp::symbolp grammar).

prefix — Guard (common-lisp::symbolp prefix).

group-table-name — Guard (common-lisp::symbolp group-table-name).

option-table-name — Guard (common-lisp::symbolp option-table-name).

repetition-table-name — Guard (common-lisp::symbolp repetition-table-name).

Returns

event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defdefparse-gen-rulename-macro

(defun defdefparse-gen-rulename-macro
       (name pkg-wit grammar prefix group-table-name
             option-table-name repetition-table-name)
 (declare
  (xargs :guard (and (common-lisp::symbolp name)
                     (common-lisp::symbolp pkg-wit)
                     (common-lisp::symbolp grammar)
                     (common-lisp::symbolp prefix)
                     (common-lisp::symbolp group-table-name)
                     (common-lisp::symbolp option-table-name)
                     (common-lisp::symbolp repetition-table-name))))
 (let ((__function__ 'defdefparse-gen-rulename-macro))
  (declare (ignorable __function__))
  (b* ((macro-name (packn-pos (list 'defparse- name '-rulename)
                              pkg-wit)))
   (cons
    'defmacro
    (cons
     macro-name
     (cons
      '(rulename &key order)
      (cons
       (cons
        'cons
        (cons
         ''make-event
         (cons
          (cons
           'cons
           (cons
            (cons
             'cons
             (cons
              ''defdefparse-gen-function-for-spec
              (cons
               (cons
                'cons
                (cons
                 '(cons 'defdefparse-function-spec-rulename
                        (cons rulename
                              (cons (cons 'quote (cons order 'nil))
                                    'nil)))
                 (cons
                  (cons
                   'cons
                   (cons
                    (cons 'quote (cons grammar 'nil))
                    (cons
                     (cons
                      'cons
                      (cons
                       (cons
                        'cons
                        (cons
                         ''quote
                         (cons
                          (cons
                              'cons
                              (cons (cons 'quote (cons prefix 'nil))
                                    '('nil)))
                          'nil)))
                       (cons
                        (cons
                         'cons
                         (cons
                          (cons 'quote
                                (cons group-table-name 'nil))
                          (cons
                           (cons
                            'cons
                            (cons
                             (cons 'quote
                                   (cons option-table-name 'nil))
                             (cons
                              (cons
                               'cons
                               (cons
                                (cons
                                  'quote
                                  (cons repetition-table-name 'nil))
                                '('nil)))
                              'nil)))
                           'nil)))
                        'nil)))
                     'nil)))
                  'nil)))
               'nil)))
            '('nil)))
          'nil)))
       'nil)))))))

Theorem: pseudo-event-formp-of-defdefparse-gen-rulename-macro

(defthm pseudo-event-formp-of-defdefparse-gen-rulename-macro
  (b* ((event (defdefparse-gen-rulename-macro
                   name pkg-wit grammar prefix
                   group-table-name option-table-name
                   repetition-table-name)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)