		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-transunit-ensemble

Validate a translation unit ensemble.

Signature
(valid-transunit-ensemble tunits ienv keep-going) → (mv erp new-tunits)
Arguments: tunits — Guard (transunit-ensemblep tunits).; ienv — Guard (ienvp ienv).; keep-going — Guard (booleanp keep-going).
Returns: erp — Type (maybe-msgp erp).; new-tunits — Type (transunit-ensemblep new-tunits).

We validate each translation unit. As mentioned in valid-transunit, we annotate the translation unit with the finval validation table. For now we do no make any use of the returned table, but in the future we should use it to validate the externally linked identifiers across different translation units of a translation unit ensemble.

Definitions and Theorems

Function: valid-transunit-ensemble-loop

(defun valid-transunit-ensemble-loop
       (map externals next-uid ienv keep-going)
 (declare (xargs :guard (and (filepath-transunit-mapp map)
                             (valid-externalsp externals)
                             (uidp next-uid)
                             (ienvp ienv)
                             (booleanp keep-going))))
 (declare (xargs :guard (filepath-transunit-map-unambp map)))
 (b*
  (((reterr) nil)
   ((when (omap::emptyp map)) (retok nil))
   (path (omap::head-key map))
   ((mv erp new-tunit table)
    (valid-transunit path (omap::head-val map)
                     externals next-uid ienv))
   ((when erp)
    (if keep-going
        (prog2$ (cw "Error in translation unit ~x0: ~@1~%"
                    (filepath->unwrap path)
                    erp)
                (valid-transunit-ensemble-loop
                     (omap::tail map)
                     externals next-uid ienv keep-going))
      (retmsg$ "Error in translation unit ~x0: ~@1"
               (filepath->unwrap path)
               erp)))
   ((valid-table table) table)
   ((erp new-map)
    (valid-transunit-ensemble-loop (omap::tail map)
                                   table.externals
                                   table.next-uid ienv keep-going)))
  (retok (omap::update path new-tunit new-map))))

Theorem: maybe-msgp-of-valid-transunit-ensemble-loop.erp

