; Copyright (C) 2020, ForrestHunt, Inc.
; Written by Matt Kaufmann
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.

; Tests for memoization with partial functions (MEMOIZE option :PARTIAL)

(in-package "ACL2")

(include-book "std/testing/must-fail" :dir :system)

(defmacro mf (form &key (expected ':soft))
  `(must-fail ,form
              :expected
              ,expected
              :with-output-off
              (proof-tree prove event summary proof-builder history)))

(set-compile-fns t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Singly-recursive example
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; A demo could be enhanced with this:
; (trace! (memoize-fn :native t))

; We introduce a function that stops when the recursion limit is reached.  Here
; we have a fibonacci function that would fail to terminate on negative
; integers without that limit.

(defun fib-limit (n limit)
  (declare (type (integer 0 *) limit)
           (type integer n))
  (declare (xargs :measure (nfix limit)))
  (if (zp limit)
      0 ; any term is fine here
    (let ((limit (1- limit)))
      (if (or (= n 0) (= n 1))
          1
        (+ (fib-limit (- n 1) limit)
           (fib-limit (- n 2) limit))))))

; Now introduce a function, fib, that is the value of fib-limit when the
; algorithm terminates.  The events that are introduced are shown just below,
; as redundant.

(memoize-partial fib) ; equivalent to (memoize-partial ((fib fib-limit)))

; Test that we get the expected value.  Note that (fib 30) is evaluated using
; the definition of fib that is installed by memoize-partial.
(assert-event (equal (fib 30)
                     (fib-limit 30 50)))

; Test memoization:
(assert-event (equal (fib 100)
                     573147844013817084101))

; The events in the encapsulate below are generated by the memoize-partial form
; just above.  They are all redundant; we ensure that they are as follows (this
; is local to the encapsulate):

(set-enforce-redundancy t)

(encapsulate
  ()

  (DEFCHOOSE FIB-LIMIT-CHANGE (LARGE) (N LIMIT)
    (AND (NATP LARGE)
         (<= LIMIT LARGE)
         (NOT (EQUAL (FIB-LIMIT N LIMIT)
                     (FIB-LIMIT N LARGE)))))

  (DEFCHOOSE FIB-LIMIT-STABLE (LIMIT) (N)
    (AND (NATP LIMIT)
         (EQUAL (FIB-LIMIT N LIMIT)
                (FIB-LIMIT N (FIB-LIMIT-CHANGE N LIMIT)))))

  (DEFUN FIB (N)
    (DECLARE (TYPE INTEGER N)
             (XARGS :GUARD T))
    (FIB-LIMIT N (NFIX (NON-EXEC (FIB-LIMIT-STABLE N)))))

  (TABLE PARTIAL-FUNCTIONS-TABLE 'FIB-LIMIT
         '((FIB FIB-LIMIT
                FIB-LIMIT-CHANGE FIB-LIMIT-STABLE
                (DEFUN FIB (N)
                  (DECLARE (IGNORABLE N))
                  (DECLARE (TYPE INTEGER N))
                  (FLET ((FIB-LIMIT (N LIMIT)
                                    (DECLARE (IGNORE LIMIT))
                                    (FIB N)))
                        (DECLARE (INLINE FIB-LIMIT))
                        (LET ((LIMIT 0))
                             (DECLARE (IGNORABLE LIMIT))
                             (IF (OR (= N 0) (= N 1))
                                 1
                                 (+ (FIB-LIMIT (- N 1) LIMIT)
                                    (FIB-LIMIT (- N 2) LIMIT)))))))))

  (MEMOIZE 'FIB :TOTAL 'FIB-LIMIT)
  )

(set-enforce-redundancy nil)

; And here is the raw Lisp memoization form evaluated above:
#||
(MEMOIZE-FN
 'FIB
 :CONDITION T
 :INLINE T
 :CL-DEFUN '(DEFUN FIB (N)
              (DECLARE (IGNORABLE N))
              (DECLARE (TYPE INTEGER N))
              (FLET ((FIB-LIMIT (N LIMIT)
                                (DECLARE (IGNORE LIMIT))
                                (FIB N)))
                    (DECLARE (INLINE FIB-LIMIT))
                    (LET ((LIMIT 0))
                         (DECLARE (IGNORABLE LIMIT))
                         (IF (OR (= N 0) (= N 1))
                             1
                             (+ (FIB-LIMIT (- N 1) LIMIT)
                                (FIB-LIMIT (- N 2) LIMIT))))))
 :FORMALS '(N)
 :STOBJS-IN '(NIL)
 :STOBJS-OUT '(NIL)
 :COMMUTATIVE NIL
 :FORGET NIL
 :MEMO-TABLE-INIT-SIZE 60
 :AOKP NIL)

||#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Singly-recursive example testing more features
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; We tweak the first example just to stress things a bit.

(defun fib2-clock (n clock)
; This time let's declare with :guard instead of type.
  (declare (xargs :guard (natp clock))
           (xargs :guard (integerp n)
                  :verify-guards nil
                  :guard-debug t))
  (declare (xargs :measure (nfix clock)))
  (if (zp clock)
      0 ; any term is fine here
    (let ((clock (1- clock)))
      (if (or (= n 0) (= n 1))
          1
        (+ (fib2-clock (- n 1) clock)
           (fib2-clock (- n 2) clock))))))

(verify-guards fib2-clock)

(memoize-partial ((fib2 fib2-clock
                        :change fib2-clock-change0
                        :stable fib2-clock-stable0
                        :condition '(eql (mod n 4) 0)))
                 :condition t)

(encapsulate ()

; The three events below are generated by the memoize-partial form just above.
; They are all redundant; we ensure that they are as follows (this is local to
; the encapsulate):
(set-enforce-redundancy t)

(DEFCHOOSE FIB2-CLOCK-CHANGE0 (LARGE) (N CLOCK)
  (AND (NATP LARGE)
       (<= CLOCK LARGE)
       (NOT (EQUAL (FIB2-CLOCK N CLOCK)
                   (FIB2-CLOCK N LARGE)))))

(DEFCHOOSE FIB2-CLOCK-STABLE0 (CLOCK) (N)
  (AND (NATP CLOCK)
       (EQUAL (FIB2-CLOCK N CLOCK)
              (FIB2-CLOCK N (FIB2-CLOCK-CHANGE0 N CLOCK)))))

(DEFUN FIB2 (N)
  (DECLARE (XARGS :GUARD (LET ((CLOCK 0))
                           (DECLARE (IGNORABLE CLOCK))
                           (AND (NATP CLOCK)
                                (INTEGERP N)))))
  (FIB2-CLOCK N (NFIX (NON-EXEC (FIB2-CLOCK-STABLE0 N)))))

)

; Test that we get the expected value:
(assert-event (equal (fib2 30)
                     (fib2-clock 30 50)))

; Test memoization:
(assert-event (equal (fib2 80) ; 100 can get us into bignums; slow!
                     37889062373143906))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Singly-recursive example with multiple value return
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun fib-mv-limit (n limit)
  (declare (type (integer 0 *) limit)
           (type integer n))
  (declare (xargs :measure (nfix limit)
                  :verify-guards nil))
  (if (zp limit)
      (mv 0 0) ; any term is fine here
    (let ((limit (1- limit)))
      (if (or (= n 0) (= n 1))
          (mv 1 1)
        (mv-let (x1 y1)
          (fib-mv-limit (- n 1) limit)
          (mv-let (x2 y2)
            (fib-mv-limit (- n 2) limit)
            (mv (+ x1 x2) (+ y1 y2))))))))

(defthm natp-fib-mv-limit-0
  (natp (car (fib-mv-limit n limit)))
  :rule-classes :type-prescription)

(defthm natp-fib-mv-limit-1
  (natp (mv-nth 1 (fib-mv-limit n limit)))
  :rule-classes :type-prescription)

(verify-guards fib-mv-limit)

(memoize-partial fib-mv)

(assert-event (mv-let (a b)
                (fib-mv 80)
                (and (equal a 37889062373143906)
                     (equal b 37889062373143906))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Mutual-recursion example 1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Adapted from :doc mutual-recursion:
(mutual-recursion
 (defun evenlp-bdd (x bound)
   (declare (xargs :guard (natp bound)))
   (if (zp bound)
       'ouch
     (let ((bound (1- bound)))
       (if (consp x) (oddlp-bdd (cdr x) bound) t))))
 (defun oddlp-bdd (x bound)
   (declare (xargs :guard (natp bound)))
   (if (zp bound)
       'ouch
     (let ((bound (1- bound)))
       (if (consp x) (evenlp-bdd (cdr x) bound) nil)))))

(memoize-partial ((evenlp evenlp-bdd) (oddlp oddlp-bdd)))

(set-enforce-redundancy t)

(encapsulate
  ()

; The events below are generated by the memoize-partial form just above.
; They are all redundant; we ensure that they are as follows (this is local to
; the encapsulate):

  (DEFCHOOSE EVENLP-BDD-CHANGE (LARGE)
    (X BOUND)
    (AND (NATP LARGE)
         (<= BOUND LARGE)
         (NOT (EQUAL (EVENLP-BDD X BOUND)
                     (EVENLP-BDD X LARGE)))))

  (DEFCHOOSE EVENLP-BDD-STABLE (BOUND)
    (X)
    (AND (NATP BOUND)
         (EQUAL (EVENLP-BDD X BOUND)
                (EVENLP-BDD X (EVENLP-BDD-CHANGE X BOUND)))))

  (DEFUN EVENLP (X)
    (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                (DECLARE (IGNORABLE BOUND))
                                (NATP BOUND))))
    (EVENLP-BDD X (NFIX (NON-EXEC (EVENLP-BDD-STABLE X)))))

  (DEFCHOOSE ODDLP-BDD-CHANGE (LARGE)
    (X BOUND)
    (AND (NATP LARGE)
         (<= BOUND LARGE)
         (NOT (EQUAL (ODDLP-BDD X BOUND)
                     (ODDLP-BDD X LARGE)))))

  (DEFCHOOSE ODDLP-BDD-STABLE (BOUND)
    (X)
    (AND (NATP BOUND)
         (EQUAL (ODDLP-BDD X BOUND)
                (ODDLP-BDD X (ODDLP-BDD-CHANGE X BOUND)))))

  (DEFUN ODDLP (X)
    (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                (DECLARE (IGNORABLE BOUND))
                                (NATP BOUND))))
    (ODDLP-BDD X (NFIX (NON-EXEC (ODDLP-BDD-STABLE X)))))

  (TABLE PARTIAL-FUNCTIONS-TABLE 'EVENLP-BDD
         '((EVENLP EVENLP-BDD
                   EVENLP-BDD-CHANGE EVENLP-BDD-STABLE
                   (DEFUN EVENLP (X)
                     (DECLARE (IGNORABLE X))
                     (FLET ((EVENLP-BDD (X BOUND)
                                        (DECLARE (IGNORE BOUND))
                                        (EVENLP X))
                            (ODDLP-BDD (X BOUND)
                                       (DECLARE (IGNORE BOUND))
                                       (ODDLP X)))
                           (DECLARE (INLINE EVENLP-BDD))
                           (LET ((BOUND 0))
                                (DECLARE (IGNORABLE BOUND))
                                (IF (CONSP X)
                                    (ODDLP-BDD (CDR X) BOUND)
                                    T)))))
           (ODDLP ODDLP-BDD
                  ODDLP-BDD-CHANGE ODDLP-BDD-STABLE
                  (DEFUN ODDLP (X)
                    (DECLARE (IGNORABLE X))
                    (FLET ((EVENLP-BDD (X BOUND)
                                       (DECLARE (IGNORE BOUND))
                                       (EVENLP X))
                           (ODDLP-BDD (X BOUND)
                                      (DECLARE (IGNORE BOUND))
                                      (ODDLP X)))
                          (DECLARE (INLINE ODDLP-BDD))
                          (LET ((BOUND 0))
                               (DECLARE (IGNORABLE BOUND))
                               (IF (CONSP X)
                                   (EVENLP-BDD (CDR X) BOUND)
                                   NIL)))))))
  (MEMOIZE 'EVENLP :TOTAL 'EVENLP-BDD)
  (MEMOIZE 'ODDLP :TOTAL 'ODDLP-BDD)
  )

(set-enforce-redundancy nil)

(assert-event (evenlp '(1 2 3 4 5 6)))

(assert-event (not (oddlp '(1 2 3 4 5 6))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Mutual-recursion example 2
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; This is a variant of the mutual-recursion nest for ACL2 source function
; worse-than-builtin-clocked.  Comments from those definitions are omitted
; here.

(defmacro xx-worse-than-builtin-clocked-body (clk)
  (declare (xargs :guard (atom clk))) ; avoid repeated evaluation of clk
  `(cond
    ((basic-xx-worse-than term1 term2 ,clk) t)
    ((pseudo-variantp term1 term2) nil)
    ((variablep term1)
     nil)
    ((fquotep term1)
     nil)
    (t (xx-worse-than-lst (fargs term1) term2 ,clk))))

(mutual-recursion

(defun xx-worse-than-builtin-clocked (term1 term2 clk)
  (declare
   (type (integer 0 *) clk)
   (xargs :guard (and (pseudo-termp term1)
                      (pseudo-termp term2))
          :measure (nfix clk)
          :well-founded-relation o<))
  (cond
   ((zp clk)
    nil)
   (t (let ((clk (1- clk)))
        (xx-worse-than-builtin-clocked-body clk)))))

(defun xx-worse-than-or-equal-builtin-clocked (term1 term2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-termp term1)
                              (pseudo-termp term2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (if (zp clk)
      nil
    (let ((clk (1- clk)))
      (if (pseudo-variantp term1 term2)
          (equal term1 term2)
        (xx-worse-than-builtin-clocked term1 term2 clk)))))

(defun basic-xx-worse-than-lst1 (args1 args2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-term-listp args1)
                              (pseudo-term-listp args2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (cond ((zp clk) nil)
        (t (let ((clk (1- clk)))
             (cond
              ((endp args1) nil)
              ((endp args1) nil)
              ((or (and (or (variablep (car args1))
                            (fquotep (car args1)))
                        (not (or (variablep (car args2))
                                 (fquotep (car args2)))))
                   (xx-worse-than-builtin-clocked (car args2)
                                               (car args1)
                                               clk))
               t)
              (t (basic-xx-worse-than-lst1 (cdr args1)
                                        (cdr args2)
                                        clk)))))))

(defun basic-xx-worse-than-lst2 (args1 args2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-term-listp args1)
                              (pseudo-term-listp args2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (cond ((zp clk) nil)
        (t (let ((clk (1- clk)))
             (cond
              ((endp args1) nil)
              ((xx-worse-than-builtin-clocked (car args1) (car args2) clk) t)
              (t (basic-xx-worse-than-lst2 (cdr args1) (cdr args2) clk)))))))

(defun basic-xx-worse-than (term1 term2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-termp term1)
                              (pseudo-termp term2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (cond ((zp clk) nil)
        (t (let ((clk (1- clk)))
             (cond
              ((variablep term2)
               (cond ((eq term1 term2) nil)
                     (t (occur term2 term1))))
              ((fquotep term2)
               (cond ((variablep term1) t)
                     ((fquotep term1)
                      (> (fn-count-evg (cadr term1))
                         (fn-count-evg (cadr term2))))
                     (t t)))
              ((variablep term1) nil)
              ((fquotep term1) nil)
              ((cond ((flambda-applicationp term1)
                      (equal (ffn-symb term1) (ffn-symb term2)))
                     (t (eq (ffn-symb term1) (ffn-symb term2))))
               (cond ((pseudo-variantp term1 term2) nil)
                     (t (cond ((basic-xx-worse-than-lst1 (fargs term1)
                                                      (fargs term2)
                                                      clk)
                               nil)
                              (t (basic-xx-worse-than-lst2 (fargs term1)
                                                        (fargs term2)
                                                        clk))))))
              (t nil))))))

(defun some-subterm-xx-worse-than-or-equal (term1 term2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-termp term1)
                              (pseudo-termp term2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (cond
   ((zp clk) nil)
   (t (let ((clk (1- clk)))
        (cond
         ((variablep term1) (eq term1 term2))
         ((if (pseudo-variantp term1 term2)
              (equal term1 term2)
            (basic-xx-worse-than term1 term2 clk))
          t)
         ((fquotep term1) nil)
         (t (some-subterm-xx-worse-than-or-equal-lst (fargs term1)
                                                  term2
                                                  clk)))))))

(defun some-subterm-xx-worse-than-or-equal-lst (args term2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-term-listp args)
                              (pseudo-termp term2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (cond
   ((zp clk) nil)
   (t (let ((clk (1- clk)))
        (cond
         ((endp args) nil)
         (t (or (some-subterm-xx-worse-than-or-equal (car args) term2 clk)
                (some-subterm-xx-worse-than-or-equal-lst (cdr args) term2 clk))))))))

(defun xx-worse-than-lst (args term2 clk)
  (declare (type (integer 0 *) clk)
           (xargs :guard (and (pseudo-term-listp args)
                              (pseudo-termp term2))
                  :measure (nfix clk)
                  :well-founded-relation o<))
  (cond ((zp clk) nil)
        (t (let ((clk (1- clk)))
             (cond
              ((endp args) nil)
              (t (or (some-subterm-xx-worse-than-or-equal (car args) term2 clk)
                     (xx-worse-than-lst (cdr args) term2 clk))))))))

)

(memoize-partial
 ((xx-worse-than* xx-worse-than-builtin-clocked
                  :condition nil) ; check that this still supports evaluation
  (xx-worse-than-or-equal* xx-worse-than-or-equal-builtin-clocked)
  (basic-xx-worse-than-lst1* basic-xx-worse-than-lst1)
  (basic-xx-worse-than-lst2* basic-xx-worse-than-lst2)
  (basic-xx-worse-than* basic-xx-worse-than)
  (some-subterm-xx-worse-than-or-equal* some-subterm-xx-worse-than-or-equal)
  (some-subterm-xx-worse-than-or-equal-lst*
   some-subterm-xx-worse-than-or-equal-lst)
  (xx-worse-than-lst* xx-worse-than-lst)))

; Tests derived from (trace$ worse-than-or-equal) followed by :mini-proveall:

(assert-event
 (equal (xx-worse-than* '(mem (car (del a x)) x)
                        '(mem (car (del a x)) y))
        nil))

(assert-event
 (equal
  (xx-worse-than-or-equal* '(mem (car z) x)
                           '(perm z y))
  nil))

(assert-event
 (equal
  (xx-worse-than-or-equal* '(perm (del (car z) x) (cdr z))
                           '(perm z x))
  t))

; Now repeat the tests above, except this time use :condition nil on all
; functions.  First check though that :recursive nil doesn't work; we wouldn't
; expect it to work, since we need the recursive calls to be executable, too.
; Note that profile is just memoize with :condition nil :recursive nil; so we
; can't exactly be profiling when we use memoize-partial.  Still we expect or
; at least hope that the overhead of :condition nil by itself is still minor.

(u)

(with-output :off :all
(memoize-partial
 ((xx-worse-than* xx-worse-than-builtin-clocked
                  :recursive nil) ; ruins support for execution
  (xx-worse-than-or-equal* xx-worse-than-or-equal-builtin-clocked)
  (basic-xx-worse-than-lst1* basic-xx-worse-than-lst1)
  (basic-xx-worse-than-lst2* basic-xx-worse-than-lst2)
  (basic-xx-worse-than* basic-xx-worse-than)
  (some-subterm-xx-worse-than-or-equal* some-subterm-xx-worse-than-or-equal)
  (some-subterm-xx-worse-than-or-equal-lst*
   some-subterm-xx-worse-than-or-equal-lst)
  (xx-worse-than-lst* xx-worse-than-lst)))
)

(mf
 (assert-event
  (equal (xx-worse-than* '(mem (car (del a x)) x)
                         '(mem (car (del a x)) y))
         nil)))

(u)

; Now memoize with :condition nil for all the functions, but not :recursive
; nil, using the same three tests that succeeded above.

(with-output :off :all
(memoize-partial
 ((xx-worse-than* xx-worse-than-builtin-clocked)
  (xx-worse-than-or-equal* xx-worse-than-or-equal-builtin-clocked)
  (basic-xx-worse-than-lst1* basic-xx-worse-than-lst1)
  (basic-xx-worse-than-lst2* basic-xx-worse-than-lst2)
  (basic-xx-worse-than* basic-xx-worse-than)
  (some-subterm-xx-worse-than-or-equal* some-subterm-xx-worse-than-or-equal)
  (some-subterm-xx-worse-than-or-equal-lst*
   some-subterm-xx-worse-than-or-equal-lst)
  (xx-worse-than-lst* xx-worse-than-lst))
 :condition nil)
)

(assert-event
 (equal (xx-worse-than* '(mem (car (del a x)) x)
                        '(mem (car (del a x)) y))
        nil))

(assert-event
 (equal
  (xx-worse-than-or-equal* '(mem (car z) x)
                           '(perm z y))
  nil))

(assert-event
 (equal
  (xx-worse-than-or-equal* '(perm (del (car z) x) (cdr z))
                           '(perm z x))
  t))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Failures
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; This section tests some more failures.

(defun bad{wrong-form}-limit (n limit)
  (declare (type (integer 0 *) limit)
           (type (integer 0 *) n)
           (xargs :verify-guards nil))
  (if (zp limit)
      0 ; any term is fine here
    (let ((limit (1+ limit)))
      (if (or (zp n) (= n 1))
          1
        (+ (bad{wrong-form}-limit (- n 1) limit)
           (bad{wrong-form}-limit (- n 2) limit))))))

(mf
#||
ACL2 Error in MEMOIZE-PARTIAL:  The function BAD{WRONG-FORM}-LIMIT
is not guard-verified.
||#
 (memoize-partial bad{wrong-form}))

(verify-guards bad{wrong-form}-limit)

(mf (memoize-partial
#||
ACL2 Error in MEMOIZE-PARTIAL:  The (untranslated) body of function
BAD{WRONG-FORM}-LIMIT is not of the appropriate form.  See :DOC memoize-
partial.
||#
     bad{wrong-form}))


(defun bad{uses-limit}-limit (n limit)
  (declare (type (integer 0 *) limit)
           (type integer n))
  (declare (xargs :measure (nfix limit)))
  (if (zp limit)
      0 ; any term is fine here
    (let ((limit (1- limit)))
      (if (or (= n 0) (= n 1))
          1
        (+ (bad{uses-limit}-limit (+ limit (- n 1)) limit)
           (bad{uses-limit}-limit (- n 2) limit))))))

(mf (memoize-partial
#||
Reason:
The limit variable LIMIT occurs free, where it should not, in the body
of the definition of function BAD{USES-LIMIT}-LIMIT.
||#
     bad{uses-limit}))

(defn bad{one-formal}-limit (limit)
  (declare (xargs :guard (natp limit)))
  (if (zp limit)
      limit
    (let ((limit (1- limit)))
      (bad{one-formal}-limit limit))))

(mf (memoize-partial
#||
Reason:
The function symbol BAD{ONE-FORMAL}-LIMIT must have at least two formal
parameters.
||#
     bad{one-formal}))

(mutual-recursion ; based on evenlp-bdd/oddlp-bdd above
 (defun evenlp{different-limit-vars}-bdd (x bound)
   (declare (xargs :guard (natp bound)))
   (if (zp bound)
       'ouch
     (let ((bound (1- bound)))
       (if (consp x) (oddlp{different-limit-vars}-bdd (cdr x) bound) t))))
 (defun oddlp{different-limit-vars}-bdd (x bound2)
   (declare (xargs :guard (natp bound2)))
   (if (zp bound2)
       'ouch
     (let ((bound2 (1- bound2)))
       (if (consp x) (evenlp{different-limit-vars}-bdd (cdr x) bound2) nil)))))

(mf
#||
Reason:
The formal parameter lists for function symbols
EVENLP{DIFFERENT-LIMIT-VARS}-BDD and ODDLP{DIFFERENT-LIMIT-VARS}-BDD
have different final elements (of BOUND and BOUND2, respectively).
||#
 (memoize-partial
  ((evenlp{different-limit-vars} evenlp{different-limit-vars}-bdd)
   (oddlp{different-limit-vars} oddlp{different-limit-vars}-bdd))))

(defmacro my-if (x y z)
  `(if ,x ,y ,z))

(defun bad{wrong-if}-limit (n limit)
  (declare (type (integer 0 *) limit)
           (type (integer 0 *) n))
  (my-if (zp limit)
         0 ; any term is fine here
         (let ((limit (1- limit)))
           (if (or (zp n) (= n 1))
               1
             (+ (bad{wrong-if}-limit (- n 1) limit)
                (bad{wrong-if}-limit (- n 2) limit))))))

(mf (memoize-partial
#||
ACL2 Error in MEMOIZE-PARTIAL:  The (untranslated) body of function
BAD{WRONG-IF}-LIMIT is not of the appropriate form.  See :DOC memoize-
partial.
||#
     bad{wrong-if}))

(defun bad{wrong-zp}-limit (n limit)
  (declare (type (integer 0 *) limit)
           (type (integer 0 *) n))
  (if (not (posp limit))
      0 ; any term is fine here
    (let ((limit (1- limit)))
      (if (or (zp n) (= n 1))
          1
        (+ (bad{wrong-zp}-limit (- n 1) limit)
           (bad{wrong-zp}-limit (- n 2) limit))))))

(mf (memoize-partial
#||
ACL2 Error in MEMOIZE-PARTIAL:  The (untranslated) body of function
BAD{WRONG-ZP}-LIMIT is not of the appropriate form.  See :DOC memoize-
partial.
||#
     bad{wrong-zp}))

(mf (memoize-partial
#||
ACL2 Error in MEMOIZE-PARTIAL:  Please define MY-UNDEF-LIMIT before
submitting your memoize-partial form.
||#
     my-undef))

(defun bad{non-rec}-limit (x limit)
  (declare (type (integer 0 *) limit))
  (if (zp limit)
      0 ; any term is fine here
    (let ((limit (1- limit)))
      (cons x limit))))

(mf (memoize-partial
#||
Reason:
The key is a non-recursive function symbol.
||#
     bad{non-rec}))

(unmemoize 'evenlp)
(unmemoize 'oddlp)

(mf (memoize-partial
#||
Reason:
The strip-cadrs of the proposed value is not the list of functions,
in order, defined by mutual-recursion with the key.  That expected
list of functions is (EVENLP-BDD ODDLP-BDD).
||#
     ((evenlp evenlp-bdd))))

(mf (memoize-partial
#||
Reason:
The strip-cadrs of the proposed value is not the list of functions,
in order, defined by mutual-recursion with the key.  That expected
list of functions is (EVENLP-BDD ODDLP-BDD).
||#
     ((oddlp oddlp-bdd))))

; The following fails too, because the tuples are out of order.
(mf (memoize-partial
#||
Reason:
The strip-cadrs of the proposed value is not the list of functions,
in order, defined by mutual-recursion with the key.  That expected
list of functions is (EVENLP-BDD ODDLP-BDD).
||#
     ((oddlp oddlp-bdd) (evenlp evenlp-bdd))))

; Let's revisit the evenlp/oddlp example above, this time seeing errors about
; missing events.

(mutual-recursion
 (defun evenlp2-bdd (x bound)
   (declare (xargs :guard (natp bound)))
   (if (zp bound)
       'ouch
     (let ((bound (1- bound)))
       (if (consp x) (oddlp2-bdd (cdr x) bound) t))))
 (defun oddlp2-bdd (x bound)
   (declare (xargs :guard (natp bound)))
   (if (zp bound)
       'ouch
     (let ((bound (1- bound)))
       (if (consp x) (evenlp2-bdd (cdr x) bound) nil)))))

(mf
#||
Reason:
The following event is missing:

(DEFUN ODDLP2 (X)
       (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                   (DECLARE (IGNORABLE BOUND))
                                   (NATP BOUND))))
       (ODDLP2-BDD X (NFIX (ODDLP2-BDD-STABLE X))))
||#
(encapsulate ()

; The events below are generated by the memoize-partial form just above.
; They are all redundant; we ensure that they are as follows (this is local to
; the encapsulate):
;(set-enforce-redundancy t)

(DEFCHOOSE EVENLP2-BDD-CHANGE (LARGE)
  (X BOUND)
  (AND (NATP LARGE)
       (<= BOUND LARGE)
       (NOT (EQUAL (EVENLP2-BDD X BOUND)
                   (EVENLP2-BDD X LARGE)))))

(DEFCHOOSE EVENLP2-BDD-STABLE (BOUND)
  (X)
  (AND (NATP BOUND)
       (EQUAL (EVENLP2-BDD X BOUND)
              (EVENLP2-BDD X (EVENLP2-BDD-CHANGE X BOUND)))))

(DEFUN EVENLP2 (X)
  (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (NATP BOUND))))
  (EVENLP2-BDD X (NFIX (NON-EXEC (EVENLP2-BDD-STABLE X)))))

(DEFCHOOSE ODDLP2-BDD-CHANGE (LARGE)
  (X BOUND)
  (AND (NATP LARGE)
       (<= BOUND LARGE)
       (NOT (EQUAL (ODDLP2-BDD X BOUND)
                   (ODDLP2-BDD X LARGE)))))

(DEFCHOOSE ODDLP2-BDD-STABLE (BOUND)
  (X)
  (AND (NATP BOUND)
       (EQUAL (ODDLP2-BDD X BOUND)
              (ODDLP2-BDD X (ODDLP2-BDD-CHANGE X BOUND)))))

; Missing!
#||
(DEFUN ODDLP2 (X)
  (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (NATP BOUND))))
  (ODDLP2-BDD X (NFIX (NON-EXEC (ODDLP2-BDD-STABLE X)))))
||#

(TABLE PARTIAL-FUNCTIONS-TABLE 'EVENLP2-BDD
       '((EVENLP2 EVENLP2-BDD
                 EVENLP2-BDD-CHANGE EVENLP2-BDD-STABLE
                 (DEFUN EVENLP2 (X)
                   (DECLARE (IGNORABLE X))
                   (FLET ((EVENLP2-BDD (X BOUND)
                                      (DECLARE (IGNORE BOUND))
                                      (EVENLP2 X))
                          (ODDLP2-BDD (X BOUND)
                                     (DECLARE (IGNORE BOUND))
                                     (ODDLP2 X)))
                         (DECLARE (INLINE EVENLP2-BDD))
                         (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (IF (CONSP X)
                                  (ODDLP2-BDD (CDR X) BOUND)
                                  T)))))
         (ODDLP2 ODDLP2-BDD
                ODDLP2-BDD-CHANGE ODDLP2-BDD-STABLE
                (DEFUN ODDLP2 (X)
                  (DECLARE (IGNORABLE X))
                  (FLET ((EVENLP2-BDD (X BOUND)
                                     (DECLARE (IGNORE BOUND))
                                     (EVENLP2 X))
                         (ODDLP2-BDD (X BOUND)
                                    (DECLARE (IGNORE BOUND))
                                    (ODDLP2 X)))
                        (DECLARE (INLINE ODDLP2-BDD))
                        (LET ((BOUND 0))
                             (DECLARE (IGNORABLE BOUND))
                             (IF (CONSP X)
                                 (EVENLP2-BDD (CDR X) BOUND)
                                 NIL)))))))

  (MEMOIZE 'EVENLP2 :TOTAL 'EVENLP2-BDD)
  (MEMOIZE 'ODDLP2 :TOTAL 'ODDLP2-BDD)
)
)

(mf
#||
Reason:
The following events are missing:

(DEFUN EVENLP2 (X)
       (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                                   (DECLARE (IGNORABLE BOUND))
                                   (NATP BOUND))))
       (EVENLP2-BDD X (NFIX (EVENLP2-BDD-STABLE X))))

(DEFUN ODDLP2 (X)
       (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (NATP BOUND))))
       (ODDLP2-BDD X (NFIX (ODDLP2-BDD-STABLE X))))
||#
(encapsulate ()

(DEFCHOOSE EVENLP2-BDD-CHANGE (LARGE)
  (X BOUND)
  (AND (NATP LARGE)
       (<= BOUND LARGE)
       (NOT (EQUAL (EVENLP2-BDD X BOUND)
                   (EVENLP2-BDD X LARGE)))))

(DEFCHOOSE EVENLP2-BDD-STABLE (BOUND)
  (X)
  (AND (NATP BOUND)
       (EQUAL (EVENLP2-BDD X BOUND)
              (EVENLP2-BDD X (EVENLP2-BDD-CHANGE X BOUND)))))

; Wrong!
(DEFUN EVENLP2 (X)
  (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (NATP BOUND))))
  x)

(DEFCHOOSE ODDLP2-BDD-CHANGE (LARGE)
  (X BOUND)
  (AND (NATP LARGE)
       (<= BOUND LARGE)
       (NOT (EQUAL (ODDLP2-BDD X BOUND)
                   (ODDLP2-BDD X LARGE)))))

(DEFCHOOSE ODDLP2-BDD-STABLE (BOUND)
  (X)
  (AND (NATP BOUND)
       (EQUAL (ODDLP2-BDD X BOUND)
              (ODDLP2-BDD X (ODDLP2-BDD-CHANGE X BOUND)))))

; Missing!
#||
(DEFUN ODDLP2 (X)
  (DECLARE (XARGS :GUARD (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (NATP BOUND))))
  (ODDLP2-BDD X (NFIX (ODDLP2-BDD-STABLE X))))
||#

(TABLE PARTIAL-FUNCTIONS-TABLE 'EVENLP2-BDD
       '((EVENLP2 EVENLP2-BDD
                 EVENLP2-BDD-CHANGE EVENLP2-BDD-STABLE
                 (DEFUN EVENLP2 (X)
                   (DECLARE (IGNORABLE X))
                   (FLET ((EVENLP2-BDD (X BOUND)
                                      (DECLARE (IGNORE BOUND))
                                      (EVENLP2 X))
                          (ODDLP2-BDD (X BOUND)
                                     (DECLARE (IGNORE BOUND))
                                     (ODDLP2 X)))
                         (DECLARE (INLINE EVENLP2-BDD))
                         (LET ((BOUND 0))
                              (DECLARE (IGNORABLE BOUND))
                              (IF (CONSP X)
                                  (ODDLP2-BDD (CDR X) BOUND)
                                  T)))))
         (ODDLP2 ODDLP2-BDD
                ODDLP2-BDD-CHANGE ODDLP2-BDD-STABLE
                (DEFUN ODDLP2 (X)
                  (DECLARE (IGNORABLE X))
                  (FLET ((EVENLP2-BDD (X BOUND)
                                     (DECLARE (IGNORE BOUND))
                                     (EVENLP2 X))
                         (ODDLP2-BDD (X BOUND)
                                    (DECLARE (IGNORE BOUND))
                                    (ODDLP2 X)))
                        (DECLARE (INLINE ODDLP2-BDD))
                        (LET ((BOUND 0))
                             (DECLARE (IGNORABLE BOUND))
                             (IF (CONSP X)
                                 (EVENLP2-BDD (CDR X) BOUND)
                                 NIL)))))))

;  (MEMOIZE 'EVENLP2 :TOTAL 'EVENLP2-BDD)
;  (MEMOIZE 'ODDLP2 :TOTAL 'ODDLP2-BDD)
)
)

(mf
#||
HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: The keyword :CHANGE appears more than once for the tuple associated
with FIB2-NEW.  See :DOC memoize-partial.
||#
 (memoize-partial ((fib2-new fib2-clock
                             :change fib2-clock-change0-new
                             :change fib2-clock-change0-new2
                             :stable fib2-clock-stable0-new
                             :condition '(eql (mod n 4) 0)))
                  :condition t)
 :expected :hard)

; Here's what was presumably intended just above:
(memoize-partial ((fib2-new fib2-clock
                            :change fib2-clock-change0-new
                            :stable fib2-clock-stable0-new
                            :condition '(eql (mod n 4) 0)))
                 :condition t)

(f-put-global 'old-world-length (length (w state)) state)

; Check redundancy (though this won't be shown as redundant):
(memoize-partial ((fib2-new fib2-clock
                            :change fib2-clock-change0-new
                            :stable fib2-clock-stable0-new
                            :condition '(eql (mod n 4) 0)))
                 :condition t)

; Redundancy check:
(assert-event (equal (length (w state)) (@ old-world-length)))

; Test that we get the expected value:
(assert-event (equal (fib2-new 30)
                     (fib2-clock 30 50)))
; Test memoization:
(assert-event (equal (fib2-new 80) ; 100 can get us into bignums; slow!
                     37889062373143906))

; Test that (partial) memoization is properly restored, and then run the two
; tests again that are just above.  Also make sure that ordinary memoization is
; handled properly by save and restore.

(defun plain-fib (n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
      0
    (if (eql n 1) 1
      (+ (plain-fib (- n 1)) (plain-fib (- n 2))))))

(memoize 'plain-fib)

(plain-fib 100)

(save-and-clear-memoization-settings)

(er-progn (comp 'plain-fib) ; for other than sbcl and ccl
          (value nil)) ; avoid different values for comp in different lisps

(plain-fib 40) ; takes 0.63 seconds on 2019 MacBook Pro

(assert-event (equal (fib2-new 30)
                     (fib2-clock 30 50)))

(assert-event (equal (fib2-new 80) ; 100 can get us into bignums; slow!
                     37889062373143906))

(restore-memoization-settings)

(plain-fib 100)

(assert-event (equal (fib2-new 80) ; 100 can get us into bignums; slow!
                     37889062373143906))

(mf
#||
HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: Not a null-terminated list.  See :DOC memoize-partial.
||#
 (memoize-partial ((fib2-new fib2-clock
                             :change fib2-clock-change0-new
                             :stable fib2-clock-stable0-new
                             :condition '(eql (mod n 4) 0))
                   . bad-cdr)
                  :condition t)
 :expected :hard)

(mf
#||
HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: The tuple associated with FIB2-NEW is not of the form (fn
fn-limit :kwd1 val1 ... :kwdn valn).  See :DOC memoize-partial.
||#
 (memoize-partial ((fib2-new fib2-clock
                             junk-that-does-not-belong
                             :change fib2-clock-change0-new
                             :stable fib2-clock-stable0-new
                             :condition '(eql (mod n 4) 0)))
                  :condition t)
 :expected :hard)

(mf
#||
HARD ACL2 ERROR in MEMOIZE-PARTIAL:  Ill-formed argument for memoize-
partial: The tuple associated with FIB2-NEW is not of the form (fn
fn-limit :kwd1 val1 ... :kwdn valn).  See :DOC memoize-partial.
||#
 (memoize-partial ((fib2-new fib2-clock
                             :change fib2-clock-change0-new
                             :stable fib2-clock-stable0-new
                             :condition))
                  :condition t)
 :expected :hard)

(mf
#||
HARD ACL2 ERROR in MEMOIZE-PARTIAL:  The argument for memoize-partial
should not be quoted.  Perhaps you intended that argument to be FIB.
||#
 (memoize-partial 'fib)
 :expected :hard)

(mf
#||
HARD ACL2 ERROR in MEMOIZE-PARTIAL:  The arguments to MEMOIZE-PARTIAL
after the first argument should be an alternating list of keywords
and values (keyword first), which will be passed to MEMOIZE.  The call
(MEMOIZE-PARTIAL ((FIB2-NEW FIB2-CLOCK
                            :CHANGE FIB2-CLOCK-CHANGE0-NEW
                            :STABLE FIB2-CLOCK-STABLE0-NEW
                            :CONDITION ...))
                 :CONDITION)
is thus illegal.
||#
 (memoize-partial ((fib2-new fib2-clock
                             :change fib2-clock-change0-new
                             :stable fib2-clock-stable0-new
                             :condition t))
                  :condition)
 :expected :hard)

; We can handle user-defined stobj inputs when there are no stobj outputs
; (which would make non-profiling memoization illegal).

(defstobj st fld)

(defun fib-st-limit (n st limit)
  (declare (type (integer 0 *) limit)
           (type integer n))
  (declare (xargs :measure (nfix limit)
                  :stobjs st))
  (if (zp limit)
      (prog2$ (er hard? 'fib-st-limit
                  "Hit the limit: n=~x0 (fld st)=~x1."
                  n (fld st))
              0) ; to return a natp
    (let ((limit (1- limit)))
      (if (or (= n 0) (= n 1))
          1
        (+ (fib-st-limit (- n 1) st limit)
           (fib-st-limit (- n 2) st limit))))))

(memoize-partial fib-st)

(assert-event (equal (fib-st 100 st)
                     573147844013817084101))

; Memoization is illegal for stobj outputs.

(defun fib-st-out-limit (n st limit)
  (declare (type (integer 0 *) limit)
           (type integer n))
  (declare (xargs :measure (nfix limit)
                  :stobjs st
                  :verify-guards nil))
  (if (zp limit)
      (mv 0 st) ; any term is fine here
    (let ((limit (1- limit)))
      (if (or (= n 0) (= n 1))
          (mv 1 st)
        (mv-let (x1 st)
          (fib-st-out-limit (- n 1) st limit)
          (mv-let (x2 st)
            (fib-st-out-limit (- n 2) st limit)
            (mv (+ x1 x2) st)))))))

(defthm natp-fib-st-out-limit-0
  (natp (car (fib-st-out-limit n limit st)))
  :rule-classes :type-prescription)

(verify-guards fib-st-out-limit)

(mf
#||
ACL2 Error in MEMOIZE-PARTIAL:
The stobj ST is returned by FIB-ST-OUT-LIMIT, which is illegal for
memoization.
See :DOC memoize-partial.
||#
 (memoize-partial fib-st-out))

; Memoization is illegal for state input.

(defun fib-state-limit (n state limit)
  (declare (type (integer 0 *) limit)
           (type integer n))
  (declare (xargs :measure (nfix limit)
                  :stobjs state
                  :verify-guards nil))
  (if (zp limit)
      (mv 0 state) ; any term is fine here
    (let ((limit (1- limit)))
      (if (or (= n 0) (= n 1))
          (mv 1 state)
        (mv-let (x1 state)
          (fib-state-limit (- n 1) state limit)
          (mv-let (x2 state)
            (fib-state-limit (- n 2) state limit)
            (mv (+ x1 x2) state)))))))

(defthm natp-fib-state-limit-0
  (natp (car (fib-state-limit n limit state)))
  :rule-classes :type-prescription)

(verify-guards fib-state-limit)

(mf
#||
ACL2 Error in MEMOIZE-PARTIAL:  STATE is among the formals of
FIB-STATE-LIMIT.
||#
 (memoize-partial fib-state))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Collatz example
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Since it's an open problem whether the 3n+1 algorithm terminates, we have an
; opportunity to show off memoize-partial.

; While we're at it, we'll test (comp t), which at one point failed to preserve
; the effect of memoize-partial, making collatz non-executable.
(set-compile-fns nil)

(defun collatz-limit (n limit)
  (declare (xargs :guard (and (natp n)
                              (natp limit))
                  :measure (acl2-count limit)))
  (if (zp limit)
      (prog2$ (er hard? 'collatz-limit
                  "Limit exceeded!")
              0)
    (let ((limit (1- limit)))
      (if (int= n 1)
          0
        (1+ (collatz-limit (if (evenp n)
                               (floor n 2)
                             (1+ (* 3 n)))
                           limit))))))

(memoize-partial collatz)

; That memoize-partial call generates the following:

(set-enforce-redundancy t)

(encapsulate
  ()

  (DEFCHOOSE COLLATZ-LIMIT-CHANGE (LARGE)
    (N LIMIT)
    (AND (NATP LARGE)
         (<= LIMIT LARGE)
         (NOT (EQUAL (COLLATZ-LIMIT N LIMIT)
                     (COLLATZ-LIMIT N LARGE)))))
  (DEFCHOOSE COLLATZ-LIMIT-STABLE (LIMIT)
    (N)
    (AND (NATP LIMIT)
         (EQUAL (COLLATZ-LIMIT N LIMIT)
                (COLLATZ-LIMIT N (COLLATZ-LIMIT-CHANGE N LIMIT)))))
  (DEFUN COLLATZ (N)
    (DECLARE (XARGS :GUARD (LET ((LIMIT 0))
                                (DECLARE (IGNORABLE LIMIT))
                                (AND (NATP N) (NATP LIMIT)))))
    (COLLATZ-LIMIT N (NFIX (NON-EXEC (COLLATZ-LIMIT-STABLE N)))))
  (TABLE PARTIAL-FUNCTIONS-TABLE 'COLLATZ-LIMIT
         '((COLLATZ
            COLLATZ-LIMIT COLLATZ-LIMIT-CHANGE
            COLLATZ-LIMIT-STABLE
            (DEFUN
              COLLATZ (N)
              (DECLARE (IGNORABLE N))
              (FLET
               ((COLLATZ-LIMIT (N LIMIT)
                               (DECLARE (IGNORE LIMIT))
                               (COLLATZ N)))
               (DECLARE (INLINE COLLATZ-LIMIT))
               (LET ((LIMIT 0))
                    (DECLARE (IGNORABLE LIMIT))
                    (IF (INT= N 1)
                        0
                        (1+ (COLLATZ-LIMIT (IF (EVENP N) (FLOOR N 2) (1+ (* 3 N)))
                                           LIMIT)))))))))

  (MEMOIZE 'COLLATZ :TOTAL 'COLLATZ-LIMIT)
  )

(set-enforce-redundancy nil)

(defun collatz-sum-rec (n acc)
  (declare (xargs :guard (and (natp n) (natp acc))))
  (if (zp n)
      acc
    (collatz-sum-rec (1- n)
                     (+ (collatz n) acc))))

(defun collatz-sum (n)
  (collatz-sum-rec n 0))

(defun collatz-limit-sum-rec (n acc limit)
  (declare (xargs :guard (and (natp n) (natp acc) (natp limit))))
  (if (zp n)
      acc
    (collatz-limit-sum-rec (1- n)
                           (+ (collatz-limit n limit) acc)
                           limit)))

(defun collatz-limit-sum (n)

; Note that (1- (expt 2 60)) should be a fixnum; see the Essay on Fixnum
; Declarations in ACL2 source file acl2-check.lisp.

  (collatz-limit-sum-rec n 0 (1- (expt 2 60))))

; Suppress output since (comp t) returns (value nil) in CCL and SBCL, else
; (value t).
(with-output :off :all (progn (comp t) (value-triple nil)))

(assert-event (equal (collatz-sum (expt 10 6)) ; 1,000,000
                     131434424)) ; 131,434,224

(assert-event (equal (collatz-limit-sum (expt 10 6)) ; 1,000,000
                     (collatz-sum (expt 10 6))))