docgen

(defun html-encode-str
  (x acc)
  (simple-html-encode-str x
    0
    (length x)
    acc))

(defun flexlist->defxdoc
  (x parents kwd-alist state)
  (declare (ignorable state))
  (b* (((flexlist x) x) (parents (getarg :parents parents kwd-alist))
      (short (or (getarg :short nil kwd-alist)
          (cat "A list of @(see? "
            (full-escape-symbol x.elt-type)
            ") objects.")))
      (long (or (getarg :long nil kwd-alist)
          (cat "<p>This is an ordinary @(see fty::deflist).</p>"))))
    (mv `((defxdoc ,FTY::X.NAME
         :parents ,FTY::PARENTS
         :short ,FTY::SHORT
         :long ,FTY::LONG
         :no-override t))
      state)))

(defun flexalist->defxdoc
  (x parents kwd-alist state)
  (declare (ignorable state))
  (b* (((flexalist x) x) (parents (getarg :parents parents kwd-alist))
      (key-link (if x.key-type
          (cat "@(see? "
            (full-escape-symbol x.key-type)
            ")")
          "anything"))
      (val-link (if x.val-type
          (cat "@(see? "
            (full-escape-symbol x.val-type)
            ")")
          "anything"))
      (short (or (getarg :short nil kwd-alist)
          (cat "An alist mapping "
            key-link
            " to "
            val-link
            ".")))
      (long (or (getarg :long nil kwd-alist)
          (cat "<p>This is an ordinary @(see fty::defalist).</p>"))))
    (mv `((defxdoc ,FTY::X.NAME
         :parents ,FTY::PARENTS
         :short ,FTY::SHORT
         :long ,FTY::LONG
         :no-override t))
      state)))

(defun defprod-field-doc
  (x acc base-pkg state)
  (b* (((flexprod-field x) x) (acc (revappend-chars "<dt>" acc))
      ((mv name-str state) (fmt-to-str-orig x.name base-pkg state))
      (acc (html-encode-str name-str acc))
      (acc (b* (((when (eq x.type nil)) acc) (fixtype (find-fixtype x.type
                (get-fixtypes-alist (w state))))
            (target (if fixtype
                (fixtype->topic fixtype)
                x.type))
            (acc (revappend-chars " &mdash; @(see? " acc))
            (acc (revappend-chars (full-escape-symbol target)
                acc))
            (acc (revappend-chars ")" acc)))
          acc))
      (acc (revappend-chars "</dt>" acc))
      (acc (cons #\
 acc))
      (acc (b* (((when (equal x.doc "")) acc) (acc (revappend-chars "<dd>" acc))
            (acc (revappend-chars x.doc acc))
            (acc (revappend-chars "</dd>" acc))
            (acc (cons #\
 acc)))
          acc))
      (acc (cons #\
 acc)))
    (mv acc state)))

(defun defprod-fields-doc-aux
  (x acc base-pkg state)
  (b* (((when (atom x)) (mv acc state)) ((mv acc state) (defprod-field-doc (car x)
          acc
          base-pkg
          state)))
    (defprod-fields-doc-aux (cdr x)
      acc
      base-pkg
      state)))

(defun defprod-fields-doc
  (x acc base-pkg state)
  (b* ((acc (revappend-chars "<dl>" acc)) ((mv acc state) (defprod-fields-doc-aux x
          acc
          base-pkg
          state))
      (acc (revappend-chars "</dl>" acc)))
    (mv acc state)))

(defun defprod-main-description
  (prod base-pkg acc state)
  (b* (((flexprod prod) prod) ((unless (consp prod.fields)) (mv (revappend-chars "<p>This is an atomic/empty structure; it has no fields.</p>"
            acc)
          state))
      (acc (revappend-chars "<h5>Fields</h5>" acc))
      (acc (cons #\
 acc))
      ((mv acc state) (defprod-fields-doc prod.fields
          acc
          base-pkg
          state))
      ((when (eq prod.require t)) (mv acc state))
      (acc (revappend-chars "<h5>Additional Requirements</h5>"
          acc))
      (acc (revappend-chars "<p>The following invariant is enforced on the fields:</p>"
          acc))
      ((mv req-str state) (fmt-to-str-orig prod.require
          base-pkg
          state))
      (acc (revappend-chars "<code>" acc))
      (acc (html-encode-str req-str acc))
      (acc (revappend-chars "</code>" acc)))
    (mv acc state)))