(defthm maybe-msgp-of-valid-transunit-ensemble-loop.erp
  (b* (((mv acl2::?erp ?new-map)
        (valid-transunit-ensemble-loop
             map
             externals next-uid ienv keep-going)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: filepath-transunit-mapp-of-valid-transunit-ensemble-loop.new-map

(defthm
   filepath-transunit-mapp-of-valid-transunit-ensemble-loop.new-map
  (implies (filepath-transunit-mapp map)
           (b* (((mv acl2::?erp ?new-map)
                 (valid-transunit-ensemble-loop
                      map
                      externals next-uid ienv keep-going)))
             (filepath-transunit-mapp new-map)))
  :rule-classes :rewrite)

Theorem: valid-transunit-ensemble-loop-of-ienv-fix-ienv

(defthm valid-transunit-ensemble-loop-of-ienv-fix-ienv
  (equal (valid-transunit-ensemble-loop
              map externals next-uid (ienv-fix ienv)
              keep-going)
         (valid-transunit-ensemble-loop
              map
              externals next-uid ienv keep-going)))

Theorem: valid-transunit-ensemble-loop-ienv-equiv-congruence-on-ienv

(defthm valid-transunit-ensemble-loop-ienv-equiv-congruence-on-ienv
 (implies
  (ienv-equiv ienv ienv-equiv)
  (equal
    (valid-transunit-ensemble-loop
         map externals next-uid ienv keep-going)
    (valid-transunit-ensemble-loop map externals
                                   next-uid ienv-equiv keep-going)))
 :rule-classes :congruence)

Theorem: valid-transunit-ensemble-loop-of-bool-fix-keep-going

(defthm valid-transunit-ensemble-loop-of-bool-fix-keep-going
  (equal (valid-transunit-ensemble-loop
              map externals
              next-uid ienv (bool-fix keep-going))
         (valid-transunit-ensemble-loop
              map
              externals next-uid ienv keep-going)))

Theorem: valid-transunit-ensemble-loop-iff-congruence-on-keep-going

(defthm valid-transunit-ensemble-loop-iff-congruence-on-keep-going
 (implies
  (iff keep-going keep-going-equiv)
  (equal
    (valid-transunit-ensemble-loop
         map externals next-uid ienv keep-going)
    (valid-transunit-ensemble-loop map externals
                                   next-uid ienv keep-going-equiv)))
 :rule-classes :congruence)

Theorem: filepath-transunit-map-unambp-of-valid-transunit-ensemble-loop

(defthm
     filepath-transunit-map-unambp-of-valid-transunit-ensemble-loop
  (implies (and (filepath-transunit-mapp map)
                (filepath-transunit-map-unambp map))
           (b* (((mv acl2::?erp ?new-map)
                 (valid-transunit-ensemble-loop
                      map
                      externals next-uid ienv keep-going)))
             (implies (not erp)
                      (filepath-transunit-map-unambp new-map)))))

Function: valid-transunit-ensemble

(defun valid-transunit-ensemble (tunits ienv keep-going)
 (declare (xargs :guard (and (transunit-ensemblep tunits)
                             (ienvp ienv)
                             (booleanp keep-going))))
 (declare (xargs :guard (transunit-ensemble-unambp tunits)))
 (b*
  (((reterr) (irr-transunit-ensemble))
   (map (transunit-ensemble->units tunits))
   ((erp new-map)
    (valid-transunit-ensemble-loop map nil (uid 0)
                                   ienv keep-going))
   (-
     (if keep-going (b* ((len-map (omap::size map))
                         (len-new-map (omap::size new-map))
                         (diff (- len-map len-new-map)))
                      (if (= (the integer diff) 0)
                          nil
                        (cw "Validated ~x0/~x1 translation units.~%"
                            len-new-map len-map)))
       nil)))
  (retok (transunit-ensemble new-map))))

Theorem: maybe-msgp-of-valid-transunit-ensemble.erp

(defthm maybe-msgp-of-valid-transunit-ensemble.erp
  (b* (((mv acl2::?erp ?new-tunits)
        (valid-transunit-ensemble tunits ienv keep-going)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: transunit-ensemblep-of-valid-transunit-ensemble.new-tunits

(defthm transunit-ensemblep-of-valid-transunit-ensemble.new-tunits
  (b* (((mv acl2::?erp ?new-tunits)
        (valid-transunit-ensemble tunits ienv keep-going)))
    (transunit-ensemblep new-tunits))
  :rule-classes :rewrite)

Theorem: transunit-ensemble-unambp-of-valid-transunit-ensemble

(defthm transunit-ensemble-unambp-of-valid-transunit-ensemble
  (implies (transunit-ensemble-unambp tunits)
           (b* (((mv acl2::?erp ?new-tunits)
                 (valid-transunit-ensemble tunits ienv keep-going)))
             (implies (not erp)
                      (transunit-ensemble-unambp new-tunits)))))

Theorem: valid-transunit-ensemble-of-transunit-ensemble-fix-tunits

(defthm valid-transunit-ensemble-of-transunit-ensemble-fix-tunits
  (equal (valid-transunit-ensemble (transunit-ensemble-fix tunits)
                                   ienv keep-going)
         (valid-transunit-ensemble tunits ienv keep-going)))

Theorem: valid-transunit-ensemble-transunit-ensemble-equiv-congruence-on-tunits

(defthm
 valid-transunit-ensemble-transunit-ensemble-equiv-congruence-on-tunits
 (implies
    (transunit-ensemble-equiv tunits tunits-equiv)
    (equal (valid-transunit-ensemble tunits ienv keep-going)
           (valid-transunit-ensemble tunits-equiv ienv keep-going)))
 :rule-classes :congruence)

Theorem: valid-transunit-ensemble-of-ienv-fix-ienv

(defthm valid-transunit-ensemble-of-ienv-fix-ienv
  (equal (valid-transunit-ensemble tunits (ienv-fix ienv)
                                   keep-going)
         (valid-transunit-ensemble tunits ienv keep-going)))

Theorem: valid-transunit-ensemble-ienv-equiv-congruence-on-ienv

(defthm valid-transunit-ensemble-ienv-equiv-congruence-on-ienv
 (implies
    (ienv-equiv ienv ienv-equiv)
    (equal (valid-transunit-ensemble tunits ienv keep-going)
           (valid-transunit-ensemble tunits ienv-equiv keep-going)))
 :rule-classes :congruence)

Theorem: valid-transunit-ensemble-of-bool-fix-keep-going

(defthm valid-transunit-ensemble-of-bool-fix-keep-going
 (equal (valid-transunit-ensemble tunits ienv (bool-fix keep-going))
        (valid-transunit-ensemble tunits ienv keep-going)))

Theorem: valid-transunit-ensemble-iff-congruence-on-keep-going

(defthm valid-transunit-ensemble-iff-congruence-on-keep-going
 (implies
    (iff keep-going keep-going-equiv)
    (equal (valid-transunit-ensemble tunits ienv keep-going)
           (valid-transunit-ensemble tunits ienv keep-going-equiv)))
 :rule-classes :congruence)