		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-transunit-ensemble

Disambiguate a translation unit ensembles.

Signature
(dimb-transunit-ensemble tuens gcc keep-going) → (mv erp new-tuens)
Arguments: tuens — Guard (transunit-ensemblep tuens).; gcc — Guard (booleanp gcc).; keep-going — Guard (booleanp keep-going).
Returns: erp — Type (maybe-msgp erp).; new-tuens — Type (transunit-ensemblep new-tuens).

We also pass a flag saying whether GCC extensions should be accepted.

We disambiguate all the translation units, independently. We leave the file path mapping unchanged.

Definitions and Theorems

Function: dimb-transunit-ensemble-loop

(defun dimb-transunit-ensemble-loop (tumap gcc keep-going)
 (declare (xargs :guard (and (filepath-transunit-mapp tumap)
                             (booleanp gcc)
                             (booleanp keep-going))))
 (let ((__function__ 'dimb-transunit-ensemble-loop))
  (declare (ignorable __function__))
  (b* (((reterr) nil)
       ((when (omap::emptyp tumap))
        (retok nil))
       ((mv path tunit) (omap::head tumap))
       ((mv erp new-tunit)
        (dimb-transunit tunit gcc))
       ((when erp)
        (if keep-going
            (prog2$ (cw "Error in translation unit ~x0: ~@1~%"
                        (filepath->unwrap path)
                        erp)
                    (dimb-transunit-ensemble-loop (omap::tail tumap)
                                                  gcc keep-going))
          (retmsg$ "Error in translation unit ~x0: ~@1"
                   (filepath->unwrap path)
                   erp)))
       ((erp new-tumap)
        (dimb-transunit-ensemble-loop (omap::tail tumap)
                                      gcc keep-going)))
    (retok (omap::update path new-tunit new-tumap)))))

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

(defthm maybe-msgp-of-dimb-transunit-ensemble-loop.erp
  (b* (((mv acl2::?erp ?new-tumap)
        (dimb-transunit-ensemble-loop tumap gcc keep-going)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: filepath-transunit-mapp-of-dimb-transunit-ensemble-loop.new-tumap

(defthm
  filepath-transunit-mapp-of-dimb-transunit-ensemble-loop.new-tumap
  (implies
       (filepath-transunit-mapp tumap)
       (b* (((mv acl2::?erp ?new-tumap)
             (dimb-transunit-ensemble-loop tumap gcc keep-going)))
         (filepath-transunit-mapp new-tumap)))
  :rule-classes :rewrite)

Theorem: dimb-transunit-ensemble-loop-of-bool-fix-gcc

(defthm dimb-transunit-ensemble-loop-of-bool-fix-gcc
  (equal (dimb-transunit-ensemble-loop tumap (bool-fix gcc)
                                       keep-going)
         (dimb-transunit-ensemble-loop tumap gcc keep-going)))

Theorem: dimb-transunit-ensemble-loop-iff-congruence-on-gcc

(defthm dimb-transunit-ensemble-loop-iff-congruence-on-gcc
 (implies
  (iff gcc gcc-equiv)
  (equal (dimb-transunit-ensemble-loop tumap gcc keep-going)
         (dimb-transunit-ensemble-loop tumap gcc-equiv keep-going)))
 :rule-classes :congruence)

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

(defthm dimb-transunit-ensemble-loop-of-bool-fix-keep-going
 (equal
      (dimb-transunit-ensemble-loop tumap gcc (bool-fix keep-going))
      (dimb-transunit-ensemble-loop tumap gcc keep-going)))

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

(defthm dimb-transunit-ensemble-loop-iff-congruence-on-keep-going
 (implies
  (iff keep-going keep-going-equiv)
  (equal (dimb-transunit-ensemble-loop tumap gcc keep-going)
         (dimb-transunit-ensemble-loop tumap gcc keep-going-equiv)))
 :rule-classes :congruence)

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

(defthm
      filepath-transunit-map-unambp-of-dimb-transunit-ensemble-loop
  (implies
       (filepath-transunit-mapp tumap)
       (b* (((mv acl2::?erp ?new-tumap)
             (dimb-transunit-ensemble-loop tumap gcc keep-going)))
         (implies (not erp)
                  (filepath-transunit-map-unambp new-tumap)))))

Function: dimb-transunit-ensemble

(defun dimb-transunit-ensemble (tuens gcc keep-going)
  (declare (xargs :guard (and (transunit-ensemblep tuens)
                              (booleanp gcc)
                              (booleanp keep-going))))
  (let ((__function__ 'dimb-transunit-ensemble))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-transunit-ensemble))
         (tumap (transunit-ensemble->units tuens))
         ((erp new-tumap)
          (dimb-transunit-ensemble-loop tumap gcc keep-going))
         (- (if keep-going
                (b* ((len-tumap (omap::size tumap))
                     (len-new-tumap (omap::size new-tumap))
                     (diff (- len-tumap len-new-tumap)))
                  (if (= (the integer diff) 0)
                      nil
                    (cw "Disambiguated ~x0/~x1 translation units.~%"
                        len-new-tumap len-tumap)))
              nil)))
      (retok (transunit-ensemble new-tumap)))))

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

(defthm maybe-msgp-of-dimb-transunit-ensemble.erp
  (b* (((mv acl2::?erp ?new-tuens)
        (dimb-transunit-ensemble tuens gcc keep-going)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: transunit-ensemblep-of-dimb-transunit-ensemble.new-tuens

(defthm transunit-ensemblep-of-dimb-transunit-ensemble.new-tuens
  (b* (((mv acl2::?erp ?new-tuens)
        (dimb-transunit-ensemble tuens gcc keep-going)))
    (transunit-ensemblep new-tuens))
  :rule-classes :rewrite)

Theorem: transunit-ensemble-unambp-of-dimb-transunit-ensemble

(defthm transunit-ensemble-unambp-of-dimb-transunit-ensemble
  (b* (((mv acl2::?erp ?new-tuens)
        (dimb-transunit-ensemble tuens gcc keep-going)))
    (implies (not erp)
             (transunit-ensemble-unambp new-tuens))))

Theorem: dimb-transunit-ensemble-of-transunit-ensemble-fix-tuens

(defthm dimb-transunit-ensemble-of-transunit-ensemble-fix-tuens
  (equal (dimb-transunit-ensemble (transunit-ensemble-fix tuens)
                                  gcc keep-going)
         (dimb-transunit-ensemble tuens gcc keep-going)))

Theorem: dimb-transunit-ensemble-transunit-ensemble-equiv-congruence-on-tuens

(defthm
 dimb-transunit-ensemble-transunit-ensemble-equiv-congruence-on-tuens
 (implies
      (transunit-ensemble-equiv tuens tuens-equiv)
      (equal (dimb-transunit-ensemble tuens gcc keep-going)
             (dimb-transunit-ensemble tuens-equiv gcc keep-going)))
 :rule-classes :congruence)

Theorem: dimb-transunit-ensemble-of-bool-fix-gcc

(defthm dimb-transunit-ensemble-of-bool-fix-gcc
  (equal (dimb-transunit-ensemble tuens (bool-fix gcc)
                                  keep-going)
         (dimb-transunit-ensemble tuens gcc keep-going)))

Theorem: dimb-transunit-ensemble-iff-congruence-on-gcc

(defthm dimb-transunit-ensemble-iff-congruence-on-gcc
  (implies
       (iff gcc gcc-equiv)
       (equal (dimb-transunit-ensemble tuens gcc keep-going)
              (dimb-transunit-ensemble tuens gcc-equiv keep-going)))
  :rule-classes :congruence)

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

(defthm dimb-transunit-ensemble-of-bool-fix-keep-going
  (equal (dimb-transunit-ensemble tuens gcc (bool-fix keep-going))
         (dimb-transunit-ensemble tuens gcc keep-going)))

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

(defthm dimb-transunit-ensemble-iff-congruence-on-keep-going
  (implies
       (iff keep-going keep-going-equiv)
       (equal (dimb-transunit-ensemble tuens gcc keep-going)
              (dimb-transunit-ensemble tuens gcc keep-going-equiv)))
  :rule-classes :congruence)