		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))))