		Search-engine friendly clone of the ACL2 documentation.

Gen-operand-type-code-doc

Signature
(gen-operand-type-code-doc info) → *
Arguments: info — Guard (alistp info).

Definitions and Theorems

Function: get-operand-type-code-doc

(defun get-operand-type-code-doc (code)
  (declare (xargs :guard (operand-type-code-p code)))
  (let ((__function__ 'get-operand-type-code-doc))
    (declare (ignorable __function__))
    (b* ((alst (cdr (assoc-equal code *operand-type-code-info*)))
         (doc (cdr (assoc-equal :doc alst)))
         ((unless doc) ""))
      doc)))

Theorem: stringp-of-get-operand-type-code-doc

(defthm stringp-of-get-operand-type-code-doc
  (b* ((str (get-operand-type-code-doc code)))
    (stringp str))
  :rule-classes :rewrite)

Function: gen-operand-type-code-doc

(defun gen-operand-type-code-doc (info)
 (declare (xargs :guard (alistp info)))
 (let ((__function__ 'gen-operand-type-code-doc))
  (declare (ignorable __function__))
  (if (endp info)
      nil
   (b*
    ((code (caar info))
     ((unless (operand-type-code-p code))
      (er hard? __function__
          "~% Bad code ~x0 encountered! ~%" code))
     (codestr
       (str::pretty code
                    :config *x86isa-printconfig-base-10-lowercase*))
     (docstr (str::cat "@(' " codestr "'): "
                       (get-operand-type-code-doc code)))
     (topic-name
      (intern$
        (str::upcase-string (str::cat codestr "-OPERAND-TYPE-CODE"))
        "X86ISA"))
     (form (cons (cons 'defxdoc
                       (cons topic-name
                             (cons ':long (cons docstr 'nil))))
                 'nil))
     (rest (gen-operand-type-code-doc (cdr info))))
    (append form rest)))))