		Search-engine friendly clone of the ACL2 documentation.

Compilation-database

Preprocess-db-to-map

Signature
(preprocess-db-to-map db) → map
Arguments: db — Guard (comp-dbp db).
Returns: map — Type (acl2::string-stringlist-mapp map).

Definitions and Theorems

Function: preprocess-db-to-map

(defun preprocess-db-to-map (db)
  (declare (xargs :guard (comp-dbp db)))
  (b* ((db (comp-db-fix db))
       ((when (endp db)) nil)
       (file (car (first db)))
       ((comp-db-entry entry)
        (cdr (first db))))
    (omap::update file
                  (comp-db-arg-list-to-string-list entry.arguments)
                  (preprocess-db-to-map (rest db)))))

Theorem: string-stringlist-mapp-of-preprocess-db-to-map

(defthm string-stringlist-mapp-of-preprocess-db-to-map
  (b* ((map (preprocess-db-to-map db)))
    (acl2::string-stringlist-mapp map))
  :rule-classes :rewrite)

Theorem: preprocess-db-to-map-of-comp-db-fix-db

(defthm preprocess-db-to-map-of-comp-db-fix-db
  (equal (preprocess-db-to-map (comp-db-fix db))
         (preprocess-db-to-map db)))

Theorem: preprocess-db-to-map-comp-db-equiv-congruence-on-db

(defthm preprocess-db-to-map-comp-db-equiv-congruence-on-db
  (implies (comp-db-equiv db db-equiv)
           (equal (preprocess-db-to-map db)
                  (preprocess-db-to-map db-equiv)))
  :rule-classes :congruence)