(defun defprod-main-autodoc
  (x parents
    kwd-alist
    base-pkg
    state)
  (b* (((flexsum x) x) (prod (car x.prods))
      (parents (getarg :parents parents kwd-alist))
      (short (cdr (assoc :short kwd-alist)))
      (long (cdr (assoc :long kwd-alist)))
      (acc nil)
      (acc (revappend-chars "<p>This is a product type introduced by @(see fty::defprod).</p>"
          acc))
      (acc (cons #\
 acc))
      ((mv acc state) (defprod-main-description prod
          base-pkg
          acc
          state))
      (acc `(revappend-chars ,(OR FTY::LONG "") ',FTY::ACC))
      (long `(rchars-to-string ,FTY::ACC)))
    (mv `((defxdoc ,FTY::X.NAME
         :parents ,FTY::PARENTS
         :short ,FTY::SHORT
         :long ,FTY::LONG
         :no-override t))
      state)))

(defun defprod-ctor-optional-fields
  (field-names pad acc)
  (declare (xargs :guard (and (symbol-listp field-names)
        (stringp pad))))
  (b* (((when (atom field-names)) acc) (name1 (name-low (symbol-name (car field-names))))
      (len1 (length name1))
      (acc (revappend-chars "[:" acc))
      (acc (simple-html-encode-str name1
          0
          len1
          acc))
      (acc (revappend-chars " <" acc))
      (acc (simple-html-encode-str name1
          0
          len1
          acc))
      (acc (revappend-chars ">]" acc))
      (acc (if (consp (cdr field-names))
          (revappend-chars pad acc)
          acc)))
    (defprod-ctor-optional-fields (cdr field-names)
      pad
      acc)))

(defun defprod-ctor-optional-call
  (name line1 field-names)
  (declare (xargs :guard (and (symbolp name)
        (stringp line1)
        (symbol-listp field-names))))
  (b* ((ctor-name (name-low (symbol-name name))) (pad (implode (cons #\

            (make-list (+ 2 (length ctor-name))
              :initial-element #\ ))))
      (acc nil)
      (acc (revappend-chars "<code>" acc))
      (acc (cons #\
 acc))
      (acc (cons #\( acc))
      (acc (simple-html-encode-str ctor-name
          0
          (length ctor-name)
          acc))
      (acc (cons #\  acc))
      (acc (if (equal line1 "")
          acc
          (revappend-chars pad
            (revappend-chars line1 acc))))
      (acc (defprod-ctor-optional-fields field-names
          pad
          acc))
      (acc (cons #\) acc))
      (acc (cons #\
 acc))
      (acc (revappend-chars "</code>" acc)))
    (rchars-to-string acc)))

(defun defprod-ctor-autodoc
  (prod)
  (b* (((flexprod prod) prod) ((when prod.no-ctor-macros) nil)
      (foo prod.type-name)
      (make-foo-fn prod.ctor-name)
      (make-foo prod.ctor-macro)
      (change-foo (da-changer-name prod.ctor-name))
      (plain-foo (let* ((foo-low (name-low (symbol-name foo))) (acc nil)
            (acc (revappend-chars "<tt>" acc))
            (acc (simple-html-encode-str foo-low
                0
                (length foo-low)
                acc))
            (acc (revappend-chars "</tt>" acc)))
          (rchars-to-string acc)))
      (see-foo (see foo))
      (see-make-foo (see make-foo))
      (see-change-foo (see change-foo))
      (fieldnames (flexprod-fields->names prod.fields))
      (call-make-foo (defprod-ctor-optional-call make-foo
          ""
          fieldnames))
      (call-change-foo (defprod-ctor-optional-call change-foo
          "x"
          fieldnames))
      (def-make-foo-fn (cat "@(def "
          (full-escape-symbol make-foo-fn)
          ")"))
      (def-make-foo (cat "@(def "
          (full-escape-symbol make-foo)
          ")"))
      (def-change-foo (cat "@(def "
          (full-escape-symbol change-foo)
          ")")))
    `((defxdoc ,FTY::MAKE-FOO
       :parents (,FTY::FOO)
       :short ,(STR::CAT "Basic constructor macro for " FTY::SEE-FOO " structures.")
       :long ,(STR::CAT "<h5>Syntax</h5>" FTY::CALL-MAKE-FOO
  "<p>This is the usual way to construct " FTY::SEE-FOO
  " structures.  It simply conses together a structure with the
                specified fields.</p>

                <p>This macro generates a new "
  FTY::PLAIN-FOO " structure from
                scratch.  See also "
  FTY::SEE-CHANGE-FOO ", which can \"change\" an
                existing structure, instead.</p>"
  "<h3>Definition</h3>

                <p>This is an ordinary @('make-') macro introduced by @(see
                fty::defprod).</p>"
  FTY::DEF-MAKE-FOO FTY::DEF-MAKE-FOO-FN)
       :no-override t) (defxdoc ,FTY::CHANGE-FOO
        :parents (,FTY::FOO)
        :short ,(STR::CAT "Modifying constructor for " FTY::SEE-FOO " structures.")
        :long ,(STR::CAT "<h5>Syntax</h5>" FTY::CALL-CHANGE-FOO
  "<p>This is an often useful alternative to " FTY::SEE-MAKE-FOO ".</p>

                <p>We construct a new "
  FTY::SEE-FOO " structure that is a copy of
                @('x'), except that you can explicitly change some particular
                fields.  Any fields you don't mention just keep their values
                from @('x').</p>

                <h3>Definition</h3>

                <p>This is an ordinary @('change-') macro introduced by @(see
                fty::defprod).</p>"
  FTY::DEF-CHANGE-FOO)
        :no-override t))))

(defun defprod->defxdoc
  (x parents
    kwd-alist
    base-pkg
    state)
  (b* (((flexsum x) x) (prod (car x.prods))
      ((flexprod prod) prod)
      (foo x.name)
      (foo-p x.pred)
      (foo-fix x.fix)
      (make-foo prod.ctor-macro)
      (change-foo (da-changer-name foo))
      ((mv main-doc state) (defprod-main-autodoc x
          parents
          kwd-alist
          base-pkg
          state))
      (make/change (defprod-ctor-autodoc prod))
      (doc-events (append main-doc
          make/change
          `((order-subtopics ,FTY::FOO
             (,FTY::FOO-P ,FTY::FOO-FIX
               ,@(AND (NOT FTY::PROD.NO-CTOR-MACROS) `(,FTY::MAKE-FOO ,FTY::CHANGE-FOO))))))))
    (mv doc-events state)))

