prev-stobj-binding

Included Books

bstar

other

(in-package "ACL2")

include-book

(include-book "std/util/bstar" :dir :system)

prev-stobjs-correspondencefunction

(defun prev-stobjs-correspondence
  (fn w)
  (b* ((table (table-alist 'prev-stobjs-table w)) (look (cdr (assoc-eq fn table)))
      ((when look) (mv (car look) (cadr look))))
    (mv (stobjs-out fn w) (formals fn w))))

set-prev-stobjs-correspondencemacro

(defmacro set-prev-stobjs-correspondence
  (fn &key stobjs-out formals)
  `(table prev-stobjs-table ',FN '(,STOBJS-OUT ,FORMALS)))

other

(set-prev-stobjs-correspondence update-nth
  :stobjs-out (stobj)
  :formals (n val stobj))

other

(set-prev-stobjs-correspondence update-nth-array
  :stobjs-out (stobj)
  :formals (j k val stobj))

other

(set-prev-stobjs-correspondence cons
  :stobjs-out (stobj)
  :formals (x stobj))

find-prev-stobj-bindingfunction

(defun find-prev-stobj-binding
  (new-term state)
  (declare (xargs :guard (pseudo-termp new-term)
      :stobjs state
      :mode :program))
  (b* (((mv valnum function args) (case-match new-term
         (('mv-nth ('quote valnum) (function . args) . &) (mv (and (symbolp function) valnum) function args))
         ((function . args) (mv (and (symbolp function) 0) function args))
         (& (mv nil nil nil)))) ((unless valnum) (mv nil nil))
      ((when (or (eq function 'if) (eq function 'return-last))) (mv nil nil))
      (w (w state))
      ((mv stobjs-out formals) (prev-stobjs-correspondence function w))
      (stobj-out (nth valnum stobjs-out))
      ((unless stobj-out) (mv nil nil))
      (pos (position stobj-out formals))
      ((unless pos) (b* ((one-formal-and-return (and (eql (len stobjs-out) 1) (eql (len formals) 1))) ((unless one-formal-and-return) (mv nil nil))
            (stobjs-in (stobjs-in function w))
            (looks-like-nested-accessor (and (car stobjs-in) (not (eq (car stobjs-in) stobj-out))))
            ((unless looks-like-nested-accessor) (mv nil nil))
            ((mv parent-ok parent-prev-stobj) (find-prev-stobj-binding (car args) state))
            ((unless parent-ok) (mv nil nil)))
          (mv t `(,FUNCTION ,PARENT-PREV-STOBJ)))))
    (mv t (nth pos args))))

prev-stobj-bindingfunction

(defun prev-stobj-binding
  (new-term prev-var mfc state)
  (declare (xargs :guard (and (pseudo-termp new-term) (symbolp prev-var))
      :stobjs state
      :mode :program)
    (ignore mfc))
  (b* (((mv ok prev-term) (find-prev-stobj-binding new-term state)))
    (if (and ok (not (equal new-term prev-term)))
      (if prev-term
        `((,PREV-VAR . ,PREV-TERM))
        (er hard?
          'prev-stobj-binding
          "prev-term was nil, new-term: ~x0~%Bad entry in prev-stobjs-table?~%"
          new-term))
      `((do-not-use-this-long-horrible-variable . do-not-use-this-long-horrible-variable)))))