		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Transunit-at-path

Translation unit at a certain path in a translation unit ensemble.

Signature
(transunit-at-path path tunits) → tunit
Arguments: path — Guard (filepathp path).; tunits — Guard (transunit-ensemblep tunits).
Returns: tunit — Type (transunitp tunit).

This is the value associated to the key (path) in the map, which the guard requires to be in the translation unit ensemble.

It is more concise, and more abstract, than accessing the map and then looking up the path.

Together with transunit-ensemble-paths, it can be used an as API to inspect a file set.

Definitions and Theorems

Function: transunit-at-path

(defun transunit-at-path (path tunits)
  (declare (xargs :guard (and (filepathp path)
                              (transunit-ensemblep tunits))))
  (declare (xargs :guard (in path
                             (transunit-ensemble-paths tunits))))
  (transunit-fix (omap::lookup (filepath-fix path)
                               (transunit-ensemble->units tunits))))

Theorem: transunitp-of-transunit-at-path

(defthm transunitp-of-transunit-at-path
  (b* ((tunit (transunit-at-path path tunits)))
    (transunitp tunit))
  :rule-classes :rewrite)

Theorem: transunit-at-path-of-filepath-fix-path

(defthm transunit-at-path-of-filepath-fix-path
  (equal (transunit-at-path (filepath-fix path)
                            tunits)
         (transunit-at-path path tunits)))

Theorem: transunit-at-path-filepath-equiv-congruence-on-path

(defthm transunit-at-path-filepath-equiv-congruence-on-path
  (implies (filepath-equiv path path-equiv)
           (equal (transunit-at-path path tunits)
                  (transunit-at-path path-equiv tunits)))
  :rule-classes :congruence)

Theorem: transunit-at-path-of-transunit-ensemble-fix-tunits

(defthm transunit-at-path-of-transunit-ensemble-fix-tunits
  (equal (transunit-at-path path (transunit-ensemble-fix tunits))
         (transunit-at-path path tunits)))

Theorem: transunit-at-path-transunit-ensemble-equiv-congruence-on-tunits

(defthm
    transunit-at-path-transunit-ensemble-equiv-congruence-on-tunits
  (implies (transunit-ensemble-equiv tunits tunits-equiv)
           (equal (transunit-at-path path tunits)
                  (transunit-at-path path tunits-equiv)))
  :rule-classes :congruence)