Generate a primitive constructor for an XML tag.
The arguments are a keyword for the tag (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.
The generated macro accepts regular and keyword arguments in any order: the former are subtrees for the content between the XML tags; the latter are attributes of the XML tag. The macro uses partition-macro-args to divide them.
The name of the macro includes an added underscore at the end
if the tag is
See also generate-primitive-constructor-for-dir/&&.
Macro:
(defmacro generate-primitive-constructor-for-tag (tag doc) (cons 'make-event (cons (cons 'generate-primitive-constructor-for-tag-fn (cons tag (cons doc 'nil))) 'nil)))
Function:
(defun generate-primitive-constructor-for-tag-fn (tag doc) (declare (xargs :guard (and (keywordp tag) (stringp doc)))) (let* ((macro-name (case tag (:table 'table_) (:u 'u_) (:see 'see_) (t (intern$ (symbol-name tag) "XDOC")))) (fn-name (add-suffix-to-fn macro-name "-FN")) (thm-name (acl2::packn (list 'stringp-of- macro-name))) (long (concatenate 'string "<p>See the <see topic='@(url primitive-constructors)' >primitive constructors topic</see> for information about the kind of arguments that must be passed to this constructor.</p>" "@(def " (string-downcase$ (symbol-name macro-name)) ")"))) (cons 'defsection (cons macro-name (cons ':parents (cons '(primitive-constructors) (cons ':short (cons doc (cons ':long (cons long (cons (cons 'defund (cons fn-name (cons '(attributes trees) (cons '(declare (xargs :guard (and (keyword-tree-alistp attributes) (tree-listp trees)))) (cons (cons 'make-tree-tag (cons tag '(attributes trees))) 'nil))))) (cons (cons 'defthm (cons thm-name (cons (cons 'equal (cons (cons 'treep (cons (cons fn-name '(attributes trees)) 'nil)) '((and (keyword-tree-alistp attributes) (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 args) (cons (cons 'mv-let (cons '(trees attributes) (cons (cons 'partition-macro-args (cons 'args (cons (cons 'quote (cons macro-name 'nil)) 'nil))) (cons (cons 'let (cons '((attributes (keyword-macro-args-to-terms attributes))) (cons (cons 'list (cons (cons 'quote (cons fn-name 'nil)) '((cons 'list attributes) (cons 'list trees)))) 'nil))) 'nil)))) 'nil)))) 'nil)))))))))))))