oracle-eval-real - ACL2 Book

other

(in-package "ACL2")

other

(defttag oracle-eval)

other

(remove-untouchable 'read-acl2-oracle t)

real-oracle-evalfunction

(defun real-oracle-eval
  (term alist state)
  (declare (xargs :guard t
      :stobjs state
      :guard-hints (("goal" :in-theory (enable read-acl2-oracle))))
    (ignorable term alist))
  (mv-let (err1 eval-error state)
    (read-acl2-oracle state)
    (mv-let (err2 evaluation state)
      (read-acl2-oracle state)
      (cond ((or err1 err2) (mv "Evaluation mysteriously failed (oracle empty)~%"
            nil
            state))
        (eval-error (mv eval-error nil state))
        (t (mv nil evaluation state))))))

state-p1-of-read-acl2-oracletheorem

(defthm state-p1-of-read-acl2-oracle
  (implies (state-p1 state)
    (state-p1 (mv-nth 2 (read-acl2-oracle state))))
  :hints (("Goal" :in-theory (enable read-acl2-oracle))))

state-p1-of-real-oracle-evaltheorem

(defthm state-p1-of-real-oracle-eval
  (implies (state-p1 state)
    (state-p1 (mv-nth 2 (real-oracle-eval term alist state)))))

in-theory

(in-theory (disable real-oracle-eval))

other

(progn! (set-raw-mode t)
  (defun real-oracle-eval
    (term alist state)
    (mv-let (erp translation-and-val state)
      (simple-translate-and-eval term
        alist
        '(state)
        "The given term"
        'real-oracle-eval
        (w state)
        state
        t)
      (if erp
        (mv erp nil state)
        (mv nil (cdr translation-and-val) state)))))