		Search-engine friendly clone of the ACL2 documentation.

Mapping-to-language-definition

Ldm-transunit

Map a translation unit to the language definition.

Signature
(ldm-transunit tunit) → (mv erp file)
Arguments: tunit — Guard (transunitp tunit).
Returns: file — Type (c::filep file).

A translation unit consists of a list of external declarations. We map all of them to the language definition (if possible), obtaining a corresponding list of external declaration, which we put into a c::file.

Definitions and Theorems

Function: ldm-transunit

(defun ldm-transunit (tunit)
  (declare (xargs :guard (transunitp tunit)))
  (declare (xargs :guard (transunit-unambp tunit)))
  (let ((__function__ 'ldm-transunit))
    (declare (ignorable __function__))
    (b* (((reterr) (c::file nil))
         (extdecls (transunit->decls tunit))
         ((erp extdecls1)
          (ldm-extdecl-list extdecls)))
      (retok (c::make-file :declons extdecls1)))))

Theorem: filep-of-ldm-transunit.file

(defthm filep-of-ldm-transunit.file
  (b* (((mv acl2::?erp ?file)
        (ldm-transunit tunit)))
    (c::filep file))
  :rule-classes :rewrite)

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

(defthm ldm-transunit-ok-when-transunit-formalp
  (implies (transunit-formalp tunit)
           (b* (((mv acl2::?erp ?file)
                 (ldm-transunit tunit)))
             (not erp))))

Theorem: ldm-transunit-of-transunit-fix-tunit

(defthm ldm-transunit-of-transunit-fix-tunit
  (equal (ldm-transunit (transunit-fix tunit))
         (ldm-transunit tunit)))

Theorem: ldm-transunit-transunit-equiv-congruence-on-tunit

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