		Search-engine friendly clone of the ACL2 documentation.

Compilation-database

Json-to-comp-db-entry

Signature
(json-to-comp-db-entry entry db warnings-onp warnings) → (mv erp db$ warnings$)
Arguments: entry — Guard (json::valuep entry).; db — Guard (comp-dbp db).; warnings-onp — Guard (booleanp warnings-onp).; warnings — Guard (acl2::msg-listp warnings).
Returns: db$ — Type (comp-dbp db$).; warnings$ — Type (acl2::msg-listp warnings$).

Definitions and Theorems

Function: json-to-comp-db-entry

(defun json-to-comp-db-entry (entry db warnings-onp warnings)
 (declare (xargs :guard (and (json::valuep entry)
                             (comp-dbp db)
                             (booleanp warnings-onp)
                             (acl2::msg-listp warnings))))
 (b* ((db (comp-db-fix db))
      (warnings (mbe :logic
                     (if (acl2::msg-listp warnings)
                         warnings
                       nil)
                     :exec warnings))
      ((reterr) nil warnings))
  (json::value-case
   entry :object
   (b* (((erp file)
         (json-to-comp-db-get-file entry))
        (warnings
             (if (and warnings-onp (assoc-equal file db))
                 (cons (msg$ "Found multiple entries for file: ~x0"
                             file)
                       warnings)
               warnings))
        ((erp output)
         (json-to-comp-db-get-output entry))
        ((erp directory)
         (json-to-comp-db-get-directory entry))
        ((erp exec arguments)
         (json-to-comp-db-get-exec-and-arguments entry))
        (entry (make-comp-db-entry :exec exec
                                   :directory directory
                                   :output output
                                   :arguments arguments)))
     (retok (cons (cons file entry)
                  (comp-db-fix db))
            warnings))
   :otherwise
   (retmsg$
    "Expected object type in ~
                           JSON compilation database entry.
                           Found ~x0 instead."
    (json::value-kind entry)))))

Theorem: comp-dbp-of-json-to-comp-db-entry.db$

(defthm comp-dbp-of-json-to-comp-db-entry.db$
  (b* (((mv acl2::?erp ?db$ ?warnings$)
        (json-to-comp-db-entry entry db warnings-onp warnings)))
    (comp-dbp db$))
  :rule-classes :rewrite)

Theorem: msg-listp-of-json-to-comp-db-entry.warnings$

(defthm msg-listp-of-json-to-comp-db-entry.warnings$
  (b* (((mv acl2::?erp ?db$ ?warnings$)
        (json-to-comp-db-entry entry db warnings-onp warnings)))
    (acl2::msg-listp warnings$))
  :rule-classes :rewrite)

Theorem: json-to-comp-db-entry-of-value-fix-entry

(defthm json-to-comp-db-entry-of-value-fix-entry
  (equal (json-to-comp-db-entry (json::value-fix entry)
                                db warnings-onp warnings)
         (json-to-comp-db-entry entry db warnings-onp warnings)))

Theorem: json-to-comp-db-entry-value-equiv-congruence-on-entry

(defthm json-to-comp-db-entry-value-equiv-congruence-on-entry
 (implies
  (json::value-equiv entry entry-equiv)
  (equal
      (json-to-comp-db-entry entry db warnings-onp warnings)
      (json-to-comp-db-entry entry-equiv db warnings-onp warnings)))
 :rule-classes :congruence)

Theorem: json-to-comp-db-entry-of-comp-db-fix-db

(defthm json-to-comp-db-entry-of-comp-db-fix-db
  (equal (json-to-comp-db-entry entry (comp-db-fix db)
                                warnings-onp warnings)
         (json-to-comp-db-entry entry db warnings-onp warnings)))

Theorem: json-to-comp-db-entry-comp-db-equiv-congruence-on-db

(defthm json-to-comp-db-entry-comp-db-equiv-congruence-on-db
 (implies
  (comp-db-equiv db db-equiv)
  (equal
      (json-to-comp-db-entry entry db warnings-onp warnings)
      (json-to-comp-db-entry entry db-equiv warnings-onp warnings)))
 :rule-classes :congruence)

Theorem: json-to-comp-db-entry-of-bool-fix-warnings-onp

(defthm json-to-comp-db-entry-of-bool-fix-warnings-onp
  (equal (json-to-comp-db-entry entry db (bool-fix warnings-onp)
                                warnings)
         (json-to-comp-db-entry entry db warnings-onp warnings)))

Theorem: json-to-comp-db-entry-iff-congruence-on-warnings-onp

(defthm json-to-comp-db-entry-iff-congruence-on-warnings-onp
 (implies
  (iff warnings-onp warnings-onp-equiv)
  (equal
      (json-to-comp-db-entry entry db warnings-onp warnings)
      (json-to-comp-db-entry entry db warnings-onp-equiv warnings)))
 :rule-classes :congruence)