		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Remove-mbe-logic/exec

Turn every call (mbe :logic a :exec b) in a term into just its :logic part a or :exec part b.

Signature
(remove-mbe-logic/exec term logic?) → new-term
Arguments: term — Guard (pseudo-termp term).; logic? — Guard (booleanp logic?).
Returns: new-term — Type (pseudo-termp new-term), given (pseudo-termp term).

The choice is determinated by the boolean flag, which is t when the :logic part is to be removed.

In translated terms, mbes have the form (return-last 'mbe1-raw b a). We turn that form into a or b, based on the flag.

Function: remove-mbe-logic/exec

(defun remove-mbe-logic/exec (term logic?)
 (declare (xargs :guard (and (pseudo-termp term)
                             (booleanp logic?))))
 (let ((__function__ 'remove-mbe-logic/exec))
   (declare (ignorable __function__))
   (b*
     (((when (variablep term)) term)
      ((when (fquotep term)) term)
      (fn (ffn-symb term))
      (args (fargs term))
      ((when (and (eq fn 'return-last)
                  (equal (first args) ''mbe1-raw)))
       (remove-mbe-logic/exec (if logic? (second args) (third args))
                              logic?))
      (new-fn (if (symbolp fn)
                  fn
                (make-lambda (lambda-formals fn)
                             (remove-mbe-logic/exec (lambda-body fn)
                                                    logic?))))
      (new-args (remove-mbe-logic/exec-lst args logic?)))
     (fcons-term new-fn new-args))))

Function: remove-mbe-logic/exec-lst

(defun remove-mbe-logic/exec-lst (terms logic?)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (booleanp logic?))))
  (let ((__function__ 'remove-mbe-logic/exec-lst))
    (declare (ignorable __function__))
    (b* (((when (endp terms)) nil)
         ((cons term terms) terms)
         (new-term (remove-mbe-logic/exec term logic?))
         (new-terms (remove-mbe-logic/exec-lst terms logic?)))
      (cons new-term new-terms))))

Theorem: return-type-of-remove-mbe-logic/exec.new-term

(defthm return-type-of-remove-mbe-logic/exec.new-term
  (implies (pseudo-termp term)
           (b* ((?new-term (remove-mbe-logic/exec term logic?)))
             (pseudo-termp new-term)))
  :rule-classes :rewrite)

Theorem: return-type-of-remove-mbe-logic/exec-lst.new-terms

(defthm return-type-of-remove-mbe-logic/exec-lst.new-terms
  (implies
       (pseudo-term-listp terms)
       (b* ((?new-terms (remove-mbe-logic/exec-lst terms logic?)))
         (and (pseudo-term-listp new-terms)
              (equal (len new-terms) (len terms)))))
  :rule-classes :rewrite)

Subtopics

Remove-mbe-logic: Turn every call (mbe :logic a :exec b) in a term into just its :exec part b.
Remove-mbe-exec: Turn every call (mbe :logic a :exec b) in a term into just its :logic part a.
Remove-mbe-logic/exec-lst