		Search-engine friendly clone of the ACL2 documentation.

Must-eval-to

A top-level assert$-like command to ensure that a form evaluates to a non-erroneous error triple with the value of a specified expression.

(must-eval-to form
              expr
              :ld-skip-proofsp ...
              :with-output-off ...
              :check-expansion ....)

Form should evaluate to an error triple (mv erp val state). If erp is nil and val is the value of expr then (must-eval-to form expr) expands to (value-triple 'val); otherwise expansion causes an appropriate soft error. Note that both form and expr are evaluated.

The :ld-skip-proofsp option sets the value of ld-skip-proofsp to use for evaluating form, unless it is :default, which is the default, in which case ld-skip-proofsp retains its current value.

The :with-output-off option serves to suppress output from form: when not nil, it is used as the :off argument of with-output. The default is :all, i.e., all output is suppressed.

The :check-expansion option determines whether form is re-run and re-checked at include-book time; see make-event. By default, it is not.

Macro: must-eval-to

(defmacro must-eval-to (&whole must-eval-to-form form
                               expr &key (ld-skip-proofsp ':default)
                               (with-output-off ':all)
                               (check-expansion 'nil
                                                check-expansion-p))
 (declare (xargs :guard (booleanp check-expansion)))
 (let*
  ((body
    (cons
     'er-let*
     (cons
      (cons (cons 'form-val-use-nowhere-else
                  (cons form 'nil))
            'nil)
      (cons
       (cons
        'let
        (cons
         (cons (cons 'expr-val
                     (cons (cons 'check-vars-not-free
                                 (cons '(form-val-use-nowhere-else)
                                       (cons expr 'nil)))
                           'nil))
               'nil)
         (cons
          (cons
           'cond
           (cons
            '((equal form-val-use-nowhere-else expr-val)
              (value (list 'value-triple
                           (list 'quote expr-val))))
            (cons
             (cons
              't
              (cons
               (cons
                'er
                (cons
                 'soft
                 (cons
                  (cons
                   'msg
                   (cons
                    '"( MUST-EVAL-TO ~@0 ~@1)"
                    (cons
                     (cons 'tilde-@-abbreviate-object-phrase
                           (cons (cons 'quote (cons form 'nil))
                                 'nil))
                     (cons
                          (cons 'tilde-@-abbreviate-object-phrase
                                (cons (cons 'quote (cons expr 'nil))
                                      'nil))
                          'nil))))
                  (cons
                   '"Evaluation returned ~X01, not the value ~x2 of ~
                            the expression ~x3."
                   (cons
                    'form-val-use-nowhere-else
                    (cons '(evisc-tuple 4 3 nil nil)
                          (cons 'expr-val
                                (cons (cons 'quote (cons expr 'nil))
                                      'nil))))))))
               'nil))
             'nil)))
          'nil)))
       'nil))))
   (form
    (cons
     'make-event
     (cons
          (if (eq ld-skip-proofsp :default)
              body
            (cons 'state-global-let*
                  (cons (cons (cons 'ld-skip-proofsp
                                    (cons ld-skip-proofsp 'nil))
                              'nil)
                        (cons body 'nil))))
          (cons ':on-behalf-of
                (cons must-eval-to-form
                      (and check-expansion-p
                           (cons ':check-expansion
                                 (cons check-expansion 'nil)))))))))
  (cond (with-output-off
             (cons 'with-output
                   (cons ':off
                         (cons with-output-off (cons form 'nil)))))
        (t form))))

Subtopics

Must-eval-to-t: A specialization of must-eval-to to ensure that a form evaluates to a non-erroneous error triple with value t.