Generate a primitive constructor for a preprocessor directive or tree concatenation.
The arguments are
a keyword for the directive (e.g.
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.
See also generate-primitive-constructor-for-tag.
Macro:
(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)))
Function:
(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)))))))))))))