(defun deftagsum-prod-doc
  (sum prod parents base-pkg state)
  (b* (((flexsum sum) sum) ((flexprod prod) prod)
      (acc nil)
      (acc (revappend-chars "<p>This is a product type, introduced by @(see "
          acc))
      (acc (revappend-chars (full-escape-symbol sum.typemacro)
          acc))
      (acc (revappend-chars ") in support of @(see " acc))
      (acc (revappend-chars (full-escape-symbol sum.name)
          acc))
      (acc (revappend-chars ").</p>" acc))
      (acc (cons #\
 acc))
      ((mv acc state) (defprod-main-description prod
          base-pkg
          acc
          state))
      (acc `(revappend-chars ,(OR FTY::PROD.LONG "") ',FTY::ACC))
      (long `(rchars-to-string ,FTY::ACC))
      (top-doc `((defxdoc ,FTY::PROD.TYPE-NAME
           :parents ,FTY::PARENTS
           :short ,FTY::PROD.SHORT
           :long ,FTY::LONG
           :no-override t)))
      (make/change (defprod-ctor-autodoc prod))
      (make-foo prod.ctor-macro)
      (change-foo (da-changer-name prod.ctor-name)))
    (mv (append top-doc
        make/change
        (and (not prod.no-ctor-macros)
          `((order-subtopics ,FTY::PROD.TYPE-NAME
             (,FTY::MAKE-FOO ,FTY::CHANGE-FOO)))))
      state)))

