		Search-engine friendly clone of the ACL2 documentation.

Primitive-constructors

Generate-primitive-constructor-for-dir/&&

Generate a primitive constructor for a preprocessor directive or tree concatenation.

The arguments are a keyword for the directive (e.g. :@def for definitions) or for tree concatenation (i.e. :&&), and a documentation string that describes the primitive constructor. This documentation string is used as the :short string of the XDOC topic generated for the primitive constructor itself.

The generated XDOC constructor consists of a macro that calls a function (also generated), as often done with macros. We also generate a theorem about the return type of the constructor.

Macro: generate-primitive-constructor-for-dir/&&

(defmacro generate-primitive-constructor-for-dir/&& (dir/&& doc)
  (cons 'make-event
        (cons (cons 'generate-primitive-constructor-for-dir/&&-fn
                    (cons dir/&& (cons doc 'nil)))
              'nil)))

Definitions and Theorems

Function: generate-primitive-constructor-for-dir/&&-fn

(defun generate-primitive-constructor-for-dir/&&-fn (dir/&& doc)
 (declare (xargs :guard (and (keywordp dir/&&) (stringp doc))))
 (let* ((macro-name (add-suffix-to-fn '||
                                      (symbol-name dir/&&)))
        (fn-name (add-suffix-to-fn macro-name "-FN"))
        (thm-name (acl2::packn (list 'stringp-of- macro-name))))
  (cons
   'defsection
   (cons
    macro-name
    (cons
     ':parents
     (cons
      '(primitive-constructors)
      (cons
       ':short
       (cons
        doc
        (cons
         ':long
         (cons
          (concatenate
               'string
               "@(def "
               (string-escape
                    (string-downcase$ (symbol-name macro-name)))
               ")")
          (cons
           (cons
            'defund
            (cons
             fn-name
             (cons
                  '(trees)
                  (cons '(declare (xargs :guard (tree-listp trees)))
                        (cons (cons 'make-tree-dir/&&
                                    (cons dir/&& '(trees)))
                              'nil)))))
           (cons
            (cons
             'defthm
             (cons
              thm-name
              (cons
               (cons
                    'equal
                    (cons (cons 'treep
                                (cons (cons fn-name '(trees)) 'nil))
                          '((tree-listp trees))))
               (cons
                ':hints
                (cons
                 (cons
                  (cons
                      '"Goal"
                      (cons ':in-theory
                            (cons (cons 'enable (cons fn-name 'nil))
                                  'nil)))
                  'nil)
                 'nil)))))
            (cons
             (cons
              'defmacro
              (cons
               macro-name
               (cons
                 '(&rest trees)
                 (cons (cons 'list
                             (cons (cons 'quote (cons fn-name 'nil))
                                   '((cons 'list trees))))
                       'nil))))
             'nil)))))))))))))