defmacrodoc - ACL2 Book

Included Books

bstar macro-args strings lookup-keyword keyword-value-lists2 downcase lookup-eq

other

(in-package "ACL2")

include-book

(include-book "std/util/bstar" :dir :system)

include-book

(include-book "macro-args")

include-book

(include-book "strings")

include-book

(include-book "kestrel/utilities/lookup-keyword" :dir :system)

include-book

(include-book "kestrel/utilities/keyword-value-lists2" :dir :system)

include-book

(include-book "kestrel/strings-light/downcase" :dir :system)

include-book

(include-book "kestrel/alists-light/lookup-eq" :dir :system)

local

(local (in-theory (disable mv-nth)))

xdoc-make-paragraphsfunction

(defund xdoc-make-paragraphs
  (forms)
  (declare (xargs :guard (true-listp forms)))
  (if (endp forms)
    nil
    (append (list "<p>" (first forms) "</p>" (newline-string))
      (xdoc-make-paragraphs (rest forms)))))

object-to-stringfunction

(defund object-to-string
  (obj package)
  (declare (xargs :guard (stringp package) :mode :program))
  (mv-let (col string)
    (fmt1-to-string "~x0"
      (acons #\0 obj nil)
      0
      :fmt-control-alist (acons 'current-package package nil))
    (declare (ignore col))
    string))

get-declaresfunction

(defun get-declares
  (forms)
  (if (endp forms)
    (mv nil nil)
    (if (and (consp (car forms)) (eq 'declare (caar forms)))
      (mv-let (declares rest)
        (get-declares (rest forms))
        (mv (cons (car forms) declares) rest))
      (mv nil forms))))

len-of-longest-macro-formalfunction

(defun len-of-longest-macro-formal
  (macro-args longest)
  (if (endp macro-args)
    longest
    (let* ((arg (first macro-args)) (len (if (symbolp arg)
            (length (symbol-name arg))
            (length (symbol-name (car arg))))))
      (len-of-longest-macro-formal (rest macro-args)
        (max longest len)))))

*xdoc-general-form-header*constant

(defconst *xdoc-general-form-header*
  "<h3>General Form:</h3>")

*xdoc-general-form-header-with-spacing*constant

(defconst *xdoc-general-form-header-with-spacing*
  (n-string-append *xdoc-general-form-header*
    (newline-string)
    (newline-string)))

*xdoc-inputs-header*constant

(defconst *xdoc-inputs-header* "<h3>Inputs:</h3>")

*xdoc-inputs-header-with-spacing*constant

(defconst *xdoc-inputs-header-with-spacing*
  (n-string-append (newline-string)
    (newline-string)
    *xdoc-inputs-header*
    (newline-string)
    (newline-string)))

*xdoc-description-header*constant

(defconst *xdoc-description-header* "<h3>Description:</h3>")

*xdoc-description-header-with-spacing*constant

(defconst *xdoc-description-header-with-spacing*
  (n-string-append (newline-string)
    (newline-string)
    *xdoc-description-header*
    (newline-string)
    (newline-string)))

xdoc-within-code-fnfunction

(defun xdoc-within-code-fn
  (strings)
  (declare (xargs :guard (string-listp strings)))
  (string-append-lst (cons "@({" (append strings (list "})")))))

xdoc-within-codemacro

(defmacro xdoc-within-code
  (&rest strings)
  `(xdoc-within-code-fn (list ,@STRINGS)))

xdoc-for-macro-general-form-required-argfunction

(defund xdoc-for-macro-general-form-required-arg
  (macro-arg indent-space firstp)
  (declare (xargs :guard (and (macro-argp macro-arg)
        (stringp indent-space)
        (booleanp firstp))))
  (if (not (symbolp macro-arg))
    (prog2$ (er hard?
        'xdoc-for-macro-general-form-required-arg
        "Required macro arg ~x0 is not a symbol."
        macro-arg)
      "")
    (n-string-append (if firstp
        ""
        indent-space)
      (string-downcase-gen (symbol-name macro-arg))
      (newline-string))))

xdoc-for-macro-general-form-required-argsfunction

(defun xdoc-for-macro-general-form-required-args
  (macro-args indent-space firstp)
  (declare (xargs :guard (and (macro-arg-listp macro-args)
        (stringp indent-space)
        (booleanp firstp))))
  (if (endp macro-args)
    ""
    (string-append (xdoc-for-macro-general-form-required-arg (first macro-args)
        indent-space
        firstp)
      (xdoc-for-macro-general-form-required-args (rest macro-args)
        indent-space
        nil))))

xdoc-for-macro-general-form-optional-argfunction

(defun xdoc-for-macro-general-form-optional-arg
  (macro-arg indent-space firstp max-len package)
  (declare (xargs :guard (and (macro-argp macro-arg)
        (stringp indent-space)
        (booleanp firstp)
        (natp max-len)
        (stringp package))
      :mode :program))
  (mv-let (name default)
    (keyword-or-optional-arg-name-and-default macro-arg)
    (let* ((name (string-downcase-gen (symbol-name name))) (name (n-string-append "[" name "]"))
        (num-spaces-before-comment (+ 1 (- max-len (length name))))
        (space-before-comment (string-append-lst (make-list num-spaces-before-comment :initial-element " "))))
      (n-string-append (if firstp
          ""
          indent-space)
        name
        space-before-comment
        "; default "
        (string-downcase-gen (object-to-string default package))
        (newline-string)))))

xdoc-for-macro-general-form-optional-argsfunction

(defun xdoc-for-macro-general-form-optional-args
  (macro-args indent-space firstp max-len package)
  (declare (xargs :guard (and (macro-arg-listp macro-args)
        (stringp indent-space)
        (booleanp firstp)
        (natp max-len)
        (stringp package))
      :mode :program))
  (if (endp macro-args)
    ""
    (string-append (xdoc-for-macro-general-form-optional-arg (first macro-args)
        indent-space
        firstp
        max-len
        package)
      (xdoc-for-macro-general-form-optional-args (rest macro-args)
        indent-space
        nil
        max-len
        package))))

xdoc-for-macro-general-form-keyword-argfunction

(defun xdoc-for-macro-general-form-keyword-arg
  (macro-arg indent-space firstp max-len package)
  (declare (xargs :guard (and (macro-argp macro-arg)
        (stringp indent-space)
        (booleanp firstp)
        (natp max-len)
        (stringp package))
      :mode :program))
  (mv-let (name default)
    (keyword-or-optional-arg-name-and-default macro-arg)
    (let* ((name (string-downcase-gen (symbol-name name))) (name (n-string-append ":" name))
        (num-spaces-before-comment (+ 1 (- max-len (length name))))
        (space-before-comment (string-append-lst (make-list num-spaces-before-comment :initial-element " "))))
      (n-string-append (if firstp
          ""
          indent-space)
        name
        space-before-comment
        "; default "
        (string-downcase-gen (object-to-string default package))
        (newline-string)))))

xdoc-for-macro-general-form-keyword-argsfunction

(defun xdoc-for-macro-general-form-keyword-args
  (macro-args indent-space firstp max-len package)
  (declare (xargs :guard (and (macro-arg-listp macro-args)
        (stringp indent-space)
        (booleanp firstp)
        (natp max-len)
        (stringp package))
      :mode :program))
  (if (endp macro-args)
    ""
    (string-append (xdoc-for-macro-general-form-keyword-arg (first macro-args)
        indent-space
        firstp
        max-len
        package)
      (xdoc-for-macro-general-form-keyword-args (rest macro-args)
        indent-space
        nil
        max-len
        package))))

xdoc-for-macro-general-form-argsfunction

(defun xdoc-for-macro-general-form-args
  (macro-args indent-space package)
  (declare (xargs :guard (and (macro-arg-listp macro-args)
        (stringp indent-space)
        (stringp package))
      :mode :program))
  (b* (((mv required-args optional-args keyword-args) (extract-required-and-optional-and-keyword-args macro-args)) (max-len (max (len-of-longest-macro-formal required-args 0)
          (max (+ 1 (len-of-longest-macro-formal keyword-args 0))
            (+ 2 (len-of-longest-macro-formal optional-args 0))))))
    (n-string-append (if required-args
        (xdoc-for-macro-general-form-required-args required-args
          indent-space
          t)
        (n-string-append "; no required args" (newline-string)))
      (if optional-args
        (n-string-append indent-space "&optional" (newline-string))
        "")
      (xdoc-for-macro-general-form-optional-args optional-args
        indent-space
        nil
        max-len
        package)
      (if keyword-args
        (n-string-append indent-space "&key" (newline-string))
        "")
      (xdoc-for-macro-general-form-keyword-args keyword-args
        indent-space
        nil
        max-len
        package))))

xdoc-for-macro-general-formfunction

(defun xdoc-for-macro-general-form
  (name macro-args package)
  (declare (xargs :mode :program :guard (and (symbolp name)
        (macro-arg-listp macro-args)
        (stringp package))))
  (let* ((name-string (string-downcase-gen (symbol-name name))) (name-len (length name-string))
      (indent-space (string-append-lst (make-list (+ 2 name-len) :initial-element " "))))
    (concatenate 'string
      *xdoc-general-form-header-with-spacing*
      (xdoc-within-code "("
        name-string
        " "
        (xdoc-for-macro-general-form-args macro-args
          indent-space
          package)
        indent-space
        ")"))))

macro-arg-descriptionspfunction

(defun macro-arg-descriptionsp
  (arg-descriptions)
  (declare (xargs :guard t :measure (len arg-descriptions)))
  (if (atom arg-descriptions)
    (null arg-descriptions)
    (let ((item (first arg-descriptions)))
      (and (true-listp item)
        (<= 2 (len item))
        (symbolp (first item))
        (true-listp (cdr item))
        (macro-arg-descriptionsp (rest arg-descriptions))))))

macro-arg-descriptionsp-forward-to-symbol-alistptheorem

(defthm macro-arg-descriptionsp-forward-to-symbol-alistp
  (implies (macro-arg-descriptionsp arg-descriptions)
    (symbol-alistp arg-descriptions))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable macro-arg-descriptionsp))))

local

(local (defthm true-listp-of-lookup-equal-when-macro-arg-descriptionsp
    (implies (macro-arg-descriptionsp arg-descriptions)
      (true-listp (lookup-equal macro-arg arg-descriptions)))
    :hints (("Goal" :in-theory (enable macro-arg-descriptionsp lookup-equal)))))

*open-blockquote-and-newline*constant

(defconst *open-blockquote-and-newline*
  (concatenate 'string "<blockquote>" (newline-string)))

*close-blockquote-and-two-newlines*constant

(defconst *close-blockquote-and-two-newlines*
  (concatenate 'string
    "</blockquote>"
    (newline-string)
    (newline-string)))

*close-p-and-newline*constant

(defconst *close-p-and-newline*
  (concatenate 'string "</p>" (newline-string)))

xdoc-for-macro-required-argfunction

(defun xdoc-for-macro-required-arg
  (macro-arg arg-descriptions)
  (declare (xargs :guard (and (symbolp macro-arg)
        (macro-arg-descriptionsp arg-descriptions))))
  (if (not (symbolp macro-arg))
    (er hard
      'xdoc-for-macro-required-arg
      "Required macro arg ~x0 is not a symbol."
      macro-arg)
    (let ((name (string-downcase-gen (symbol-name macro-arg))) (description-forms (lookup-eq macro-arg arg-descriptions)))
      `("<p>@('" ,NAME
        "') &mdash; (required)</p>

"
        ,*OPEN-BLOCKQUOTE-AND-NEWLINE*
        ,@(XDOC-MAKE-PARAGRAPHS DESCRIPTION-FORMS)
        ,*CLOSE-BLOCKQUOTE-AND-TWO-NEWLINES*))))

xdoc-for-macro-required-argsfunction

(defun xdoc-for-macro-required-args
  (macro-args arg-descriptions)
  (declare (xargs :guard (and (symbol-listp macro-args)
        (macro-arg-descriptionsp arg-descriptions))))
  (if (endp macro-args)
    nil
    (append (xdoc-for-macro-required-arg (first macro-args)
        arg-descriptions)
      (xdoc-for-macro-required-args (rest macro-args)
        arg-descriptions))))

xdoc-for-macro-optional-argfunction

(defun xdoc-for-macro-optional-arg
  (macro-arg arg-descriptions package)
  (declare (xargs :guard (and (stringp package)
        (macro-arg-descriptionsp arg-descriptions)
        (macro-argp macro-arg))))
  (b* (((mv name default) (keyword-or-optional-arg-name-and-default macro-arg)) (name-to-lookup name)
      (description-strings (lookup-eq name-to-lookup arg-descriptions))
      (name (n-string-append "["
          (string-downcase-gen (symbol-name name))
          "]"))
      (default-form `(string-downcase-gen (object-to-string ,DEFAULT ,PACKAGE))))
    `("<p>@('" ,NAME
      "') &mdash; default @('"
      ,DEFAULT-FORM
      "')</p>

"
      ,*OPEN-BLOCKQUOTE-AND-NEWLINE*
      ,@(XDOC-MAKE-PARAGRAPHS DESCRIPTION-STRINGS)
      ,*CLOSE-BLOCKQUOTE-AND-TWO-NEWLINES*)))

xdoc-for-macro-optional-argsfunction

(defun xdoc-for-macro-optional-args
  (macro-args arg-descriptions package)
  (declare (xargs :guard (and (macro-arg-listp macro-args)
        (macro-arg-descriptionsp arg-descriptions)
        (stringp package))))
  (if (endp macro-args)
    nil
    (append (xdoc-for-macro-optional-arg (first macro-args)
        arg-descriptions
        package)
      (xdoc-for-macro-optional-args (rest macro-args)
        arg-descriptions
        package))))

xdoc-for-macro-keyword-argfunction

(defun xdoc-for-macro-keyword-arg
  (macro-arg arg-descriptions package)
  (declare (xargs :guard (and (stringp package)
        (macro-arg-descriptionsp arg-descriptions)
        (macro-argp macro-arg))))
  (b* (((mv name default) (keyword-or-optional-arg-name-and-default macro-arg)) (name-to-lookup name)
      (description-strings (lookup-eq name-to-lookup arg-descriptions))
      (name (string-append ":" (string-downcase-gen (symbol-name name))))
      (default-form `(string-downcase-gen (object-to-string ,DEFAULT ,PACKAGE))))
    `("<p>@('" ,NAME
      "') &mdash; default @('"
      ,DEFAULT-FORM
      "')</p>

"
      ,*OPEN-BLOCKQUOTE-AND-NEWLINE*
      ,@(XDOC-MAKE-PARAGRAPHS DESCRIPTION-STRINGS)
      ,*CLOSE-BLOCKQUOTE-AND-TWO-NEWLINES*)))

xdoc-for-macro-keyword-argsfunction

(defun xdoc-for-macro-keyword-args
  (macro-args arg-descriptions package)
  (declare (xargs :guard (and (macro-arg-listp macro-args)
        (macro-arg-descriptionsp arg-descriptions)
        (stringp package))))
  (if (endp macro-args)
    nil
    (append (xdoc-for-macro-keyword-arg (first macro-args)
        arg-descriptions
        package)
      (xdoc-for-macro-keyword-args (rest macro-args)
        arg-descriptions
        package))))

defxdoc-for-macro-fnfunction

(defund defxdoc-for-macro-fn
  (name macro-args
    parents
    short
    arg-descriptions
    description
    state)
  (declare (xargs :guard (and (symbolp name)
        (or (eq :auto macro-args) (macro-arg-listp macro-args))
        (symbol-listp parents)
        (macro-arg-descriptionsp arg-descriptions))
      :mode :program :stobjs state))
  (b* (((when (not (consp parents))) (er hard?
         'defxdoc-for-macro-fn
         "No :parents supplied for ~x0."
         name)) (expected-macro-args (getprop name
          'macro-args
          :unavailable 'current-acl2-world
          (w state)))
      ((when (and (eq :unavailable expected-macro-args)
           (eq :auto macro-args))) (er hard?
          'defxdoc-for-macro-fn
          "No macro-args supplied for ~x0 and it doesn't exist."
          name))
      (macro-args (if (eq :auto macro-args)
          expected-macro-args
          macro-args))
      ((when (and (not (eq :unavailable expected-macro-args))
           (not (equal macro-args expected-macro-args)))) (er hard?
          'defxdoc-for-macro-fn
          "Mismatch between supplied macro args (not counting &whole), ~X01, and existing args, ~X23."
          macro-args
          nil
          expected-macro-args
          nil))
      (macro-arg-names (macro-arg-names macro-args))
      (described-arg-names (strip-cars arg-descriptions))
      ((when (not (subsetp-eq described-arg-names macro-arg-names))) (er hard?
          'defxdoc-for-macro-fn
          "Descriptions given for arguments, ~x0, that are not among the macro args, ~x1."
          (set-difference-eq described-arg-names macro-arg-names)
          macro-args))
      ((when (not (subsetp-eq macro-arg-names described-arg-names))) (er hard?
          'defxdoc-for-macro-fn
          "No descriptions given for macro arguments, ~x0."
          (set-difference-eq macro-arg-names described-arg-names)))
      (package (symbol-package-name name))
      ((mv required-args optional-args keyword-args) (extract-required-and-optional-and-keyword-args macro-args))
      (description-forms (if (null description)
          nil
          (if (atom description)
            (list description)
            (if (symbolp (car description))
              (list description)
              description)))))
    `(defxdoc ,NAME
      ,@(AND PARENTS `(:PARENTS ,PARENTS))
      ,@(AND SHORT `(:SHORT ,SHORT))
      :long (n-string-append ,@(AND DESCRIPTION-FORMS
       (CONS *XDOC-DESCRIPTION-HEADER-WITH-SPACING*
             (XDOC-MAKE-PARAGRAPHS DESCRIPTION-FORMS)))
        ,(XDOC-FOR-MACRO-GENERAL-FORM NAME MACRO-ARGS PACKAGE)
        ,*XDOC-INPUTS-HEADER-WITH-SPACING*
        ,@(XDOC-FOR-MACRO-REQUIRED-ARGS REQUIRED-ARGS ARG-DESCRIPTIONS)
        ,@(XDOC-FOR-MACRO-OPTIONAL-ARGS OPTIONAL-ARGS ARG-DESCRIPTIONS PACKAGE)
        ,@(XDOC-FOR-MACRO-KEYWORD-ARGS KEYWORD-ARGS ARG-DESCRIPTIONS PACKAGE)))))

defxdoc-for-macromacro

(defmacro defxdoc-for-macro
  (name &key
    (macro-args ':auto)
    (parents 'nil)
    (short 'nil)
    (arg-descriptions 'nil)
    (description 'nil))
  `(make-event (defxdoc-for-macro-fn ',NAME
      ',MACRO-ARGS
      ',PARENTS
      ',SHORT
      ',ARG-DESCRIPTIONS
      ',DESCRIPTION
      state)))

defmacrodoc-fnfunction

(defun defmacrodoc-fn
  (name macro-args rest state)
  (declare (xargs :mode :program :guard (and (symbolp name) (macro-arg-listp macro-args))
      :stobjs state))
  (b* (((mv declares rest) (get-declares rest)) (body (first rest))
      (xdoc-stuff (rest rest))
      ((when (not (keyword-value-listp xdoc-stuff))) (er hard
          'defmacrodoc
          "Ill-formed xdoc args (should be a keyword-value-list): ~x0"
          xdoc-stuff))
      (allowed-keys '(:parents :short :description :args))
      ((when (not (subsetp-eq (keyword-value-list-keys xdoc-stuff)
             allowed-keys))) (er hard
          'defmacrodoc
          "Bad keys in ~x0 (allowed keys are ~x1)"
          xdoc-stuff
          allowed-keys))
      (parents (lookup-keyword :parents xdoc-stuff))
      (short (lookup-keyword :short xdoc-stuff))
      (description (lookup-keyword :description xdoc-stuff))
      (arg-descriptions (lookup-keyword :args xdoc-stuff))
      ((when (not (symbol-alistp arg-descriptions))) (er hard?
          'defmacrodoc
          "Ill-formed :args: ~x0."
          arg-descriptions))
      ((when (not (no-duplicatesp-equal (strip-cars arg-descriptions)))) (er hard?
          'defmacrodoc
          "Duplicate keys among the :args: ~x0."
          arg-descriptions))
      ((when (not short)) (er hard 'defmacrodoc "No :short supplied for ~x0" name))
      ((when (and macro-args (not arg-descriptions))) (er hard
          'defmacrodoc
          "No :args supplied for ~x0 (should contain descriptions of the macro args)"
          name)))
    `(progn (defmacro ,NAME ,MACRO-ARGS ,@DECLARES ,BODY)
      ,(DEFXDOC-FOR-MACRO-FN NAME MACRO-ARGS PARENTS SHORT ARG-DESCRIPTIONS
  DESCRIPTION STATE))))

defmacrodocmacro

(defmacro defmacrodoc
  (name macro-args &rest rest)
  `(make-event (defmacrodoc-fn ',NAME ',MACRO-ARGS ',REST state)))