		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Ldm-ienv

Map an implementation environment of type ienv to one in the language formalization of type c::ienv.

Signature
(ldm-ienv ienv) → ienv1
Arguments: ienv — Guard (ienvp ienv).
Returns: ienv1 — Type (c::ienvp ienv1).

The ldm part of this function's name is related to the one used for the functions in mapping-to-language-definition, since we are mapping from the C syntax for tools to the formal language definition.

Given our assumptions (stated in ienv) that bytes are 8 bits, that signed integers are two's complement, and that there are no padding bits and no trap representations, this mapping could still be defined in different ways, based on the exact choice of bit layouts, which is captured in c::ienv but not in ienv. We pick a simple layout, already defined in the language formalization, consisting of increasing bit values, ended by the sign bit for signed integers. The exact choice of bit layout does not matter, since the main purpose of the mapping is to exhibit a correspondence.

For now we map to the C17 version.

Definitions and Theorems

Theorem: ldm-ienv-wfp-lemma

(defthm ldm-ienv-wfp-lemma
 (c::char+short+int+long+llong+bool-format-wfp
  (c::char+short+int+long+llong+bool-format
   '((c::size . 8))
   '((c::signed :twos-complement) (c::trap))
   char-format
   (c::integer-format-inc-sign-tcnpnt
        (* 8 (ienv->short-bytes ienv)))
   (c::integer-format-inc-sign-tcnpnt (* 8 (ienv->int-bytes ienv)))
   (c::integer-format-inc-sign-tcnpnt (* 8 (ienv->long-bytes ienv)))
   (c::integer-format-inc-sign-tcnpnt
        (* 8 (ienv->llong-bytes ienv)))
   '((byte-size . 1)
     (c::value-index . 0)
     (c::trap)))))

Function: ldm-ienv

(defun ldm-ienv (ienv)
  (declare (xargs :guard (ienvp ienv)))
  (b*
   (((ienv ienv) ienv)
    (uchar-format (c::uchar-format-8))
    (schar-format (c::schar-format-8tcnt))
    (char-format (c::char-format ienv.plain-char-signedp))
    (short-format
         (c::integer-format-inc-sign-tcnpnt (* 8 ienv.short-bytes)))
    (int-format
         (c::integer-format-inc-sign-tcnpnt (* 8 ienv.int-bytes)))
    (long-format
         (c::integer-format-inc-sign-tcnpnt (* 8 ienv.long-bytes)))
    (llong-format
         (c::integer-format-inc-sign-tcnpnt (* 8 ienv.llong-bytes)))
    (bool-format (c::bool-format-lsb))
    (char+short+int+long+llong+bool-format
         (c::char+short+int+long+llong+bool-format
              uchar-format schar-format
              char-format short-format int-format
              long-format llong-format bool-format)))
   (c::make-ienv :version ienv.version
                 :char+short+int+long+llong+bool-format
                 char+short+int+long+llong+bool-format)))

Theorem: ienvp-of-ldm-ienv

(defthm ienvp-of-ldm-ienv
  (b* ((ienv1 (ldm-ienv ienv)))
    (c::ienvp ienv1))
  :rule-classes :rewrite)

Theorem: ldm-ienv-of-ienv-fix-ienv

(defthm ldm-ienv-of-ienv-fix-ienv
  (equal (ldm-ienv (ienv-fix ienv))
         (ldm-ienv ienv)))

Theorem: ldm-ienv-ienv-equiv-congruence-on-ienv

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