memoize - ACL2 Book

other

(in-package "ACL2")

other

(defn clear-memoize-table (fn) fn)

other

(defn clear-memoize-tables nil nil)

other

(defn memoize-summary nil nil)

other

(defn clear-memoize-statistics nil nil)

memsummacro

(defmacro memsum nil '(memoize-summary))

*hons-primitive-fns*constant

(defconst *hons-primitive-fns*
  '(hons-copy hons
    hons-equal
    hons-equal-lite
    hons-clear
    hons-clear!
    hons-wash
    hons-wash!
    hons-summary
    hons-resize-fn
    get-slow-alist-action
    hons-get
    hons-acons
    hons-acons!
    fast-alist-fork
    fast-alist-fork!
    fast-alist-clean
    fast-alist-clean!
    fast-alist-len
    fast-alist-free
    fast-alist-summary
    cons-subtrees
    number-subtrees
    flush-hons-get-hash-table-link
    clear-memoize-table
    clear-memoize-tables
    memoize-summary
    clear-memoize-statistics))

*hons-primitives*constant

(defconst *hons-primitives*
  (append '(hons-resize set-slow-alist-action memoize unmemoize memsum)
    *hons-primitive-fns*))

*mht-default-size*constant

(defconst *mht-default-size* 60)

memoize-formfunction

