		Search-engine friendly clone of the ACL2 documentation.

Database

Flextypes-containing-flextype

Find, in the FTY table, the information for a type clique containing a type of the given name.

Signature
(flextypes-containing-flextype name fty-table) → flextype?
Arguments: name — Guard (symbolp name).; fty-table — Guard (alistp fty-table).

Each type has a unique name, so we stop as soon as we find a match. We return nil if there is no match.

Based on the format as described in database, we do an outer loop on the entries of the table, and for each element an inner loop on the elements of the mutually recursive clique (which may be a singleton).

Definitions and Theorems

Function: flextypes-containing-flextype-loop

(defun flextypes-containing-flextype-loop (name flextype-list)
  (declare (xargs :guard (symbolp name)))
  (let ((__function__ 'flextypes-containing-flextype-loop))
    (declare (ignorable __function__))
    (b* (((when (atom flextype-list)) nil)
         (flextype (car flextype-list))
         (foundp (cond ((flexsum-p flextype)
                        (eq name (flexsum->name flextype)))
                       ((flexlist-p flextype)
                        (eq name (flexlist->name flextype)))
                       ((flexalist-p flextype)
                        (eq name (flexalist->name flextype)))
                       ((flextranssum-p flextype)
                        (eq name (flextranssum->name flextype)))
                       ((flexset-p flextype)
                        (eq name (flexset->name flextype)))
                       ((flexomap-p flextype)
                        (eq name (flexomap->name flextype)))
                       (t nil))))
      (or foundp
          (flextypes-containing-flextype-loop
               name (cdr flextype-list))))))

Function: flextypes-containing-flextype

(defun flextypes-containing-flextype (name fty-table)
 (declare (xargs :guard (and (symbolp name)
                             (alistp fty-table))))
 (let ((__function__ 'flextypes-containing-flextype))
   (declare (ignorable __function__))
   (b*
     (((when (endp fty-table)) nil)
      ((cons & flextypes) (car fty-table))
      ((unless (flextypes-p flextypes))
       (raise "Internal error: malformed type clique ~x0."
              flextypes))
      (flextype-list (flextypes->types flextypes))
      (foundp
           (flextypes-containing-flextype-loop name flextype-list)))
     (if foundp flextypes
       (flextypes-containing-flextype name (cdr fty-table))))))