		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Untranslate$

A logic-mode guard-verified version of untranslate.

This is a logic mode version of the function, untranslate. See untranslate, but note that instead of (untranslate term iff-flg wrld) one calls (untranslate$ term iff-flg state); that is, the world has been replaced by state.

The untranslation operated by this utility does not make any use of the user-defined-functions-table: neither the untranslate-preprocess capability nor wholesale replacement of untranslate. (Technical Note: Untranslate$ calls untranslate1 instead of untranslate, using a preprocess-fn argument of nil to avoid certain hard errors.)

If the call to untranslate1 causes a hard error, so does untranslate$; this is achieved by passing nil as the hard-error-returns-nilp argument of magic-ev-fncall. If the magic-ev-fncall fails, we also stop with a hard error.

Definitions and Theorems

Function: untranslate$

(defun untranslate$ (term iff-flg state)
  (declare (xargs :stobjs state
                  :guard (pseudo-termp term)))
  (let* ((wrld (w state))
         (tbl (untrans-table wrld))
         (fn nil))
    (mv-let (erp val)
            (magic-ev-fncall 'untranslate1
                             (list term iff-flg tbl fn wrld)
                             state nil t)
      (if erp (er hard? 'untranslate$ "~@0" val)
        val))))