		Search-engine friendly clone of the ACL2 documentation.

Add-const-to-untranslate-preprocess

Extend untranslate-preprocess to keep a constant unexpanded in output.

This macro defines a new function and stores it into the user-defined-functions-table as the untranslation preprocessing function. This new function recognizes a term that is the expanded value of the given constant const and turns it into the symbol that names the constant const, while it delegates all other terms to the previous untranslation preprocessing function. If there was no previous untranslation preprocessing function, the new function returns nil on all other terms, meaning that untranslation preprocessing is finished. The new function is in program mode, in case the previous untranslation preprocessing function is also in program mode.

Definitions and Theorems

Function: add-const-to-untranslate-preprocess-fn

(defun
 add-const-to-untranslate-preprocess-fn
 (const state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (symbolp const)))
 (let
  ((__function__ 'add-const-to-untranslate-preprocess-fn))
  (declare (ignorable __function__))
  (b*
   ((user-defined-functions-table
         (table-alist 'user-defined-functions-table
                      (w state)))
    (old-untranslate-preprocess
         (cdr (assoc-eq 'untranslate-preprocess
                        user-defined-functions-table)))
    (new-untranslate-preprocess
         (intern-in-package-of-symbol
              (string-append "UNTRANSLATE-PREPROCESS-"
                             (symbol-name const))
              const)))
   (cons
    'progn
    (cons
     (cons
      'defun
      (cons
       new-untranslate-preprocess
       (cons
        (cons 'term (cons 'wrld 'nil))
        (cons
         (cons 'declare
               (cons (cons 'xargs
                           (cons ':mode (cons ':program 'nil)))
                     'nil))
         (cons
          (cons
           'if
           (cons
            (cons
             'equal
             (cons
                  'term
                  (cons (cons 'list
                              (cons (cons 'quote (cons 'quote 'nil))
                                    (cons const 'nil)))
                        'nil)))
            (cons (cons 'quote (cons const 'nil))
                  (cons (and old-untranslate-preprocess
                             (cons old-untranslate-preprocess
                                   (cons 'term (cons 'wrld 'nil))))
                        'nil))))
          'nil)))))
     (cons
      (cons
       'table
       (cons
           'user-defined-functions-table
           (cons (cons 'quote
                       (cons 'untranslate-preprocess 'nil))
                 (cons (cons 'quote
                             (cons new-untranslate-preprocess 'nil))
                       'nil))))
      'nil))))))

Theorem: pseudo-event-formp-of-add-const-to-untranslate-preprocess-fn

(defthm
  pseudo-event-formp-of-add-const-to-untranslate-preprocess-fn
  (b* ((event (add-const-to-untranslate-preprocess-fn const state)))
      (pseudo-event-formp event))
  :rule-classes :rewrite)