(defun deftagsum-prods-doc
  (sum prods parents base-pkg state)
  (b* (((when (atom prods)) (mv nil state)) ((mv events1 state) (deftagsum-prod-doc sum
          (car prods)
          parents
          base-pkg
          state))
      ((mv events2 state) (deftagsum-prods-doc sum
          (cdr prods)
          parents
          base-pkg
          state)))
    (mv (append events1 events2) state)))

(defun deftagsum-summarize-prod
  (sum prod base-pkg acc state)
  (declare (ignorable sum base-pkg))
  (b* (((flexprod prod) prod) (acc (revappend-chars "<dt><tt>" acc))
      ((mv kind-str state) (fmt-to-str-orig prod.kind
          base-pkg
          state))
      (acc (html-encode-str kind-str acc))
      (acc (revappend-chars "</tt> &rarr; @(see " acc))
      (acc (revappend-chars (full-escape-symbol prod.type-name)
          acc))
      (acc (revappend-chars ")</dt>" acc))
      (acc (cons #\
 acc))
      ((unless prod.short) (mv acc state))
      (acc (revappend-chars "<dd>" acc))
      (acc (revappend-chars prod.short acc))
      (acc (revappend-chars "</dd>" acc))
      (acc (cons #\
 acc)))
    (mv acc state)))

(defun deftagsum-summarize-prods
  (sum prods base-pkg acc state)
  (b* (((when (atom prods)) (mv acc state)) ((mv acc state) (deftagsum-summarize-prod sum
          (car prods)
          base-pkg
          acc
          state))
      ((mv acc state) (deftagsum-summarize-prods sum
          (cdr prods)
          base-pkg
          acc
          state)))
    (mv acc state)))

(defun flexprodlist->type-names
  (x)
  (if (atom x)
    nil
    (cons (flexprod->type-name (car x))
      (flexprodlist->type-names (cdr x)))))

(defun flexsum-case-macro-defxdoc.examples
  (kinds acc)
  (b* (((when (atom kinds)) acc) (acc (cons #\
 acc))
      (acc (revappend-chars "      :" acc))
      (acc (revappend-chars (downcase-string (symbol-name (car kinds)))
          acc))
      (acc (revappend-chars " ..." acc)))
    (flexsum-case-macro-defxdoc.examples (cdr kinds)
      acc)))

