nld - ACL2 Book

other

(in-package "ACL2")

error-stack-summaryfunction

(defun error-stack-summary
  (s)
  (let* ((d (assoc-eq :free-variables s)) (l (and d (cadr (assoc-keyword :location (cdr d))))))
    (cond ((equal l "body of") :free-variables-body)
      ((equal l "guard for") :free-variables-guard)
      ((assoc-eq :termination-proof s) :termination-proof)
      ((assoc-eq :guard-proof s) :guard-proof)
      (t :other-error))))

prepend-ld-resultfunction

(defun prepend-ld-result
  (ld-history)
  (let* ((entry (car ld-history)) (error-flg (ld-history-entry-error-flg entry))
      (stobjs-out/value (ld-history-entry-stobjs-out/value entry)))
    (cond (error-flg (assert$ (eq stobjs-out/value nil)
          (cons error-flg stobjs-out/value)))
      (t (case-match stobjs-out/value
          ((stobjs-out ((:error-stack . error-stack) . er) . rest) `(,STOBJS-OUT (,(ERROR-STACK-SUMMARY ERROR-STACK) (:error-stack . ,ERROR-STACK) . ,ER) . ,REST))
          (& (cons error-flg stobjs-out/value)))))))

nldmacro

(defmacro nld
  (form &rest args)
  (cond ((keyword-value-listp args) (let* ((tail (assoc-keyword :ld-verbose args)) (args (if tail
              args
              (list* :ld-verbose nil args)))
          (tail (assoc-keyword :ld-prompt args))
          (args (if tail
              args
              (list* :ld-prompt nil args))))
        `(er-progn (ld (list ,FORM) ,@ARGS)
          (value (prepend-ld-result (ld-history state))))))
    (t (er hard
        'nld
        "Bad call of nld, since this is not a keyword-value-listp:~&~s"
        args))))