translate

(defun translate-term-with-defaults
  (term ctx wrld)
  (declare (xargs :mode :program))
  (translate-cmp term t t t ctx wrld (default-state-vars nil)))

(defun translate-term
  (term ctx wrld)
  (declare (xargs :mode :program))
  (mv-let (ctx msg-or-val)
    (translate-term-with-defaults term ctx wrld)
    (if ctx
      (er hard!
        ctx
        "Failed to translate term ~x0. ~@1"
        term
        msg-or-val)
      msg-or-val)))

(defun translate-terms
  (terms ctx wrld)
  (declare (xargs :mode :program))
  (if (endp terms)
    nil
    (cons (translate-term (first terms) ctx wrld)
      (translate-terms (rest terms) ctx wrld))))

(defun translatable-termp
  (untranslated-term wrld)
  (declare (xargs :mode :program :guard (plist-worldp wrld)))
  (mv-let (ctx msg-or-val)
    (translate-term-with-defaults untranslated-term
      'translatable-termp
      wrld)
    (declare (ignore msg-or-val))
    (not ctx)))

(defun translatable-term-listp
  (untranslated-terms wrld)
  (declare (xargs :mode :program :guard (and (true-listp untranslated-terms) (plist-worldp wrld))))
  (if (endp untranslated-terms)
    t
    (and (translatable-termp (first untranslated-terms) wrld)
      (translatable-term-listp (rest untranslated-terms) wrld))))

(defun translate-term-allowing-ignored-vars
  (term ctx wrld)
  (declare (xargs :mode :program))
  (let ((wrld (table-programmatic 'acl2-defaults-table :ignore-ok t wrld)))
    (translate-term term ctx wrld)))