(defun memoize-form
  (fn condition
    condition-p
    condition-fn
    hints
    otf-flg
    inline
    commutative
    forget
    memo-table-init-size
    aokp
    stats
    total
    invoke
    ideal-okp)
  (declare (xargs :guard t))
  (let ((condition (cond ((equal condition ''t) t)
         ((equal condition ''nil) nil)
         (t condition))))
    (cond ((and condition-fn (null condition-p)) `(progn (table memoize-table
            (deref-macro-name ,FN (macro-aliases world))
            (list* (cons :condition-fn ,CONDITION-FN)
              (cons :inline ,INLINE)
              (cons :commutative ,COMMUTATIVE)
              (cons :forget ,FORGET)
              (cons :memo-table-init-size ,(OR MEMO-TABLE-INIT-SIZE *MHT-DEFAULT-SIZE*))
              (cons :aokp ,AOKP)
              (cons :stats ,STATS)
              (cons :total ,TOTAL)
              (cons :invoke ,INVOKE)
              (and (not (eq ,IDEAL-OKP :default))
                (list (cons :ideal-okp ,IDEAL-OKP)))))
          (value-triple (deref-macro-name ,FN (macro-aliases (w state))))))
      ((and condition-p
         (not (eq condition t))
         (not (eq condition nil))) `(make-event (let* ((wrld (w state)) (fn (deref-macro-name ,FN (macro-aliases wrld)))
              (condition ,CONDITION)
              (formals (and (symbolp fn) (getpropc fn 'formals t wrld)))
              (stobjs-in (getpropc fn 'stobjs-in t wrld))
              (condition-fn (or ,CONDITION-FN (add-suffix fn "-MEMOIZE-CONDITION")))
              (hints ,HINTS)
              (otf-flg ,OTF-FLG)
              (inline ,INLINE)
              (commutative ,COMMUTATIVE)
              (forget ,FORGET)
              (memo-table-init-size ,MEMO-TABLE-INIT-SIZE)
              (aokp ,AOKP)
              (stats ,STATS)
              (total ,TOTAL)
              (invoke ,INVOKE)
              (ideal-okp ,IDEAL-OKP))
            (cond ((not (and (symbolp fn)
                   (not (eq t formals))
                   (not (eq t stobjs-in))
                   (not (eq t (getpropc fn 'stobjs-out t wrld)))
                   (cltl-def-from-name fn wrld))) (er hard
                  'memoize
                  "The symbol ~x0 is not a known function symbol, and thus ~
                      it cannot be memoized."
                  fn))
              ((not (member-eq inline '(t nil))) (er hard
                  'memoize
                  "The value ~x0 for inline is illegal (must be ~x1 or ~
                      ~x2)."
                  inline
                  t
                  nil))
              (t `(progn (defun ,CONDITION-FN
                    ,FORMALS
                    (declare (ignorable ,@FORMALS)
                      (xargs :guard ,(GETPROPC FN 'GUARD *T* WRLD)
                        :verify-guards nil
                        ,@(LET ((STOBJS (COLLECT-NON-NIL-DF STOBJS-IN)))
    (AND STOBJS `(:STOBJS ,STOBJS))))
                      ,@(LET ((DFS (COLLECT-BY-POSITION '(:DF) STOBJS-IN FORMALS)))
    (AND DFS `((TYPE DOUBLE-FLOAT ,@DFS)))))
                    ,CONDITION)
                  (verify-guards ,CONDITION-FN
                    ,@(AND HINTS `(:HINTS ,HINTS))
                    ,@(AND OTF-FLG `(:OTF-FLG ,OTF-FLG)))
                  (table memoize-table
                    ',FN
                    (list* (cons :condition-fn ',CONDITION-FN)
                      (cons :inline ',INLINE)
                      (cons :commutative ',COMMUTATIVE)
                      (cons :forget ',FORGET)
                      (cons :memo-table-init-size (or ,MEMO-TABLE-INIT-SIZE *mht-default-size*))
                      (cons :aokp ',AOKP)
                      (cons :stats ,STATS)
                      (cons :total ',TOTAL)
                      (cons :invoke ',INVOKE)
                      (and (not (eq ',IDEAL-OKP :default))
                        (list (cons :ideal-okp ',IDEAL-OKP)))))
                  (value-triple ',FN)))))))
      (t `(progn (table memoize-table
            (deref-macro-name ,FN (macro-aliases world))
            (list* (cons :condition-fn ,CONDITION)
              (cons :inline ,INLINE)
              (cons :commutative ,COMMUTATIVE)
              (cons :forget ,FORGET)
              (cons :memo-table-init-size (or ,MEMO-TABLE-INIT-SIZE *mht-default-size*))
              (cons :aokp ',AOKP)
              (cons :stats ,STATS)
              (cons :total ,TOTAL)
              (cons :invoke ,INVOKE)
              (and (not (eq ',IDEAL-OKP :default))
                (list (cons :ideal-okp ',IDEAL-OKP)))))
          (value-triple (deref-macro-name ,FN (macro-aliases (w state)))))))))

memoizemacro

(defmacro memoize
  (fn &key
    (condition 't condition-p)
    condition-fn
    hints
    otf-flg
    (recursive ':default)
    commutative
    forget
    memo-table-init-size
    aokp
    (stats ':default)
    total
    invoke
    (ideal-okp ':default)
    (verbose 'nil))
  (declare (xargs :guard (member-eq recursive '(t nil :default)))
    (ignorable condition-p
      condition
      condition-fn
      hints
      otf-flg
      recursive
      commutative
      forget
      memo-table-init-size
      aokp
      stats
      total
      invoke
      ideal-okp
      verbose))
  (cond ((symbolp fn) (er hard
        'memoize
        "It is illegal for the first argument of MEMOIZE to be a symbol.  ~
         Note that the arguments to MEMOIZE are evaluated; so perhaps you ~
         intended the first argument to be (QUOTE ~x0) or, equivalently, '~x0."
        fn))
    ((and invoke (symbolp invoke)) (er hard
        'memoize
        "It is illegal for the :INVOKE argument of MEMOIZE to be a symbol.  ~
         Note that the arguments to MEMOIZE are evaluated; so perhaps you ~
         intended that argument to be (QUOTE ~x0) or, equivalently, '~x0."
        invoke))
    (t (let* ((inline (if (eq recursive :default)
             (if invoke
               nil
               t)
             recursive)) (condition (cond ((and invoke (not condition-p) (not condition-fn)) nil)
              (t condition)))
          (stats (if (and invoke (eq stats :default))
              nil
              stats))
          (form (cond ((eq commutative t) `(make-event (let* ((fn ,FN) (commutative (add-suffix fn "-COMMUTATIVE")))
                    (list 'encapsulate
                      nil
                      (list 'value-triple
                        (kwote (cons (max-absolute-event-number (w state))
                            (car (global-val 'include-book-path (w state))))))
                      (list 'defthm
                        commutative
                        (list 'equal (list fn 'x 'y) (list fn 'y 'x))
                        :rule-classes nil)
                      (memoize-form (kwote fn)
                        ',CONDITION
                        ',CONDITION-P
                        ',CONDITION-FN
                        ',HINTS
                        ',OTF-FLG
                        ',INLINE
                        (kwote commutative)
                        ',FORGET
                        ',MEMO-TABLE-INIT-SIZE
                        ',AOKP
                        ',STATS
                        ',TOTAL
                        ',INVOKE
                        ',IDEAL-OKP)))))
              (t (memoize-form fn
                  condition
                  condition-p
                  condition-fn
                  hints
                  otf-flg
                  inline
                  commutative
                  forget
                  memo-table-init-size
                  aokp
                  stats
                  total
                  invoke
                  ideal-okp)))))
        (cond (verbose form)
          (t `(with-output :off (summary prove event) :gag-mode nil ,FORM)))))))

unmemoizemacro

(defmacro unmemoize
  (fn)
  (declare (xargs :guard t))
  `(with-output :off summary
    (progn (table memoize-table
        (deref-macro-name ,FN (macro-aliases world))
        nil)
      (value-triple (deref-macro-name ,FN (macro-aliases (w state)))))))

profilemacro

(defmacro profile
  (fn &rest r)
  (declare (xargs :guard (and (keyword-value-listp r)
        (not (assoc-keyword :condition r))
        (not (assoc-keyword :condition-fn r))
        (not (assoc-keyword :recursive r)))))
  `(memoize ,FN :condition nil :recursive nil ,@R))

memoizedp-worldmacro

(defmacro memoizedp-world
  (fn wrld)
  `(cdr (assoc-eq ,FN (table-alist 'memoize-table ,WRLD))))

memoizedpmacro

(defmacro memoizedp
  (fn)
  (declare (xargs :guard t))
  `(memoizedp-world ,FN (w state)))

never-memoize-fnfunction

(defun never-memoize-fn
  (fn)
  (declare (xargs :guard (symbolp fn))
    (ignore fn))
  nil)

never-memoizemacro

(defmacro never-memoize
  (fn)
  (declare (xargs :guard (symbolp fn)))
  `(make-event (prog2$ (never-memoize-fn ',FN) '(value-triple :invisible))
    :check-expansion t))

*bad-lisp-consp-memoization*constant

(defconst *bad-lisp-consp-memoization*
  '(bad-lisp-consp :forget t))

*thread-unsafe-builtin-memoizations*constant

(defconst *thread-unsafe-builtin-memoizations*
  (list *bad-lisp-consp-memoization*))

set-bad-lisp-consp-memoizefunction

(defun set-bad-lisp-consp-memoize
  (arg)
  (declare (xargs :guard t)
    (ignore arg))
  nil)

*special-cltl-cmd-attachment-mark-name*constant

(defconst *special-cltl-cmd-attachment-mark-name*
  ':apply$-userfn/badge-userfn)

*special-cltl-cmd-attachment-mark*constant

(defconst *special-cltl-cmd-attachment-mark*
  `(attachment ,*SPECIAL-CLTL-CMD-ATTACHMENT-MARK-NAME*))