		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modalist-named->indexed

Signature
(modalist-named->indexed x moddb &key (quiet 'nil)) → (mv errmsg xx)
Arguments: x — Guard (modalist-p x).; moddb — Guard (moddb-ok moddb).
Returns: xx — Type (modalist-p xx).

Definitions and Theorems

Function: modalist-named->indexed-fn

(defun
     modalist-named->indexed-fn
     (x moddb quiet)
     (declare (xargs :stobjs (moddb)))
     (declare (xargs :guard (and (modalist-p x) (moddb-ok moddb))))
     (declare (xargs :guard (svarlist-addr-p (modalist-vars x))))
     (let ((__function__ 'modalist-named->indexed))
          (declare (ignorable __function__))
          (b* ((x (modalist-fix x))
               ((when (atom x)) (mv nil nil))
               ((cons name mod) (car x))
               (modidx (moddb-modname-get-index name moddb))
               ((unless modidx)
                (and (not quiet)
                     (cw "Warning! Module ~x0 not found in moddb.~%"
                         name))
                (modalist-named->indexed (cdr x)
                                         moddb
                                         :quiet quiet))
               ((mv err1 first)
                (module-named->indexed mod modidx moddb))
               (- (clear-memoize-table 'svex-named->indexed))
               ((mv err2 rest)
                (modalist-named->indexed (cdr x)
                                         moddb
                                         :quiet quiet)))
              (mv (or err1 err2)
                  (cons (cons name first) rest)))))

Theorem: modalist-p-of-modalist-named->indexed.xx

(defthm modalist-p-of-modalist-named->indexed.xx
        (b* (((mv ?errmsg ?xx)
              (modalist-named->indexed-fn x moddb quiet)))
            (modalist-p xx))
        :rule-classes :rewrite)

Theorem: modalist-named->indexed-fn-of-modalist-fix-x

(defthm modalist-named->indexed-fn-of-modalist-fix-x
        (equal (modalist-named->indexed-fn (modalist-fix x)
                                           moddb quiet)
               (modalist-named->indexed-fn x moddb quiet)))

Theorem: modalist-named->indexed-fn-modalist-equiv-congruence-on-x

(defthm
  modalist-named->indexed-fn-modalist-equiv-congruence-on-x
  (implies (modalist-equiv x x-equiv)
           (equal (modalist-named->indexed-fn x moddb quiet)
                  (modalist-named->indexed-fn x-equiv moddb quiet)))
  :rule-classes :congruence)

Theorem: modalist-named->indexed-fn-of-moddb-fix-moddb

(defthm modalist-named->indexed-fn-of-moddb-fix-moddb
        (equal (modalist-named->indexed-fn x (moddb-fix moddb)
                                           quiet)
               (modalist-named->indexed-fn x moddb quiet)))

Theorem: modalist-named->indexed-fn-moddb-equiv-congruence-on-moddb

(defthm
  modalist-named->indexed-fn-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (modalist-named->indexed-fn x moddb quiet)
                  (modalist-named->indexed-fn x moddb-equiv quiet)))
  :rule-classes :congruence)

Theorem: modalist-all-idxaddr-okp-of-modalist-named->indexed

(defthm modalist-all-idxaddr-okp-of-modalist-named->indexed
        (b* (((mv err res)
              (modalist-named->indexed x moddb
                                       :quiet quiet)))
            (implies (and (moddb-ok moddb) (not err))
                     (modalist-all-idxaddr-okp res moddb))))