unsound-eval

(in-package "ACL2")

(define unsound-eval
  :parents (interfacing-tools programming-with-state)
  :short "A somewhat robust evaluator."
  ((sexpr "An s-expression to evaluate, typically this should be a well-formed
           ACL2 form without guard violations, etc.  It may mention @(see
           stobj)s.") &key
    (state 'state))
  :returns (mv (errmsg "An error @(see acl2::msg) on failure, or @('nil') on success.
               Note that this message is likely to be very terse/unhelpful when
               evaluating @('sexpr') causes any ACL2 error.")
    (values "The list of return values from evaluating @('sexpr'), with
               stobjs elided with their names.")
    (state state-p1 :hyp (state-p1 state)))
  :long "<p>In the logic, this is implemented as oracle reads, so you can't
prove anything about what it returns.  Even so, it is generally <b>unsound</b>
since it lets you to modify @('state') and other @(see stobj)s without
accounting for how they have been modified.</p>

<p>In the execution, we basically call ACL2's @(tsee trans-eval) function
(technically: @('trans-eval-no-warning')).  But we wrap up the call in some
error handlers so that, e.g., guard violations and @('er') calls can be trapped
and returned as error messages.  Unfortunately these error messages are not
very informative&mdash;they will just say something like @('ACL2 Halted')
instead of explaining the problem.</p>"
  (declare (ignorable sexpr))
  (b* ((- (raise "Raw lisp definition not installed?")) ((mv err1 errmsg? state) (read-acl2-oracle state))
      ((mv err2 values state) (read-acl2-oracle state))
      ((when (or err1 err2)) (mv (msg "Reading oracle failed.") nil state))
      ((when errmsg?) (mv errmsg? nil state)))
    (mv nil values state)))

(defttag :unsound-eval)

(include-raw "unsound-eval-raw.lsp")