		Search-engine friendly clone of the ACL2 documentation.

Database

Components-of-flexoption-with-name

Components of a named option type.

Signature
(components-of-flexoption-with-name name fty-table) → (mv base-name some-accessor)
Arguments: name — Guard (symbolp name).; fty-table — Guard (alistp fty-table).
Returns: base-name — Type (symbolp base-name).; some-accessor — Type (symbolp some-accessor).

We return the name of the base type, and the name of the accessor for the :some case. These are both nil if the given option type name does not resolve to an actual option type.

We look up the information for the option type. We find the product for the :some summand. We obtain the field recognizer and accessor. We use the recognizer to look up the base type.

Definitions and Theorems

Function: components-of-flexoption-with-name

(defun components-of-flexoption-with-name (name fty-table)
 (declare (xargs :guard (and (symbolp name)
                             (alistp fty-table))))
 (let ((__function__ 'components-of-flexoption-with-name))
  (declare (ignorable __function__))
  (b*
   ((flextype (flextype-with-name name fty-table))
    ((unless flextype) (mv nil nil))
    ((unless (flexsum-p flextype))
     (mv nil nil))
    ((unless (eq (flexsum->typemacro flextype)
                 'defoption))
     (mv nil nil))
    (flexprod-list (flexsum->prods flextype))
    ((unless (and (flexprod-listp flexprod-list)
                  (consp flexprod-list)
                  (consp (cdr flexprod-list))
                  (endp (cddr flexprod-list))))
     (raise "Internal error: malformed option products ~x0."
            flexprod-list)
     (mv nil nil))
    (flexprod1 (first flexprod-list))
    (flexprod2 (second flexprod-list))
    (flexprod
     (cond
        ((eq (flexprod->kind flexprod1) :some)
         flexprod1)
        ((eq (flexprod->kind flexprod2) :some)
         flexprod2)
        (t (prog2$ (raise "Internal error: no :SOME product in ~x0."
                          flexprod-list)
                   flexprod1))))
    (flexfield-list (flexprod->fields flexprod))
    ((unless (and (flexprod-field-listp flexfield-list)
                  (= (len flexfield-list) 1)))
     (raise "Internal error: malformed option :SOME fields ~x0."
            flexfield-list)
     (mv nil nil))
    (flexfield (car flexfield-list))
    (base-recog (flexprod-field->type flexfield))
    ((unless (symbolp base-recog))
     (raise "Internal error: malformed :SOME field recognizer ~x0."
            base-recog)
     (mv nil nil))
    (base-flextype (flextype-with-recognizer base-recog fty-table))
    (base-name (flextype->name base-flextype))
    ((unless (symbolp base-name))
     (raise "Internal error: malformed type name ~x0."
            base-name)
     (mv nil nil))
    (some-accessor (flexprod-field->acc-name flexfield))
    ((unless (symbolp some-accessor))
     (raise "Internal error: malformed accessor name ~x0."
            some-accessor)
     (mv nil nil)))
   (mv base-name some-accessor))))

Theorem: symbolp-of-components-of-flexoption-with-name.base-name

(defthm symbolp-of-components-of-flexoption-with-name.base-name
  (b* (((mv ?base-name ?some-accessor)
        (components-of-flexoption-with-name name fty-table)))
    (symbolp base-name))
  :rule-classes :rewrite)

Theorem: symbolp-of-components-of-flexoption-with-name.some-accessor

(defthm symbolp-of-components-of-flexoption-with-name.some-accessor
  (b* (((mv ?base-name ?some-accessor)
        (components-of-flexoption-with-name name fty-table)))
    (symbolp some-accessor))
  :rule-classes :rewrite)