		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-transunit-ensemble

Map a translation unit ensemble to the language definition.

Signature
(ldm-transunit-ensemble tunits) → (mv erp fileset)
Arguments: tunits — Guard (transunit-ensemblep tunits).
Returns: fileset — Type (c::filesetp fileset).

Currently we only support translation unit ensembles consisting of a single translation unit. We map that to a c::fileset without header, just with a source file that corresponds to the translation unit. We set the path of the c::fileset to the empty string for now, as we are not concerned with any actual interaction with the file system.

Note that c::fileset is quite different from fileset. We plan to make the terminology more consistent.

Definitions and Theorems

Function: ldm-transunit-ensemble

(defun ldm-transunit-ensemble (tunits)
 (declare (xargs :guard (transunit-ensemblep tunits)))
 (declare (xargs :guard (transunit-ensemble-unambp tunits)))
 (let ((__function__ 'ldm-transunit-ensemble))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c::fileset "" nil (c::file nil)))
    (map (transunit-ensemble->units tunits))
    ((unless (= (omap::size map) 1))
     (reterr
      (msg
       "Unsupported translation unit ensemble ~
                      with ~x0 translation units."
       (omap::size map))))
    (tunit (omap::head-val map))
    ((erp file) (ldm-transunit tunit)))
   (retok (c::make-fileset :path-wo-ext ""
                           :dot-h nil
                           :dot-c file)))))

Theorem: filesetp-of-ldm-transunit-ensemble.fileset

(defthm filesetp-of-ldm-transunit-ensemble.fileset
  (b* (((mv acl2::?erp ?fileset)
        (ldm-transunit-ensemble tunits)))
    (c::filesetp fileset))
  :rule-classes :rewrite)

Theorem: ldm-transunit-ensemble-ok-when-transunit-ensemble-formalp

(defthm ldm-transunit-ensemble-ok-when-transunit-ensemble-formalp
  (implies (transunit-ensemble-formalp tunits)
           (b* (((mv acl2::?erp ?fileset)
                 (ldm-transunit-ensemble tunits)))
             (not erp))))

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

(defthm ldm-transunit-ensemble-of-transunit-ensemble-fix-tunits
  (equal (ldm-transunit-ensemble (transunit-ensemble-fix tunits))
         (ldm-transunit-ensemble tunits)))

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

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