untranslate-dollar

(in-package "ACL2")

(defsection untranslate$
  :parents (std/system/term-transformations)
  :short "A logic-mode guard-verified version of @(tsee untranslate)."
  :long (topstring (p "This is a @(see logic) mode version of the function,
     @('untranslate').  See @(see untranslate), but note
     that instead of @('(untranslate term iff-flg wrld)')
     one calls @('(untranslate$ term iff-flg state)'); that
     is, the @(see world) has been replaced by @(see state).")
    (p "The untranslation operated by this utility does not
     make any use of the @(tsee
     user-defined-functions-table): neither the
     untranslate-preprocess capability nor wholesale
     replacement of untranslate.  (Technical Note:
     @('Untranslate$') calls @('untranslate1') instead of
     @(tsee untranslate), using a @('preprocess-fn')
     argument of @('nil') to avoid certain hard errors.)")
    (p "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 @(tsee magic-ev-fncall).
     If the @(tsee magic-ev-fncall) fails,
     we also stop with a hard error."))
  (defund 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)))))