(defun flexsum-case-macro-defxdoc
  (sum)
  (b* (((flexsum sum) sum) (kinds (flexprods->kinds sum.prods))
      (name-link (see sum.name))
      (name-plain (downcase-string (symbol-name sum.name)))
      (case-str (downcase-string (symbol-name sum.case)))
      (kind-fn-str (downcase-string (symbol-name sum.kind)))
      (kind1-str (downcase-string (symbol-name (car kinds))))
      (examples (rchars-to-string (flexsum-case-macro-defxdoc.examples kinds nil))))
    `((defxdoc ,FTY::SUM.CASE
       :parents (,FTY::SUM.NAME)
       :short ,(FTY::CAT "Case macro for the different kinds of " FTY::NAME-LINK
  " structures.")
       :long ,(FTY::CAT "<p>This is an @(see fty::fty) sum-type case macro,
typically introduced by @(see fty::defflexsum) or @(see fty::deftagsum).  It
allows you to safely check the type of a "
  FTY::NAME-LINK " structure, or to split
into cases based on its type.</p>

<h3>Short Form</h3>

<p>In its short form, @('"
  FTY::CASE-STR "') allows you to safely check the type of
a @('"
  FTY::NAME-PLAIN "') structure.  For example:</p>

@({
    ("
  FTY::CASE-STR " x :" FTY::KIND1-STR ")
})
"
  (IF FTY::SUM.KIND
      (FTY::CAT "<p>is essentially just a safer alternative to writing:</p>
              @({
                  (equal ("
       FTY::KIND-FN-STR " x) :" FTY::KIND1-STR ")
              })

              <p>Why is using "
       FTY::CASE-STR " safer?  When we directly inspect the
              kind with @('equal'), there is no static checking being done to
              ensure that, e.g., @(':"
       FTY::KIND1-STR "') is a valid kind of " FTY::NAME-LINK
       " structure.  That means there is nothing to save you
              if, later, you change the kind keyword for this type from @(':"
       FTY::KIND1-STR "') to something else.  It also means you get no help
              if you just make a typo when writing the @(':"
       FTY::KIND1-STR "')
              symbol.  Over the course of developing VL, we found that such
              issues were very frequent sources of errors!</p>")
      (FTY::CAT "<p>can be used to determine whether @('x') is a @('"
       FTY::KIND1-STR "') instead of some other kind of " FTY::NAME-PLAIN
       " structure.</p>"))
  "<h3>Long Form</h3>

<p>In its longer form, @('"
  FTY::CASE-STR "') allows you to split into cases based
on the kind of structure you are looking at.  A typical example would be:</p>

@({
    ("
  FTY::CASE-STR " x" FTY::EXAMPLES ")
})

<p>It is also possible to consolidate ``uninteresting'' cases using
@(':otherwise').</p>

<p>For convenience, the case macro automatically binds the fields of @('x') for
you, as appropriate for each case.  That is, in the @(':"
  FTY::KIND1-STR "') case,
you can use @(see fty::defprod)-style @('foo.bar') style accessors for @('x')
without having to explicitly add a @('"
  FTY::KIND1-STR "') @(see b*)
binder.</p>")
       :no-override t))))

(defun deftagsum->defxdoc
  (x parents
    kwd-alist
    base-pkg
    state)
  (declare (ignorable x parents base-pkg))
  (b* (((flexsum x) x) (short (cdr (assoc :short kwd-alist)))
      (long (cdr (assoc :long kwd-alist)))
      (acc nil)
      (acc (revappend-chars "<p>This is a tagged union type, introduced by @(see fty::deftagsum).</p>"
          acc))
      (acc (cons #\
 acc))
      (acc (revappend-chars "<h5>Member Tags &rarr; Types</h5>"
          acc))
      (acc (revappend-chars "<dl>" acc))
      ((mv acc state) (deftagsum-summarize-prods x
          x.prods
          base-pkg
          acc
          state))
      (acc (revappend-chars "</dl>" acc))
      (acc (cons #\
 acc))
      (acc `(revappend-chars ,(OR FTY::LONG "") ',FTY::ACC))
      (long `(rchars-to-string ,FTY::ACC))
      (main-doc `((defxdoc ,FTY::X.NAME
           :parents ,FTY::PARENTS
           :short ,FTY::SHORT
           :long ,FTY::LONG
           :no-override t)))
      (type-names (flexprodlist->type-names x.prods))
      (case-doc (flexsum-case-macro-defxdoc x))
      ((mv prods-doc state) (deftagsum-prods-doc x
          x.prods
          (list x.name)
          base-pkg
          state)))
    (mv (append main-doc
        prods-doc
        case-doc
        `((order-subtopics ,FTY::X.NAME
           ,(REMOVE NIL
         (LIST* FTY::X.PRED FTY::X.KIND FTY::X.CASE FTY::X.FIX FTY::X.EQUIV
                FTY::X.COUNT FTY::TYPE-NAMES)))))
      state)))

(defun defflexsum->defxdoc
  (x parents
    kwd-alist
    base-pkg
    state)
  (declare (ignorable x parents base-pkg))
  (b* (((flexsum x) x) (short (cdr (assoc :short kwd-alist)))
      (long (cdr (assoc :long kwd-alist)))
      (acc nil)
      (acc (revappend-chars "<p>This is a sum-of-products (i.e., union) type, introduced by @(see fty::defflexsum).</p>"
          acc))
      (acc (cons #\
 acc))
      (acc (revappend-chars "<h5>Members</h5>" acc))
      (acc (revappend-chars "<dl>" acc))
      ((mv acc state) (deftagsum-summarize-prods x
          x.prods
          base-pkg
          acc
          state))
      (acc (revappend-chars "</dl>" acc))
      (acc (cons #\
 acc))
      (acc `(revappend-chars ,(OR FTY::LONG "") ',FTY::ACC))
      (long `(rchars-to-string ,FTY::ACC))
      (main-doc `((defxdoc ,FTY::X.NAME
           :parents ,FTY::PARENTS
           :short ,FTY::SHORT
           :long ,FTY::LONG
           :no-override t)))
      (type-names (flexprodlist->type-names x.prods))
      (sum-name-shared-with-prod-name (member x.name type-names))
      (parents (if sum-name-shared-with-prod-name
          parents
          (list x.name)))
      ((mv prods-doc state) (deftagsum-prods-doc x
          x.prods
          parents
          base-pkg
          state)))
    (mv (append (and (not sum-name-shared-with-prod-name)
          main-doc)
        prods-doc
        `((order-subtopics ,FTY::X.NAME
           ,(REMOVE NIL
         (REMOVE FTY::X.NAME
                 (LIST* FTY::X.PRED FTY::X.FIX FTY::X.KIND FTY::X.EQUIV
                        FTY::X.COUNT FTY::TYPE-NAMES))))))
      state)))

(defun defoption->defxdoc
  (x parents
    kwd-alist
    base-pkg
    state)
  (declare (ignorable x parents base-pkg))
  (b* (((flexsum x) x) ((fixtype base) (cdr (assoc :basetype x.kwd-alist)))
      (short (or (cdr (assoc :short kwd-alist))
          (cat "Option type; @(see? "
            (full-escape-symbol base.name)
            ") or @('nil').")))
      (long (cdr (assoc :long kwd-alist)))
      (acc nil)
      (acc (revappend-chars "<p>This is an option type introduced by @(see fty::defoption).
              Note that @('defoption') is just a wrapper for @(see
              fty::defflexsum), so there are @(':none') and @(':some') member
              types, a case macro, and so forth.</p>"
          acc))
      (acc (revappend-chars "<h5>Member Types</h5>" acc))
      (acc (revappend-chars "<dl>" acc))
      ((mv acc state) (deftagsum-summarize-prods x
          x.prods
          base-pkg
          acc
          state))
      (acc (revappend-chars "</dl>" acc))
      (acc (cons #\
 acc))
      (acc `(revappend-chars ,(OR FTY::LONG "") ',FTY::ACC))
      (long `(rchars-to-string ,FTY::ACC))
      ((mv prods-doc state) (deftagsum-prods-doc x
          x.prods
          (list x.name)
          base-pkg
          state))
      (case-doc (flexsum-case-macro-defxdoc x))
      (main-doc `((defxdoc ,FTY::X.NAME
           :parents ,FTY::PARENTS
           :short ,FTY::SHORT
           :long ,FTY::LONG
           :no-override t))))
    (mv (append main-doc
        prods-doc
        case-doc
        `((order-subtopics ,FTY::X.NAME
           ,(REMOVE NIL (LIST FTY::X.PRED FTY::X.FIX FTY::X.EQUIV FTY::X.COUNT)))))
      state)))

(defun flexset->defxdoc
  (x parents kwd-alist state)
  (declare (ignorable state))
  (b* (((flexset x) x) (parents (getarg :parents parents kwd-alist))
      (short (or (getarg :short nil kwd-alist)
          (cat "A set of @(see? "
            (full-escape-symbol x.elt-type)
            ") objects.")))
      (long (or (getarg :long nil kwd-alist)
          (cat "<p>This is an ordinary @(see fty::defset).</p>"))))
    (mv `((defxdoc ,FTY::X.NAME
         :parents ,FTY::PARENTS
         :short ,FTY::SHORT
         :long ,FTY::LONG
         :no-override t))
      state)))

(defun flexomap->defxdoc
  (x parents kwd-alist state)
  (declare (ignorable state))
  (b* (((flexomap x) x) (parents (getarg :parents parents kwd-alist))
      (key-link (if x.key-type
          (cat "@(see? "
            (full-escape-symbol x.key-type)
            ")")
          "anything"))
      (val-link (if x.val-type
          (cat "@(see? "
            (full-escape-symbol x.val-type)
            ")")
          "anything"))
      (short (or (getarg :short nil kwd-alist)
          (cat "An omap mapping "
            key-link
            " to "
            val-link
            ".")))
      (long (or (getarg :long nil kwd-alist)
          (cat "<p>This is an ordinary @(see fty::defomap).</p>"))))
    (mv `((defxdoc ,FTY::X.NAME
         :parents ,FTY::PARENTS
         :short ,FTY::SHORT
         :long ,FTY::LONG
         :no-override t))
      state)))

(defun flextranssum-members->xdoc
  (members acc state)
  (b* (((when (atom members)) acc) ((flextranssum-member x1) (car members))
      (target (fixtype->topic (find-fixtype x1.name
            (get-fixtypes-alist (w state)))))
      (acc (revappend-chars "<li>" acc))
      (acc (revappend-chars "@(see? " acc))
      (acc (revappend-chars (full-escape-symbol target)
          acc))
      (acc (revappend-chars ")</li>" acc))
      (acc (cons #\
 acc)))
    (flextranssum-members->xdoc (cdr members)
      acc
      state)))

(defun flextranssum->defxdoc
  (x parents kwd-alist state)
  (b* (((flextranssum x) x) (short (cdr (assoc :short kwd-alist)))
      (long (cdr (assoc :long kwd-alist)))
      (acc nil)
      (acc (revappend-chars "<p>This is a ``transparent'' sum type introduced using @(see fty::deftranssum).  It
              is simply any one of the following types:</p>"
          acc))
      (acc (revappend-chars "<ul>" acc))
      (acc (cons #\
 acc))
      (acc (flextranssum-members->xdoc x.members
          acc
          state))
      (acc (revappend-chars "</ul>" acc))
      (acc (cons #\
 acc))
      (acc `(revappend-chars ,(OR FTY::LONG "") ',FTY::ACC))
      (long `(rchars-to-string ,FTY::ACC))
      (main-doc `((defxdoc ,FTY::X.NAME
           :parents ,FTY::PARENTS
           :short ,FTY::SHORT
           :long ,FTY::LONG
           :no-override t))))
    (mv (append main-doc
        `((order-subtopics ,FTY::X.NAME
           (,FTY::X.PRED ,FTY::X.FIX ,FTY::X.EQUIV))))
      state)))

(defun flexsum->defxdoc
  (x parents kwd-alist state)
  (b* ((__function__ 'flexsum->defxdoc) ((flexsum x) x)
      (parents (or (cdr (assoc :parents kwd-alist)) parents))
      (base-pkg (pkg-witness (f-get-global 'current-package state)))
      ((unless (symbol-listp parents)) (mv (raise "~x0: :parents must be a list of symbols."
            x.name)
          state)))
    (case x.typemacro
      (defprod (defprod->defxdoc x
          parents
          kwd-alist
          base-pkg
          state))
      (deftagsum (deftagsum->defxdoc x
          parents
          kwd-alist
          base-pkg
          state))
      (defflexsum (defflexsum->defxdoc x
          parents
          kwd-alist
          base-pkg
          state))
      (defoption (defoption->defxdoc x
          parents
          kwd-alist
          base-pkg
          state))
      (t (mv (raise "~x0: unknown typemacro" x.name)
          state)))))

(defun flextype->defxdoc
  (x parents kwd-alist state)
  (b* ((__function__ 'flextype->defxdoc) ((mv events state) (with-flextype-bindings x
          (flex*->defxdoc x
            parents
            (append kwd-alist (flex*->kwd-alist x))
            state)
          :default (mv (raise "Unexpected flex type: ~x0." (tag x))
            state))))
    (mv `(progn . ,FTY::EVENTS) state)))

(defun flextypes-collect-defxdoc
  (types parents)
  (if (atom types)
    nil
    (cons `(make-event (b* (((mv val state) (flextype->defxdoc ',(CAR FTY::TYPES)
               ',FTY::PARENTS
               nil
               state)))
          (value val)))
      (flextypes-collect-defxdoc (cdr types)
        parents))))

(defun remove-topic
  (name x)
  (declare (xargs :mode :program))
  (if (atom x)
    nil
    (if (equal (cdr (assoc :name (car x))) name)
      (cdr x)
      (cons (car x)
        (remove-topic name (cdr x))))))

(defun find-subtype-kwd-alist
  (types name)
  (if (atom types)
    (mv nil nil)
    (with-flextype-bindings (x (car types))
      (if (eq name (flex*->name x))
        (mv (flex*->kwd-alist x) x)
        (find-subtype-kwd-alist (cdr types) name))
      :default (find-subtype-kwd-alist (cdr types) name))))

(defun flextypes-final-xdoc-fn
  (x world)
  (b* (((flextypes x) x) (parents-look (assoc :parents x.kwd-alist))
      (short (getarg :short nil x.kwd-alist))
      (long (getarg :long nil x.kwd-alist))
      ((mv sub-kwd-alist subtype) (find-subtype-kwd-alist x.types x.name))
      (sub-parents-look (assoc :parents sub-kwd-alist))
      ((when (and parents-look sub-parents-look)) (er hard?
          'deftypes
          "Parents listed for both top-level ~x0 and type ~x0.~%"
          x.name))
      (parents (or (cdr parents-look)
          (cdr sub-parents-look)
          (get-default-parents world)
          '(undocumented)))
      (sub-short (getarg :short nil sub-kwd-alist))
      (sub-long (getarg :long nil sub-kwd-alist))
      ((unless subtype) `(defxdoc ,FTY::X.NAME
          :parents ,FTY::PARENTS
          :short ,FTY::SHORT
          :long ,FTY::LONG
          :no-override t))
      ((when (and short sub-short)) (er hard?
          'deftypes
          "Can't give a top-level :short when you are also ~
                   putting :short documentation on the interior ~x0."
          x.name))
      ((when (and long sub-long)) (er hard?
          'deftypes
          "Can't give a top-level :long when you are also ~
                   putting :long documentation on the interior ~x0."
          x.name))
      (short (or short sub-short))
      (long (or long sub-long))
      (new-event `(make-event (b* (((mv val state) (flextype->defxdoc ',FTY::SUBTYPE
                 ',FTY::PARENTS
                 '((:short . ,FTY::SHORT) (:long . ,FTY::LONG))
                 state)))
            (value val)))))
    `(progn (table xdoc
        'doc
        (remove-topic ',FTY::X.NAME
          (get-xdoc-table world)))
      ,FTY::NEW-EVENT)))

(defun flextypes-defxdoc
  (x world)
  (b* (((flextypes x) x) (parents-look (assoc :parents x.kwd-alist))
      (mutually-recursive-p (consp (cdr x.types)))
      (parents (or (cdr parents-look)
          (get-default-parents world)
          '(undocumented)))
      (parents-for-each-type (if mutually-recursive-p
          (list x.name)
          parents)))
    (append (flextypes-collect-defxdoc x.types
        parents-for-each-type)
      `((flextypes-final-xdoc ,FTY::X)))))