• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
      • Must-fail
      • Assert!-stobj
      • Must-eval-to
        • Must-eval-to-t
      • Assert!
      • Must-succeed
      • Must-succeed*
      • Assert?
      • Must-fail-with-soft-error
      • Must-fail-with-hard-error
      • Must-fail-with-error
      • Must-eval-to-t
      • Must-not-prove
      • Must-prove
      • Must-be-redundant
      • Must-not-be-table-key
      • Must-fail-local
      • Must-be-table-key
      • Assert-equal
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/testing
• Errors

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.